海廷算术

直觉主义的一阶算术，记作HA。HA建立在直觉主义一阶谓词逻辑IQC上。HA的语言包括符号：=，+，·，S，0。HA的公理是：

I．关于等词=的公理。

(7)对每一HA的公式φ，

φ(0)∧x〔φ(x)→φ(Sx)〕→xφ(x)。

(7)是归纳公理模式，对每一公式φ都是一个公理。HA是皮亚诺算术PA的子系统。HA具有被看作是构造性理论的标志的析取性质DP和存在性质

EP：

DP：HA┝φ∨ψ蕴涵HA┝φ或HA┝ψ。

EP：HA┝xφ(x)蕴涵HA┝φ(n)对某个n。

把EP看作构造性的特征刻划看起来是很吸引人的：如果能表明存在一个有性质φ的客体，就能够能行地指出这样的一个客体。这是古典的“纯存在”概念的构造性对应物。但是已经证明，对于构造性理论，具有EP既不是必要条件也不是充分条件。HA和PA具有相同的可证的递归函数。换句话说，把我们的论证限制于直觉主义逻辑，我们并没失去任何递归函数。应用哥德尔转换，可以把PA的每一公式φ变成HA中的公式φ，对于一切公式φ，有

PA┝φ当且仅当HA┝φ。

(参看哥德尔转换)。这样，PA和HA是相对协调的。因此，从基础的观点看，直觉主义算术恰如PA一样需要一个协调性的证明。S．C．克里尼用可实现性给出了HA的一个解释。1958年，K．哥德尔用有穷类型原始递归泛涵提出了HA的一个新的解释。上面提到的(以及其它的)解释，已经导致大量的证明论结果。