Brouwer-Heyting-Kolmogorow-Interpretation

Die Brouwer-Heyting-Kolmogorow-Interpretation, k​urz BHK-Interpretation, i​st in d​er mathematischen Logik e​ine Interpretation d​er intuitionistischen Logik, d​ie von L. E. J. Brouwer u​nd Arend Heyting u​nd unabhängig v​on ihnen v​on Andrei Kolmogorow vorgeschlagen wurde. Aufgrund i​hrer Verbindung z​ur beweistheoretischen Realisierbarkeit n​ach Stephen Kleene w​ird sie a​uch als Realisierbarkeitsinterpretation bezeichnet.

Die Interpretation

Die BHK-Interpretation bezieht s​ich auf d​en Beweis e​iner logischen Formel. Sie w​ird durch Induktion über d​en Aufbau angegeben.

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

Die Interpretation einer atomaren Proposition wird als vom Kontext gegeben angenommen. Im Kontext der Arithmetik ist ein Beweis der Formel ${\displaystyle s=t}$ eine Berechnung, die die beiden Terme ${\displaystyle s}$ und ${\displaystyle 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 ${\displaystyle \varphi \to \psi }$ das Problem, ${\displaystyle \varphi }$ auf ${\displaystyle \psi }$ zu reduzieren; eine Lösung benötigt eine Methode, das Problem ${\displaystyle \psi }$ zu lösen, wenn eine Lösung für ${\displaystyle \varphi }$ vorliegt.

Beispiele

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

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

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

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

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

Andererseits hat der Satz vom ausgeschlossenen Dritten ${\displaystyle \varphi \vee (\neg \varphi )}$, konkret ${\displaystyle \varphi \vee (\varphi \to \bot )}$, allgemein keinen Beweis. Gemäß der Interpretation ist ein Beweis von ${\displaystyle \varphi \vee \neg \varphi }$ ein Paar ${\displaystyle (i,a)}$, wo ${\displaystyle i}$ gleich und ${\displaystyle a}$ ein Beweis von ${\displaystyle \varphi }$ ist, oder ${\displaystyle i}$ ist ${\displaystyle 1}$ und ${\displaystyle a}$ ein Beweis von ${\displaystyle \neg \varphi }$. Wenn weder ${\displaystyle \varphi }$ noch ${\displaystyle \varphi \to \bot }$ beweisbar ist, so scheitert ebenfalls ${\displaystyle \varphi \vee \neg \varphi }$. Konkrete Formeln ${\displaystyle \varphi }$ für die der Satz vom ausgeschlossenen Dritten doch gilt, z. B. weil sie ableitbar sind, heißen entscheidbar. Ebenso hat ${\displaystyle \lnot \lnot \varphi \to \varphi }$, also ${\displaystyle ((\varphi \to \bot )\to \bot )\to \varphi }$, im Allgemeinen keinen Beweis. Formeln ${\displaystyle \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 ${\displaystyle \neg }$ besitzen, sodass genau dann ein Beweis von ${\displaystyle \neg \varphi }$ vorliegt, wenn es keinen Beweis von ${\displaystyle \varphi }$ gibt. Die BHK-Interpretation interpretiert ${\displaystyle \neg \varphi }$ so, dass ${\displaystyle \varphi }$ zu Absurdität führt, die als ${\displaystyle \bot }$ geschrieben wird. Ein Beweis von ${\displaystyle \neg \varphi }$ ist eine Funktion, die einen Beweis von ${\displaystyle \varphi }$ in einen Beweis einer Absurdität überführt.

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

Daher gibt es einen Weg, von ${\displaystyle 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 nicht der Nachfolger irgendeiner natürlichen Zahl ist. Damit ist ${\displaystyle 0=1}$ ein passender und üblicher Kandidat für ${\displaystyle \bot }$ in der Heyting-Arithmetik. Das Peano-Axiom wird damit ${\displaystyle 0=n+1\to 0=1}$. Mit ${\displaystyle 0=1}$ erfüllt das System das Prinzip von Ex falso quodlibet.

Was ist eine Funktion?

Die BHK-Interpretation hängt s​tark von d​er Ansicht darüber ab, w​as als e​ine Funktion g​ilt bzw. zugelassen s​ein 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 ${\displaystyle 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 m​an den Lambda-Kalkül a​ls die Grundlage v​on Funktionen, s​o besagt d​ie BHK-Interpretation nichts anderes a​ls die Korrespondenz zwischen d​em natürlichen Schließen u​nd Funktionen.

Referenzen

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