Die Korrektheit des Kalküls besagt, dass nur gültige Sequenzen abgeleitet werden können. Von grosser Bedeutung ist, dass auf diese Weise alle logischen Folgerungen abgeleitet werden können! Es gilt also auch die Umkehrung der Korrektheit:
Satz: Gilt
, so ist
ableitbar.
Das Ableiten ist ein maschinell prüfbares Verfahren, das in endlich vielen Schritten aus endlich vielen Formeln eine korrekte Folgerung erzeugt. Das ist genau das, was in der Mathematik als Beweis gilt. Der Satz besagt also, dass sich alle logischen Folgerungen auf diese Weise beweisen lassen.
Wir beweisen den Satz nach einer Idee des amerikanischen Logikers Leon Henkin. Dazu nehmen wir an, dass
gilt und konstruieren ein Bewertung
, die
zeigt:
macht also alle Formeln aus
wahr und alle Formeln aus
falsch. Wir vergrössern
und
zu
und
, so dass diese maximal sind aber weiterhin
gilt. Mit diesen Formelmengen wird dann die Bewertung definiert.[1]
Beweis:
Wir zeigen die Kontraposition. Sei also
, d.h. aus
ist
nicht ableitbar, und
die Mächtigkeit der Sprache. Weiterhin sei
mit
eine Aufzählung aller Formeln. Wir definieren rekursiv
und
für
.
und
.
- Für Limeszahlen
sei:
und
.
- Für Nachfolgerzahlen
werden drei Fälle unterschieden:
- wenn
, dann
und ![{\displaystyle \Delta _{i+1}:=\Delta _{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1f21af7d15093fe29a9844352d2cb7e36d0b5df)
- wenn
und
, dann
und ![{\displaystyle \Delta _{i+1}:=\Delta _{i}\cup \{\phi _{i}\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/644e0b062edd845ef5b4e67dfadb1ff8765c7377)
- wenn
und
, dann
und ![{\displaystyle \Delta _{i+1}:=\Delta _{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1f21af7d15093fe29a9844352d2cb7e36d0b5df)
Wir werden später sehen, dass der letzte Fall nicht auftritt und setzen nun:
und
Lemma 1: Es gilt
.
Beweis:
Durch Induktion über
folgt:
für alle
. Für
gilt das nach Voraussetzung undfür Nachfolgerzahlen nach Konstruktion. Gälte für Limeszahlen
, dann gälte
für ein
, denn für die Ableitung werden nur endlich viele Formeln aus
und
benötigt. Das widerspricht aber der Induktionsvoraussetzung für
.
Insbesondere gilt also
.✔
Lemma 2:
und
sind maximal, d.h. es gilt für eine beliebige Formel
:
und
.
Beweis: Die eine Richtung (
) folgt mit der Nichtableitbarkeit nach Lemma 1.
Sei
und
der Index von
in der Aufzählung aller Formeln. Dann ist
, sonst wäre
. Also gilt
.
Sei nun
. Ist
, dann folgt mit der Annahmenregel
. Sei also
und
der Index von
. Dann ist
und
, sonst wäre
. Also gilt auch in diesem Fall
. ✔
Lemma 3: Abgeschlossenheit von
und
nach unten, d.h. für beliebige Formeln
und
gilt:
- 1.
![{\displaystyle \phi \notin \Gamma ^{*}\cap \Delta ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8bc3ed31bfd6e9bc15ff10e15f5cbe4975b9f6d)
- 2.
und ![{\displaystyle \bot \notin \Gamma ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de523e041cfb975b8a955680854461b8ed4b9d59)
- 3. wenn
, dann ![{\displaystyle \phi \in \Delta ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4bf0d870411b916aad75dbd49c6764da838e550b)
- 4. wenn
, dann ![{\displaystyle \phi \in \Gamma ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e80b8ca27082180cad7a5d099359d6ba99e22a4b)
- 5. wenn
, dann
und ![{\displaystyle \psi \in \Gamma ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bcf0f15cd6d2fecfd0314da39fcd88d59bc40b43)
- 6. wenn
, dann
oder ![{\displaystyle \psi \in \Delta ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0694944e854b1226ba6001ee191ec6b55dc4d950)
- 7. wenn
, dann
oder ![{\displaystyle \psi \in \Gamma ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bcf0f15cd6d2fecfd0314da39fcd88d59bc40b43)
- 8. wenn
, dann
und ![{\displaystyle \psi \in \Delta ^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0694944e854b1226ba6001ee191ec6b55dc4d950)
Beweis:
-
folgt mit der Annahmenregel und Lemma 1.
-
ergibt sich mit den Regeln für Verum und Falsum, sowie Lemma 1.
-
Sei
. Mit Lemma 2 folgt
und mit der Linken Negationsregel
. Erneut mit Lemma 2 folgt
.
-
Sei
. Mit Lemma 2 folgt
und mit der Rechten Negationsregel
. Erneut mit Lemma 2 folgt
.
-
Sei
oder
. Mit Lemma 2 folgt
oder
, also mit Verdünnung auch
. Mit der Linken Konjunktionsregel folgt
und wieder mit Lemma 2:
.
-
Sei
und
. Mit Lemma 2 folgt
und
. Mit der Rechten Konjunktionsregel folgt
und erneut mit Lemma 2:
.
-
Sei
und
. Mit Lemma 2 folgt
und
. Mit der Linken Disjunktionsregel folgt
und mit Lemma 2;
.
-
Sei
oder
. Mit Lemma 2 folgt
oder
und mit Verdünnng
. Mit der Rechten Disjunktionsregel folgt
und mit Lemma 2:
.
Damit ist der Beweis beendet. ✔
Die eben gezeigten Eigenschaften reichen aus, um eine Bewertung
zu definieren, die
beweist:.
Definition der Bewertung
:
- Für alle Aussagenkonstanten
sei
Wahr genau dann, wenn
.
Lemma 4: Für alle Formeln
gilt:
- wenn
, dann ist
Wahr,
- wenn
, dann ist
Falsch.
Beweis durch Induktion über den Aufbau der Formeln:
- Für Aussagenkonstanten gilt die Behauptung nach Definition von
.
- Für Verum und Falsum gilt die Behauptung wegen Lemma 3 Punkt 2.
- Gelte
. Dann gilt nach Lemma 3 Punkt 3.
und nach Induktionsvoraussetzung ist
Falsch. Also ist
Wahr.
Ist
, ist nach Lemma 3 Punkt 4.
und somit
Wahr. Also ist
Falsch.
- Gelte
. Nach Lemma 3 Punkt 5. und Induktionsvorraussetzung sind dann
Wahr und
Wahr. Also ist auch
Wahr.
Ist
, ist nach Lemma 3 Punkt 6. und der Induktionsvoraussetzung
Falsch oder
Falsch. Damit ist auch
Wahr.
- Gelte
. Nach Lemma 3 Punkt 7. und Induktionsvorraussetzung ist dann
Wahr oder
Wahr. Also ist auch
Wahr.
Ist
, sind nach Lemma 3 Punkt 8. und der Induktionsvoraussetzung
Falsch und
Falsch. Daher ist auch
Falsch.
Damit ist Lemma 4 bewiesen. ✔
Da ja
und
gilt auch:
beweist
.
Zusammen mit der Korrektheit des Kalküls gilt also:
Vollständigkeisatz:
ist ableitbar genau dann, wenn
gilt.
- ↑ Jürgen-Michael Glubrecht: Ein Vollständigkeitsbeweis für schnittfreie Kalküle mit der Maximalisierungsmethode von Henkin, im Archiv für mathematische Logik und Grundlagenforschung Band 22 (1982) S. 159 - 166