Heyting arithmetic

In mathematical logic, Heyting arithmetic ${\mathsf {HA}}$ is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

Axiomatization

As with first-order Peano arithmetic ${\mathsf {PA}}$, the intended model of this theory are the natural numbers ${\mathbb {N} }$ and the theories characterize addition and multiplication. Heyting arithmetic adopts the axioms of Peano arithmetic, including the signature with zero "$0$" and the successor "$S$", but uses intuitionistic logic for inference. In particular, the law of the excluded middle ${\mathrm {LEM} }$ does not hold in general.

Metalogic and theorems

As with other theories over intuitionistic logic, various instances of ${\mathrm {LEM} }$ can be proven. For instance, ${\mathsf {HA}}$ proves equality "$=$" is decidable for all numbers,

${\mathsf {HA}}\vdash \forall n.\forall m.{\big (}(n=m)\lor \neg (n=m){\big )}$

In fact, since equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula $\phi$, where $n,\dots ,m$ are the free variables in $\phi$,

${\mathsf {HA}}\vdash \forall n.\cdots \forall m.{\big (}\phi \lor \neg \phi {\big )}$

Through the induction axiom, infinitely many non-trivial statement instances can be derived. Indeed, ${\mathsf {PA}}$ is $\Pi _{2}^{0}$-conservative over ${\mathsf {HA}}$, as shown via the Friedman translation. For recursive $\varphi$,

${\mathsf {PA}}\vdash \forall n.\exists m.\varphi (n,m)\implies {\mathsf {HA}}\vdash \forall n.\exists m.\varphi (n,m)$

Roughly, this means all statements about "simple mappings" provable in the classical arithmetic theory are already provable in the constructive one.

Moreover, for any formula provable in ${\mathsf {PA}}$, the classically equivalent Gödel–Gentzen negative translation of that formula is already provable in ${\mathsf {HA}}$. That is to say, all Peano arithmetic theorems have a proof that consists of a constructive proof followed by a classical logical rewriting. Roughly, the final step amounts to applications of the classical double-negation elimination $\neg \neg \psi \vdash _{\mathsf {PA}}\psi$ as well as $\neg \forall n.\psi (n)\vdash _{\mathsf {PA}}\exists n.\neg \psi (n)$.

Insights into Hilbert's tenth problem provide a classically trivially provable mathematical statement that, in the direct formulation below, is not provable constructively. The resolution of Hilbert's question states that there is a polynomial $f$ and a corresponding polynomial equation such that it is computably undecidable whether the latter has a solution. Decidability may be expressed as the excluded middle statement for the proposition $\exists n.\cdots \exists m.f(n,\dots ,m)=0$.

Consistency

Kurt Gödel introduced the above negative translation and proved that if Heyting arithmetic is consistent, then so is Peano arithmetic. That is to say, he reduced the consistency task for ${\mathsf {PA}}$ to that of ${\mathsf {HA}}$.

However, Gödel's incompleteness theorems also applies to Heyting arithmetic.

Indeed, the search for an inconsistency of those theories can be formalized in Peano arithmetic. As established by Gödel, if the theory is consistent, then there is no proof in ${\mathsf {PA}}$ that this search does halt (succeed), nor is there a proof in ${\mathsf {PA}}$ that this search does not halt. Nevertheless, in ${\mathsf {PA}}$, there is a (classically trivial and non-constructive) proof that this search does either halt or not halt.

Anti-classical extensions

Relatedly, there are predicates $A$ such that the theory ${\mathsf {HA}}+{\mathsf {U}}_{A}$ is consistent, where ${{\mathsf {U}}_{A}}$ is

$\neg \forall n.{\big (}A(n)\lor \neg A(n){\big )}$

With a constructive reading of a disjunction, this is an internal version of the claim that the predicate $A$ is not decidable. Note that constructively, the above is not equivalent to the existence of a particular counter-example to excluded middle, as in $\exists n.\neg {\big (}A(n)\lor \neg A(n){\big )}$.

Indeed, already minimal logic proves the double-negated excluded middle for all propositions, and so $\forall n.\neg \neg {\big (}P(n)\lor \neg P(n))$, which is equivalent to $\neg \exists n.\neg {\big (}P(n)\lor \neg P(n){\big )}$.

Church's rule is an admissible rule in Heyting arithmetic. Church's thesis principle may be adopted in ${\mathsf {HA}}$, while ${\mathsf {PA}}$ rejects it. This is because of the computable undecidability for the statement $A$ defined as the diagonal of Kleene's T predicate (see halting problem), which Church's principle then also establishes in the above sense.

Models

Realizability

Kleene, a student of Church, introduced important realizability models of the theory. In turn, his student Nels David Nelson established that all closed formulas (all variables bound) of Heyting arithmetic can be realized. See also BHK interpretation.

They also established, informally expressed here, that if

${\mathsf {PA}}\vdash \forall n.\exists m.\varphi (n,m)$

for "simple $\varphi$", then in ${\mathsf {HA}}$ there is a general recursive function realizing an $m$ for each $n$ so that $\varphi (n,m)$. This can be extended to any finite number of function arguments $n$.

See disjunction and existence properties.

Markov's rule is an admissible rule in Heyting arithmetic. Typed versions of realizability have been introduced by Georg Kreisel. With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories.

Set theory

There are constructive set theory models for full ${\mathsf {HA}}$ and its intended semantics. Relatively weak set theories suffice: They shall adopt the Axiom of infinity, the Axiom schema of predicative separation to prove induction of arithmetical formulas in $\omega$, as well as the existence of function spaces on finite domains for recursive definitions. Specifically, those theories do not require ${\mathrm {LEM} }$, the full axiom of separation or set induction (let alone the axiom of regularity), nor general function spaces (let alone the full axiom of power set).

${\mathsf {HA}}$ furthermore is bi-interpretable with a weak constructive set theory in which the class of ordinals is $\omega$, so that the von Neumann naturals do not exist as a set in the theory. Meta-theoretically, the domain of that theory is as big as the class of its ordinals and essentially given through the class ${\mathrm {Fin} }$ of all sets that are in bijection with a natural $n\in \omega$. As an axiom this is called $V={\mathrm {Fin} }$ and the other axioms are those related to set algebra and order: Union and Binary Intersection, which is tightly related to the Predicative Separation schema, Extensionality, Pairing, and the Set induction schema. This theory is then already identical with the theory given by ${\mathsf {CZF}}$ without Strong Infinity and with the finitude axiom added. The discussion of ${\mathsf {HA}}$ in this set theory is as in model theory. And in the other direction, the set theoretical axioms are proven with respect to the primitive recursive relation

$x\in y\iff \exists (r<2^{x}).\exists (s<y).{\big (}2^{x}(2s+1)+r=y{\big )}$

That small universe of sets can be understood as the ordered collection of finite binary sequences which encode their mutual membership. For example, the $100_{2}$'th set contains one other set and the $110101_{2}$'th set contains four other sets. See BIT predicate.

The standard model of the classical first-order theory ${\mathsf {PA}}$ as well as any of its non-standard models is also a model for Heyting arithmetic ${\mathsf {HA}}$. Any consistent recursive extension of ${\mathsf {ZF}}$ is also modeled, again via the Ackerman coding, by some subset of any non-standard model of ${\mathsf {PA}}$ - however, just as the syntactic arithmetic theory itself cannot know of non-standardness of numbers, it does not know of the infinitude of the sets in such semantics.

Type theory

Type theoretical realizations mirroring inference rules based logic formalizations have been implemented in various languages.

Extensions

Many typed extensions of ${\mathsf {HA}}$ have been extensively studied in proof theory, e.g. with function types.

Early on, variants with intensional equality and Brouwerian choice sequence have been investigated.

History

Formal axiomatization of the theory trace back to Heyting (1930), Herbrand and Kleene. Gödel proved the consistency result concerning ${\mathsf {PA}}$ in 1933.

Related concepts

Heyting arithmetic should not be confused with Heyting algebras, which are the intuitionistic analogue of Boolean algebras.

See also

• BHK interpretation
• Constructive analysis
• Constructive set theory
• Harrop formula
• Realizability

References

• Ulrich Kohlenbach (2008), Applied proof theory, Springer.
• Anne S. Troelstra, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer, 1973.

External links

• Stanford Encyclopedia of Philosophy: "Intuitionistic Number Theory" by Joan Moschovakis.
• Fragments of Heyting Arithmetic by Wolfgang Burr