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 InterpretationBearbeiten

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.

BeispieleBearbeiten

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

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

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.

ReferenzenBearbeiten

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