Formale Beweise

 Wir begnügen uns an dieser Stelle mit einer intuitiven und etwas vereinfachenden Beschreibung von formalen Beweisen. Der interessierte Leser findet am Ende dieses Kapitels eine detaillierte Beschreibung eines formalen Beweissystems, des sog. Hilbert-Kalküls.

 Sei Σ ein Axiomensystem von ℒ. Ein formaler Beweis Δ aus Σ ist eine Liste

ψ0,  ψ1,   … ,  ψm;  φ0,  φ1,   … ,  φn

von Formeln von ℒ, die nach bestimmten Regeln gebildet ist. ψ0, … , ψm sind dabei Axiome aus Σ. Intuition ist: Die Formelliste Δ ist ein Beweis von φn mit Hilfe der Axiome ψ0, … , ψm. Die eigentliche Ableitung ist φ0, … , φn. Hierbei entsteht ein φk durch Anwendung einer Regel des Kalküls auf Elemente von ψ0, … , ψm, φ0, … , φk − 1.

 Beispiele für Regeln sind:

(R1)  Aus  φ  und  ψ  bilde  φ ∧ ψ (Und-Einführung),
(R2)  Aus  φ → ψ  und  φ  bilde  ψ (Modus Ponens).

 Seien φ, ψ, χ drei beliebige Sätze von ℒ. Wir betrachten als Beispiel das Axiomensystem

Σ  =  φ,  ψ,  φ ∧ ψ → χ.

Wir können nun die Aussage χ aus Σ formal beweisen, denn

Δ  =  φ, ψ, φ ∧ ψ → χ; φ ∧ ψ, χ.
➀➁   ➂  ➃➄

ist ein Beweis von χ mit Hilfe der Axiome aus Σ: Die ersten drei Elemente ➀, ➁, ➂ von Δ sind Axiome. ➃ entsteht durch Anwendung von (R1) auf ➀ und ➁. ➄, die durch Δ bewiesene Aussage, entsteht durch Anwendung von (R2) auf ➂ und ➃.

 Im Prinzip ließe sich jeder umgangssprachlich bewiesene Satz der Mengenlehre in einer solchen Weise herleiten. Obwohl formale Beweise nur für sehr einfache Sätze der Mengenlehre oder allgemein der Mathematik direkt durchgeführt worden sind, ist man von der prinzipiellen Möglichkeit überzeugt, jeden in üblicher Weise bewiesenen Satz der Mathematik in einen formalen Beweis umwandeln zu können. Die Situation ist ähnlich zur prinzipiellen Auflösbarkeit einer Eigenschaft in ihre Bestandteile, ihre Umwandlung in eine Formel von ℒ: Schreiben wir einen üblichen, umgangssprachlichen mathematischen Beweis immer ausführlicher auf, so nähert sich seine Gestalt einem formalen Beweis. Umgangssprachliche Beweise von wenigen Zeilen können dann Hunderte von Regelanwendungen erforderlich machen − so wie die Auflösung von „R ist eine Relation“ schon eine relativ lange Formel ergibt.