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

[Bearbeiten | Quelltext bearbeiten]

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

  • Ein Beweis von ist ein Paar , wobei ein Beweis von und ein Beweis von ist.
  • Ein Beweis von ist ein Paar , wo gleich ist und ein Beweis von , oder ist und ein Beweis von .
  • Ein Beweis von ist eine Funktion , die Beweise von in Beweise von überführt.
  • Ein Beweis von ist ein Paar , wobei ein Element von ist, und ein Beweis von .
  • Ein Beweis von ist eine Funktion , die Elemente von in einen Beweis von überführt.
  • Die Formel ist keine Formel im eigentlichen Sinn und wird als Abkürzung für verstanden, hat also als Beweis eine Funktion , die Beweise von in Beweise von überführt.
  • Es gibt keinen Beweis der Absurdität, dargestellt durch .

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

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

Das Gesetz der Nonkontradiktion wird zu :

  • Ein Beweis von ist eine Funktion , die einen Beweis von in einen Beweis von überführt.
  • Ein Beweis von ist ein Paar von Beweisen , wobei ein Beweis von und ein Beweis von ist.
  • Ein Beweis von ist eine Funktion , die einen Beweis von in einen Beweis von überführt.

Die Funktion passt zu der Aufgabe und beweist das Gesetz der Nonkontradiktion, unabhängig davon, welche Formel ist.

Derselbe Ansatz liefert einen Beweis des Modus ponens , wobei eine beliebige Formel ist.

Andererseits hat der Satz vom ausgeschlossenen Dritten , konkret , allgemein keinen Beweis. Gemäß der Interpretation ist ein Beweis von ein Paar , wo gleich und ein Beweis von ist, oder ist und ein Beweis von . Wenn weder noch beweisbar ist, so scheitert ebenfalls . Konkrete Formeln für die der Satz vom ausgeschlossenen Dritten doch gilt, z. B. weil sie ableitbar sind, heißen entscheidbar. Ebenso hat , also , im Allgemeinen keinen Beweis. Formeln , für die die Implikation gilt, heißen stabil.

Was ist Absurdität?

[Bearbeiten | Quelltext bearbeiten]

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

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

Daher gibt es einen Weg, von 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 ein passender und üblicher Kandidat für in der Heyting-Arithmetik. Das Peano-Axiom wird damit . Mit erfüllt das System das Prinzip von Ex falso quodlibet.

Was ist eine Funktion?

[Bearbeiten | Quelltext bearbeiten]

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 . 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.

  • 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]).