Heyting Arithmetic (HA)

Origin. Arend Heyting's formalization of intuitionistic logic (1930) supplied the base; the arithmetic is Peano's axioms over it. Gödel (1933) and Gentzen (independently) gave the negative translation showing PA is interpretable in HA, so the classical theory is consistent if the constructive one is. Kleene's realizability (1945) supplied the semantics that made HA an object of study rather than a restriction.

Models. Peano arithmetic with excluded middle removed and nothing else changed. The axioms are identical; the logic is intuitionistic. What this costs is small and what it buys is specific: HA proves every Π⁰₂ theorem of PA, so no computational content is lost, while gaining the disjunction and existence properties — a proof of ∃x φ(x) yields a numeral. The negative translation shows the classical theory was never stronger in the arithmetical sense; it was only less informative.

Formalism.

Language: 0, S, +, ×, = — identical to PA.

Axioms: identical to PA (Q1–Q7 plus full induction), over intuitionistic predicate logic. HA = PA − (excluded middle).

Gödel–Gentzen negative translation: For each φ, a translation φᴺ inserting ¬¬ before atoms and eliminating ∨, ∃: PA ⊢ φ ⟺ HA ⊢ φᴺ Hence Con(HA) → Con(PA). HA and PA are equiconsistent, and PA is a subtheory of HA under the translation, not an extension of it in strength.

Disjunction and existence properties: HA ⊢ φ ∨ ψ ⟹ HA ⊢ φ or HA ⊢ ψ HA ⊢ ∃x φ(x) ⟹ HA ⊢ φ(n̄) for some numeral n̄ Neither holds for PA. Both fail for HA + Markov's principle + excluded middle for Δ₀.

Realizability (Kleene 1945): n realizes ∃x φ(x) iff n = ⟨m, k⟩ and k realizes φ(m̄) Soundness: HA ⊢ φ ⟹ some numeral realizes φ. HA + ECT₀ (extended Church's thesis) is realizability-complete: HA + ECT₀ ⊢ φ ↔ ∃n (n realizes φ).

Admissible rules: Markov's rule: from HA ⊢ ¬¬∃x φ(x) with φ decidable, infer HA ⊢ ∃x φ(x). Admissible, not derivable — Markov's principle is not a theorem of HA. Church's rule, the independence-of-premise rule: likewise admissible.

Proof-theoretic ordinal: ε₀, the same as PA.

Fragments and relatives: HA^ω: finite types, the setting for the Dialectica interpretation. iΣ₁ and the intuitionistic induction hierarchy, which does not collapse the way its classical counterpart does. IZF, CZF: the set-theoretic analogues, in Constructive Set Theory.

Symbols.

Metatheory. HA and PA are equiconsistent and share the ordinal ε₀, so the classical/constructive divide in arithmetic is not a divide in strength. It is a divide in what a proof delivers: HA's existence property makes every proof of ∃x φ(x) an algorithm, and the fact that PA lacks this while proving the same Π⁰₂ sentences is exactly the content of the negative translation. Gödel's second theorem applies unchanged — HA ⊬ Con(HA). The admissibility of Markov's rule together with the underivability of Markov's principle is the standard example of the two notions coming apart, and the intuitionistic induction hierarchy's failure to collapse shows the fragment structure is genuinely different, not a shadow of PA's.

Applies to. Program extraction from proofs — the existence property is the mechanism. Proof mining and the Dialectica interpretation, via HA^ω. Constructive reverse mathematics. Type theory, through the Curry–Howard reading of HA's proofs as terms. The foundations of intuitionistic mathematics, where HA is the arithmetical base every other constructive system is measured against.

Limitations. Placement here follows the boundary clause: HA's individuation is the signature and axioms of PA, and its intuitionistic base is catalogued in Algebraic/Heyting rather than defined here. HA is not the constructivist's actual working theory — that is HA^ω or a type theory. Classical results must be translated to be used, and the translation is not free of distortion for statements above Π⁰₂. The disjunction and existence properties are metatheorems about HA, not theorems of it, and adding principles that make them internal (ECT₀) makes the theory classically unsound.

© 2026 Lingenic LLC