Hier sind sieben aussagenlogischen Tautologien, wobei
A, B, C beliebige Formeln sind:
|
Als Nächstes geben wir eine Liste von fünf Axiomen, die Quantoren enthalten:
|
Dazu kommen noch zwei Schlussregeln:
|
Abtrennungsregel oder Modus Ponens:
Die Formel B ist eine direkte Konsequenz der
beiden Formeln A und A ® B.
Generalisierung: Für jede Variable x ist " x A eine direkte Konsequenz der Formel A. |
Mit Hilfe dieser 12 Axiome und dieser 2 Schlussregeln wollen wir nun aus den gegebenen Axiomen einer Theorie gültige Sätze ableiten, d.h. beweisen.
Q sei eine Theorie. Eine Folge von Formeln
A1, A2,... , An
heißt Ableitungsfolge oder formaler Beweis
aus Q, wenn für jedes i wenigstens eine eine der Bedingungen
erfüllt ist:
Abl(Q) ist die Menge aller aus Q ableitbaren Formeln. |
"Abl" ist ein Hüllenoperator, d.h.
|
Schon abgeleitete Formeln können auch benutzt werden. So setzen wir voraus, daß alle in der Liste aufgeführten Äquivalenzen schon abgeleitet sind---das Erleichtert das sonst immens mühsame Ableiten deutlich.
Der folgende Satz ist fast trivial:
|
Endlichkeitssatz fürs Ableiten
Ist eine Formel A aus einer Theorie Q ableitbar, so ist
A bereits aus einer endlichen Teilmenge von Q ableitbar.
|
Der wichtige Zusammenhang zwischen Semantik und Syntax bei Sprachen 1. Stufe wird durch diesen fundamentalen Satz hergestellt: Relativ leicht ist der Beweis, daß jeder aus einer Theorie ableitbare Ausdruck aus ihr folgt. Die Umkehrung gilt auch, ist aber schwerer zu beweisen.
|
Gödelscher Vollständigkeitssatz:
Es sei Q eine Theorie der Sprache (1. Stufe)
L.
Für jede Aussage A der Sprache gilt:
A folgt genau dann aus Q wenn A aus Q
ableitbar ist.
|