A big part of the metatheoretical discussion will concern classically provable existence claims.
Here the distinction is between existence of numerical counter-examples versus absurd conclusions when assuming validity for all numbers.
More generally, Heyting arithmetic proves this classical equivalence for any Harrop formula.
Stronger yet, as equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula
Induction also plays a crucial role in Friedman's result: For example, the more workable theory obtained by strengthening
,[2] Indeed, this and its numerical generalization are also exhibited by constructive second-order arithmetic and common set theories such as
by adopting an excluded middle statement axiomatically without validating either of the disjuncts, as is the case in
Knowledge of Gödel's incompleteness theorems aids in understanding the type of statements that are
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).
Friedman established another interesting unprovable statement, namely that a consistent and adequate theory never proves its arithmetized disjunction property.
may be read as a provable double-negated excluded middle disjunction (or existence claim).
However, the schema granting double-negated least number existence for every non-trivial predicate, denoted
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.
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
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
: In Peano arithmetic, where double-negation elimination is always valid, this proves the least number principle in its common formulation.
is non-empty and the associated (classical) least number principle can be used to prove some statement of negated form (such as
But strong induction principles, that constructively do not imply unrealizable existence claims, are also still available.
To see how it is in conflict with excluded middle, one merely needs to define a predicate that is not computably decidable.
The intuitionist school of L. E. J. Brouwer extends Heyting arithmetic by a collection of principles that negate both
However, Gödel's incompleteness theorems, about the incapability of certain theories to prove their own consistency, also applies to Heyting arithmetic itself.
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.
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.
Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic.
With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories.
In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to
Type theoretical realizations mirroring inference rules based logic formalizations have been implemented in various languages.
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
Early on, also variants with intensional equality and Brouwerian choice sequence have been investigated.
[5] Formal axiomatization of the theory trace back to Heyting (1930), Herbrand and Kleene.