Die Axiome der Aussagenlogik – Warum selbst die Logik Regeln braucht
Dieser Beitrag erklärt die Axiome der klassischen Aussagenlogik zunächst für Nichtlogiker und zeigt anschließend vereinfacht, warum das verwendete System widerspruchsfrei und vollständig ist.
Wer glaubt, Logik brauche keine Axiome, hat schon angefangen zu schummeln
Logik klingt zunächst nach dem Gegenteil von Dogma.
Keine Gefühle. Keine Meinungen. Keine politischen Bauchentscheidungen. Keine Tante Erna, die sagt: „Das war schon immer so.“
Nur klare Regeln.
Dumm nur: Auch die Logik muss irgendwo anfangen.
Denn bevor man beweisen kann, dass eine Aussage logisch aus anderen Aussagen folgt, muss festgelegt sein, was überhaupt als gültiger Beweis gilt. Und genau hier kommen die Axiome ins Spiel.
Ein Axiomensystem ist dabei kein göttliches Regelbuch aus dem Himmel. Es ist ein formal festgelegter Ausgangspunkt. Man entscheidet sich für bestimmte Grundsätze und definiert eine Schlussregel. Danach darf man nicht mehr nach Lust und Laune argumentieren.
Das ist bereits mehr Disziplin, als manche politischen Debatten seit Jahren aufbringen.
1. Die drei Ebenen: Syntax, Axiome und Bedeutung
Die Aussagenlogik arbeitet zunächst mit Symbolen.
Zum Beispiel:
p, q, r
Dazu kommen logische Verknüpfungen wie:
¬p (nicht p)
p ∧ q (p und q)
p ∨ q (p oder q)
p → q (wenn p, dann q)
Das allein ist aber noch keine Logik.
Wir brauchen zunächst eine Syntax: Welche Zeichenfolgen gelten überhaupt als korrekt gebildete Formeln?
Danach brauchen wir ein Beweissystem: Welche Formeln dürfen wir aus welchen anderen Formeln ableiten?
Und schließlich brauchen wir eine Semantik: Wann ist eine Formel wahr?
Damit entstehen zwei unterschiedliche Begriffe:
syntaktisch:„Diese Formel lässt sich formal beweisen.“
semantisch:„Diese Formel ist unter jeder zulässigen Wahrheitsbelegung wahr.“
Die große Frage lautet nun:
Fallen diese beiden Begriffe zusammen?
Wenn ja, haben wir Vollständigkeit.
2. Ein mögliches Axiomensystem
Wir verwenden ein klassisches Hilbert-System mit nur einer logischen Verknüpfung:
→ für die materiale Implikation und ¬ für die Negation.
Dazu drei Axiomenschemata:
A1:
p → (q → p)
A2:
[p → (q → r)] → [(p → q) → (p → r)]
A3:
(¬q → ¬p) → (p → q)
Dazu kommt genau eine Schlussregel:
Modus Ponens
Aus
p
und
p → q
darf man schließen:
q
Mehr braucht das System nicht.
Das wirkt zunächst beinahe beleidigend bescheiden. Keine 47 Regeln, kein „ich habe da noch ein Gefühl“, kein „das müsste doch eigentlich“. Nur drei Axiomenschemata und eine Schlussregel.
Aus diesen Bausteinen lassen sich die übrigen klassischen logischen Operationen definieren beziehungsweise entsprechende Gesetze herleiten.
Zum Beispiel kann man
p ∧ q
und
p ∨ q
über geeignete Definitionen auf ¬ und → zurückführen.
Die Axiome sind also nicht einzelne Behauptungen über die Welt. Sie sind formale Schemata. Sie sagen nicht: „Heute regnet es.“ Sie bestimmen, welche logischen Strukturen grundsätzlich akzeptiert werden.
3. Widerspruchsfreiheit: Das System darf sich nicht selbst erledigen
Ein Axiomensystem wäre ziemlich nutzlos, wenn man daraus sowohl eine Aussage als auch deren Negation beweisen könnte.
Formal wollen wir also vermeiden, dass für irgendeine Formel φ sowohl
⊢ φ
als auch
⊢ ¬φ
gilt.
Noch stärker formuliert: Das System soll nicht jede beliebige Formel beweisen können.
Denn wenn alles beweisbar wäre, wäre zwar jeder Streit entschieden – aber leider auf dieselbe Weise wie ein Computer, dessen Antwort auf jede Frage „42“ lautet.
Der Beweis der Widerspruchsfreiheit
Wir verwenden dafür die Korrektheit bzw. Soundness des Systems.
Zunächst gilt:
Alle Axiome sind logisch gültig.
Das bedeutet:
Für jede Wahrheitsbelegung v gilt
v(A) = wahr
für jedes Axiom A.
Beispielsweise ist
p → (q → p)
immer wahr.
Warum?
Wenn p wahr ist, ist die Implikation erfüllt. Wenn p falsch ist, ist die äußere Implikation ebenfalls wahr. Ein hübsches kleines Beispiel dafür, dass die klassische Logik nicht erst einen Untersuchungsausschuss braucht, um eine einfache Struktur zu erkennen.
Auch die anderen Axiome sind unter jeder Wahrheitsbelegung wahr.
Nun kommt Modus Ponens:
Sind p und p → q unter einer Belegung wahr, dann muss auch q wahr sein.
Damit gilt durch Induktion über jeden formalen Beweis:
Alles, was beweisbar ist, ist logisch gültig.
Also:
⊢ φ ⇒ ⊨ φ
Das ist die Soundness-Aussage.
Nun nehmen wir an, das System wäre widersprüchlich. Dann wären sowohl
⊢ φ
als auch
⊢ ¬φ
möglich.
Nach Soundness wären dann sowohl φ als auch ¬φ unter jeder Belegung wahr.
Das ist unmöglich.
Denn keine klassische Wahrheitsbelegung macht gleichzeitig
φ = wahr
und
φ = falsch.
Also:
Das Axiomensystem ist widerspruchsfrei.
Die Logik kann sich damit wenigstens nicht legal selbst widersprechen. Was Menschen anschließend mit ihr anstellen, steht auf einem anderen Blatt.
4. Vollständigkeit: Beweisbare Wahrheit und wahre Beweisbarkeit
Jetzt kommt der interessantere Teil.
Soundness sagt:
Was beweisbar ist, ist logisch gültig.
Aber reicht das?
Vielleicht gibt es ja logisch gültige Formeln, die unser Axiomensystem trotzdem nicht beweisen kann.
Dann wäre das System zwar korrekt, aber zu schwach.
Genau hier kommt die Vollständigkeit ins Spiel:
Jede logisch gültige Formel muss formal beweisbar sein.
Formal:
⊨ φ ⇒ ⊢ φ
Zusammen mit Soundness erhalten wir:
⊢ φ ⇔ ⊨ φ
Das ist einer der großen Sätze der mathematischen Logik.
5. Der Vollständigkeitsbeweis – ohne Zauberei
Der Beweis lässt sich über die sogenannte Lindenbaum-Konstruktion führen.
Nehmen wir an, φ sei nicht beweisbar:
⊬ φ
Wir wollen zeigen, dass φ dann auch nicht logisch gültig sein kann.
Dazu betrachten wir die Formel ¬φ.
Da φ nicht beweisbar ist, ist das System zusammen mit ¬φ konsistent.
Nun erweitern wir diese Menge schrittweise zu einer maximal konsistenten Menge Γ.
„Maximal konsistent“ bedeutet vereinfacht:
Γ enthält keinen Widerspruch.
Für jede Formel ψ enthält Γ entweder ψ oder ¬ψ.
Jetzt bauen wir aus Γ eine Wahrheitsbelegung v.
Wir definieren:
v(p) = wahr genau dann, wenn p ∈ Γ.
Die entscheidende Arbeit besteht anschließend im sogenannten Wahrheitslemma:
Für jede Formel ψ gilt:ψ ∈ Γ genau dann, wenn v(ψ) = wahr.
Der Beweis erfolgt strukturell über den Aufbau der Formel.
Für Negation etwa gilt:
¬ψ ∈ Γ ⇔ ψ ∉ Γ
und damit entsprechend:
v(¬ψ) = wahr ⇔ v(ψ) = falsch.
Für die Implikation gilt:
ψ → χ ∈ Γ
genau dann, wenn aus ψ nicht χ folgt – und damit genau dann, wenn
v(ψ) = falsch
oder
v(χ) = wahr.
Damit stimmt die syntaktische Konstruktion mit der semantischen Wahrheitsbewertung überein.
Da ¬φ ∈ Γ, erhalten wir:
v(¬φ) = wahr
also
v(φ) = falsch.
Damit existiert eine Wahrheitsbelegung, unter der φ falsch ist.
Folglich ist φ keine Tautologie.
Wir haben also gezeigt:
⊬ φ ⇒ ⊭ φ
Durch Kontraposition:
⊨ φ ⇒ ⊢ φ
Und genau das ist die Vollständigkeit.
6. Warum das philosophisch interessanter ist, als es aussieht
Der Vollständigkeitssatz sagt etwas ziemlich Erstaunliches.
Die formale Beweismaschine und die semantische Vorstellung von logischer Wahrheit passen exakt zusammen.
Nicht ungefähr.
Nicht „meistens“.
Sondern:
Eine Formel ist genau dann logisch gültig, wenn sie im System beweisbar ist.
Damit treffen zwei völlig unterschiedliche Perspektiven aufeinander.
Die eine sagt:
„Zeig mir einen formalen Beweis.“
Die andere:
„Zeig mir eine Wahrheitsbelegung, unter der die Formel falsch wird.“
Und zwischen beiden gibt es keinen geheimen dritten Weg.
Das ist die eigentliche Schönheit formaler Logik: Sie ersetzt Autorität durch überprüfbare Struktur.
7. Die unangenehme Pointe
Axiome sind keine Wahrheiten, die das Universum persönlich unterschrieben hat.
Sie definieren zusammen mit den Schlussregeln ein formales System.
Seine Qualität zeigt sich anschließend darin, ob dieses System konsistent ist und ob es die gewünschte Semantik vollständig erfasst.
Für die klassische Aussagenlogik gelingt beides:
Widerspruchsfreiheit:
⊢ φ ⇒ ⊨ φ
Vollständigkeit:
⊨ φ ⇒ ⊢ φ
Also:
⊢ φ ⇔ ⊨ φ
Das ist mehr als ein hübscher mathematischer Satz.
Es bedeutet, dass wir bei der klassischen Aussagenlogik tatsächlich darauf vertrauen können, dass zwischen „formal beweisbar“ und „logisch gültig“ keine Lücke klafft.
Und genau deshalb ist Logik so unbequem.
Man kann ihre Regeln kritisieren. Man kann andere Logiken wählen. Man kann über die Bedeutung von Wahrheit philosophieren.
Aber innerhalb eines sauber definierten Systems reicht es nicht mehr, überzeugt zu sein.
Man muss beweisen.
Und das ist vermutlich die grausamste Zumutung, die man einem Menschen machen kann, der gerade „Das ist doch logisch!“ gesagt hat.
Quellen und weiterführende Literatur
Die Darstellung der Axiome, der Korrektheit, der Widerspruchsfreiheit und der Vollständigkeit orientiert sich an grundlegenden Arbeiten und Standardwerken der mathematischen Logik.
Primärquelle zur Vollständigkeit
Kurt Gödel: Die Vollständigkeit der Axiome des logischen Funktionenkalküls (1930).
Gödels Arbeit gehört zu den historischen Grundlagen des Vollständigkeitssatzes. In ihr wird gezeigt, dass die Axiome des logischen Funktionenkalküls ausreichen, um jede logisch gültige Aussageformel formal abzuleiten. Die Arbeit ist in Gödels Collected Works, Volume I dokumentiert.
Standardwerk zur mathematischen Logik
Herbert B. Enderton: A Mathematical Introduction to Logic, 2. Auflage.
Endertons Lehrbuch behandelt die grundlegenden Konzepte und Sätze der mathematischen Logik und eignet sich als systematische Einführung in Aussagenlogik, Prädikatenlogik und weitere Bereiche der Logik.
Standardwerk zu Axiomensystemen und Beweisen
Elliott Mendelson: Introduction to Mathematical Logic, 6. Auflage, CRC Press.
Das Werk behandelt unter anderem den Aussagenkalkül, Wahrheitstabellen, Tautologien, Axiomensysteme sowie die Vollständigkeitstheoreme der mathematischen Logik.
Weiterführende Einführung
Dirk van Dalen: Logic and Structure, 5. Auflage, Springer.
Van Dalens Lehrbuch behandelt klassische und intuitionistische Logik, darunter Aussagenlogik, Prädikatenlogik sowie ein eigenes Kapitel zu „Completeness and Applications“.
Hinweis zur Darstellung
Der vorliegende Beitrag ist keine vollständige mathematische Beweisführung im Sinne eines Logiklehrbuchs, sondern eine didaktisch vereinfachte Einführung. Insbesondere die Konstruktion maximal konsistenter Mengen und das Wahrheitslemma wurden bewusst auf ihre Grundidee reduziert.
Wer den Vollständigkeitssatz formal und in allen technischen Einzelheiten nachvollziehen möchte, sollte die genannten Standardwerke beziehungsweise Gödels Originalarbeit heranziehen.
FAQ: Die wichtigsten Begriffe der Aussagenlogik einfach erklärt
Was ist Aussagenlogik?
Die Aussagenlogik untersucht Aussagen, die einen Wahrheitswert haben können: wahr oder falsch.
Beispielsweise:
p: „Es regnet.“
Die Aussagenlogik interessiert sich dabei nicht dafür, ob es tatsächlich regnet. Sie untersucht, wie Aussagen logisch miteinander verbunden sind.
Was ist eine Aussage?
Eine Aussage ist ein Satz, der grundsätzlich wahr oder falsch sein kann.
Beispiel:
„Berlin ist die Hauptstadt Deutschlands.“
Das ist eine Aussage.
Keine Aussage im logischen Sinn wäre dagegen:
„Mach das Fenster zu!“
Das ist eine Aufforderung und daher weder wahr noch falsch.
Was ist eine Aussagevariable?
Eine Aussagevariable ist ein Buchstabe, der für eine Aussage steht.
Zum Beispiel:
p: „Es regnet.“
q: „Die Straße ist nass.“
Der Buchstabe p steht dabei nicht für eine bestimmte Wahrheit. Er ist zunächst nur ein Platzhalter.
Was ist ein Wahrheitswert?
Eine Aussage kann in der klassischen Aussagenlogik zwei Wahrheitswerte besitzen:
wahr
oder
falsch.
Man schreibt häufig:
w = wahr
f = falsch.
Mehr Möglichkeiten gibt es in der klassischen zweiwertigen Aussagenlogik nicht.
Das ist übrigens keine Behauptung darüber, dass die Welt immer schön übersichtlich wäre. Es ist eine Festlegung des verwendeten logischen Systems.
Was ist eine Wahrheitsbelegung?
Eine Wahrheitsbelegung legt fest, welchen Wahrheitswert die einzelnen Aussagevariablen erhalten.
Zum Beispiel:
v(p) = wahr
v(q) = falsch
Damit wissen wir, wie sich zusammengesetzte Aussagen unter dieser Belegung verhalten.
Eine andere Belegung könnte natürlich lauten:
v(p) = falsch
v(q) = wahr.
Was ist eine logische Verknüpfung?
Eine logische Verknüpfung verbindet Aussagen miteinander.
Zum Beispiel:
¬p (nicht p)
p ∧ q (p und q)
p ∨ q (p oder q)
p → q (wenn p, dann q)
Damit können aus einfachen Aussagen komplizierte Formeln entstehen.
Was bedeutet Negation?
Die Negation kehrt den Wahrheitswert einer Aussage um.
Aus
p: „Es regnet.“
wird:
¬p: „Es regnet nicht.“
Ist p wahr, ist ¬p falsch.
Ist p falsch, ist ¬p wahr.
Was ist eine Implikation?
Eine Implikation hat die Form:
p → q
Sie bedeutet:
Wenn p gilt, dann gilt q.
Wichtig: Die klassische logische Implikation sagt zunächst nichts darüber aus, ob zwischen p und q ein ursächlicher Zusammenhang besteht.
Die Aussage
„Wenn es regnet, ist die Straße nass“
ist logisch etwas anderes als die Behauptung:
„Der Regen verursacht die Nässe der Straße.“
Wer beides verwechselt, hat bereits begonnen, Logik und Weltbeschreibung durcheinanderzuwerfen.
Was ist ein Axiom?
Ein Axiom ist ein grundsätzlich zugelassener Ausgangssatz eines formalen Systems.
Man beweist ein Axiom innerhalb dieses Systems nicht erst aus anderen Sätzen. Es dient als Ausgangspunkt.
Wichtig ist allerdings:
Ein Axiom ist nicht automatisch eine ewige Wahrheit des Universums.
Es gehört zu einem bestimmten formalen System.
Was ist ein Axiomenschema?
Ein Axiomenschema ist eine allgemeine Form, aus der durch Einsetzen konkreter Formeln einzelne Axiome entstehen.
Beispielsweise:
p → (q → p)
ist ein Schema.
Für konkrete Formeln kann man an die Stelle von p und q beliebige passende Formeln einsetzen.
Das erklärt auch, warum man von Axiomenschemata und nicht einfach von drei einzelnen Axiomen spricht.
Was ist eine Schlussregel?
Eine Schlussregel legt fest, wie man aus bereits akzeptierten Formeln neue Formeln ableiten darf.
Eine der wichtigsten Regeln der Aussagenlogik ist der Modus Ponens.
Aus:
p
und:
p → q
darf man schließen:
q
Beispiel:
Es regnet.
Wenn es regnet, wird die Straße nass.
Also wird die Straße nass.
Die Schlussregel schreibt vor, dass dieser Übergang logisch zulässig ist.
Was ist Modus Ponens?
Modus Ponens ist eine konkrete Schlussregel.
Formal:
p
p → q
——————
q
Er ist eine der grundlegenden Regeln des verwendeten Hilbert-Kalküls.
Was bedeutet „beweisbar“?
Eine Formel ist beweisbar, wenn man sie mit den zugelassenen Axiomen und Schlussregeln in endlich vielen Schritten herleiten kann.
Man schreibt:
⊢ φ
und liest:
„φ ist beweisbar.“
Das Zeichen ⊢ gehört zur sogenannten syntaktischen Ebene.
Was bedeutet „logisch gültig“?
Eine Formel ist logisch gültig, wenn sie unter jeder möglichen Wahrheitsbelegung wahr ist.
Man schreibt:
⊨ φ
und liest:
„φ ist logisch gültig“ oder „φ folgt semantisch.“
Ein klassisches Beispiel ist:
p ∨ ¬p
Diese Formel ist unabhängig davon wahr, ob p selbst wahr oder falsch ist.
Was ist eine Tautologie?
Eine Tautologie ist eine Formel, die unter jeder Wahrheitsbelegung wahr ist.
Beispiel:
p ∨ ¬p
Egal, ob p wahr oder falsch ist: Die Formel bleibt wahr.
Eine Tautologie ist damit ein Sonderfall einer logisch gültigen Formel.
Was ist der Unterschied zwischen „⊢“ und „⊨“?
Das ist einer der wichtigsten Unterschiede des gesamten Beitrags.
⊢ bedeutet:
„Es gibt einen formalen Beweis.“
⊨ bedeutet:
„Die Formel ist unter jeder zulässigen Wahrheitsbelegung wahr.“
Kurz:
⊢ = beweisbar
⊨ = logisch gültig
Die zentrale Leistung des Vollständigkeitssatzes besteht darin, zu zeigen, dass beide Ebenen in der klassischen Aussagenlogik zusammenpassen:
⊢ φ ⇔ ⊨ φ
Was bedeutet Syntax?
Syntax beschreibt die Form eines logischen Systems.
Sie beantwortet beispielsweise:
Welche Zeichenfolgen sind überhaupt gültige Formeln?
p → q
ist eine korrekt gebildete Formel.
Eine völlig beliebige Zeichenfolge ist dagegen keine logische Formel.
Syntax kümmert sich zunächst nicht darum, ob eine Formel wahr ist.
Was bedeutet Semantik?
Semantik beschäftigt sich mit der Bedeutung beziehungsweise Wahrheit von Formeln.
Sie fragt:
Unter welchen Wahrheitsbelegungen ist eine Formel wahr?
Die Syntax sagt also:
„Ist das überhaupt eine korrekt gebildete Formel?“
Die Semantik fragt:
„Wann ist diese Formel wahr?“
Was bedeutet Soundness oder Korrektheit?
Soundness bedeutet:
Alles, was das formale System beweist, ist auch logisch gültig.
Formal:
⊢ φ ⇒ ⊨ φ
Das System produziert also keine formal beweisbaren Formeln, die semantisch ungültig sind.
Was bedeutet Vollständigkeit?
Vollständigkeit geht in die andere Richtung.
Sie bedeutet:
Formal:
⊨ φ ⇒ ⊢ φ
Damit bleibt keine logische Wahrheit außerhalb des Beweissystems liegen.
Zusammen mit der Korrektheit ergibt sich:
⊢ φ ⇔ ⊨ φ
Was bedeutet Widerspruchsfreiheit oder Konsistenz?
Ein System ist widerspruchsfrei, wenn es nicht gleichzeitig eine Aussage und ihre Negation beweisen kann.
Also nicht:
⊢ φ
und gleichzeitig:
⊢ ¬φ
In einem klassischen logischen System wäre ein solcher Widerspruch fatal, weil das System dann seine Trennschärfe verlieren würde.
Was ist eine konsistente Formelmenge?
Eine Formelmenge ist konsistent, wenn sich aus ihr kein Widerspruch ableiten lässt.
Eine solche Menge kann beispielsweise enthalten:
p
p → q
und daraus:
q
Sie darf aber nicht zugleich p und ¬p enthalten beziehungsweise beweisbar machen.
Was ist eine maximal konsistente Menge?
Eine maximal konsistente Menge ist eine widerspruchsfreie Sammlung von Formeln, die so weit erweitert wurde, dass für jede Formel φ grundsätzlich entschieden ist:
φ
oder
¬φ.
„Maximal“ bedeutet hier nicht einfach „sehr groß“.
Es bedeutet:
Man kann keine weitere Formel hinzufügen, ohne die Konsistenz zu verlieren.
Genau diese Eigenschaft wird im Vollständigkeitsbeweis benötigt.
Was ist die Lindenbaum-Konstruktion?
Die Lindenbaum-Konstruktion ist ein Verfahren, mit dem man eine konsistente Formelmenge zu einer maximal konsistenten Menge erweitert.
Vereinfacht gesagt:
Wir haben zunächst eine widerspruchsfreie Sammlung. Dann prüfen wir nacheinander weitere Formeln und nehmen jeweils eine konsistente Entscheidung auf, bis jede Formel entschieden ist.
Damit erhalten wir den vollständigen Wahrheitsplan, den wir für den Vollständigkeitsbeweis benötigen.
Was ist das Wahrheitslemma?
Das Wahrheitslemma stellt die Verbindung zwischen unserer formalen Formelmenge und der daraus konstruierten Wahrheitsbelegung her.
Vereinfacht lautet es:
Eine Formel steht genau dann in unserer maximal konsistenten Menge, wenn sie unter der daraus konstruierten Wahrheitsbelegung wahr ist.
Formal:
ψ ∈ Γ ⇔ v(ψ) = wahr
Das ist der entscheidende Brückenschlag zwischen Syntax und Semantik.
Was bedeutet „Kontraposition“?
Die Kontraposition erlaubt es, eine Aussage der Form
A ⇒ B
gleichwertig als
¬B ⇒ ¬A
zu formulieren.
Im Vollständigkeitsbeweis haben wir gezeigt:
⊬ φ ⇒ ⊭ φ
Also:
Wenn φ nicht beweisbar ist, ist φ nicht logisch gültig.
Daraus folgt per Kontraposition:
⊨ φ ⇒ ⊢ φ
Also:
Wenn φ logisch gültig ist, ist φ beweisbar.
Und genau das ist die Vollständigkeit.
Was ist ein Hilbert-Kalkül?
Ein Hilbert-Kalkül ist ein besonders minimalistisches formales Beweissystem.
Es arbeitet mit:
einigen Axiomenschemata,
wenigen Schlussregeln,
formal exakt definierten Beweisen.
Die Idee lautet nicht:
„Wir brauchen möglichst viele Regeln.“
Sondern eher:
„Wie wenig Regeln brauchen wir, um trotzdem die gesamte gewünschte Logik beweisen zu können?“
Das macht Hilbert-Systeme mathematisch elegant, didaktisch allerdings manchmal so charmant wie eine Steuererklärung.
Was ist der wichtigste Satz des gesamten Beitrags?
Wenn man nur eine Formel mitnehmen möchte, dann diese:
⊢ φ ⇔ ⊨ φ
Sie sagt:
Eine Formel ist genau dann formal beweisbar, wenn sie logisch gültig ist.
Die eine Seite ist die Korrektheit:
⊢ φ ⇒ ⊨ φ
Die andere Seite ist die Vollständigkeit:
⊨ φ ⇒ ⊢ φ
Damit treffen formaler Beweis und logische Wahrheit zusammen.
Und genau hier wird aus „Das ist doch logisch!“ endlich etwas, mit dem man arbeiten kann.
Kommentare