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 Bearbeiten
Die Heyting-Arithmetik übernimmt die Axiome der Peano-Arithmetik (PA), verwendet aber 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 ein Satz ist (zwei natürliche Zahlen sind gleich oder ungleich). Weil das einzige Prädikatensymbol in der Heyting-Arithmetik ist, folgt für jede quantorfreie Formel : ist beweisbar, wobei , , … die freien Variablen in sind.
Geschichte Bearbeiten
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 Bearbeiten
Die Heyting-Arithmetik sollte nicht mit Heyting-Algebren verwechselt werden, die das intuitionistische Analogon zu Booleschen Algebren sind.
Siehe auch Bearbeiten
- Harrop-Formel
- BHK-Interpretation
- Realisierbarkeit (Logik)
Referenzen Bearbeiten
- Ulrich Kohlenbach: Applied proof theory. Springer, 2008.
- Anne S. Troelstra (Hrsg.): Metamathematical investigation of intuitionistic arithmetic and analysis. Springer, 1973.
Weblinks Bearbeiten
- Stanford Encyclopedia of Philosophy: Intuitionistic Number Theory von Joan Moschovakis.
- Fragments of Heyting Arithmetic von Wolfgang Burr