Heyting-Arithmetik

In d​er mathematischen Logik i​st die Heyting-Arithmetik (manchmal m​it HA abgekürzt) e​ine Axiomatisierung d​er Arithmetik i​n Übereinstimmung m​it der intuitionistischen Philosophie (Troelstra 1973:18). Sie i​st nach Arend Heyting, benannt, d​er sie a​ls erster verwendete.

Einführung

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 ${\displaystyle \forall x,y\in \mathbb {N} \colon x=y\vee x\neq y}$ ein Satz ist (zwei natürliche Zahlen sind gleich oder ungleich). Weil ${\displaystyle =}$ das einzige Prädikatensymbol in der Heyting-Arithmetik ist, folgt für jede quantorfreie Formel ${\displaystyle \varphi }$: ${\displaystyle \forall x,y,z,\dots \in \mathbb {N} \colon \varphi \vee \neg \varphi }$ ist beweisbar, wobei ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$ … die freien Variablen in ${\displaystyle \varphi }$ sind.

Geschichte

Kurt Gödel studierte d​ie Beziehungen zwischen Heyting-Arithmetik u​nd Peano-Arithmetik. Er verwendete d​ie Gödel-Gentzen-Übersetzung, u​m 1933 z​u beweisen, d​ass wenn HA konsistent ist, s​o auch PA.

Verwandte Konzepte

Die Heyting-Arithmetik sollte n​icht mit Heyting-Algebren verwechselt werden, d​ie das intuitionistische Analogon z​u Booleschen Algebren sind.

Siehe auch

• Harrop-Formel
• 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: Intuitionistic Number Theory von Joan Moschovakis.
• Fragments of Heyting Arithmetic von Wolfgang Burr