Heyting arithmetic

Heyting arithmetic can be characterized just like the first-order theory of Peano arithmetic $\{\backslash mathsf\{PA\}\}$, except that it uses the intuitionistic predicate calculus $\{\backslash mathsf\{IQC\}\}$ for inference. In particular, this means that the double-negation elimination principle, as well as the principle of the excluded middle $\{\backslash mathrm\{PEM\}\}$, do not hold. Note that to say $\{\backslash mathrm\{PEM\}\}$ does not hold exactly means that the excluded middle statement is not automatically provable for all propositions—indeed many such statements are still provable in $\{\backslash mathsf\{HA\}\}$ and the negation of any such disjunction is inconsistent. $\{\backslash mathsf\{PA\}\}$ is strictly stronger than $\{\backslash mathsf\{HA\}\}$ in the sense that all $\{\backslash mathsf\{HA\}\}$-theorems are also $\{\backslash mathsf\{PA\}\}$-theorems.

Heyting arithmetic comprises the axioms of Peano arithmetic and the intended model is the collection of natural numbers $\{\backslash mathbb\; N\}$. The signature includes zero "$0$" and the successor "$S$", and the theories characterize addition and multiplication. This impacts the logic: With $1:=S0$, it is a metatheorem that $\backslash bot$ can be defined as $0=1$ and so that $\backslash neg\; P$ is $P\backslash to\backslash bot$ for every proposition $P$. The negation of $\backslash bot$ is of the form $P\backslash to\; P$ and thus a trivial proposition.

For terms, write $s\backslash neq\; t$ for $\backslash neg(s=\; t)$.

For a fixed term $t$, the equality $t=t$ is true by reflexivity and a proposition $P$ is equivalent to $(t=t)\backslash to\; P$.

It may be shown that $P\backslash lor\; Q$ can then be defined as $\backslash exists\; n.\; (n=0\backslash to\; P)\backslash land(n\backslash neq\; 0\backslash to\; Q)$. This formal elimination of disjunctions was not possible in the quantifier-free primitive recursive arithmetic $\{\backslash mathsf\{PRA\}\}$. The theory may be extended with function symbols for any primitive recursive function, making $\{\backslash mathsf\{PRA\}\}$ also a fragment of this theory. For a total function $f$, one often considers predicates of the form $f(n)=0$.

With explosion valid in any intuitionistic theory, if $\backslash neg\backslash neg\; P$ is a theorem for some $P$, then by definition $\backslash neg\; P$ is provable if and only if the theory is inconsistent. Indeed, in Heyting arithmetic the double-negation explicitly expresses $\backslash neg\; P\backslash to\; 0=1$. For a predicate $Q$, a theorem of the form $\backslash neg\backslash neg\; \backslash exists\; n.\; Q(n)$ expresses that it is inconsistent to rule out that $Q(t)$ could be validated for some $t$. Constructively, this is weaker than the existence claim of such a $t$.

A big part of the metatheoretical discussion will concern classically provable existence claims.

A double-negation $\backslash neg\backslash neg\; P$ entails $(\backslash alpha\backslash to\backslash neg\; P)\backslash to(\backslash alpha\backslash to\; 0=1)$. So a theorem of the form $\backslash neg\backslash neg\; P$ also always gives new means to conclusively reject (also positive) statements $\backslash alpha$.

Recall that the implication in $\backslash mathsf\{HA\}\backslash vdash\backslash alpha\backslash to\backslash neg\backslash neg\backslash alpha$ can classically be reversed, and with that so can the one in $\backslash mathsf\{HA\}\backslash vdash\backslash big(\backslash exists\; n.\; \backslash neg\; \backslash psi(n)\backslash big)\; \backslash to\; \backslash neg\backslash forall\; n.\; \backslash psi(n)$. Here the distinction is between existence of numerical counter-examples versus absurd conclusions when assuming validity for all numbers. Inserting double-negations turns $\{\backslash mathsf\{PA\}\}$-theorems into $\{\backslash mathsf\{HA\}\}$-theorems. More exactly, for any formula provable in $\{\backslash mathsf\{PA\}\}$, the classically equivalent Gödel–Gentzen negative translation of that formula is already provable in $\{\backslash mathsf\{HA\}\}$. In one formulation, the translation procedure includes a rewriting of $\backslash big(\backslash exists\; n.\; Q(n)\backslash big)^N$ to $\backslash neg\backslash forall\; n.\backslash neg\; Q^N(n).$ The result means that 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 double-negation elimination.

In particular, with undecidable atomic propositions being absent, for any proposition $\backslash psi$ not including existential quantifications or disjunctions at all, one has $\{\backslash mathsf\{PA\}\}\backslash vdash\backslash psi\; \backslash iff\; \{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash psi$.

Minimal logic proves double-negation elimination for negated formulas, $\backslash neg\backslash neg(\backslash neg\backslash alpha)\backslash leftrightarrow(\backslash neg\backslash alpha)$. More generally, Heyting arithmetic proves this classical equivalence for any Harrop formula.

And $\backslash Sigma\_1^0$-results are well behaved as well: Markov's rule at the lowest level of the arithmetical hierarchy is an admissible rule of inference, i.e. for $\backslash varphi$ with $n$ free,

:$\{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash neg\backslash neg\backslash exists\; m.\; \backslash varphi(n,\; m)\backslash iff\; \{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash exists\; m.\; \backslash varphi(n,\; m)$

Instead of speaking of quantifier-free predicates, one may equivalently formulate this for primitive recursive predicate or Kleene's T predicate, called $\{\backslash mathrm\{MR\}\}\_\backslash mathrm\{QF\}$, resp. $\{\backslash mathrm\{MR\}\_\backslash mathrm\{PR\}\}$ and $\{\backslash mathrm\{MR\}\_0\}$.

Even the related rule $\{\backslash mathrm\{MR\}\}\_\backslash mathrm\{Dec\}$ is admissible, in which the tractability aspect of $\backslash varphi$ is not e.g. based on a syntactic condition but where the left hand side also requires $\backslash vdash\; \backslash forall\; m.\backslash varphi(n,\; m)\backslash lor\; \backslash neg\backslash varphi(n,\; m)$.

Beware that in classifying a proposition based on its syntactic form, one ought not mistakenly assign a lower complexity based on some only classical valid equivalence.

As with other theories over intuitionistic logic, various instances of $\{\backslash mathrm\{PEM\}\}$ can be proven in this constructive arithmetic. By disjunction introduction, whenever either the proposition $P$ or $\backslash neg\; P$ is proven, then $P\backslash lor\backslash neg\; P$ is proven as well. So for example, equipped with $0=0$ and $\backslash forall\; n.\; Sn\backslash neq\; 0$ from the axioms, one may validate the premise for induction of excluded middle for the predicate $n=0$. One then says equality to zero is decidable. Indeed, $\{\backslash mathsf\{HA\}\}$ proves equality "$=$" decidable for all numbers, i.e. $\backslash forall\; n.\; \backslash forall\; m.\; (n\; =\; m\backslash lor\; n\; \backslash neq\; m)$. Stronger yet, as equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula $\backslash phi$, where $n,\backslash dots,m$ are the free variables, the theory is closed under the rule

:$\{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash forall\; n.\; \backslash cdots\; \backslash forall\; m.\backslash ,\backslash phi(n,\; \backslash dots,\; m)\backslash lor\backslash neg\backslash phi(n,\; \backslash dots,\; m)$

Any theory over minimal logic proves $\backslash neg\backslash neg(P\backslash lor\; \backslash neg\; P)$ for all propositions. So if the theory is consistent, it never proves the negation of an excluded middle statement.

Practically speaking, in rather conservative constructive frameworks such as $\{\backslash mathsf\{HA\}\}$, when it is understood what type of statements are algorithmically decidable, then an unprovability result of an excluded middle disjunction expresses the algorithmic undecidability of $P$.

For simple statements, the theory does not just validate such classically valid binary dichotomies $\backslash phi(n,\backslash dots)\backslash lor\backslash neg\backslash phi(n,\backslash dots)$. The Friedman translation can be used to establish that $\{\backslash mathsf\{PA\}\}$'s $\backslash Pi\_2^0$-theorems are all proven by $\{\backslash mathsf\{HA\}\}$: For any $n$ and quantifier-free $\backslash varphi$,

:$\{\backslash mathsf\{PA\}\}\backslash vdash\; \backslash exists\; m.\; \backslash varphi(n,\; m)\backslash iff\; \{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash exists\; m.\; \backslash varphi(n,\; m)$

This result may of course also be expressed with explicit universal closures $\backslash forall\; n$. Roughly, simple statements about computable relations provable classically are already provable constructively. Although in halting problems, not just quantifier-free propositions but also $\backslash Pi\_1^0$-propositions play an important role, and as will be argued these can be even classically independent. Similarly, already unique existence $\backslash exists!n.\; Q(n)$ in an infinite domain, i.e. $\backslash exists\; n.\; \backslash forall\; w.\; \backslash big(n=w\; \backslash leftrightarrow\; Q(w)\backslash big)$, is formally not particularly simple.

So $\{\backslash mathsf\{PA\}\}$ is $\backslash Pi\_2^0$-conservative over $\{\backslash mathsf\{HA\}\}$. For contrast, while the classical theory of Robinson arithmetic $\{\backslash mathsf\{Q\}\}$ proves all $\backslash Sigma\_1^0$-$\{\backslash mathsf\{PA\}\}$-theorems, some simple $\backslash Pi\_1^0$-$\{\backslash mathsf\{PA\}\}$-theorems are independent of it. Induction also plays a crucial role in Friedman's result: For example, the more workable theory obtained by strengthening $\{\backslash mathsf\{Q\}\}$ with axioms about ordering, and optionally decidable equality, does prove more $\backslash Pi\_2^0$-statements than its intuitionistic counterpart.

The discussion here is by no means exhaustive. There are various results for when a classical theorem is already entailed by the constructive theory. Also note that it can be relevant what logic was used to obtain metalogical results. For example, many results on realizability were indeed obtained in a constructive metalogic. But when no specific context is given, stated results need to be assumed to be classical.

Independence results concern propositions such that neither they, nor their negations can be proven in a theory. If the classical theory is consistent (i.e. does not prove $\backslash bot$) and the constructive counterpart does not prove one of its classical theorems $P$, then that $P$ is independent of the latter. Given some independent propositions, it is easy to define more from them, especially in a constructive framework.

Heyting arithmetic has the disjunction property $\{\backslash mathrm\{DP\}\}$: For all propositions $\backslash alpha$ and $\backslash beta$,{{Citation|first1=Morten|last1=Sørenson|first2=Paweł|last2=Urzyczyn|title=Lectures on the Curry-Howard Isomorphism|citeseerx = 10.1.1.17.7385 |year=1998}}, pp. 240-249

:$\{\backslash mathsf\{HA\}\}\backslash vdash\backslash alpha\backslash lor\backslash beta\backslash iff\{\backslash mathsf\{HA\}\}\backslash vdash\backslash alpha\backslash text\{\; or\; \}\{\backslash mathsf\{HA\}\}\backslash vdash\backslash beta$

Indeed, this and its numerical generalization are also exhibited by constructive second-order arithmetic and common set theories such as $\{\backslash mathsf\{CZF\}\}$ and $\{\backslash mathsf\{IZF\}\}$. It is a common desideratum for the informal notion of a constructive theory.

Now in a theory with $\{\backslash mathrm\{DP\}\}$, if a proposition $P$ is independent, then the classically trivial $P\backslash lor\; \backslash neg\; P$ is another independent proposition, and vice versa. A schema is not valid if there is at least one instance that cannot be proven, which is how $\{\backslash mathrm\{PEM\}\}$ comes to fail. One may break $\{\backslash mathrm\{DP\}\}$ by adopting an excluded middle statement axiomatically without validating either of the disjuncts, as is the case in $\{\backslash mathsf\{PA\}\}$.

More can be said: If $P$ is even classically independent, then also the negation $\backslash neg\; P$ is independent—this holds whether or not $\backslash neg\backslash neg\; P$ is equivalent to $P$. Then, constructively, the weak excluded middle $\{\backslash mathrm\{WPEM\}\}$ does not hold, i.e. the principle that $\backslash neg\backslash alpha\backslash lor\backslash neg\backslash neg\backslash alpha$ would hold for all propositions is not valid. If such $P$ is $\backslash Sigma\_1^0$, unprovability of the disjunction manifests the breakdown of $\backslash Pi\_1^0$-$\{\backslash mathrm\{PEM\}\}$, or what amounts to an instance of $\{\backslash mathrm\{WLPO\}\}$ for a primitive recursive function.

Knowledge of Gödel's incompleteness theorems aids in understanding the type of statements that are $\{\backslash mathsf\{PA\}\}$-provable but not $\{\backslash mathsf\{HA\}\}$-provable.

The resolution of Hilbert's tenth problem provided some concrete polynomials $f$ and corresponding polynomial equations, such that the claim that the latter have a solution is algorithmically undecidable. The proposition can be expressed as

:$\backslash exists\; w\_1.\backslash cdots\backslash exists\; w\_n.\; f(w\_1,\; \backslash dots,\; w\_n)=0$

Certain such zero value existence claims have a more particular interpretation: Theories such as $\{\backslash mathsf\{PA\}\}$ or $\{\backslash mathsf\{ZFC\}\}$ prove that these propositions are equivalent to the arithmetized claim of the theories own inconsistency. Thus, such propositions can even be written down for strong classical set theories.

In a consistent and sound arithmetic theory, such an existence claim $\{\backslash mathrm\{I\}\_f\}$ is an independent $\backslash Sigma\_1^0$-proposition. Then $\{\backslash mathrm\{C\}\_f\}:=\backslash neg\; \{\backslash mathrm\{I\}\_f\}$, by pushing a negation through the quantifier, is seen to be an independent Goldbach-type- or $\backslash Pi\_1^0$-proposition. To be explicit, the double-negation $\backslash neg\backslash neg\{\backslash mathrm\{I\}\_f\}$ (or $\backslash neg\{\backslash mathrm\{C\}\_f\}$) is also independent. And any triple-negation is, in any case, already intuitionistically equivalent to a single negation.

The following illuminates the meaning involved in such independent statements. Given an index in an enumeration of all proofs of a theory, one can inspect what proposition it is a proof of. $\{\backslash mathsf\{PA\}\}$ is adequate in that it can correctly represent this procedure: there is a primitive recursive predicate $\backslash mathrm\{F\}(w):=\backslash mathrm\{Prf\}(w,\; \backslash ulcorner\; 0=1\; \backslash urcorner)$ expressing that a proof is one of the absurd proposition $0=1$. This relates to the more explicitly arithmetical predicate above, about a polynomial's return value being zero. One may metalogically reason that if $\{\backslash mathsf\{PA\}\}$ is consistent, then it indeed proves $\backslash neg\backslash mathrm\{F\}(\{\backslash underline\{\backslash mathrm\; w\}\})$ for every individual index $\{\backslash mathrm\; w\}$.

In an effectively axiomatized theory, one may successively perform an inspection of each proof. If a theory is indeed consistent, then there does not exist a proof of an absurdity, which corresponds to the statement that the mentioned "absurdity search" will never halt. Formally in the theory, the former is expressed by the proposition $\backslash neg\backslash exists\; w.\; \backslash mathrm\{F\}(w)$, negating the arithmetized inconsistency claim. The equivalent $\backslash Pi\_1^0$-proposition $\backslash forall\; w.\; \backslash neg\; \backslash mathrm\{F\}(w)$ formalizes the never halting of the search by stating that all proofs are not a proof of an absurdity. And indeed, in an omega-consistent theory that accurately represents provability, there is no proof that the absurdity search would ever conclude by halting (explicit inconsistency not derivable), nor—as shown by Gödel—can there be a proof that the absurdity search would never halt (consistency not derivable). Reformulated, there is no proof that the absurdity search never halts (consistency not derivable), nor is there a proof that the absurdity search does not never halt (consistency not rejectible).

To reiterate, neither of these two disjuncts is $\{\backslash mathsf\{PA\}\}$-provable, while their disjunction is trivially $\{\backslash mathsf\{PA\}\}$-provable. Indeed, if $\{\backslash mathsf\{PA\}\}$ is consistent then it violates $\{\backslash mathrm\{DP\}\}$.

The $\backslash Sigma\_1^0$-proposition expressing the existence of a proof of $0=1$ is a logically positive statement. Nonetheless, it is historically denoted $\backslash neg\{\backslash mathrm\{Con\}\}\_\{\backslash mathsf\{PA\}\}$, while its negation is a $\backslash Pi\_1^0$-proposition denoted by $\{\backslash mathrm\{Con\}\}\_\{\backslash mathsf\{PA\}\}$. In a constructive context, this use of the negation sign may be misleading nomenclature.

Friedman established another interesting unprovable statement, namely that a consistent and adequate theory never proves its arithmetized disjunction property.

Already minimal logic logically proves all non-contradiction claims, and in particular $\backslash neg(\{\backslash mathrm\{I\}\_f\}\backslash land\backslash neg\{\backslash mathrm\{I\}\_f\})$ and $\backslash neg(\{\backslash mathrm\{C\}\_f\}\backslash land\backslash neg\{\backslash mathrm\{C\}\_f\})$. Since also $(\{\backslash mathrm\{C\}\_f\}\backslash land\backslash neg\{\backslash mathrm\{C\}\_f\})\backslash leftrightarrow\backslash neg(\{\backslash mathrm\{I\}\_f\}\backslash lor\backslash neg\{\backslash mathrm\{I\}\_f\})$, the theorem $\backslash neg(\{\backslash mathrm\{C\}\_f\}\backslash land\backslash neg\{\backslash mathrm\{C\}\_f\})$ may be read as a provable double-negated excluded middle disjunction (or existence claim). But in light of the disjunction property, the plain excluded middle $\{\backslash mathrm\{C\}\_f\}\backslash lor\backslash neg\{\backslash mathrm\{C\}\_f\}$ cannot be $\{\backslash mathsf\{HA\}\}$-provable. So one of the De Morgan's laws cannot intuitionistically hold in general either.

The breakdown of the principles $\{\backslash mathrm\{WPEM\}\}$ and $\{\backslash mathrm\{WLPO\}\}$ have been explained.

Now in $\{\backslash mathsf\{PA\}\}$, the least number principle $\{\backslash mathrm\{LNP\}\}$ is just one of many statements equivalent to the induction principle. The proof below shows how $\{\backslash mathrm\{LNP\}\}$ implies $\{\backslash mathrm\{PEM\}\}$, and therefore why this principle also cannot be generally valid in $\{\backslash mathsf\{HA\}\}$. However, the schema granting double-negated least number existence for every non-trivial predicate, denoted $\backslash neg\backslash neg\{\backslash mathrm\{LNP\}\}$, is generally valid. In light of Gödel's proof, the breakdown of these three principles can be understood as Heyting arithmetic being consistent with the provability reading of constructive logic.

Markov's principle for primitive recursive predicates $\{\backslash mathrm\{MP\}\_\backslash mathrm\{PR\}\}$ does already not hold as an implication schema for $\{\backslash mathsf\{HA\}\}$, let alone the strictly stronger $\{\backslash mathrm\{MP\}\_\backslash mathrm\{Dec\}\}$. Although in the form of the corresponding rules, they are admissible, as mentioned.

Similarly, the theory does not prove the independence of premise principle $\{\backslash mathrm\{IP\}\}$ for negated predicates, albeit it is closed under the rule for all negated propositions, i.e. one may pull out the existential quantifier in $\backslash neg\; P\backslash to\backslash exists\; n.Q(n)$. The same holds for the version where the existential statement is replaced by a mere disjunction.

The valid implication $\backslash neg\backslash neg(\backslash alpha\backslash to\backslash beta)\backslash to(\backslash alpha\backslash to\backslash neg\backslash neg\backslash beta)$ can be proven to hold also in its reversed form, using the disjunctive syllogism. However, the double-negation shift $\{\backslash mathrm\{DNS\}\}$ is not intuitionistically provable, i.e. the schema of commutativity of "$\backslash neg\backslash neg$" with universal quantification over all numbers. This is an interesting breakdown that is explained by the consistency of $\backslash neg\{\backslash mathrm\{Dec\}\_M\}$ for some $M$, as discussed in the section on Church's thesis.

Making use of the order relation on the naturals, the strong induction principle reads

:

In class notation, as familiar from set theory, an arithmetic statement $Q(n)$ is expressed as $n\backslash in\; B$ where $B:=\backslash \{m\backslash in\{\backslash mathbb\; N\}\backslash mid\; Q(m)\backslash \}$. For any given predicate of negated form, i.e. $\backslash phi(n):=\backslash neg(n\backslash in\; B)$, a logical equivalent to induction is

:

The insight is that among subclasses $B\backslash subseteq\{\backslash mathbb\; N\}$, the property of (provably) having no least member is equivalent to being uninhabited, i.e. to being the empty class. Taking the contrapositive results in a theorem expressing that for any non-empty subclass, it cannot consistently be ruled out that there exists a member $n\backslash in\; B$ such that there is no member $k\backslash in\; B$ smaller than $n$:

:

In Peano arithmetic, where double-negation elimination is always valid, this proves the least number principle in its common formulation. In the classical reading, being non-empty is equivalent to (provably) being inhabited by some least member.

A binary relation "" that validates the strong induction schema in the above form is always also irreflexive: Considering $\backslash phi\_c(n):=(n\backslash neq\; c)$ or equivalently

:$Q\_c(n):=(n=c)$

for some fixed number $c$, the above simplifies to the statement that no member $k$ of $B=\backslash \{c\backslash \}$ validates

More generally, if $B$ is non-empty and the associated (classical) least number principle can be used to prove some statement of negated form (such as

But in general, over constructive logic, the weakening of the least number principle can not be lifted. The following example demonstrates this: For some proposition $P$ (say $\{\backslash mathrm\{C\}\_f\}$ as above), consider the predicate

:$Q\_P(n)\; :=\; (n=0\backslash land\; P)\backslash lor(n=1)$

This $Q\_P$ corresponds to a subclass $b\_P:=\backslash \{z\backslash in\backslash \{0\backslash \}\backslash mid\; P\backslash \}\backslash cup\backslash \{1\backslash \}$ of the natural numbers. Any number proven or assumed to be in this class provably either equals $0$ or $1$, i.e. $b\_P\backslash subseteq\backslash \{0,1\backslash \}$. As $1=1$, the proposition $Q\_P(1)$ or $1\backslash in\; b\_P$ is trivially true and so the class is inhabited. Further, using decidability of equality and the disjunctive syllogism proves the equivalence $Q\_P(0)\backslash leftrightarrow\; P$. In other words, whether $0$ is a member of the class is exactly as hard as $P$. If the underlying proposition $P$ is independent, then also the predicate is undecidable in the theory.

One may ask what the least member of the class $b\_P$ may be. As it is inhabited, the least number existence for this class cannot be rejected. In fact, given a conjunction with $Q\_P(1)$ is trivial, the existence claim of a least number validating $Q\_P$ itself translates to the excluded middle statement for $P$. Knowledge of such a number's value does determine whether or not $P$ holds. So for independent $P$, the least number principle instance with $Q\_P$ is also independent of $\{\backslash mathsf\{HA\}\}$.

In set theory notation, $P$ is also equivalent to $b\_P=\backslash \{0,1\backslash \}$, while its negation is equivalent to $b\_P=\backslash \{1\backslash \}$. This demonstrates that elusive predicates can define elusive subsets. And so also in constructive set theory, while the standard order on the class of naturals is decidable, the naturals are not well-ordered. But strong induction principles, that constructively do not imply unrealizable existence claims, are also still available.

In a computable context, for a predicate $M$, the classically trivial infinite disjunction

:$\backslash forall\; n.\backslash big(M(n)\backslash lor\backslash neg\; M(n)\backslash big)$,

also written $\{\backslash mathrm\{Dec\}\}\_M$, can be read as a validation of the decidability of a decision problem. In class notation, $M(n)$ is also written $n\backslash in\; M$.

$\{\backslash mathsf\{HA\}\}$ proves no propositions not provable by $\{\backslash mathsf\{PA\}\}$ and so, in particular, it does not reject any theorems of the classical theory. But there are also predicates $M$ such that the axioms $\{\backslash mathsf\{HA\}\}+\backslash neg\{\backslash mathrm\{Dec\}\}\_M$ are consistent. Again, constructively, such a negation is not equivalent to the existence of a particular numerical counter-example $t$ to excluded middle for $M(t)$. Indeed, already minimal logic proves the double-negated excluded middle for all propositions, and so $\backslash forall\; n.\; \backslash neg\backslash neg\backslash big(\; Q(n)\backslash lor\backslash neg\; Q(n)\; \backslash big)$, which is equivalent to $\backslash neg\backslash exists\; n.\backslash neg\backslash big(\; Q(n)\backslash lor\backslash neg\; Q(n)\; \backslash big)$, for any predicate $Q$.

Church's rule is an admissible rule in $\{\backslash mathsf\{HA\}\}$. Church's thesis principle $\{\backslash mathrm\{CT\}\_0\}$ may be adopted in $\{\backslash mathsf\{HA\}\}$, while $\{\backslash mathsf\{PA\}\}$ rejects it: It implies negations such as the ones just described.

Consider the principle in the form stating that all predicates that are decidable in the logic sense above are also decidable by a total computable function. To see how it is in conflict with excluded middle, one merely needs to define a predicate that is not computably decidable.

To this end, write $\backslash Delta\_e(w):=T\_1(e,\; e,\; w)$ for predicates defined from Kleene's T predicate. The indices $e$ of total computable functions fulfill $\backslash forall\; x.\; \backslash exists\; w.\; T\_1(e,\; x,\; w)$. While $T\_1$ can be realized in a primitive recursive fashion, the predicate $\backslash exists\; w.\; \backslash Delta\_e(w)$ in $e$, i.e. the class $H:=\backslash \{e\backslash mid\; \backslash exists\; w.\; \backslash Delta\_e(w)\backslash \}$ of partial computable function indices with a witness describing how they halt on the diagonal, is computably enumerable but not computable. The classical compliment $M$ defined using $\backslash neg\backslash exists\; w.\; \backslash Delta\_e(w)$ is not even computably enumerable, see halting problem. This provenly undecidable problem $e\backslash in\; M$ provides a violating example. For any index $e$, the equivalent form $\backslash forall\; w.\; \backslash neg\; \backslash Delta\_e(w)$ expresses that when the corresponding function is evaluated (at $e$), then all conceivable descriptions of evaluation histories ($w$) do not describe the evaluation at hand. Specifically, this not being decidable for functions establishes the negation of what amounts to $\{\backslash mathrm\{WLPO\}\}$.

The formal Church's principles are associated with the recursive school, naturally. Markov's principle $\{\backslash mathrm\{MP\}\_\backslash mathrm\{Dec\}\}$ is commonly adopted, by that school and by constructive mathematics more broadly. In the presence of Church's principle, $\{\backslash mathrm\{MP\}\_\backslash mathrm\{Dec\}\}$ is equivalent to its weaker form $\{\backslash mathrm\{MP\}\_\backslash mathrm\{PR\}\}$. The latter can generally be expressed as a single axiom, namely double-negation elimination for any $\backslash neg\backslash neg\backslash exists\; w.\; T\_1(e,\; x,\; w)$. Heyting arithmetic together with both $\{\backslash mathrm\{MP\}\_\backslash mathrm\{Dec\}\}$+$\{\backslash mathrm\{ECT\}\_0\}$ prove independence of premise for decidable predicates, $\{\backslash mathrm\{IP\}\}\_0$. But they do not go together, consistently, with $\{\backslash mathrm\{IP\}\}$.

$\{\backslash mathrm\{CT\}\_0\}$ also negates $\{\backslash mathrm\{DNS\}\}$. The intuitionist school of L. E. J. Brouwer extends Heyting arithmetic by

a collection of principles that negate both $\{\backslash mathrm\{PEM\}\}$ as well as $\{\backslash mathrm\{CT\}\_0\}$.

If a theory is consistent, then no proof is one of an absurdity. Kurt Gödel introduced the 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 $\{\backslash mathsf\{PA\}\}$ to that of $\{\backslash mathsf\{HA\}\}$. However, Gödel's incompleteness theorems, about the incapability of certain theories to prove their own consistency, also applies to Heyting arithmetic itself.

The standard model of the classical first-order theory $\{\backslash mathsf\{PA\}\}$ as well as any of its non-standard models is also a model for Heyting arithmetic $\{\backslash mathsf\{HA\}\}$.

There are also constructive set theory models for full $\{\backslash 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 $\backslash omega$, as well as the existence of function spaces on finite domains for recursive definitions.

Specifically, those theories do not require $\{\backslash mathrm\{PEM\}\}$, 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).

$\{\backslash mathsf\{HA\}\}$ furthermore is bi-interpretable with a weak constructive set theory in which the class of ordinals is $\backslash omega$, so that the collection of von Neumann naturals do not exist as a set in the theory.{{citation|first=Hanul|last=Jeon|arxiv=2010.04270|title=Constructive Ackermann's interpretation|journal=Annals of Pure and Applied Logic |year=2022|volume=173 |issue=5 |page=103086 |doi=10.1016/j.apal.2021.103086 |s2cid=222271938 }}Shapiro, S., McCarty, C. & Rathjen, M., [https://link.springer.com/article/10.1007/s00153-024-00935-4 Intuitionistic sets and numbers: small set theory and Heyting arithmetic], https://doi.org/10.1007/s00153-024-00935-4, Arch. Math. Logic (2024) Meta-theoretically, the domain of that theory is as big as the class of its ordinals and essentially given through the class $\{\backslash mathrm\{Fin\}\}$ of all sets that are in bijection with a natural $n\backslash in\backslash omega$. As an axiom this is called $V\; =\; \{\backslash 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 $\{\backslash mathsf\{CZF\}\}$ without Strong Infinity and with the finitude axiom added. The discussion of $\{\backslash 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

:

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.

For some number $\backslash mathrm\{n\}$ in the metatheory, the numeral in the studied object theory is denoted by $\backslash underline\{\backslash mathrm\{n\}\}$.

In intuitionistic arithmetics, the disjunction property $\{\backslash mathrm\{DP\}\}$ is typically valid. And it is a theorem that any c.e. extension of arithmetic for which it holds also has the numerical existence property $\{\backslash mathrm\{NEP\}\}$:

:$\{\backslash mathsf\{HA\}\}\backslash vdash\backslash exists\; n.\; \backslash psi(n)\backslash iff\backslash text\{\; exists\; \}\{\backslash mathrm\{n\}\}\backslash text\{\; \}\{\backslash mathsf\{HA\}\}\backslash vdash\backslash psi(\{\backslash underline\{\backslash mathrm\{n\}\}\})$

So these properties are metalogical equivalent in Heyting arithmetic. The existence and disjunction property in fact still holds when relativizing the existence claim by a Harrop formula $\backslash alpha$, i.e. for provable $\backslash alpha\backslash to\backslash exists\; n.\; \backslash psi(n)$.

Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic.

In turn, his student Nels David Nelson established (in an extension of $\{\backslash mathsf\{HA\}\}$) that all closed theorems of $\{\backslash mathsf\{HA\}\}$ (meaning all variables are bound) can be realized. Inference in Heyting arithmetic preserves realizability. Moreover, if $\{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash forall\; n.\; \backslash exists\; m.\; \backslash varphi(n,\; m)$ then there is a partial recursive function realizing $\backslash varphi$ in the sense that whenever the function evaluated at $\{\backslash mathrm\{n\}\}$ terminates with $\{\backslash mathrm\{m\}\}$, then $\{\backslash mathsf\{HA\}\}\backslash vdash\; \backslash varphi(\{\backslash underline\{\backslash mathrm\{n\}\}\},\; \{\backslash underline\{\backslash mathrm\{m\}\}\})$. This can be extended to any finite number of function arguments $\{\backslash mathrm\{n\}\}$.

There are also classical theorems that are not $\{\backslash mathsf\{HA\}\}$-provable but do have a realization.

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.

See also BHK interpretation and Dialectica interpretation.

In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to $\backslash Sigma\_1$ is categorical. Categoricity here is reminiscent of Tennenbaum's theorem. The model validates $\{\backslash mathsf\{HA\}\}$ but not $\{\backslash mathsf\{PA\}\}$ and so completeness fails in this context.

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

Heyting arithmetic has been discussed with potential function symbols added for primitive recursive functions. That theory proves the Ackermann function total.

Beyond this, axiom and formalism selection always has been a debate even within the constructivist circle. Many typed extensions of $\{\backslash mathsf\{HA\}\}$ have been extensively studied in proof theory, e.g. with types of functions between numbers, and function between those, etc. The formalities naturally become more complicated, with different possible axioms governing the application of functions. The class of functions being total can be enriched this way. The theory with finite types $\{\backslash mathsf\; \{HA\}\}^\backslash omega$ when further combined with function extensionality plus an axiom of choice in $\{\backslash mathbb\; N\}^\{\backslash mathbb\; N\}$ still proves the same arithmetic formulas as just $\{\backslash mathsf\; \{HA\}\}$ and has a type theoretic interpretation. However, that theory rejects Church’s thesis for $\{\backslash mathbb\; N\}^\{\backslash mathbb\; N\}$ as well as that all functions in $\{\backslash mathbb\; N\}^\{\backslash mathbb\; N\}\backslash to\; \{\backslash mathbb\; N\}$ would be continuous. But adopting, say, different extensionality rules, choice axioms, Markov's and independence principles and even the Kőnig's lemma—all together but each at specific strength or levels—one can define rather "stuffed" arithmetics that may still fail to prove excluded middle at the level of $\backslash Pi\_1^0$-formulas.

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

Reverse mathematics studies of constructive second-order arithmetic have been performed.{{Cite arXiv|eprint=1804.05495|title=Constructive Reverse Mathematics

|class=math.LO|last1=Diener|first1=Hannes|year=2020}}

Formal axiomatization of the theory trace back to Heyting (1930), Herbrand and Kleene.

Gödel proved the consistency result concerning $\{\backslash mathsf\{PA\}\}$ in 1933.

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

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

{{Reflist}}

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

• Stanford Encyclopedia of Philosophy: "[http://plato.stanford.edu/entries/logic-intuitionistic/#IntNumTheHeyAri Intuitionistic Number Theory]" by Joan Moschovakis.
• [https://www.jstor.org/stable/2586698?seq=1 Fragments of Heyting Arithmetic] by Wolfgang Burr

{{Non-classical logic}}

Category:Constructivism (mathematics)

Category:Formal theories of arithmetic

Category:Intuitionism