Wie passen Beweise über Logik in einen logischen Rahmen?

Deduktive Beweise in der Logik erster Ordnung sind im Wesentlichen Transformationen einer Aussage der Sprache in eine andere. Sie beginnen mit einer Aussage (oder mehreren oder gar keiner) und produzieren dann daraus eine geordnete Folge neuer Aussagen, die durch sukzessive Anwendung der etablierten Regeln des Systems abgeleitet werden. Sie können diese Sequenz jederzeit beenden und jede neue Aussage, die in diesem Prozess produziert wird, wird als „abgeleitet“ oder „bewiesen“ bezeichnet. Dieser einfache, hochstrukturierte Prozess ist der Grund, warum das Theorembeweisen automatisiert werden kann: Computer sind wirklich gut darin, Regeln zu befolgen.

Beweise sind Sammlungen von Aussagen im System, und Aussagen über Beweise sind keine Aussagen im System – sie sind Aussagen in natürlicher Sprache (z. B. Englisch). Daher sind Aussagen in englischer Sprache über Aussagen im System nicht an die Regeln des Systems gebunden und leben nicht innerhalb des Systems. Genauso wie es möglich ist, im Rahmen der Arithmetik zu sagen, ob $2+2=4$ richtig oder falsch ist, ohne Arithmetik zu verwenden, kann man feststellen, ob ein Beweis im System gültig ist, ohne das System dafür zu verwenden. Denn jeder unvoreingenommene Beobachter kann im Regelbuch nachsehen, ob die Regeln korrekt befolgt wurden oder nicht.

Hier ist der Haken: Es ist vernünftig zu glauben, dass die Logik des Systems auch die Logik ist, die wir verwenden, um Aussagen über das System zu analysieren, aber das ist einfach nicht der Fall. Wenn wir das System analysieren, überprüfen wir lediglich das Regelwerk, und die Schlussfolgerungen, die wir ziehen, sind objektiv wahr oder falsch. Ein anderes System mit einem anderen Regelwerk könnte jedoch zu einer anderen Schlussfolgerung führen.

Das heißt, ich sympathisiere mit (was ich glaube) Ihrer Sorge - nämlich. „Wir verwenden Logik, um Logik zu analysieren, also ist das nicht ein Zirkelschluss? Wie können wir Logik verwenden, bevor wir wissen, wie sie funktioniert?“ Die Antwort ist, dass die natürliche, intuitionistische Logik nicht unbedingt auf ein formales System angewiesen ist, weil ihre Wahrheit selbstverständlich ist. Lassen Sie es mich so sagen: Warum glauben Sie an Arithmetik? Liegt es daran, dass Sie die Regeln studiert haben und sie intern konsistent erscheinen, oder liegt es daran, dass ihre Schlussfolgerungen offenkundig sind? 2 Äpfel und 3 Äpfel sind 5 Äpfel, also 2$+3=5$. Tappen Sie nicht in die Falle, den Karren vor das Pferd zu spannen. Das System modelliert die Realität, nicht umgekehrt. Das Modell ist unvollkommen, aber wir verwenden das System, weil das Modell mit unserer Intuition übereinstimmt.

Nehmen wir als letzten Punkt zum Beispiel den Unvollständigkeitssatz. Der Satz ist im Wesentlichen ein Beweis dafür, dass die Aussage "Diese Aussage ist nicht beweisbar." existiert im System der Arithmetik. Dies ist wichtig, weil eine solche Aussage offenkundig wahr ist (die Alternative – dh beweisbar zu sein – wäre ein Widerspruch und daher unmöglich), aber nicht beweisbar ist (von Natur aus). Ihre Wahrheit ist jedoch innerhalb der Arithmetik nicht offensichtlich, da dies einen Beweis erfordern würde. Nur innerhalb unseres intuitiven Verständnisses der Bedeutung der Aussage können wir erkennen, dass sie wahr sein muss, unabhängig davon, was das System sagen kann oder nicht.

Ein formales logisches System sagt Ihnen nie, was es bedeutet, etwas zu beweisen. Es sagt Ihnen, was in dem Modell funktioniert. Der Punkt ist, dass Sie darauf vertrauen müssen, dass das Modell Ihr wirkliches Denken modelliert und nicht etwas anderes. Andernfalls können Sie es nicht verwenden, um die Natur des Denkens zu diskutieren.

Ohne einen eher beiläufigen Beweis dafür, dass die Beweise, die Sie diskutieren werden, auf unser gewöhnliches Verständnis der wirklichen Bedeutung abbilden, gibt es keinen Grund für den Formalismus. Wenn wir nicht wirklich glauben, dass wir die Rudimente der Sprache zuverlässig darstellen, können wir alle möglichen Dinge über Systeme und Modelle beweisen, und das sagt nicht wirklich etwas über Logik aus.

Dies alles ist Teil von Hilberts Programm des Formalismus, um grundlegende Mathematik von einer platonischen Interpretation zu trennen, indem er beweist, dass alles, was Logik zum Funktionieren bringt, ein Satz von Regeln zur Manipulation von Symbolen ist. Aber dazu müssten wir ein konsistentes und vollständiges Logikmodell finden. Gödel beweist, dass Hilbert falsch liegt. Wir können ein solches System nicht haben, wenn wir Arithmetik in unsere Argumentation einbeziehen wollen.

Argumentation muss also eine Grundlage außerhalb der axiomatischen Methode haben, wenn sie sowohl sinnvoll sein als auch die Grenzen der Argumentation erfassen soll. Sie brauchen entweder eine externe Referenz, die Ihnen eine Möglichkeit gibt, die Vorzüge beider Seiten verschiedener unentscheidbarer Behauptungen zu argumentieren. Oder Sie müssen akzeptieren, dass die Grenzen der Entscheidungsfindung über das hinausgehen, was durch strenge Argumentation in präziser Sprache festgestellt werden kann.