In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it.
Axiomatization Heyting arithmetic can be characterized just like the first-order theory of Peano arithmetic , except that it uses the intuitionistic predicate calculus for inference. In particular, this means that the double-negation elimination principle, as well as the principle of the excluded middle , do not hold. Note that to say 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 and the negation of any such disjunction is inconsistent. is strictly stronger than in the sense that all -theorems are also -theorems.
Heyting arithmetic comprises the axioms of Peano arithmetic and the intended model is the collection of natural numbers . The signature includes zero "" and the successor "", and the theories characterize addition and multiplication. This impacts the logic: With , it is a metatheorem that can be defined as and so that is for every proposition . The negation of is of the form and thus a trivial proposition.
For terms, write for . For a fixed term , the equality is true by reflexivity and a proposition is equivalent to . It may be shown that can then be defined as . This formal elimination of disjunctions was not possible in the quantifier-free primitive recursive arithmetic . The theory may be extended with function symbols for any primitive recursive function, making also a fragment of this theory. For a total function , one often considers predicates of the form .
Theorems Double negations With explosion valid in any intuitionistic theory, if is a theorem for some , then by definition is provable if and only if the theory is inconsistent. Indeed, in Heyting arithmetic the double-negation explicitly expresses . For a predicate , a theorem of the form expresses that it is inconsistent to rule out that could be validated for some . Constructively, this is weaker than the existence claim of such a . A big part of the metatheoretical discussion will concern classically provable existence claims.
A double-negation entails . So a theorem of the form also always gives new means to conclusively reject (also positive) statements .
Proofs of classically equivalent statements Recall that the implication in can classically be reversed, and with that so can the one in . Here the distinction is between existence of numerical counter-examples versus absurd conclusions when assuming validity for all numbers. Inserting double-negations turns -theorems into -theorems. More exactly, for any formula provable in , the classically equivalent Gödel–Gentzen negative translation of that formula is already provable in . In one formulation, the translation procedure includes a rewriting of to 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 not including existential quantifications or disjunctions at all, one has .
Valid principles and rules Minimal logic proves double-negation elimination for negated formulas, . More generally, Heyting arithmetic proves this classical equivalence for any Harrop formula.
And -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 with free,
Instead of speaking of quantifier-free predicates, one may equivalently formulate this for primitive recursive predicate or Kleene's T predicate, called , resp. and . Even the related rule is admissible, in which the tractability aspect of is not e.g. based on a syntactic condition but where the left hand side also requires .
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.
Excluded middle As with other theories over intuitionistic logic, various instances of can be proven in this constructive arithmetic. By disjunction introduction, whenever either the proposition or is proven, then is proven as well. So for example, equipped with and from the axioms, one may validate the premise for induction of excluded middle for the predicate . One then says equality to zero is decidable. Indeed, proves equality "" decidable for all numbers, i.e. . Stronger yet, as equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula , where are the free variables, the theory is closed under the rule
Any theory over minimal logic proves 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 , 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 .
Conservativity For simple statements, the theory does not just validate such classically valid binary dichotomies . The Friedman translation can be used to establish that 's -theorems are all proven by : For any and quantifier-free ,
This result may of course also be expressed with explicit universal closures . Roughly, simple statements about computable relations provable classically are already provable constructively. Although in halting problems, not just quantifier-free propositions but also -propositions play an important role, and as will be argued these can be even classically independent. Similarly, already unique existence in an infinite domain, i.e. , is formally not particularly simple.
So is -conservative over . This can be contrasted with the situation for Robinson arithmetic , which is a weaker theory in that it lacks Induction. First off, classical proves all --theorems, but some simple --theorems are already independent of it. Induction can be seen to play a crucial role in Friedman's result, as the more workable theory obtained by strengthening with axioms about ordering, and optionally decidable equality, does prove more -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.
Unprovable statements 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 ) and the constructive counterpart does not prove one of its classical theorems , then that 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 : For all propositions and ,, pp. 240-249
Indeed, this and its numerical generalization are also exhibited by constructive second-order arithmetic and common set theories such as and . It is a common desideratum for the informal notion of a constructive theory. Now in a theory with , if a proposition is independent, then the classically trivial 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 comes to fail. One may break by adopting an excluded middle statement axiomatically without validating either of the disjuncts, as is the case in .
More can be said: If is even classically independent, then also the negation is independent—this holds whether or not is equivalent to . Then, constructively, the weak excluded middle does not hold, i.e. the principle that would hold for all propositions is not valid. If such is , unprovability of the disjunction manifests the breakdown of -, or what amounts to an instance of for a primitive recursive function.
Classically independent propositions Knowledge of Gödel's incompleteness theorems aids in understanding the type of statements that are -provable but not -provable.
The resolution of Hilbert's tenth problem provided some concrete polynomials and corresponding polynomial equations, such that the claim that the latter have a solution is algorithmically undecidable. The proposition can be expressed as
Certain such zero value existence claims have a more particular interpretation: Theories such as or 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 is an independent -proposition. Then , by pushing a negation through the quantifier, is seen to be an independent Goldbach-type- or -proposition. To be explicit, the double-negation (or ) is also independent. And any triple-negation is, in any case, already intuitionistically equivalent to a single negation.
PA violates DP 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. is adequate in that it can correctly represent this procedure: there is a primitive recursive predicate expressing that a proof is one of the absurd proposition . This relates to the more explicitly arithmetical predicate above, about a polynomial's return value being zero. One may metalogically reason that if is consistent, then it indeed proves for every individual index .
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 , negating the arithmetized inconsistency claim. The equivalent -proposition 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 -provable, while their disjunction is trivially -provable. Indeed, if is consistent then it violates .
The -proposition expressing the existence of a proof of is a logically positive statement. Nonetheless, it is historically denoted , while its negation is a -proposition denoted by . 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.
Unprovable classical principles