Heyting Arithmetik - Heyting arithmetic
In der mathematischen Logik ist die Heyting-Arithmetik (manchmal abgekürzt HA ) eine Axiomatisierung der Arithmetik gemäß der Philosophie des Intuitionismus . Es ist nach Arend Heyting benannt , der es zuerst vorgeschlagen hat.
Einführung
Die Heyting-Arithmetik übernimmt die Axiome der Peano-Arithmetik (PA), verwendet jedoch die intuitionistische Logik als Inferenzregeln. Insbesondere gilt das Gesetz der ausgeschlossenen Mitte im Allgemeinen nicht, obwohl das Induktionsaxiom verwendet werden kann, um viele spezifische Fälle zu beweisen. Zum Beispiel kann man beweisen, dass ∀ x , y ∈ N : x = y ∨ x ≠ y ein Theorem ist (zwei beliebige natürliche Zahlen sind entweder gleich oder nicht gleich). In der Tat, da "=" der einzige ist Prädikat in Heyting arithmetischen Symbol, folgt dann , daß für jede quantifier -freie Formel φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ ist ein Satz ( wobei x , y , z ... die freien Variablen in φ ) sind.
Geschichte
Kurt Gödel untersuchte die Beziehung zwischen Heyting-Arithmetik und Peano-Arithmetik. Er verwendete die negative Übersetzung von Gödel-Gentzen , um 1933 zu beweisen, dass PA auch konsistent ist, wenn HA konsistent ist.
Verwandte konzepte
Die Heyting-Arithmetik sollte nicht mit den Heyting-Algebren verwechselt werden , die das intuitionistische Analogon der Booleschen Algebren sind .
Siehe auch
Verweise
- Ulrich Kohlenbach (2008), Angewandte Beweistheorie , Springer.
- Anne S. Troelstra , Hrsg. (1973), Metamathematische Untersuchung intuitionistischer Arithmetik und Analyse , Springer, 1973.
Externe Links
- Stanford Encyclopedia of Philosophy : " Intuitionistische Zahlentheorie " von Joan Moschovakis .
- Fragmente der Heyting-Arithmetik von Wolfgang Burr
 |
Dieser Artikel, der sich auf die mathematische Logik bezieht, ist ein Stummel . Sie können Wikipedia helfen, indem Sie es erweitern . |