Heyting arithmetic

In mathematical logic, Heyting arithmetic (sometimes abbreviated as HA ) is an axiomatization of arithmetic in accordance with intuitionist philosophy (Troelstra 1973: 18). It is named after Arend Heyting , who was the first to use it.

introduction

Heyting arithmetic adopts the axioms of Peano arithmetic (PA), but uses intuitionist logic as rules of inference; in particular, the theorem of the excluded third party does not apply in general, even if the induction axiom provides many concrete instances. For example, one can prove that a proposition is (two natural numbers are equal or not equal). Because the only predicate symbol is Heyting arithmetic, follows for each quantifier -free formula : is provable, where , , ... the free variables in are. ${\ displaystyle \ forall x, y \ in \ mathbb {N} \ colon x = y \ vee x \ neq y}$ ${\ displaystyle =}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ forall x, y, z, \ dots \ in \ mathbb {N} \ colon \ varphi \ vee \ neg \ varphi}$ ${\ displaystyle x}$ ${\ displaystyle y}$ ${\ displaystyle z}$ ${\ displaystyle \ varphi}$

history

Kurt Gödel studied the relationships between Heyting arithmetic and Peano arithmetic. He used the Gödel-Gentzen translation to prove in 1933 that if HA is consistent, so is PA.

Related concepts

Heyting arithmetic should not be confused with Heyting algebras , which are the intuitionist analog of Boolean algebras .

credentials

Ulrich Kohlenbach: Applied proof theory. Springer, 2008.
Anne S. Troelstra (Ed.): Metamathematical investigation of intuitionistic arithmetic and analysis. Springer, 1973.

Web links

Stanford Encyclopedia of Philosophy : Intuitionistic Number Theory by Joan Moschovakis.
Fragments of Heyting Arithmetic by Wolfgang Burr