# Heyting arithmetic

In mathematical logic, Heyting arithmetic (sometimes abbreviated HA) is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. Heyting arithmetic_sentence_0

It is named after Arend Heyting, who first proposed it. Heyting arithmetic_sentence_1

## Introduction Heyting arithmetic_section_0

Heyting arithmetic adopts the axioms of Peano arithmetic (PA), but uses intuitionistic logic as its rules of inference. Heyting arithmetic_sentence_2

In particular, the law of the excluded middle does not hold in general, though the induction axiom can be used to prove many specific cases. Heyting arithmetic_sentence_3

For instance, one can prove that ∀ x, y ∈ N : x = y ∨ x ≠ y is a theorem (any two natural numbers are either equal to each other, or not equal to each other). Heyting arithmetic_sentence_4

In fact, since "=" is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula p, ∀ x, y, z, … ∈ N : p ∨ ¬p is a theorem (where x, y, z… are the free variables in p). Heyting arithmetic_sentence_5

## History Heyting arithmetic_section_1

Kurt Gödel studied the relationship between Heyting arithmetic and Peano arithmetic. Heyting arithmetic_sentence_6

He used the Gödel–Gentzen negative translation to prove in 1933 that if HA is consistent, then PA is also consistent. Heyting arithmetic_sentence_7

## Related concepts Heyting arithmetic_section_2

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