Brouwer-Heyting-Kolmogorow-Interpretation

Die Brouwer-Heyting-Kolmogorow-Interpretation, kurz BHK-Interpretation, ist in der mathematischen Logik eine Interpretation der intuitionistischen Logik, die von L. E. J. Brouwer und Arend Heyting und unabhängig von ihnen von Andrei Kolmogorow vorgeschlagen wurde. Aufgrund ihrer Verbindung zur beweistheoretischen Realisierbarkeit nach Stephen Kleene wird sie auch als Realisierbarkeitsinterpretation bezeichnet.

Die Interpretation

Die BHK-Interpretation bezieht sich auf den Beweis einer logischen Formel. Sie wird durch Induktion über den Aufbau angegeben.

• Ein Beweis von $\varphi \wedge \psi$ ist ein Paar $(a,b)$, wobei $a$ ein Beweis von $\varphi$ und $b$ ein Beweis von $\psi$ ist.
• Ein Beweis von $\varphi \vee \psi$ ist ein Paar $(i,a)$, wo $i$ gleich $0$ ist und $a$ ein Beweis von $\varphi$, oder $i$ ist $1$ und $a$ ein Beweis von $\psi$.
• Ein Beweis von $\varphi \to \psi$ ist eine Funktion $f$, die Beweise von $\varphi$ in Beweise von $\psi$ überführt.
• Ein Beweis von $\exists x\in S:\varphi (x)$ ist ein Paar $(t,a)$, wobei $t$ ein Element von $S$ ist, und $a$ ein Beweis von $\varphi (t)$.
• Ein Beweis von $\forall x\in S:\varphi (x)$ ist eine Funktion $f$, die Elemente $t$ von $S$ in einen Beweis von $\varphi (t)$ überführt.
• Die Formel $\neg \varphi$ ist keine Formel im eigentlichen Sinn und wird als Abkürzung für $\varphi \to \bot$ verstanden, hat also als Beweis eine Funktion $f$, die Beweise von $\varphi$ in Beweise von $\bot$ überführt.
• Es gibt keinen Beweis der Absurdität, dargestellt durch $\bot$.

Die Interpretation einer atomaren Proposition wird als vom Kontext gegeben angenommen. Im Kontext der Arithmetik ist ein Beweis der Formel $s=t$ eine Berechnung, die die beiden Terme $s$ und $t$ auf dieselbe Zahl reduziert.

Kolmogorow folgte demselben Pfad, formulierte sie aber mit den Begriffen Problem und Lösung. Die Gültigkeit einer Formel zu bestätigen ist demnach die Behauptung, eine Lösung zu dem Problem zu kennen, das die Formel darstellt. Beispielsweise ist $\varphi \to \psi$ das Problem, $\varphi$ auf $\psi$ zu reduzieren; eine Lösung benötigt eine Methode, das Problem $\psi$ zu lösen, wenn eine Lösung für $\varphi$ vorliegt.

Beispiele

Die Identität ist ein Beweis für die Formel $\varphi \to \varphi$, unabhängig davon welche konkrete Formel $\varphi$ ist.

Das Gesetz der Nonkontradiktion $\neg (\varphi \wedge \neg \varphi )$ wird zu $(\varphi \wedge (\varphi \to \bot ))\to \bot$:

• Ein Beweis von $(\varphi \wedge (\varphi \to \bot ))\to \bot$ ist eine Funktion $f$, die einen Beweis von $(\varphi \wedge (\varphi \to \bot ))$ in einen Beweis von $\bot$ überführt.
• Ein Beweis von $(\varphi \wedge (\varphi \to \bot ))$ ist ein Paar von Beweisen $(a,b)$, wobei $a$ ein Beweis von $\varphi$ und $b$ ein Beweis von $\varphi \to \bot$ ist.
• Ein Beweis von $\varphi \to \bot$ ist eine Funktion $g$, die einen Beweis von $\varphi$ in einen Beweis von $\bot$ überführt.

Die Funktion $f(a,g)=g(a)$ passt zu der Aufgabe und beweist das Gesetz der Nonkontradiktion, unabhängig davon, welche Formel $\varphi$ ist.

Derselbe Ansatz liefert einen Beweis des Modus ponens $(\varphi \wedge (\varphi \to \psi ))\to \psi$, wobei $\psi$ eine beliebige Formel ist.

Andererseits hat der Satz vom ausgeschlossenen Dritten $\varphi \vee (\neg \varphi )$, konkret $\varphi \vee (\varphi \to \bot )$, allgemein keinen Beweis. Gemäß der Interpretation ist ein Beweis von $\varphi \vee \neg \varphi$ ein Paar $(i,a)$, wo $i$ gleich $0$ und $a$ ein Beweis von $\varphi$ ist, oder $i$ ist $1$ und $a$ ein Beweis von $\neg \varphi$. Wenn weder $\varphi$ noch $\varphi \to \bot$ beweisbar ist, so scheitert ebenfalls $\varphi \vee \neg \varphi$. Konkrete Formeln $\varphi$ für die der Satz vom ausgeschlossenen Dritten doch gilt, z. B. weil sie ableitbar sind, heißen entscheidbar. Ebenso hat $\lnot \lnot \varphi \to \varphi$, also $((\varphi \to \bot )\to \bot )\to \varphi$, im Allgemeinen keinen Beweis. Formeln $\varphi$, für die die Implikation gilt, heißen stabil.

Was ist Absurdität?

Nach dem Gödelschen Unvollständigkeitssatz kann ein formales System keine formale Negation $\neg$ besitzen, sodass genau dann ein Beweis von $\neg \varphi$ vorliegt, wenn es keinen Beweis von $\varphi$ gibt. Die BHK-Interpretation interpretiert $\neg \varphi$ so, dass $\varphi$ zu Absurdität führt, die als $\bot$ geschrieben wird. Ein Beweis von $\neg \varphi$ ist eine Funktion, die einen Beweis von $\varphi$ in einen Beweis einer Absurdität überführt.

Ein Standardbeispiel von Absurdität ist in der Arithmetik die Formel $0=1$. Mittels vollständiger Induktion folgt daraus, dass alle natürlichen Zahlen gleich sind.

Daher gibt es einen Weg, von $0=1$ zu einem Beweis jeder grundlegenden arithmetischen Gleichheit zu gelangen, und damit zu einem Beweis einer beliebig komplexen Aussage. Dieses Resultat benötigt außerdem nicht das Axiom der Peano-Arithmetik, dass $0$ nicht der Nachfolger irgendeiner natürlichen Zahl ist. Damit ist $0=1$ ein passender und üblicher Kandidat für $\bot$ in der Heyting-Arithmetik. Das Peano-Axiom wird damit $0=n+1\to 0=1$. Mit $0=1$ erfüllt das System das Prinzip von Ex falso quodlibet.

Was ist eine Funktion?

Die BHK-Interpretation hängt stark von der Ansicht darüber ab, was als eine Funktion gilt bzw. zugelassen sein soll. Im Konstruktivismus werden verschiedene Ansichten vertreten.

Kleenes Realisierbarkeitstheorie lässt nur die berechenbaren Funktionen zu. Sie verwendet die Heyting-Arithmetik, wobei der quantifizierte Bereich aus den natürlichen Zahlen besteht. Basisformeln haben die Form $x=y$. Ein Beweis besteht aus dem Algorithmus, der beide Seiten auswertet und zurückgibt, ob es derselbe Zahl war. Andernfalls gibt es keinen Beweis. Darauf bauen dann komplexere Algorithmen auf.

Nimmt man den Lambda-Kalkül als die Grundlage von Funktionen, so besagt die BHK-Interpretation nichts anderes als die Korrespondenz zwischen dem natürlichen Schließen und Funktionen.

Referenzen

• Anne Troelstra: History of Constructivism in the Twentieth Century. 1991 (englisch, [1] [PDF; 4,0 MB]). 
• Anne Troelstra: Constructivism and Proof Theory (draft). 2003 ([2] [PDF; 286 kB]).