Utente:Acondolu/Heyting Arithmetic

In mathematical logic, Heyting arithmetic (sometimes abbreviated HA) is a first-order axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it. Heyting arithmetic adopts the axioms of Peano arithmetic (PA), but uses intuitionistic predicate logic as its rules of inference.

Heyting arithmetic should not be confused with Heyting algebras, which are the intuitionistic analogue of boolean algebras.

Decidability

In HA, the law of the excluded middle does not hold in general, though the induction axiom can be used to prove many specific cases. For instance, one can prove that $\forall xy.x=y\lor x\neq y$ 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 quantifier-free formula $P$, $\forall x.P(x)\lor \neg P(x)$ is a theorem (where $x$ is the only free variable in $P$).

Relationship with Peano arithmetic

In 1933, Kurt Gödel used the Gödel–Gentzen negative translation to prove that if HA is consistent, then PA is also consistent.

Since $PA\equiv HA^{c}$, that is, Peano arithmetic is just Heyting arithmetic with classical predicate logic rules, the relationship between Peano and Heyting arithmetic can be shown through the Gödel–Gentzen negative translation. In fact, from the corresponding theorem for logic, follows that

$PA\vdash A\Leftrightarrow HA\vdash A^{g},$

where $A$ is a predicate in the language of arithmetic, and A^g is the negative translation of A, with the additional rule that (t = s)^g  := t = s, for t and s terms (justified by the fact that . It means that A is derivable in Peano arithmetic if and only if its negative translation A^g is derivable in Heyting arithmetic: as a consequence, HA is only apparently weaker than PA, and its consistency can be used to prove PA's.

See also

• Harrop formula
• BHK interpretation

External links

• Stanford Encyclopedia of Philosophy: "Intuitionistic Number Theory" by Joan Moschovakis.
• A. S. Troelstra and Dirk Van Dalen (1988), "Constructivism in Mathematics", Elsevir Science Publishers B.V., ISBN 0-444-70358-6