Quelltext der Seite Heyting-Arithmetik

In der mathematischen Logik ist die '''Heyting-Arithmetik''' (manchmal mit '''HA''' abgekürzt) eine [[Axiomatisierung]] der Arithmetik in Übereinstimmung mit der intuitionistischen Philosophie (Troelstra 1973:18).  Sie ist nach [[Arend Heyting]], benannt, der sie als erster verwendete.

== Einführung ==
Die Heyting-Arithmetik übernimmt die Axiome der [[Peano-Axiome|Peano-Arithmetik]] (PA), verwendet aber [[Intuitionismus (Logik und Mathematik)|intuitionistische Logik]] als Inferenzregeln, insbesondere gilt der [[Satz vom ausgeschlossenen Dritten]] nicht allgemein, wenn auch das Induktionsaxiom für viele konkrete Instanzen sorgt. Beispielsweise kann man beweisen, dass <math>\forall x, y \in \N \colon x = y \vee x \ne y</math> ein Satz ist (zwei [[Natürliche Zahl|natürliche Zahlen]] sind gleich oder ungleich). Weil <math>=</math> das einzige [[Prädikat (Logik)|Prädikaten]]<nowiki/>symbol in der Heyting-Arithmetik ist, folgt für jede [[quantor]]<nowiki/>freie [[Formel]] <math>\varphi</math>: <math>\forall x, y, z, \dots \in \N \colon \varphi  \vee \neg \varphi</math> ist beweisbar, wobei <math>x</math>, <math>y</math>, <math>z</math> … die [[Freie Variable und gebundene Variable|freien Variablen]] in <math>\varphi</math> sind.

== Geschichte ==
[[Kurt Gödel]] studierte die Beziehungen zwischen Heyting-Arithmetik und Peano-Arithmetik.  Er verwendete die [[Gödel-Gentzen-Übersetzung]], um 1933 zu beweisen, dass wenn HA konsistent ist, so auch PA.

== Verwandte Konzepte ==
Die Heyting-Arithmetik sollte nicht mit [[Heyting-Algebra|Heyting-Algebren]] verwechselt werden, die das intuitionistische Analogon zu [[Boolesche Algebra|Booleschen Algebren]] sind.

== Siehe auch ==
* [[Harrop-Formel]]
* [[Brouwer-Heyting-Kolmogorow-Interpretation|BHK-Interpretation]]
* [[Realisierbarkeit (Logik)]]

== Referenzen ==
* Ulrich Kohlenbach: ''Applied proof theory.'' Springer, 2008.
* Anne S. Troelstra (Hrsg.): ''Metamathematical investigation of intuitionistic arithmetic and analysis.'' Springer, 1973.

== Weblinks ==
* [[Stanford Encyclopedia of Philosophy]]: [http://plato.stanford.edu/entries/logic-intuitionistic/#IntNumTheHeyAri Intuitionistic Number Theory] von Joan Moschovakis.
* [http://wwwmath.uni-muenster.de/logik/Personen/burr/HA.ps Fragments of Heyting Arithmetic] von Wolfgang Burr

[[Kategorie:Arithmetik]]