In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
As with first-order Peano arithmetic , the intended model of this theory are the natural numbers and the theories characterize addition and multiplication. Heyting arithmetic adopts the axioms of Peano arithmetic, including the signature with zero "" and the successor "", but uses intuitionistic logic for inference. In particular, the principle of the excluded middle does not hold in general.
Metalogic and theorems
As with other theories over intuitionistic logic, various instances of can be proven. For instance, proves equality "" is decidable for all numbers,
In fact, since equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula , where are the free variables in ,
Through the induction axiom, infinitely many non-trivial statement instances can be derived. Indeed, is -conservative over , as shown via the Friedman translation. For recursive ,
So, roughly speaking, the simple statements about computable functions provable in the classical arithmetic theory are already provable in the constructive one.
Moreover, for any formula provable in , the classically equivalent Gödel–Gentzen negative translation of that formula is already provable in . 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 variants of and the double-negation elimination .
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 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 .
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 to that of .
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 that this search does halt (succeed), nor is there a proof in that this search does not halt. Nevertheless, in , there is a (classically trivial and non-constructive) proof that this search does either halt or not halt.
Relatedly, there are predicates such that the theory is consistent, where is
With a constructive reading of a disjunction, this is an internal version of the claim that the predicate is not decidable. Note that constructively, the above is not equivalent to the existence of a particular counter-example to excluded middle, as in .
Indeed, already minimal logic proves the double-negated excluded middle for all propositions, and so , which is equivalent to .
Church's rule is an admissible rule in Heyting arithmetic. Church's thesis principle may be adopted in , while rejects it. This is because of the computable undecidability for the statement defined as the diagonal of Kleene's T predicate (see halting problem), which Church's principle then also establishes in the above sense.
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
for "simple ", then in there is a general recursive function realizing an for each so that . This can be extended to any finite number of function arguments .
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.
The standard model of the classical first-order theory as well as any of its non-standard models is also a model for Heyting arithmetic . But there are also constructive set theory models for full 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 , as well as the existence of function spaces on finite domains for recursive definitions. Specifically, those theories do not require , 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).
furthermore is bi-interpretable with a weak constructive set theory in which the class of ordinals is , 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 of all sets that are in bijection with a natural . As an axiom this is called 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 without Strong Infinity and with the finitude axiom added. The discussion of 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 'th set contains one other set and the 'th set contains four other sets. See BIT predicate.
Type theoretical realizations mirroring inference rules based logic formalizations have been implemented in various languages.
Many typed extensions of 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.
Formal axiomatization of the theory trace back to Heyting (1930), Herbrand and Kleene. Gödel proved the consistency result concerning in 1933.
Heyting arithmetic should not be confused with Heyting algebras, which are the intuitionistic analogue of Boolean algebras.
- ^ Troelstra 1973:18
- ^ Jeon, Hanul (2020), Constructive Ackermann's interpretation, arXiv:2010.04270
- Ulrich Kohlenbach (2008), Applied proof theory, Springer.
- Anne S. Troelstra, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer, 1973.