Einführung in die Mathematische Logik Universität Bonn, Sommersemester 2002

Vorläufiges Skript

Peter Koepke 12. Mai 2002

1 Einleitung

Ausgehend von der üblichen mathematischen Praxis motivieren wir skizzenartig Fragen und Techniken der Mathematischen Logik. 1.1. Was ist Mathematik?

• Inhalte und \underline{Methoden}

• \underline{Definitionen} und \underline{Beweise}.

• Mathematische \underline{Sprache}: ”Buchstabenrechnen“, (Rechen-)terme, mathematische \underline{Zeichen}: =, <,…; wenn … dann …, für alle x ….

• Exaktheit und Eindeutigkeit der mathematischen Sprache, z.B. durch Klammerung: (a + b) + c, a + (b + c).

• \underline{Logische Schlüsse}. 1.2. Logische Schlüsse

• Logische Schlüsse führen von wahren Aussagen zu wahren Aussagen.

• Logische Schlüsse sind \underline{allgemeingültig} und \underline{sicher}, sie treffen in allen beschriebenen Situationen mit vollkommener Sicherheit zu.

• Alle eingehenden Voraussetzungen sind \underline{explizit}, es gibt keine versteckten Nebenbedingungen.

• Die Schlüsse bauen auf Grundannahmen auf (\underline{Axiome}).

1.3. Die axiomatische Methode

• Definitionen und logische Schlüsse.

• Entstehung: klassische griechische Mathematik, 500 - 300 v. Chr., Thales, Pythagoras, Euklid, (Aristoteles, Platon).

• Entwicklung: Landvermessung, Rechnen, Rechenregeln ⇒ Geometrie, Arithmetik.

1.4. Neuzeit

• Nicht-euklidische Geometrie, Gruppentheorie, Peano-Axiome für die Zahlentheorie, Hausdorffsche Axiome für die Topologie, …

• Mengenlehre: Axiome von Zermelo, Fraenkel u.a.; ein umfassendes Axiomensystem, in dem sich alle mathematischen Theorien entwickeln lassen.

• Mathematik = Zermelo-Fraenkelsche Axiome für Mengen + logische Schlüsse.

1.5. Vorlesungsinhalte

• Formale Sprachen, Interpretationen von formalen Sätzen in mathematischen Strukturen, Beweise, Beweiskalküle.

• Formale Sprachen können selbst als mathematische Strukturen verstanden werden, auf denen der Beweiskalkül operiert.

• Mathematische Beschreibung von Sprachen und Beweisen.

• Sätze über Sprachen und Beweise.

• Wir arbeiten zunächst in der Aussagenlogik, die dem Boole’schen Verknüpfen von Wahrheitswerten entspricht. Danach wenden wir uns der Prädikatenlogik zu, in der mit Hilfe von Quantoren ”quantitative“ Aussagen formalisiert werden können.

• Ziel der Vorlesung: Gödelscher Vollständigkeitssatz: es gibt Beweiskalküle, in denen sich jeder mathematische Beweis nachbilden lässt.

• In der Vorlesung werden auch formale Kalküle vorgestellt, deren Aussagen in grammatikalisch korrektem Deutsch formuliert sind und die zur Formalisierung von Teilen der Mathematik praktisch geeignet sind (Mizar - MSE).

1.6. Literaturhinweise:

1.7. Beispiele von (formalen) Beweisen Zunächst ein gewöhnlicher Beweis für die Irrationalität von \sqrt{2}.

1.8. Satz. Hippasus ? \sqrt{2} ist irrational.

\underline{Beweis}: Angenommen, die Behauptung ist falsch. Wähle m, n aus den natürlichen Zahlen, so dass \sqrt{2} = \frac{m}{n} und (m ist ungerade oder n ist ungerade). 2 = \frac{m^{2}}{n^{2}} . 2 · n · n = m · m. m · m ist gerade. m ist gerade. Wähle m′ aus den natürlichen Zahlen so dass m = 2 · m′. 2 · n · n = (2 · m′) · (2 · m′). n · n = 2 · m′ · m′. n · n ist gerade. n ist gerade. Also Widerspruch. qed.

Derselbe Beweis mit unterstrichenen Schlüsselwörtern (Keywords):

1.9. Satz. Hippasus ? \sqrt{2} \underline{ist} irrational.

\underline{Beweis}: \underline{Angenommen}, die \underline{Behauptung} \underline{ist falsch}. \underline{Wähle} m, n \underline{aus} den natürlichen Zahlen \underline{so dass} \sqrt{2} = \frac{m}{n} \underline{und} (m ist ungerade \underline{oder} n ist ungerade). 2 = \frac{m^{2}}{n^{2}} . 2 · n · n = m · m. m · m ist gerade. m ist gerade. \underline{Wähle} m′ \underline{aus} den natürlichen Zahlen \underline{so dass} m = 2 · m′. 2 · n · n = (2 · m′) · (2 · m′). n · n = 2 · m′ · m′. n · n ist gerade. n ist gerade. \underline{Also} \underline{Widerspruch}. \underline{qed}.

1.10. Beweisstrukturen

• Grossräumige Beweisstruktur: … Beweis … qed.

• Folge mathematischer Aussagen.

• Strukturierung durch Schlüsselwörter.

• innerhalb der Aussagen: und, oder, ….

• Beweisstruktur, Beweismethoden: Beweis, angenommen, Behauptung, wähle, aus, also, ….

1.11. Weitere Aspekte

• Implizite Benutzung zahlreicher Begriffe und Eigenschaften von natürlichen Zahlen.

• Benutzung abkürzender oder suggestiver sprachlicher Konventionen.

• Mathematische ”Eleganz“ versus Genauigkeit / Beweislänge.

• Kompromiss in Abhängigkeit vom mathematischen Verständnis des Lesers.

• Analoge Situation: umgangssprachliche Beschreibung eines Algorithmus versus Computerprogramm.

1.12. Das System Mizar-MSE

• Beweisprüfer (proof checker).

• Autoren: A. Trybulec, P. Rudnicki u.a., 1973 - .

• Sprache: Kompromiss zwischen mathematischer ”Umgangssprache“und formaler Sprache.

• Beweissystem akzeptiert recht komplizierte logische Schlüsse (Intelligenz, kleiner integrierter automatischer Beweiser).

• Online proof checker:

http://ugweb.cs.ualberta.ca/ c272/Online/mizar.cgi

1.13. Der Irrationalitätsbeweis in Mizar-MSE Es folgt eine Version des obigen Beweises in einer deutschen Version des Systems Mizar-MSE. Wörter wie ”Benutze, Fixiere, Beweis“ sind Schlüsselworte der Sprache. Die geschickt gewählte Grammatik der formalen Sprache und die Automatisierung trivialer logischer Zwischenschritte führt zu formalen Beweisen, die auch von Menschen gelesen und akzeptiert werden können. Der folgende Beweis ist strikt formal. Er ist direkt aus dem Beweissystem kopiert, das den Beweis mit den Worten ”Danke, OK“ akzeptiert hat.

======================= == \sqrt{2} ist irrational ======================= Axiome == Einfache zahlentheoretische Axiome Benutze m,m’,n,p,q,q1,q2 fuer Zahlen. Fixiere 2 aus Zahlen. == Das Praedikat prod[m,n,p] bedeutet, dass == p das Produkt von m und n ist. == Das Praedikat Q[m] bedeutet, dass der Exponent der 2 == in der Primfaktor-Zerlegung von m gerade ist. == N ist zu Q komplementaer.

Ax1: Fuer m ist Q[m] gdw nicht N[m]. Ax2: N[2]. Ax3: Fuer m,n,p mit prod[m,n,p] und Q[m] und Q[n] ist Q[p]. Ax4: Fuer m,n,p mit prod[m,n,p] und N[m] und N[n] ist Q[p]. Ax5: Fuer m,n,p mit prod[m,n,p] und Q[m] und N[n] ist N[p].

Folgerungen

== Quadratzahlen erfüllen Q: Lemma: Fuer m,q mit prod[m,m,q] ist Q[q] Beweis Betrachte m,q. Angenommen 1: prod[m,m,q]. Fallunterscheidung: Q[m] oder nicht Q[m]. Fall1: Nun angenommen a: Q[m]. Also Q[q] nach a,1,Ax3. Ende. Fall2: Nun angenommen a: nicht Q[m]. b: N[m] nach a,Ax1. Also Q[q] nach b,1,Ax4. Ende. Also Q[q] nach Fallunterscheidung, Fall1, Fall2. Ende. == Der Irrationalitätssatz: Satz: Nicht (existieren m,n,q1,q2 mit prod[m,m,q1] und prod[n,n,q2] und prod[q1,2,q2]) Beweis Angenommen a: nicht Behauptung. Waehle m,n,q1,q2 so dass b: prod[m,m,q1] und prod[n,n,q2] und prod[q1,2,q2] nach a. c: Q[q1] nach Lemma, b. d: Q[q2] nach Lemma, b. e: N[q2] nach b,c,Ax2,Ax5. Also Widerspruch nach d,e,Ax1. Ende. !! !! Danke, OK !! ———-

2 Aussagenlogik

Ziel der Vorlesung ist die Entwicklung und Untersuchung eines abstrakten und angemessenen Formalisierung von ”Beweisen“ und damit zusammenhängenden Begriffen. Wir beginnen mit einer radikalen Abstraktion, bei der komplette Aussagen als Grundeinheiten verwendet werden. Von der inneren Struktur, etwa ob es sich überhaupt um mathematische Aussagen handelt, wird vollkommen abstrahiert. Derartige Aussagen können durch einfache logische Operatoren verknüpft werden. Die Berechnung von Wahrheitswerten erfolgt in einer einfachen binären Algebra von Wahrheitswerten. Die Analyse der Aussagenlogik zeigt in sehr einfacher Form bereits einige Phänomene der später zu behandelnden Prädikatenlogik auf. Die Prädikatenlogik kann als Erweiterung der Aussagenlogik verstanden werden.

2.1. • Reduktion auf: ⋯ oder, und, nicht, impliziert · · · .

• “Mathematische Sätze” sind dann beispielsweise von der Form: ((A und B) impliziert A) ((A und (A impliziert B)) impliziert B).

• Aussagenvariablen: A, B, …, X_{0}, X_{1}, …; A ist wahr/falsch.

• aussagenlogische Verknüpfungen: oder, und, ….

2.2. Definition. Die Algebra der Wahrheitswerte Definiere eine Algebra

({0, 1}, oder, und, nicht, impliziert, gdw)

der Wahrheitswerte durch:

a: 0 ˆ= falsch, 1 ˆ= wahr b: Definiere Verknüpfungen auf 0, 1:

oder 0 1  und 0 1
0 0 1  0 0 0
1 1 1  1 0 1
nicht  impliziert 0 1
0 1  0  1 1
1 0  1  0 1
gdw 0 1
0 1 0
1 0 1

2.3. Zur Implikation Prinzipiell stellen die obigen ”Wahrheitstafeln“ willkürlich gewählte Operationen auf den Wahrheitswerten 0 und 1 dar. Während die Setzungen für ”oder, und, nicht und gdw“ sofort akzeptiert werden, stößt das ”impliziert“ gelegentlich auf Ablehnung.

• (falsch impliziert wahr) = wahr

• ”Der Mond ist blau“ impliziert ”(−1) · (−1) = +1“?

Die letzte Frage muss nach Definition von ”impliziert“ mit ”ja“ beantwortet werden. Dies bedeutet allerdings nicht, dass hier ein kausaler Zusammenhang vorläge. Vielmehr ist der Wahrheitswert links kleiner oder gleich dem Wahrheitswert auf der rechten Seite. Diese Setzung kann auch dadurch motiviert werden, dass die Gesetze der Logik andernfalls komplizierter werden würden. Ein Vergleich mit der Arithmtik: die intuitiv schwer zu vermittelnde Rechenregel (−1)×(−1) = +1 ist notwendig, um Rechengesetze der nicht-negativen ganzen Zahlen unverändert auf alle ganzen Zahlen ausdehnen zu können. Die Festlegung von ”impliziert“ erscheint vielleicht einsichtiger im Zusammenhang von Aussagen mit Variablen. Es gilt:

• für x aus den reellen Zahlen ist x ≥ 0 impliziert \sqrt[3]{x} existiert.

Für den Spezialfall x = −1 haben wir dann eine Situation, die dem obigen ”blauen“ Mond entspricht; als Spezialfall einer wahren Aussage sollte sie ebenfalls den Wahrheitswert ”wahr“ erhalten:

• −1 ≥ 0 impliziert \sqrt[3]{−1} existiert!

• Merke: A impliziert B heißt nicht: ”A ist der Grund für B“.

Die Sprache der Aussagenlogik

2.4. Definition. Die Sprache der Aussagenlogik besteht aus folgenden Komponenten: a: Konstanten F und W für ”falsch“ und ”wahr“. b: Variablen: X_{0}, X_{1}, · · · . c: Ausdrücken: jede Variable ist ein Ausdruck,

jede Konstante ist ein Ausdruck,

wenn A und B Ausdrücke sind, so auch (A ∨ B) (A oder B) (A ∧ B) (A und B) ¬A (nichtA) (A → B) (A impliziert B) (A ↔ B) (A gdw. B).

Beispiele: A ∧ (A → B)

((A ∧ (A → B)) → B).

Konventionen: Weglassen äußerer Klammern, ... Interpretationen von Ausdrücken

2.5. Definition. a: Eine Belegung ist eine Funktion β : ℕ → {0, 1}, d.h. eine Zuordnung von Wahrheitswerten 0/1 zu den Variablen. b: Definiere für einen Ausdruck A und eine Belegung β die Interpretation A^{β} rekursiv:

X_{n}^{β} = β(n)

F^{β} = 0
W^{β} = 1
(A ∨ B)^{β} = A^{β} oder B^{β}
(A ∧ B)^{β} = A^{β} und b^{β}
(¬A)^{β} = nicht A^{β}
(A → B)^{β} = A^{β} impliziert B^{β}
(A ↔ B)^{β} = A^{β} gdw B^{β}

Bemerkung: Nur die in A vorkommenden Variablen sind für A^{β} relevant. c: Definiere: β ist ein Modell von A, β ⊧ A, oder β erfüllt A, falls A^{β} = 1.

2.6. Boolesche Funktionen

• Ein Ausdruck A bestimmt die Boolesche Funktion β ↦ A^{β}.

• Beispiel: A = ((X_{0} ∧ (X_{0} → X_{1})) → X_{1}).

\begin{matrix}X_{0} & X_{1} & (X_{0} → X_{1}) & (X_{0} ∧ (X_{0} → X_{1})) & A \\ 0 & 0 & 1 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 1 & 1 & 1 & 1 & 1 \end{matrix}

Dieser Ausdruck A ist also unter allen Interpretationen richtig, man sagt, dass A eine Tautologie ist.

• Identifiziere A mit der entsprechenden Operation β ↦ A^{β}.

Rechengesetze

2.7. Satz. β ⊧ (X_{0} ∧ X_{1}) ↔ ¬(¬X_{0} ∨ ¬X_{1}).

Beweis:

\begin{matrix}X_{0} & X_{1} & ¬X_{0} & ¬X_{1} & ¬X_{0} ∨ ¬X_{1} & ¬(¬X_{0} ∨ ¬X_{1}) \\ 0 & 0 & 1 & 1 & 1 & 0 \\ 0 & 1 & 1 & 0 & 1 & 0 \\ 1 & 0 & 0 & 1 & 1 & 0 \\ 1 & 1 & 0 & 0 & 0 & 1 \end{matrix}

QED

2.8. Satz. (X_{0} → X_{1}) ↔ (¬X_{0} ∨ X_{1}).

2.9. Satz. (X_{0} ↔ X_{1}) = (X_{0} ∧ X_{1}) ∨ (¬X_{0} ∧ ¬X_{1}).

In die obigen Identitäten können beliebige Ausdrücke A, B, … eingesetzt werden: A ∧ B = ¬(¬A ∨ ¬B). A → B = ¬A ∨ B.) ⋯

2.10. Boolesche Axiome Wie oben kann man die folgenden Gesetze für beliebige Ausdrücke A, B, C nachweisen:

(A ∨ B) ∨ C = A ∨ (B ∨ C)  |  (A ∧ B) ∧ C = A ∧ (B ∧ C)
A ∨ B = B ∨ C  |  A ∧ B = B ∧ C
A ∨ F = A  |  A ∧ W = A
A ∨ W = W  |  A ∧ F = F
¬F = W  |  ¬W = F
A ∨ ¬A = W  |  A ∧ ¬A = F
¬¬A = A
A ∨ (B ∧ C) = (A ∨ B) ∧ (A ∨ C)  |  A ∧ (B ∨ C) = (A ∧ B) ∨ (A ∧ C)

D.h.: ({0, 1}, 0, 1, ∨, ∧) erfüllt die Gesetze einer Booleschen Algebra. Man beachte die in diesen Axiomen ausgedrückte Dualität zwischen ∨ und ∧. Es gibt noch weitere Modelle dieses Axiomensystems, z.B. Potenzmengen P(X).

Theorien

2.11. Definition. a: Eine Theorie ist eine Menge von aussagenlogischen Ausdrücken. Sei Φ eine Theorie und A ein Ausdruck. Definiere weiter: b: β ⊧ Φ, β ist ein Modell von Φ, falls für alle B ∈ Φ : β ⊧ B. c: Φ ist erfüllbar, Erf(Φ), falls es ein β ≠ Φ gibt. d: Φ ⊧ A, Φ impliziert A, falls jedes Modell von Φ auch ein Modell von A ist. e: Φ ist allgemeingültig, falls für jedes β : β ⊧ Φ.

2.12. Satz. Φ ist erfüllbar gdw.Φ |̸= F.

Beweis: (in einem pseudo-formalen Beweisformat) ⇒: Nun angenommen, Φ ist erfüllbar.

Wähle eine Belegung β, so dass β ⊧ Φ.

β ⊧ Φ und nicht β ⊧ F

Also nicht Φ ⊧ F. Ende.

⇐: Nun angenommen Φ |̸= F.

Wähle eine Belegung β, so dass nicht (β ⊧ Φ impliziert β ⊧ F)

nicht (nicht β ⊧ Φ oder β ⊧ F)

nicht (nicht β ⊧ Φ).

β ⊧ Φ.

Also ist Φ erfüllbar. QED

2.13. Erfüllbarkeit, Allgemeingültigkeit, Implikationen

• Wenn Φ endlich viele Ausdrücke enthält, ist Erf(Φ) und auch der Allgemeingültigkeit von Φ ein endliches Problem.

• Beispiel: Φ entspricht einer Reihe von Abhängigkeiten zwischen atomaren Aussagen vom Typ: Φ: (b hat a ermordet.) oder (c hat a ermordet). (b hasst a)

⋮

A: (a hat a ermordet).

Φ ⊧^{?} A.

• Kriminalfall könte gelöst werden durch Testen aller Belegungen β. Dieses Verfahren ist aber i.A. wegen der Anzahl der vorhandenen Variablen zu groß. Daher wird man versuchen, Φ ⊧ A durch einen Beweis zu begründen.

3 Kalküle für die Aussagenlogik

In Beispielen haben wir bereits gesehen, dass mathematische Beweise sehr formal durchgeführt werden können. Es stellt sich die Frage, ob, zunächst im Bereich der Aussagenlogik, sämtliche Implikationen durch einen formalen Kalkül generiert werden können? Implikationen erfüllen formale Gesetze, die Ausgangspunkt eines Kalküls seien könnten. Beispielsweise:

• Φ ⊧ A, falls A ∈ Φ;

• wenn Φ ⊧ A und Φ ⊧ B dann Φ ⊧ (A ∧ B).

Dies führt zu einem Kalkül, der auf Sequenzen der Form ΦA, auch geschrieben φ_{1} ⋯ φ_{n}A operiert. Zur Vereinfachung beschränken wir die aussagenlogische Sprache auf die Verknüpfungen ∨ und ¬. Ein Sequenzenkalkül

3.1. Definition. a: Eine Sequenz ist ein Paar ΦA, wobei Φ eine Ausdrucksmenge und A ein Ausdruck ist, in denen nur die Symbole ∨, ¬ verwendet werden. Schreibe auch ΦBA statt Φ ∪ {B} A, um das Element B des Antezedens hervorzuheben. b: Φ ist der Antezedens von ΦA, und A ist der Sukzedens.

3.2. Definition. Der Sequenzenkalkül der Aussagenlogik erzeugt Sequenzen aus gegebenen Sequenzen nach den nachfolgenden Regeln; die Regeln werden wie Rechenregeln notiert, über dem Strich stehen benutzten Sequenzen, darunter steht das Ergebnis der Regelanwendung.

\underline{Voraussetzungsregel} (Vor) , falls A ∈ Φ; ΦA \underline{Antezedensregel} (Ant) ΦA

, falls Φ ⊆ Φ′;
Φ′A

\underline{Fallunterscheidungsregel} (FU) ΦAB Φ¬AB

ΦB

\underline{Widerspruchsregel} (Wid) Φ¬AB Φ¬A¬B

ΦA

\underline{∨-Einführung im Antezedens} (∨A) ΦAC ΦBC

Φ(A ∨ B)C
\underline{∨-Einführung im Sukzedens} (∨S)  ΦA  ΦA
Φ(A ∨ B) Φ(B ∨ A)

3.3. Bemerkungen

• Obiger Kalkül ist ein vollkommen formales, syntaktisches Operieren auf Zeichen; die Erzeugungsregeln sind unabhängig von einer “Bedeutung”.

• Kalküle definieren eine Sprache der in ihnen erzeugbaren Sequenzen und Ausdrücke. Formale Sprachen in der Informatik, lassen sich ebenfalls mit Hilfe von Kalkülen definieren.

• In der Mathematik gibt es zahlreiche Kalküle zum rein formalen Behandeln von Termen. Z.B. können in der Differentialrechnung die Ableitungsregeln für Polynome als syntaktische Transformationen bestimmter Ausdrücke angesehen werden. Die Differential- und Integralrechnung wird im Englischen gelegentlich als ”Calculus“ bezeichnet.

• Kalküle können in der Aussagenlogik auch zum Generieren aller aus-

sagenlogischen Ausdrücke (in ∨ und ¬) eingesetzt werden:

, für n ∈ ℕ;

X_{n}

A

; ¬A

A
B
(A ∨ B).

Ableitungen

3.4. Definition. Eine Ableitung ist eine Folge

Φ_{0}A_{0} , Φ_{1}A_{1}, ⋯, Φ_{n−1}A_{n−1}

von Sequenzen, in der jede Sequenz Φ_{j}A_{j} mit Regeln des Sequenzenkalküls aus Sequenzen Φ_{i}A_{i} mit i < j gebildet werden kann. Man sagt dann Φ_{n−1}A_{n−1} ist ableitbar, oder A_{n−1} ist aus Φ_{n−1} ableitbar. Schreibweise: ⊢ Φ_{n−1}A_{n−1} oder auch Φ_{n−1} ⊢ A_{n−1}.

Beispiel: 0 : A A nach Vor. 1 : A (A ∨ ¬A) nach ∨S, 0. 2 : ¬A ¬A nach Vor. 3 : ¬A (A ∨ ¬A) nach ∨S, 2. 4 : (A ∨ ¬A) nach FU, 1, 3. Korrektheit

3.5. Definition. a: Eine Sequenz ΦA ist korrekt, falls Φ ⊧ A. b: Eine (Kalkül-)regel ist korrekt, falls sie korrekte Sequenzen in korrekte Sequenzen transformiert. c: Ein Kalkül ist korrekt, falls in ihm nur korrekte Sequenzen ableitbar sind.

3.6. Satz. (Korrektheitssatz) Der Sequenzenkalkül für die Aussagenlogik ist korrekt.

Beweis: Es genügt zu zeigen, dass alle Regeln des Sequenzenkalküls korrekt sind. Vor: Betrachte eine Sequenz ΦA mit A ∈ Φ. Φ ⊧ A. Also ist ΦA korrekt.

Ant: Betrachte eine Sequenz ΦA mit ΦA korrekt. Φ ⊧ A. Betrachte Φ′ mit Φ ⊆ Φ′. Φ′ ⊧ A. Also ist Φ′A korrekt. FU: Betrachte korrekte Sequenzen ΦAB, Φ¬AB. Nun betrachte eine Belegung β mit β ⊧ Φ. Fall 1: Nun sei angenommen β ⊧ A. β ⊧ Φ ∪ {A}. Also β ⊧ B, da ΦAB korrekt ist. Fall 2: Nun sei angenommen nicht β ⊧ A. β ⊧ Φ ∪ {¬A}. Also β ⊧ B, da Φ¬AB korrekt ist. Also Φ ⊧ B. Wid: Betrachte korrekte Sequenzen Φ¬AB, Φ¬A¬B. Betrachte eine Belegung β mit β ⊧ Φ. Nun sei angenommen nicht β ⊧ A. β ⊧ ¬A, β ⊧ Φ ∪ {¬A}. β ⊧ B, da Φ¬AB korrekt. β ⊧ ¬B da Φ¬A¬B korrekt ist. Also nicht β ⊧ B, Widerspruch. Also β ⊧ A. ∨-Regeln: Übungsaufgabe. QED

3.7. Abgeleitete Regeln. Durch Komposition von Kalkülregeln ergeben sich weitere Regeln, unter denen die durch den Kalkül definierte Sprache ebenfalls abgeschlossen ist und die die Anwendung des Kalküls vereinfachen können. Folgende Regeln sind korrekt und lassen sich im Sequenzenkalkül zeigen: \underline{Modifizierte Widerspruchsregel}, (mWid), ex falsum quodlibet:

ΦA

Φ¬A
ΦB

Ableitung der Regel. 0: ΦA.

1: Φ¬A.

2: Φ¬BA nach Ant, 0. 3: Φ¬B¬A nach Ant, 1. 4: ΦB nach Wid, 2,3.

\underline{Kettenschlussregel}, modus ponens (KS):

ΦA

ΦAB

ΦB

Ableitung der Regel: 0: ΦA 1: ΦAB 2: Φ¬AA nach Ant, 0 3: Φ¬A¬A nach Vor. 4: Φ¬AB nach mWid,2,3 5: ΦB nach FU,1,4.

\underline{Kontraposititionsregel},(KP):

ΦAB

Φ¬B¬A

Ableitung der Regel: 0: ΦAB 1: Φ¬BA¬B nach Vor. 2: Φ¬BAB nach Ant,1. 3: Φ¬BA¬A nach mWid, 1,2 4: Φ¬B¬A¬A nach Vor. 5: Φ¬B¬A nach FU,3,4.

4 Ein Vollständigkeitssatz für die Aussagenlogik

Wir haben gesehen, dass jede ableitbare Sequenz korrekt ist. Die naheliegende Frage ist nun umgekehrt, ob jede korrekte Sequenz auch in dem Kalkül abgeleitet werden kann. Wir führen einige für diese Frage relevante Begriffe ein:

4.1. Definition. a: Der Sequenzenkalkül ist vollständig, gdw.jede korrekte Sequenz ableitbar ist. b: Eine Menge Φ von Ausdrücken (der Aussagenlogik in ∨, ¬) ist konsistent oder widerspruchsfrei, gdw. es einen Ausdruck A gibt mit Φ ⊬ A. Andernfalls ist Φ inkonsistent oder widerspruchsvoll. c: Eine Menge Φ von Ausdrücken ist erfüllbar, gdw. wenn Φ ein Modell β ⊧ Φ besitzt.

4.2. Satz. Sei Φ eine Theorie, d.h. eine Ausdrucksmenge. Dann sind äquivalent: a: Φ ist widerspruchsfrei; b: für alle A gilt Φ ⊬ A oder Φ ⊬ ¬A; c:Φ ⊬ ¬(X_{0} ∨ ¬X_{0}).

Beweis: a → b: Angenommen Φ ist widerspruchsfrei. Wähle B so, dass Φ ⊬ B. Betrachte A. Angenommen Φ ⊢ A und Φ ⊢ ¬A. Dann Φ ⊢ B nach mWid. Widerspruch. b → c: Angenommen b gilt. Daraus folgt: Φ ⊬ (X_{0} ∨ ¬X_{0}) oder Φ ⊬ ¬(X_{0} ∨ ¬X_{0}). Φ ⊢ (X_{0} ∨ ¬X_{0}) war bereits abgeleitet. Also Φ ⊬ ¬(X_{0} ∨ ¬X_{0}). c → a: ist trivial. QED Der folgende Satz ist der entscheidende Schritt im Beweis des Vollständigkeitssatzes für die Aussagenlogik:

4.3. Satz. (Modellexistenzsatz) Sei Φ widerspruchsfei. Dann ist Φ erfüllbar.

Wir werden diesen Satz später beweisen. Schon jetzt erhalten wir als Korollar den gewünschten:

4.4. Satz. (Vollständigkeitssatz) Der aussagenlogische Kalkül ist vollständig.

Beweis: Betrachte eine korrekte Sequenz ΦA. Angenommen ΦA ist nicht ableitbar. Φ ⊬ A. Beh: Φ ∪ {¬A} ist widerspruchsfrei. Beweis: Angenommen nicht. Φ¬A ⊢ A. ΦA ⊢ A nach Vor. Φ ⊢ A nach FU. Widerspruch. QED(Beh) Wähle β, so dass β ⊧ Φ ∪ {¬A} nach Beh und Satz 4.3. ΦA ist nicht korrekt. Also Widerspruch. QED 4.5. Satz. (Maximierungssatz) Sei Φ eine widerspruchsfreie Ausdrucksmenge. Dann existiert eine Ausdrucksmenge Φ′ ⊇ Φ, die maximal widerspruchsfrei ist, d.h., Φ′ ist widerspruchsfrei und jede echte Obermenge von Φ′ ist widerspruchsvoll.

Beweis: Wähle eine Aufzählung (A_{n})_{n∈ℕ} aller Ausdrücke der Sprache der Aussagenlogik in ∨, ¬. Definiere rekursiv eine Folge (Φ_{n})_{n∈ℕ} von Ausdrucksmengen: Φ_{0} = Φ. Φ_{n+1} = Φ_{n} ∪ {A_{n}}, falls Φ_{n} ∪ {A_{n}} widerspruchsfrei ist; Φ_{n+1} = Φ_{n} ∪ {¬A_{n}}, falls Φ_{n} ∪ {A_{n}} widerspruchsvoll ist.

Behauptung: Für alle n ist Φ_{n} konsistent. Beweis: Φ_{0} = Φ ist nach Voraussetzung konsistent. Wir nehmen an, dass Φ_{n} konsistent ist. Angenommen, Φ_{n+1} ist nicht konsistent. Dann ist Φ_{n+1} = Φ_{n} ∪ {¬A_{n}} und Φ_{n} ∪ {A_{n}} ist widerspruchsvoll. 0: Φ_{n}¬A_{n}¬(X_{0} ∨ ¬X_{0}).

1. Φ_{n}A_{n}¬(X_{0} ∨ ¬X_{0}).

2. Φ_{n}¬(X_{0} ∨ ¬X_{0}) nach FU, 0,1. Damit ist Φ_{n} nicht konsistent, Widerspruch. Damit ist die Behauptung bewiesen nach dem Prinzip der vollständigen Induktion. qed (Behauptung)

Definiere Φ′ = ⋃_{n∈ℕ} Φ_{n}. Φ′ ⊇ Φ. Φ′ ist konsistent: angenommen das Falsum ließe sich aus Φ′ ableiten. In der Ableitung wird das Antezedens Φ′ nur endlich oft im Rahmen der Voraussetzungsregel herangezogen. Die in der Ableitung benötigten Voraussetzungen sind bereits sämtlich in einem Φ_{n} enthalten. Dann könnten wir die Ableitung eines Widerspruchs aus Φ′ zu einer mit Antezedens Φ_{n} modifizieren und Φ_{n} wäre widerspruchsvoll. Widerspruch. Nach Konstruktion der Folge der Φ_{n} gilt für alle m, dass A_{m} ∈ Φ′ oder ¬A_{m} ∈ Φ′. Da Φ′ konsistent ist, ist genau ein Ausdruck von A_{m}, ¬A_{m} in Φ′. Betrachte eine echte Obermenge Ψ von Φ′. Dann gibt es ein m, so dass A_{m} ∈ Ψ und ¬A_{m} ∈ Ψ. Damit ist Ψ widerspruchsvoll. Also ist Φ′ maximal konsistent. QED

Wir brauchen noch ein paar Informationen über maximal konsistente Mengen.

4.6. Satz. Wir nehmen Ψ maximal konsistent an. Dann a: für alle A gilt Ψ ⊢ A impliziert A ∈ Ψ; b: für alle A gilt A ∈ Ψ gdw nicht ¬A ∈ Ψ; c: für alle A, B gilt (A ∨ B) ∈ Ψ gdw A ∈ Ψ oder B ∈ Ψ.

Beweis: Wir betrachten einen Ausdruck A. Angenommen Ψ ⊢ A. Wir nehmen an dass Ψ ∪ {A} inkonsistent ist. 0: Ψ A. 1: Ψ A ¬(X_{0} ∨ ¬X_{0}). 2: Ψ ¬(X_{0} ∨ ¬X_{0}) nach KS, 0,1. Also ist Ψ inkonsistent, Widerspruch. Also ist Ψ ∪ {A} konsistent, und wegen der Maximalität von Ψ ist A ∈ Ψ.

Wir betrachten einen Ausdruck A. Wir nehmen an A ∈ Ψ. Angenommen ¬A ∈ Ψ. Dann wäre Ψ inkonsistent. Daher nicht ¬A ∈ Ψ; wie gewünscht. Umgekehrt sei angenommen nicht A ∈ Ψ. Da Ψ maximal konsistent ist, ist ψ ∪ {A} inkonsistent. 0: ΨA ¬(X_{0} ∨ ¬X_{0}). 1: ΨA ¬A nach Widerspruchsregel. 2: Ψ¬A ¬A nach Vor. 3: Ψ¬A nach FU, 1,2. Dann gilt ¬A ∈ Ψ nach a.

Wir betrachten Ausdrücke A, B. Wir nehmen an (A∨B) ∈ Ψ. Angenommen es sei nicht A ∈ Ψ und nicht B ∈ Ψ. ¬A ∈ Ψ und ¬B ∈ Ψ nach b. 0: Ψ ¬A nach Vor. 1: Ψ ¬B nach Vor. 2: Ψ (A ∨ B) nach Vor. 3: Ψ A A nach Vor. 4: Ψ A ¬A nach Ant,0. 5: Ψ A ¬(X_{0} ∨ ¬X_{0}) nach mWid,3,4. 6: Ψ B B nach Vor. 7: Ψ B ¬B nach Ant,1. 8: Ψ B ¬(X_{0} ∨ ¬X_{0}) nach mWid,6,7. 9: Ψ (A ∨ B) ¬(X_{0} ∨ ¬X_{0}) nach ∨A,5,8. 10:Ψ ¬(X_{0} ∨ ¬X_{0}) nach KS,2,9.

Also ist Ψ widerspruchsvoll, Widerspruch. Also ist A ∈ Ψ oder B ∈ Ψ; wie gewünscht.

Umgekehrt sei A ∈ Ψ. Man sieht sofort, dass Ψ ⊢ (A ∨ B) und nach a ist (A ∨ B) ∈ Ψ. QED

Wir beginnen nun den Beweis des Modellexistenzsatzes: Betrachte eine widerspruchsfreie Ausdrucksmenge Φ. Nach dem Maximierungssatz 4.5 wähle eine Ausdrucksmenge Φ′ ⊇ Φ, die maximal widerspruchsfrei ist. Definiere eine Belegung β : ℕ → {0, 1} durch β(n) = 1 gdw X_{n} ∈ Φ′.

Behauptung: Für alle Ausdrücke A ist β ⊧ A gdw A ∈ Φ′. Aus dieser Behauptung folgt unmittelbar der Satz: β ⊧ Φ′, und da Φ′ ⊇ Φ, ist β ⊧ Φ. Die Behauptung wird durch Induktion über den Aufbau des Ausdrucks A bewiesen: wir müssen sie für die elementaren Ausdrücke X_{n} zeigen und nachweisen, dass sie bei Negationen und Implikationen bewahrt wird. Der Induktionsanfang ergibt sich sofort aus der Definition von β: Behauptung 1: Für n ∈ ℕ gilt β ⊧ X_{n} gdw X_{n} ∈ Φ′. Behauptung 2: Wir betrachten A mit der Induktionsvoraussetzung: β ⊧ A gdw A ∈ Φ′. Dann gilt β ⊧ ¬A gdw ¬A ∈ Φ′. Beweis: Wir nehmen an β ⊧ ¬A. Nicht β ⊧ A. Nicht A ∈ Φ′ nach Induktionsvoraussetzung. Damit gilt ¬A ∈ Φ′ nach Satz 4.6, b; wie gewünscht. Umgekehrt sei ¬A ∈ Φ′. Da Φ′ konsistent ist, ist nicht A ∈ Φ′. Es gilt nicht β ⊧ A nach Induktionsvoraussetzung. β ⊧ ¬A; wie gewünscht. qed (Behauptung 2) Behauptung 3: Wir betrachten A, B mit Induktionsvoraussetzung: β ⊧ A gdw A ∈ Φ′ und β ⊧ B gdw B ∈ Φ′. Dann gilt β ⊧ (A∨B) gdw (A∨B) ∈ Φ′. Beweis: Wir nehmen an β ⊧ (A ∨ B). β ⊧ A oder β ⊧ B. Nun sei angenommen β ⊧ A. A ∈ Φ′ nach Induktionsvoraussetzung. 0: Φ′A nach Vor.

1. Φ′(A ∨ B) nach ∨S, 0. (A ∨ B) ∈ Ψ′ nach Satz 4.6, c; wie gewünscht. Der Fall B ∈ Φ′ wird genauso behandelt.

Umgekehrt sei (A ∨ B) ∈ Φ′. Nach Satz 4.6,c ist A ∈ Φ′ oder B ∈ Φ′. β ⊧ A oder β ⊧ B nach Induktionsvoraussetzung. β ⊧ (A∨B); wie gewünscht. qed (Behauptung 3) Nach den Behauptungen 1-3 und dem Prinzip der Induktion über den Aufbau von Ausdrücken ist damit die Behauptung gezeigt. QED

5 Ein Aussagenkalkül

Der bisher eingeführte Kalkül formalisiert Beweise als Folgen von Sequenzen. Ein üblicher mathematischer Beweis ist allerdings eine Folge von Aussagen, in der Aussagen aus früheren Aussagen der Folge folgen. Wir geben nun einen aussagenlogischen Kalkül an, der mit Aussagen arbeitet. Wiederum wird eine kleine formale Sprache gewählt, um die mathematische Analyse des Kalkül zu vereinfachen. Das Prinzip des Kalküls lässt sich aber ohne Schwierigkeiten auf die volle Sprache der Aussagenlogik anwenden.

5.1. Lokale Annahmen In Beweisen werden häufig Unterbeweise mit eigenen, lokalen Annahmen geführt: ⋮ Nun angenommen A_{m}. ⋮ A_{n} nach …. Also: (A_{m} → A_{n}).

⋮ Ein Unterargument ergibt eine Implikation von lokalen Annahmen zu lokalen Folgerungen. Wir werden daher mit der Sprache in den Verknüpfungen “→ , ¬” arbeiten.

5.2. Aussagen-Regeln Wir betrachten Regeln für das Schließen mit Aussagen in der betrachteten Sprache. Diese Regeln entsprechen Grundregeln oder abgeleiteten Regeln des Sequenzenkalküls.

\underline{Fallunterscheidungsregel}, (FU^{∗}): \underline{(A → B) (¬A → B)} ; B .

\underline{Widerspruchsregel}, (Wid^{∗}): \underline{(¬A → B) (¬A → ¬B)} ; A

\underline{Modus Ponens}, (MP^{∗}): \underline{A (A → B)} ; B

Diese Regeln können auch als Sequenzenregeln mit 1-elementigen Sequenzen verstanden werden. Sie sind offensichtlich korrekt.

”Texte“ Wir wollen ”mathematische Texte“ formalisieren, in denen Argumentationen mit lokalen Annahmen und Voraussetzungen stattfinden.

5.3. Definition. Eine endliche Folge T_{0}, …, T_{n−1} ist ein Text gdw es für jedes i < n einen aussagenlogischen Ausdruck A_{i} gibt, so dass T_{i} = A_{i} oder T_{i} = > A_{i} oder T_{i} = < A_{i}. Dabei kann > A als ”Angenommen A“ und < A als ”Also A“ gelesen werden.

In einem Text sollen Aussagen aus vorangehenden Aussagen folgen. Wir legen fest, was jeweils die Menge der augenblicklichen lokalen Voraussetzungen ist:

5.4. Definition. Zu einem Text T_{0}, …, T_{n−1} definiere die Folge V_{0}, …, V_{n−1} der lokalen Voraussetzungen und die Folge z_{0}, …, z_{n−1} von Zeigern durch Rekursion: V_{0} = ∅, z_{0} = −∞; Für i + 1 < n und einen aussagenlogischen Ausdruck A_{i} gilt: T_{i} = A_{i} impliziert V_{i+1} = V_{i} ∪ {A_{i}} und z_{i+1} = z_{i}; T_{i} = > A_{i} impliziert V_{i+1} = V_{i} ∪ {A_{i}} und z_{i+1} = i; T_{i} = < A_{i} impliziert V_{i+1} = V_{z_{i}} ∪ {A_{i}} und z_{i+1} = z_{z_{i}}.

Ein Beispiel für diese Definition und für einen Beweis in dem intendierten Kalkül (die R_{i} werden später erklärt):

\begin{aligned}i & T_{i} & V_{i} & z_{i} & R_{i} \\ 0 : & > A & ∅ & −∞ & ∅ \\ 1 : & > B & \{A\} & 0 & \{A\} \\ 2 : & A & \{A, B\} & 1 & \{A, B\} \\ 3 : & < (B → A) & \{A, B\} & 1 & \{A, B\} \\ 4 : & < (A → (B → A)) & \{A, (B → A)\} & 0 & \{A\} \\ 5 : & (A → (B → A)) & \{(A → (B → A))\} & −∞ & ∅ \end{aligned}

Beweise Beweise sind Texte, in denen die Aussagen mit Hilfe von Regeln aus den lokalen Voraussetzungen folgen.

5.5. Definition. Ein Text T_{0}, …, T_{n−1} mit lokalen Voraussetzungen V_{0}, …, V_{n−1} und Zeigern z_{0}, …, z_{n−1} ist ein Beweis gdw für i < n und einen aussagenlogischen Ausdruck A_{i} gilt:

T_{i} = A_{i} impliziert, dass eine Instanz einer Aussagenregel \underline{C_{0}, …, C_{l−1}} ; A_{i} mit

Ausdrücken C_{0}, …, C_{l−1} ∈ V_{i} existiert; T_{i} = < A_{i} impliziert, dass z_{i} ≥ 0 und A_{i} = (A_{z_{i}} → A_{i−1}); oder T_{i} = > A_{i}. Ein solcher Beweis ist ein Beweis von T_{n−1} = A_{n−1} gdw z_{n−1} = −∞. Wir schreiben Φ ⊢^{∗} B gdw es A_{0}, …, A_{l−1} ∈ Φ und einen Beweis von (A_{0} → (A_{1} → (… (A_{l−1} → B) …))) gibt.

Unser Ziel ist es zu zeigen, dass der Beweisbegriff ⊢^{∗} wie ⊢ zum Modellbegriff ⊧ äquivalent ist. Zunächst überprüfen wir die Korrektheit des Aussagenkalküls. Im Vergleich zum Sequenzenkalkül besteht die Schwierigkeit darin, aus einem Beweis die jeweils relevanten Annahmen zu entnehmen.

5.6. Definition. Sei T_{0}, …, T_{n−1} ein Beweis im Aussagenkalkül mit lokalen Voraussetzungen V_{0}, …, V_{n−1} und Zeigern z_{0}, …, z_{n−1}. Für j < n definiere die Menge R_{j} der relevanten Annahmen durch Rekursion: R_{0} = ∅; T_{i} = A_{i} impliziert R_{i+1} = R_{i}; T_{i} = > A_{i} impliziert R_{i+1} = R_{i} ∪ {A_{i}}; T_{i} = < A_{i} impliziert R_{i+1} = R_{z_{i}}.

5.7. Satz. (Korrektheitssatz) Unter den Annahmen der vorangehenden Definition gilt: a: Für i < n ist R_{i} ⊧ V_{i}. b: Für i < n, so dass T_{i} = A_{i} ein aussagenlogischer Ausdruck ist, ist R_{i} ⊧ A_{i}. c: Wenn Φ ⊢^{∗} A so Φ ⊧ A.

Beweis: Wir beweisen a: induktiv auf der Grundlage der rekursiven Definitionen von R_{i} und V_{i}. Induktionsanfang: R_{0} = V_{0} = ∅, daher R_{0} ⊧ V_{0}. Induktionsschritt: Angenommen i + 1 < n und für j < i + 1 gilt R_{j} ⊧ V_{j}. Fall 1: T_{i} = A_{i} ist ein aussagenlogischer Ausdruck. Nach Definition ist R_{i+1} = R_{i}, V_{i} ⊧ A_{i}, V_{i+1} = V_{i} ∪ {A_{i}}. Also ist R_{i+1} ⊧ V_{i+1}, wie erforderlich. Fall 2: T_{i} = > A_{i}. Nach Definition ist R_{i+1} = R_{i} ∪ {A_{i}}, V_{i+1} = V_{i} ∪ {A_{i}}. Also ist R_{i+1} ⊧ V_{i+1} wie erforderlich. Fall 3: T_{i} = < A_{i}. Nach Definition ist R_{i+1} = R_{z_{i}}, A_{i} = (A_{z_{i}} → A_{i−1}), V_{i+1} = V_{z_{i}} ∪ {A_{i}}, R_{i} = R_{z_{i}} ∪ {A_{z_{i}}}, A_{i−1} ∈ V_{i}. Nach Induktionsvoraussetzung ist R_{i} ⊧ V_{i} und R_{i} = R_{z_{i}} ∪{A_{z_{i}}} ⊧ A_{i−1}. Dann R_{z_{i}} ⊧ (A_{z_{i}} → A_{i−1}) = A_{i}. Nach Induktionsvoraussetzung R_{i+1} = R_{z_{i}} ⊧ V_{z_{i}} ∪ {A_{i}} = V_{i+1}, wie erforderlich. Die Teile b: und c: folgen sofort aus a: und der Definition eines Beweises. qed

5.8. Einige Beweise

0 : > A
1 : A  nach 0.
2 : > (A → A)
3 : (A → A)

Hier kann man auch die Zeile 1 fortlassen:

\begin{aligned}0 : & > A \\ 1 : & > (A → A) \\ 2 : & (A → A) \end{aligned}

Also ist ∅ ⊢^{∗} (A → A).

0 : > A
1 : > ¬A
2 : > ¬B
3 : A  nach 0.
4 : < (¬B → A)
5 : (¬B → A)  nach 4.
6 : > ¬B
7 : ¬A  nach 1.
8 : < (¬B → ¬A)
9 : (¬B → ¬A)  nach 8.
10 : B  nach Wid^{∗},5,9.
11 : < (¬A → B)
12 : < (A → (¬A → B))
13 : (A → (¬A → B)) nach 12.

Also ist ∅ ⊢^{∗} (A → (¬A → B)) für beliebige Ausdrücke A und B. Aus diesem Beweis ergibt sich die folgende Widerspruchsregel:

\underline{modifizierte Widerspruchsregel}, mWid^{∗}: \underline{A ¬A} ; B .

Genauer gesagt kann man die Beweiszeilen 2 bis 10 in jeden Beweis an Stellen einsetzen, an denen die Voraussetzungen A und ¬A bestehen, um zu B zu gelangen.

0 : > (¬A → A)
1 : > A
2 : < (A → A)
3 : (A → A)  nach 2.
4 : A  nach FU^{∗},0,3.
5 : < ((¬A → A) → A) nach 4.
6 : ((¬A → A) → A) nach 5.

Die im Folgende abgeleitete Regel erlaubt es, die Prämissen einer Implikation der Form (A_{0} → (A_{1} → … (A_{l−1} → B) …)) beliebig zu permutieren:

\underline{Permutationsregel}, PR^{∗}: \underline{(A → (B → C))} ; (B → (A → C)) .

0 : > (A → (B → C))
1 : > B
2 : > A
3 : (B → C)  nach MP^{∗},0,2.
4 : C  nach MP^{∗},1,3.
5 : < (A → C)
6 : < (B → (A → C))
7 : (B → (A → C)) nach 6.

Die folgende abgeleitete Regel erlaubt es, mehrfaches Auftreten von Prämissen in Implikationen der Form (A_{0} → (A_{1} → … (A_{l−1} → B) …)) zu eliminieren:

\underline{Absorptionsregel}, AR^{∗}: \underline{(A → (A → B))} ; (A → B)) .

0 : > (A → (A → B))
1 : > A
2 : (A → B)  nach MP^{∗},0,1.
3 : B  nach MP^{∗},2,1.
4 : < (A → B)
5 : (A → B)  nach 4.

Nützlich sind auch \underline{Transpositionsregeln}, TP^{∗}: \underline{(A → B)} ; (¬B → ¬A)

0 : > (A → B)
1 : > ¬B
2 : > A
3 : B  nach MP^{∗},0,2.
4 : ¬A  nach mWid^{∗},1,3.
5 : < (A → ¬A)
6 : (¬A → ¬A) war schon gezeigt.
7 : ¬A  nach FU^{∗},5,6.
8 : < (¬B → ¬A)
9 : (¬B → ¬A) nach 8.

Es folgen noch zwei Ableitungen, die im Vollständigkeitssatz benutzt werden:

0 : > ¬(A → B)
1 : > ¬A
2 : > A
3 : B  nach mWid^{∗},1,2.
4 : < (A → B)
5 : A  nach mWid^{∗},0,4.
6 : < (¬A → A)
7 : (A → A)  nach früherer Ableitung.
8 : A  nach FU∗,6,7
9 : < (¬(A → B) → A)
10 : (¬(A → B) → A) nach 10.

Ähnlich erhält man:

0 : > ¬(A → B)
1 : > B
2 : > A
3 : B  nach 1.
4 : < (A → B)
5 : ¬B  nach mWid^{∗},0,4.
6 : < (B → ¬B)
7 : (¬B → ¬B)  nach früherer Ableitung.
8 : ¬B  nach FU∗,6,7
9 : < (¬(A → B) → ¬B)
10 : (¬(A → B) → ¬B) nach 10.

6 Der Vollständigkeitssatz für ⊢^{∗}

Wir werden im Folgenden wie beim Vollständigkeitssatz für ⊢ vorgehen. Wir definieren vorübergehend die ⊢^{∗}-Versionen der relevanten Begriffe. Beachte, dass wir hier mit der aussagenlogischen Sprache in → und ¬ arbeiten. Φ ist ∗-konsistent, falls es einen Ausdruck A gibt mit Φ ⊬^{∗} A. Andernfalls ist Φ ∗-inkonsistent.

6.1. Satz. Es sind äquivalent: a: Φ ist ∗-konsistent; b: für alle A ist Φ ⊬^{∗} A oder Φ ⊬^{∗} ¬A; c: Φ ⊬^{∗} ¬(X_{0} → X_{0}).

Beweis: a→b: Angenommen Φ ist ∗-konsistent. Wähle B so dass Φ ⊬^{∗} B. Betrachte A. Angenommen Φ ⊢^{∗} A und Φ ⊢^{∗} ¬A. Es gibt dann Beweise ... (C_{0} → (C_{1} … (C_{k−1} → A) …)) und ... (C_{k} → (C_{k+1} … (C_{l−1} → ¬A) …)) mit C_{0}, …, C_{l−1} ∈ Φ. Wir können die beiden Beweise folgendermaßen verknüpfen und weiterführen: ... (C_{0} → (C_{1} … (C_{k−1} → A) …))

⋮ (C_{k} → (C_{k+1} … (C_{l−1} → ¬A) …)) > C_{0} > C_{1} ⋮ > C_{l−1} (C_{1} … (C_{k−1} → A) …) nach MP^{∗}

⋮ (C_{k−1} → A) nach MP^{∗} A (C_{k} … (C_{l−1} → ¬A) …)

⋮ (C_{l−1} → ¬A) nach MP^{∗} ¬A nach MP^{∗} B nach mWid^{∗} < (C_{l−1} → B) < (C_{l−2} → (C_{l−1} → B))

⋮ < (C_{0} → … (C_{l−2} → (C_{l−1} → B)) …) (C_{0} → … (C_{l−2} → (C_{l−1} → B)) …) Das heißt aber, dass Φ ⊢^{∗} B, Widerspruch zur Wahl von B. b→c: Wir hatten früher gesehen, dass Φ ⊢^{∗} (X_{0} → X_{0}). Nach b ist dann Φ ⊬^{∗} ¬(X_{0} → X_{0}). c→a is trivial. QED

Wie früher werden wir einen Modellexistenzsatz zeigen:

6.2. Satz. (Modellexistenzsatz) Wenn Φ ∗-konsistent ist, so ist Φ erfüllbar.

Hieraus ergibt sich ähnlich wie früher:

6.3. Satz. (Vollständigkeitssatz) Der Kalkül ⊢^{∗} für die Aussagenlogik ist vollständig.

Beweis: Betrachte eine korrekte Sequenz ΦA. Angenommen Φ ⊬^{∗} A. Behauptung: Φ ∪ {¬A} ist ∗-konsistent. Beweis: Angenommen, die Behauptung gelte nicht. Dann gibt es einen Beweis von (C_{0} → (C_{1} → … (C_{l−1} → (¬A → A)) …)) mit C_{0}, …, C_{l−1} ∈ Φ. Hier wird benutzt, dass wir die Prämissen einer derartigen Implikation geeignet arrangieren können. Wir hatten früher die Formel ((¬A → A) → A) in ⊢^{∗} abgeleitet. Die Beweise lassen sich zu einem Beweis von (C_{0} → (C_{1} → … (C_{l−1} → A) …)) zusammensetzen. Also ist Φ ⊢^{∗} A, Widerspruch. qed(Behauptung) Nach dem noch zu beweisenden Modellexistenzsatz 6.2 gibt es nun ein Modell für Φ¬A. Dann aber ist die Sequenz ΦA nicht korrekt. Widerspruch. QED

6.4. Maximal ∗-konsistente Mengen Betrachte eine ∗-konsistente Ausdrucksmenge Φ. Wir konstruieren eine maximal ∗-konsistente Obermenge Ψ wie zuvor: die Ausdrücke der →, ¬-Sprache werden als (A_{n}|n ∈ ℕ) aufgezählt und rekursiv für jedes A_{n} entschieden, ob es in Ψ aufgenommen wird. Dafür ist die folgende Eigenschaft entscheidend:

6.5. Satz. Angenommen, die Ausdrucksmengen Φ ∪ {A} und Φ ∪ {¬A} sind ∗-inkonsistent. Dann ist Φ ∗-inkonsistent.

Beweis: Wähle Beweise für Φ ∪ {A} ⊢^{∗} ¬(X_{0} → X_{0}) und Φ ∪ {¬A} ⊢^{∗} ¬(X_{0} → X_{0}). Hieraus lassen sich Beweise für Φ ⊢^{∗} (A → ¬(X_{0} → X_{0})) und Φ ⊢^{∗} (¬A → ¬(X_{0} → X_{0})) bilden. Mit der Fallunterscheidungsregel FU^{∗} lassen sich diese zu einem Beweis von Φ ⊢^{∗} ¬(X_{0} → X_{0}) zusammensetzen. Aber dann ist Φ ∗-inkonsistent, Widerspruch. End

Wir müssen dann die offensichtlichen Struktureigenschaften für maximal ∗- konsistente Mengen zeigen:

6.6. Satz. Wir nehmen Ψ maximal ∗-konsistent an. Dann: a: für alle A gilt: Ψ ⊢^{∗} A impliziert A ∈ Ψ; b: für alle A gilt: A ∈ Ψ gdw nicht ¬A ∈ Ψ; c: für alle A, B gilt: (A → B) ∈ Ψ gdw (A ∈ Ψ impliziert B ∈ Ψ).

Beweis a: Betrachte A. Angenommen Ψ ⊢^{∗} A. Dann kann jeder Beweis für ein Ψ ∪ {A} ⊢^{∗} B in einen Beweis für Ψ ⊢^{∗} B verändert werden. Da Ψ ∗- konsistent ist, ist auch Ψ ∪ {A} ∗-konsistent. Wegen der Maximalität von Ψ ist dann A ∈ Ψ. b: Betrachte A. Es sei angenommen A ∈ Ψ. Sei weiter angenommen ¬A ∈ Ψ. Betrachte die folgende Ableitung:

0 : > A
1 : > ¬A
2 : ¬(X_{0} → X_{0})  nach mWid^{∗},0,1.
3 : < (¬A → ¬(X_{0} → X_{0}))
4 : < (A → (¬A → ¬(X_{0} → X_{0})))

Damit Ψ ⊢^{∗} ¬(X_{0} → X_{0}). Dann ist Ψ ∗-inkonsistent, Widerspruch. Umgekehrt sie nicht ¬A ∈ Ψ. Wegen der Maximalität von Ψ ist Ψ ∪ {¬A} ∗- inkonsistent. Ψ∪{¬A} ⊢^{∗} ¬(X_{0} → X_{0}). Nach den Eigenschaften ∗-inkonsistenter Mengen folgt hieraus für einen Ausdruck B: Ψ ⊢^{∗} (¬A → B) und Ψ ⊢^{∗} (¬A → ¬B). Nach der Widerspruchsregel Wid^{∗} ergibt sich hieraus Ψ ⊢^{∗} A. Nach a ist dann A ∈ Ψ. c: Betrachte A, B. Angenommen (A → B) ∈ Ψ und A ∈ Ψ. Nach der Regel modus ponens ist dann Ψ ⊢^{∗} B. Nach a ist B ∈ Ψ. Umgekehrt sei nicht (A → B) ∈ Ψ. Nach a ist dann ¬(A → B) ∈ Ψ. Nach den letzten Herleitungen in dem Absatz über Beweise sind (¬(A → B) → A) ∈ Ψ und (¬(A → B) → ¬B) ∈ Ψ. Da Ψ bezüglich modus ponens abgeschlossen ist, sind A ∈ Ψ und ¬B ∈ Ψ. B ∉ Ψ. Damit impliziert A ∈ Ψ nicht B ∈ Ψ. QED

Mit diesem Satz kann der Beweis der Modellexistenzsatzes genauso durchgeführt werden wie zuvor. Damit ist der Vollständigkeitssatz für ⊢^{∗} gezeigt, und wir erhalten:

6.7. Satz. ⊧ = ⊢ = ⊢^{∗}.