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).
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
