Heyting arithmetic

From Wikipedia, the free encyclopedia

Heyting arithmetic is the basic arithmetic of intuitionism (not to be confused with Heyting algebra). It is named after Arend Heyting. It is the system whose axioms are the same as those of Peano arithmetic, but whose rules of inference are those of intuitionistic logic (which, in particluar, does not assert the law of the excluded middle, although special cases of this law can be derived as theorems of Heyting arithmetic). For instance, one can prove, using mathematical induction, that is a theorem (any two natural numbers are either equal to each other, or not equal to each other). In fact, since "=" is the only predicate symbol in Heyting arithmetic, it then follows that, for any proposition p which does not contain quantifiers, is a theorem (where x,y,z... are the free variables in the proposition p).