Formale Beweise im Hilbert-Kalkül

Wir besprechen nun ausführlicher einen formalen Beweisbegriff für die Sprache ℒ der Mengenlehre. Damit wird die Formalisierung − oder genauer: die prinzipielle Möglichkeit der Formalisierung − der Mengenlehre vollständig.

Ansätze zu formalen Beweissystemen finden sich in der Syllogistik des Aristoteles. Die Logik blieb dann auch viele Jahrhunderte unter dem Dach der Philosophie hängen, bis sie von der Mathematik als Objekt der Begierde erkannt wurde und in Folge dann endlich den Auszug aus dem Elternhaus hinter sich brachte. Den wichtigsten Fortschritt nach Aristoteles bildeten die Arbeiten von Gottlob Frege (1848 − 1925), und in den Jahrzehnten nach 1900 wurden dann die ersten brauchbaren mathematischen Logikkalküle entwickelt. Prominent sind heute der (Frege-) Hilbert-Kalkül und der Kalkül des natürlichen Schließens von Gerhard Gentzen. Wir verwenden hier den Hilbert-Kalkül, der sich einfach definieren lässt, und der darüber hinaus zur Gewinnung von Resultaten der mathematischen Logik überaus gut zu handhaben ist.

Für das formale Beweisen selbst ist der Kalkül des natürlichen Schließens angenehmer, insbesondere in seiner zweidimensionalen Form, bei der Beweise in Form von Bäumen notiert werden. Der Leser konsultiere Lehrbücher zur mathematischen Logik für die Feinheiten der verschiedenen Kalküle. Die verschiedenen Kalküle sind aber allesamt logisch äquivalent, d. h. sie beweisen dieselben Aussagen. Die Beweise der Kalküle lassen sich darüber hinaus effektiv ineinander übersetzen.

Der Hilbert-Kalkül für ℒ ist ein syntaktisches System auf der Metaebene. Es beschreibt, welche endlichen Folgen von Formeln einen formalen Beweis bilden. Ein formaler Beweis beweist dann immer seine letzte Formel.

Der Hilbert-Kalkül hat zwei Bestandteile: die logischen Axiome und die Schlussregel Modus Ponens. Die logischen Axiome zerfallen in aussagenlogische Axiome, Identitätsaxiome und Quantoraxiome.

Die logischen Axiome des Hilbert-Kalküls

Wir zeichnen bestimmte Formeln von ℒ als logische Grundaxiome aus. Man kann diese Formeln als stillschweigende Axiome ansehen, die jedes Axiomensystem schon mitbringt. Sie liefern keinen mathematischen Inhalt, sondern verbinden die logischen Zeichen miteinander, getreu der intendierten Semantik.

Im Hilbert-Kalkül tauchen wegen des ständigen Einsatzes der Modus-Ponens-Schlussregel (s. u.) sehr häufig Implikationsketten auf. Wir vereinbaren hier Rechtsklammerung, um Klammern zu sparen:

φ → ψ → χ ist φ → (ψ → χ),

φ → ψ → χ → ξ ist φ → (ψ → (χ → ξ)), usw.

Hilfreich für das Lesen solcher Ketten ist die semantische Äquivalenz von „aus φ folgt: aus ψ folgt χ“ mit „aus φ und ψ folgt χ“. Allgemein ist „φ₁ folgt φ₂ folgt … folgt φ_n folgt φ_n + 1“ mit Rechtsklammerung äquivalent zu „aus φ₁ und … und φ_n folgt φ_n + 1“, wobei hier die φ_i beliebige umgangssprachliche mathematische Aussagen sein sollen. Mit dieser Lesart wird etwa (i) und (ii) in der folgenden Definition sofort einsichtig.

Definition (aussagenlogische Axiome)

Eine Formel von ℒ heißt ein aussagenlogisches Axiom von ℒ, wenn sie von einer der folgenden Formen ist:

(i)	φ → ψ → φ,

(ii)	(φ → ψ → χ) → (φ → ψ) → φ → χ,

(iii)

φ ∧ ψ → φ,

(iv)	φ ∧ ψ → ψ,

(v)	φ → ψ → φ ∧ ψ,

(vi)	φ → φ ∨ ψ,

(vii)

φ → ψ ∨ φ,

(viii)

(φ → χ) → (ψ → χ) → φ ∨ ψ → χ,

(ix)	(φ → ψ) → (ψ → φ) → (φ ↔ ψ),

(x)	(φ ↔ ψ) → (φ → ψ) ∧ (ψ → φ),

(xi)	φ ∧ ¬ φ → ψ,

(xii)

¬ ¬ φ → φ.

Man erhält insgesamt einen logisch äquivalenten Kalkül, wenn man hier liberaler jede aussagenlogische Tautologie als Axiom zulässt. Eine aussagenlogische Tautologie ist dabei eine Formel von ℒ, die, quantorfrei notiert, durch das bekannte Wahrheitstafelverfahren für lange Winterabende als wahr in jedem Falle nachgewiesen werden kann. Wir können zum Beispiel ∀xφ → ∀xφ ∨ ∃yφ in der quantorfreien Form ψ → ψ ∨ χ notieren, und alle vier Kombinationen von Wahrheitswerten w (für wahr) oder f (für falsch) für ψ und χ durchspielen, um zu sehen, dass die Auswertung von ∨ und → mit der üblichen Semantik am Ende in allen vier Fällen w ergibt. Es gilt etwa f ∨ f = f, f → f = w, also f → (f ∨ f) = f → f = w, ebenso für die anderen drei Fälle. Allgemeiner hat man 2ⁿ-viele Kombinationen zu überprüfen, wenn eine quantorfreie Formel aus φ₁, …, φ_n zusammengesetzt ist.

Obige Liste von Schemata ist aber übersichtlicher und interessanter als ein allgemeines Tautologie-Schema (alle Axiome der Liste sind Tautologien). Mit ihrer Hilfe kann man zudem sehr leicht sinnvolle restriktive Logiken genau definieren: Der einzige Stein, an dem sich die konstruktive Mathematik im ganzen Hilbert-Park das Knie schlägt, ist das Axiom (xii). Dieses Stabilitäts- oder reductio ad absurdum-Schema ¬ ¬ φ → φ macht die Logik zur klassischen Logik. Lässt man (xii) weg, so erhält man den Hilbert-Kalkül für die − für den klassisch geschulten Geist nicht unbedingt intuitive − intuitionistische Logik (befürwortet vor allem von Brouwer, und formalisiert von Heyting (1930); vgl. auch [Kolmogorov 1925]). Intuitionistisch ist dagegen spaßigerweise immer noch ¬ ¬ ¬ φ → ¬ φ beweisbar, von drei Negationen kann man also zwei fallen lassen.

Gleichwertig zu (xii) über den anderen logischen Axiomen ist das tertium non datur-Schema φ ∨ ¬ φ, das die konstruktive Mathematik ebenso scheut wie das Wegstreichen einer doppelten Negation.

Die sog. Brouwer-Heyting-Kolmogorov Interpretation klärt, was die intuitionistische Logik will: Unter dieser (informalen) Interpretation gilt: Ein Beweis von φ ∧ ψ liegt genau dann vor, wenn ein Beweis von φ und ein Beweis von ψ vorliegt. (Das gilt klassisch genauso.) Ein Beweis von φ ∨ ψ liegt genau dann vor, wenn ein Beweis von φ oder ein Beweis von ψ vorliegt. (Das gilt klassisch nicht: klassisch ist z. B. φ ∨ ¬φ für jede Aussage φ beweisbar, während für jede offene Frage oder jede unabhängige Aussage φ weder ein Beweis von φ noch ein Beweis von ¬ φ vorliegt.) Weiter liegt ein Beweis von φ → ψ genau dann vor, wenn es ein Verfahren gibt, das einen beliebigen Beweis von φ in einen Beweis von ψ transformiert. Und schließlich liegt ein Beweis von ¬ φ genau dann vor, wenn es ein Verfahren gibt, das einen Beweis von φ in einen Beweis einer Formel verwandeln würde, deren Nichtbeweisbarkeit man akzeptiert. (Dies gilt klassisch ebenfalls nicht. Das Schema (xii) ¬ ¬ φ → φ ist gerade etwas, was man mit einer reinen Beweistransformation nicht begründen kann, im Gegensatz zu ¬ ¬ ¬ φ → ¬ φ oder auch φ → ¬ ¬ φ.)

¬ ¬ φ → φ wird in der Mathematik durchgehend verwendet, und die Art und Weise der Verwendung erklärt den Namen reductio ad absurdum: Man will φ zeigen. Hierzu macht man die Annahme non(φ), und zeigt, dass aus dieser Annahme Unfug wie „0 = 1“ hergeleitet werden kann. Dann hat man gezeigt, dass non(φ) nicht gelten kann, d. h. man hat durch das Argument non(non(φ)) gezeigt. Bis hierhin spielt der Konstruktivist mit (bei konstruktiver Argumentation), nicht aber bei dem letzten Schluss von non(non(φ)) auf φ. Man muss den Konstruktivisten rechtgeben, dass ein ständiges „Annahme non(φ)“ zur Manie werden kann, und häufig auch dort eingesetzt wird, wo es nicht nötig ist. Ob das schlimm ist, ist die andere Frage.

Verwandt zu reductio ad absurdum ist das Kontrapositionsgesetz oder das Schema des indirekten Beweisens φ → ψ ↔ ¬ ψ → ¬ φ. Intuitionistisch gilt

(φ → ψ) → ¬ ψ → ¬ φ,

im Allgemeinen aber nicht die Umkehrung, die für das indirekte Beweisen gebraucht wird.

Ein noch restriktiveres System ist die Minimallogik [ Johansson 1937]. Hier lässt man neben (xii) auch noch das ex contradictio quodlibet-Schema

(xi) φ ∧ ¬ φ → ψ

weg. Zudem streicht man das Negationszeichen ¬ aus der Sprache, führt einen 0-stelligen logischen Junktor ⊥, falsum genannt, ein, und definiert dann ¬ φ als die Formel φ → ⊥. Das Zeichen ⊥ selbst gilt als Primformel. Dieses Vorgehen ist auch im Intuitionismus üblich, und ¬ φ als φ → ⊥ zu lesen deckt sich mit der obigen Interpretation, sobald ⊥ als eine Formel ohne Beweis angesehen wird. Klassisch kann man den unbestreitbaren formalen Komfort eines Falsums erreichen, indem man ⊥ als Abkürzung für ψ ∧ ¬ ψ einführt, mit einem beliebigen ψ. Damit ist die nützliche Äquivalenz ¬ φ ↔ φ → ⊥ für alle φ formal beweisbar.

In grober Analogie: Die klassische Logik verhält sich zur intuitionistischen Logik so wie ZFC zu ZF. Und so wie ZF eine interessante Teiltheorie von ZFC ist, ist eine Logik ohne Stabilität zwar etwas wackelig, aber nicht uninteressant.

Definition (Identitätsaxiome)

Eine Formel von ℒ heißt ein Identitätsaxiom von ℒ, wenn sie von einer der folgenden Formen ist:

(i)

x = x,

(ii)	x = y → φ_z(x) → φ_z(y), wobei φ eine Primformel ist.

Definition (Quantoraxiome)

Eine Formel von ℒ heißt ein Quantoraxiom von ℒ, wenn sie von einer der folgenden Formen ist:

(i)	φ → ∀x φ, wobei x nicht frei in φ vorkommt,

(ii)	∀x(φ → ψ) → ∀x φ → ∀x ψ,

(iii)

∀x φ → φ_x(y),

(iv)	φ_x(y) → ∃x φ,

(v)	∀x(φ → ψ) → ∃x φ → ψ, wobei x nicht frei in ψ vorkommt.

Die an dieser Stelle etwas seltsame Variablenbedingung im ersten Schema wird unten klar werden. Semantisch sind die fünf Schemata sicher korrekt.

Definition (logische Axiome des Hilbert-Kalküls für ℒ)

Eine Formel φ von ℒ heißt ein logisches Axiom von ℒ, falls φ eine Generalisierung eines aussagenlogischen Axioms, eines Identitätsaxioms oder eines Quantoraxioms ist.

Ist also φ ein logisches Axiom, so ist ∀x φ ein logisches Axiom für alle Variablen x. Eine Formel φ gilt als Generalisierung von φ, und damit sind alle aufgelisteten Axiome auch logische Axiome. Die Motivation für die technische Variablenbehandlung in der Definition der logischen Axiome wird aus dem Beweis der Generalisierungsregel hervorgehen (s. u.).

Die Schlussregel des Hilbert-Kalküls

Im Hilbert-Kalkül gibt es nur eine Schlussregel, den Modus Ponens:

Definition (Modus Ponens)

Seien φ, ψ, χ Formeln von ℒ. χ entsteht aus φ, ψ durch Anwendung der Regel Modus Ponens, falls ψ von der Form φ → χ ist.

Die Idee ist: Haben wir φ und φ → χ bewiesen, so können wir auf χ schließen. Und diesen Schluss nennen wir Modus Ponens.

Formale Beweise im Hilbert-Kalkül

Definition (formale Beweise im Hilbert-Kalkül für die Sprache der Mengenlehre)

Sei Σ ein Axiomensystem von ℒ. Weiter sei Δ = φ₁, …, φ_n eine endliche Liste von ℒ-Formeln. Δ heißt ein (formaler) Beweis aus Σ oder eine Herleitung aus Σ, falls für alle 1 ≤ i ≤ n gilt:

(i)	φ_i ist ein logisches Axiom oder

(ii)	φ_i  ∈  Σ oder

(iii)

es existieren 1 ≤ k, ℓ < i derart, dass φ_i aus φ_k, φ_ℓ durch Anwendung von Modus Ponens entsteht.

Beim Beweisen darf man also die logischen Axiome und die Axiome der gewählten untersuchten Axiomatik Σ frei einsezten. Alles andere ist ein Übergang von zwei bereits bewiesenen Formeln der Form φ und φ → χ auf die Formel χ mit Hilfe der einzigen Schlussregel des Kalküls. Es ist bemerkenswert, dass sich das Beweisen so einfach und übersichtlich formal fassen lässt.

Definition (Beweisbarkeit einer Formel, Länge eines Beweises)

Sei Σ ein Axiomensystem von ℒ, und sei φ eine Formel von ℒ. φ heißt (formal) beweisbar aus Σ oder herleitbar aus Σ, in Zeichen Σ ⊢ φ [gelesen: Σ beweist φ], falls gilt:

Es existiert ein Beweis Δ = φ₁, …, φ_n aus Σ mit φ = φ_n.

Δ heißt dann ein Beweis von φ aus Σ der Länge n.

Wir schreiben ⊢ φ, falls ein leeres Axiomensystem φ beweist, d. h. falls ein Beweis von φ existiert, der nur (i) und (iii) verwendet. Gilt ⊢ φ, so nennen wir φ (logisch) beweisbar.

Analog sind Σ, Σ′ ⊢ φ sowie Σ, ψ ⊢ φ definiert für Axiomensysteme Σ, Σ′ und Formeln ψ. Σ, Σ′ ⊢ φ heißt, dass in einem Beweis von φ Axiome aus Σ und Σ′ verwendet werden dürfen. Σ, ψ ⊢ φ heißt, dass in einem Beweis von φ neben Axiomen aus Σ auch die Formel ψ als Axiom verwendet werden darf.

Es gilt Σ ⊢ φ (in einem Schritt) für alle φ  ∈  Σ und φ ⊢ φ für alle Formeln φ.

Durchgehend verwendet werden die folgenden Beobachtungen einfacher Natur:

Übung

Für alle Axiomensysteme Σ und alle Formeln φ gilt:

(i)	Ist Δ = φ₁, …, φ_n ein Beweis aus Σ, so gilt Σ ⊢ φ_i für alle 1 ≤ i ≤ n.

(ii)	Gilt Σ ⊢ φ, so existieren Axiome ψ₁, …, ψ_n aus Σ mit ψ₁, …, ψ_n ⊢ φ.

Anfangsstücke von Beweisen sind Beweise. Und formale Beweise sind immer finit: Obwohl ein Axiomensystem aus unendlich vielen Formeln bestehen kann, werden in einem Beweis immer nur endlich viele Axiome verwendet.

In jedem Kalkül verwenden Beweise Grundannahmen, und ziehen Schlüsse aus diesen Annahmen. Die eigentliche Dynamik eines Beweises im Hilbert-Kalkül steckt im Modus Ponens. Wenn wir in nichttrivialer Weise χ beweisen wollen, müssen wir vorher irgendwann für ein φ die Formeln φ → χ und φ bewiesen haben. Welches φ man hierbei anstrebt, ist die Kunst. Das gleiche gilt nun aber für φ: φ ist entweder ein Axiom, oder entstanden aus ψ → φ und ψ. Ähnliches gilt für ψ. Trivial oder Modus Ponens. Tertium non datur.

Das tatsächliche formale Beweisen im Hilbert-Kalkül ist qualvoll. Dante hätte es in seiner Göttlichen Komödie gut verwenden können. Wer während seines Lebens etwas gegen die Logik gesagt hat, muss in der Hölle formale Beweise im Hilbert-Kalkül führen. Auf Erden verschafft der folgende Satz aus der logischen Apotheke Linderung:

Satz (Deduktionstheorem)

Seien Σ ein Axiomensystem und ψ, φ Formeln von ℒ. Dann sind äquivalent:

(i)

Σ, ψ ⊢ φ,

(ii)	Σ ⊢ ψ → φ.

Beweis

(i) ↷ (ii): Wir zeigen die Aussage durch metamathematische Induktion über die Länge n ≥ 1 eines formalen Beweises Δ von φ aus Σ, ψ. Entscheidend hierbei sind die aussagenlogischen Axiome (i) und (ii).

Induktionsschritt n

Sei Δ = φ₁, φ₂, …, φ_n ein Beweis von φ_n = φ aus Σ, ψ.

1. Fall: φ ist ein logisches Axiom oder ein Axiom von Σ.

Dann ist φ, φ → ψ → φ, ψ → φ ein Beweis von ψ → φ aus Σ.

2. Fall: φ entsteht durch Anwendung von Modus Ponens.

Dann existieren k, ℓ < n mit φ_ℓ = φ_k → φ. Nach Induktionsvoraussetzung existieren Beweise

(a)	η₁, …, η_m	von η_m = ψ → φ_ℓ = ψ → φ_k → φ aus Σ,
(b)	ξ₁, …, ξ_m′	von ξ_m′ = ψ → φ_k aus Σ.

Dann ist

η₁, …, η_m − 1, ψ → φ_k → φ, ξ₁, …, ξ_m′ − 1, ψ → φ_k,

(ψ → φ_k → φ) → (ψ → φ_k) → ψ → φ, (ψ → φ_k) → ψ → φ, ψ → φ

ein Beweis von ψ → φ aus Σ.

(ii) ↷ (i): Sei φ₁, … φ_n ein Beweis von φ_n = ψ → φ aus Σ. Dann ist

φ₁, …, φ_n − 1, ψ → φ, ψ, φ

ein Beweis von φ aus Σ, ψ.

Die absolutistische Existenz des Modus Ponens ist eine Besonderheit des Hilbert-Kalküls. Diese Regierungsform wird zwar von einer Unzahl logischer Axiome gestützt, aber ohne das Deduktionstheorem käme es sofort zur Revolution. Der Leser wird bei den Übungen unten sehen, wie nützlich das Deduktionstheorem tatsächlich ist.

Beispiel

Wir zeigen φ → ψ → χ ⊢ ψ → φ → χ. Es gilt φ → ψ → χ ⊢ φ → ψ → χ. Zweimalige Anwendung des Deduktionstheorems liefert, dass φ → ψ → χ, φ, ψ ⊢ χ. Damit gilt auch φ → ψ → χ, ψ, φ ⊢ χ. Eine erneute zweimalige Anwendung des Deduktionstheorems liefert nun φ → ψ → χ ⊢ ψ → φ → χ.

Daneben ist der Satz von theoretischer Bedeutung. Hierzu betrachten wir noch eine Verallgemeinerung. Durch Induktion folgt aus dem Deduktionstheorem, dass für alle Axiomensysteme Σ und alle Formeln φ, ψ₁, …, ψ_n gilt:

Σ, ψ₁, …, ψ_n ⊢ φ gdw Σ ⊢ ψ₁ → … → ψ_n → φ.

Es folgt, dass alles, was ein endliches Axiomensystem beweisen kann, sich im wesentlichen in der reinen Logik abspielt. Denn ist Σ = ψ₁, …, ψ_n, so gilt für alle φ:

Σ ⊢ φ gdw ⊢ ψ₁ → … → ψ_n → φ.

Ein zum Beweis des Deduktionstheorems analoges Argument liefert die folgende Generalisierungsregel:

Satz (Generalisierungsregel)

Sei Σ ein Axiomensystem von ℒ, und sei φ eine Formel von ℒ mit Σ ⊢ φ. Weiter sei x eine Variable, die in keiner Formel von Σ frei vorkommt. Dann gilt Σ ⊢ ∀x φ.

Beweis

Wir zeigen die Aussage durch metamathematische Induktion über die Länge n ≥ 1 eines formalen Beweises Δ von φ aus Σ. Entscheidend hierbei sind die Quantoraxiome (i) und (ii).

Induktionsschritt n

Sei Δ = φ₁, φ₂, …, φ_n ein Beweis von φ_n = φ aus Σ.

1. Fall: φ ist ein logisches Axiom oder ein Element von Σ.

Dann ist φ, φ → ∀x φ, ∀x φ ein Beweis von ∀x φ aus Σ, denn nach Voraussetzung ist x nicht frei in φ_n.

2. Fall: φ entsteht durch Anwendung von Modus Ponens.

Dann existieren k, ℓ < n mit φ_ℓ = φ_k → φ. Nach Induktionsvoraussetzung existieren Beweise

(a)	η₁, …, η_m	von η_m = ∀x φ_ℓ = ∀x. φ_k → φ aus Σ,
(b)	ξ₁, …, ξ_m′	von ξ_m′ = ∀x φ_k aus Σ.

Dann ist

η₁, …, η_m − 1, ∀x. φ_k → φ, ξ₁, …, ξ_m′ − 1, ∀x φ_k,

(∀x. φ_k → φ) → ∀x φ_k → ∀x φ, ∀x φ_k → ∀x φ, ∀x φ

ein Beweis von ∀x φ aus Σ.

Die Generalisierungsregel entspricht der Anschauung: Hat man φ(x) bewiesen und über x nichts vorausgesetzt (vgl. „Sei x beliebig.“), so hat man φ(x) für alle x bewiesen.

Besteht ein Axiomensystem Σ, wie etwa ZFC, nur aus Aussagen, so beweist Σ eine Formel φ(x₁, …. x_n) genau dann, wenn Σ die Aussage ∀x₁, …, x_n φ beweist. (Die Richtung von rechts nach links erhält man durch iterierte Anwendung des Quantoraxioms ∀x ψ → ψ_x(y) und Modus Ponens.)

In manchen Formulierungen des Hilbert-Kalküls wird eine Generalisierungsregel als zweite Schlussregel neben dem Modus Ponens verwendet: Von φ darf man immer auf die Formel ∀x φ schließen, wenn x nicht frei in φ vorkommt. Ein Axiomensystem Σ muss dann ausschließlich aus Aussagen bestehen, was keine wesentliche Einschränkung ist. Eine einzige Schlussregel zu haben wird aber dem Hilbert-Kalkül als Staatsform sicher gerechter und vereinfacht seine metatheoretische Untersuchung.

Übung

Für alle Formeln φ, ψ, χ, alle Variablen x und alle Axiomensysteme Σ gilt:

(i)	⊢ φ → ψ → χ ↔ φ ∧ ψ → χ,

(ii)	⊢ ¬ φ ↔ φ → ψ ∧ ¬ ψ,

(iii)

⊢ φ ∨ ¬ φ,

(iv)	Σ, φ ⊢ ψ und Σ, ¬ φ ⊢ ψ folgt Σ ⊢ ψ,

(v)	⊢ (φ → ¬ φ) → ¬ φ,

(vi)	⊢ (φ ∨ ψ ) → ¬ ψ → φ,

(vii)

⊢ φ → ψ ↔ ¬ φ ∨ ψ,

(viii)

⊢ φ → ψ ↔ ¬ ψ → ¬ φ,

(ix)	⊢ φ ∨ ψ ↔ ¬ (¬ φ ∧ ¬ ψ),

(x)	⊢ ∀x φ ↔ ¬ ∃x ¬ φ.

(xi)	⊢ ∃x φ ↔ ¬ ∀x ¬ φ.

Es ist instruktiv zu verfolgen, für welche formale Beweise hierbei (und für welche Richtungen von ↔) das Schema ¬ ¬ φ → φ verwendet wird.

Widerspruchsfreiheit

Definition (Widerspruchsfreiheit)

Sei Σ ein Axiomensystem von ℒ. Σ heißt widerspruchsfrei oder konsistent, falls es eine Formel φ gibt mit non(Σ ⊢ φ).

Nach der Übung oben gilt: Σ ist widerspruchsfrei gdw jeder endliche Teil Σ′ von Σ ist widerspruchsfrei.

Wir halten eine fundamentale Äquivalenz fest.

Satz (widerspruchsfreie Erweiterungen)

Seien Σ ein Axiomensystem und φ eine Formel von ℒ. Dann sind äquivalent:

(i)	Σ erweitert um das Axiom φ ist widerspruchsfrei.

(ii)	non(Σ ⊢ ¬ φ).

Beweis

(i) ↷ (ii): Sei ψ eine Formel mit non(Σ, φ ⊢ ψ). Annahme, es gilt Σ ⊢ ¬ φ. Sei dann φ₁, …, φ_n = ¬ φ ein Beweis von ¬ φ aus Σ. Dann ist

φ₁, …, φ_n − 1, ¬ φ, φ, ¬ φ → φ → ψ, φ → ψ, ψ,

ein Beweis von ψ aus Σ, φ, wobei wir die beweisbare Formel ¬ φ → φ → ψ verwenden. Dies ist ein Widerspruch zur Wahl von ψ.

(ii) ↷ (i): Wir zeigen non(i) ↷ non(ii). Sei also Σ erweitert um φ widerspruchsvoll. Dann gilt Σ, φ ⊢ ¬ φ. Nach dem Deduktionstheorem gilt also Σ ⊢ φ → ¬ φ. Aber (φ → ¬ φ) → ¬ φ ist beweisbar. Modus Ponens liefert dann Σ ⊢ ¬ φ, also non(ii).

Aus non(Σ ⊢ φ) kann i.a. nicht auf Σ ⊢ ¬ φ geschlossen werden. Die Existenz unabhängiger Aussagen macht diesen Schluss zunichte.

Definition (unabhängig)

Sei Σ ein Axiomensystem, und sei φ eine Formel von ℒ. φ heißt unabhängig von Σ, falls gilt:

non (Σ ⊢ φ) und non (Σ ⊢ ¬ φ).

Die Existenz einer von Σ unabhängigen Aussage impliziert offenbar die Widerspruchsfreiheit von Σ. Andererseits besagt der erste Gödelsche Unvollständigkeitssatz: Ist eine axiomatische Erweiterung Σ von ZFC widerspruchsfrei, so existieren immer von Σ unabhängige Aussagen. Also decken auch beliebig starke Erweiterungen von ZFC nie alles ab. Die unabhängigen Aussagen des Gödelresultats sagen etwa „ich bin nicht beweisbar in Σ“. Dass solche Aussagen unabhängig sind, irritiert nicht unbedingt. Das wirklich Aufregende ist nun aber, dass wir über ZFC unabhängige Aussagen mit einem klaren mengentheoretischen Gehalt kennen:

Formale Form des Fundamentalsatzes der Mengenlehre

Ist ZFC widerspruchsfrei, so ist (CH) unabhängig von ZFC.

Dieser Satz ist (wie etwa das Deduktionstheorem) ein Metatheorem. Für den Beweis wird viel Mengenlehre verwendet, und keine Syntaxanalyse des Kalküls. Letztendlich liefert der Beweis des Fundamentalsatzes dann aber sogar ein Verfahren, das zeigt, wie wir einen Beweis von (CH) oder von ¬ (CH) in ZFC in einen Beweis eines Widerspruchs ψ ∧ ¬ ψ verwandeln können.

Übersetzung des formalen Rahmens in die Objektebene

Man kann mathematische Logik ganz allgemein in der Mengenlehre entwickeln, und ℒ erscheint dann in der Objektebene als spezielle prädikatenlogische Sprache. Als Zeichen der Sprache wählt man geeignete Mengen, etwa ∧ = 3, ∀ = 7, v₀ = 0, v₁ = 2, v₂ = 4, usw. Formeln sind dann wieder bestimmte Folgen von Zeichen, und formale Beweise auf der Objektebene sind bestimmte endliche Folgen von Formeln. Der Transport von Begriffen und Resultaten funktioniert problemlos von der Metaebene in die Objektebene, und wird üblicherweise durch Klammern ⌈, ⌉ bezeichnet. Etwa ⌈∧⌉ = 3, ⌈∀ v₂ ∧ ∧⌉ = (7, 4, 3, 3). Formale Beweise der wirklichen Welt übersetzen sich in formale Beweise im Mengenuniversum. ZFC wird zu einer Menge ⌈ZFC⌉ von Aussagen auf der Objektebene. Con(⌈ZFC⌉) ist die Aussage, das es keinen Beweis in ⌈ZFC⌉ von ⌈∃v₀ v₀ ≠ v₀⌉ gibt (hierbei steht „Con“ für engl. „consistent“).

Auf der Metaebene haben wir:

(i)	Ist ZFC widerspruchsfrei, so gilt non(ZFC ⊢ CH).

(ii)	Ist ZFC widerspruchsfrei, so gilt non(ZFC ⊢ ¬ CH).

In die Objektebene übersetzt sich das etwa als:

(i)	ZFC ⊢ Con(⌈ZFC⌉) → Con(⌈ZFC + ¬ CH⌉).

(ii)	ZFC ⊢ Con(⌈ZFC⌉) → Con(⌈ZFC + CH⌉).

De facto lässt sich die Spiegelung der Metaebene in eine Objektebene in einer viel schwächeren Theorie ausführen, und man kann ZFC links von ⊢ in (i) und (ii) etwa durch die Peano-Dedekind-Arithmetik PA ersetzen, wobei dann nicht nur Zeichen, sondern auch z. B. Formeln und Beweise als Zahlen kodiert werden müssen. Die Arithmetik kann sehr gut darüber nachdenken, was die Mengenlehre ⌈ZFC⌉ beweisen kann.

Die Übersetzung von der Objektebene in die Metaebene ist wesentlich problematischer. Hierzu betrachten wir den zweiten Gödelschen Unvollständigkeitssatz für ZFC. Er lautet schlicht und ergreifend:

(+) Ist ZFC widerspruchsfrei, so gilt non(ZFC ⊢ Con(⌈ZFC⌉)).

Im Folgenden nehmen wir an, dass ZFC widerspruchsfrei ist. Dann ist nach (+) auch das schräge Axiomensystem ZFC* = ZFC + ¬ Con(⌈ZFC⌉) widerspruchsfrei. Es gilt:

ZFC* ⊢ ⌈es gibt einen Beweis b von ⌈0 = 1⌉ in ⌈ZFC⌉ ⌉.

Ein Beweis b von 0 = 1 in ZFC auf der Objektebene kann aber dann nicht in einen Beweis von 0 = 1 in ZFC auf der Metaebene übersetzt werden, d. h. es gibt keinen Beweis Δ mit ⌈Δ⌉ = b. Andernfalls wäre ZFC widerspruchsvoll. Wie kann eine solche Übersetzung schiefgehen? Der Grund ist: b ist unendlich lang, die Objektebene eines ZFC*-Universums hat einen anderen Endlichkeitsbegriff als die Metaebene − und als das platonische Mengenuniversum V. „Das“ ω von ZFC*, ω* genannt, ist länger als ein platonisches ω, obwohl die Theorie ZFC* felsenfest davon überzeugt ist, dass ω* die erste Limesordinalzahl ist und genau die Menge der endlichen Ordinalzahlen darstellt.

Für den Platoniker ist Con(⌈ZFC⌉) äquivalent mit der Widerspruchsfreiheit von ZFC. Zudem beweisen große Kardinalzahlen die Aussage Con(⌈ZFC⌉). Axiomensysteme wie ZFC* sind für den Platoniker lediglich ein weiteres Beispiel dafür, dass es wahre Aussagen gibt, die sich nicht in einer begrenzten Theorie wie ZFC beweisen lassen.

Man kann den zweiten Gödelschen Unvollständigkeitssatz in die Objektebene übersetzen und erhält dann:

(+) ZFC ⊢ Con(⌈ZFC⌉) → Con(⌈ZFC + ¬ Con(⌈ZFC⌉)⌉).

Das ist interessant, aber unbedenklich. Sehr bedenklich wäre dagegen:

(−) ZFC ist widerspruchsfrei, aber ZFC ⊢ ¬ Con(⌈ZFC⌉).

Dieses metamathematische Kuriosum kann niemand als Nonsens entlarven, der ganz in ZFC verbleibt.

Der Platonist sagt: „Man lasse sich durch diese logischen Tricks im Umfeld der Gödelresultate nicht verwirren, sondern eher in seiner platonischen Haltung bestärken. ZFC ist eine hübsche Sammlung von wahren Aussagen über das Universum V, die Sätze von ZFC erfassen aber nicht alle wahren Aussagen. Z. B. ist Con(⌈ZFC⌉) eine wahre Aussage, die nicht in ZFC beweisbar ist.“ Für den Erzplatonisten ist (CH) viel beunruhigender als ZFC*-Spielereien: Er weiß nicht, ob (CH) in V gilt oder nicht. Er sucht nach mehr Wissen über Mengen, um irgendwann zu sehen, ob (CH) wahr ist oder falsch. ZFC gilt ihm als ein guter Anfang, aber sicher nicht als das letzte Wort.

Es gibt viele andere Dinge, die ZFC nicht beweisen kann, die ein Platoniker aber fast für selbstverständlich hält. Nach dem Gödelschen Vollständigkeitssatz gilt:

ZFC ⊢ Con(⌈ZFC⌉) ↔ ∃M M ⊨ ⌈ZFC⌉.

Nach dem zweiten Unvollständigkeitssatz kann also ein widerspruchsfreies ZFC nicht zeigen, dass es ein Modell von ⌈ZFC⌉ gibt.