DISKRETE MATHEMATIK
Erich Prisner
Sommersemester 2000
Ableitungen
Es gibt verschiedene Ableitungssysteme. Wir werden hier das im Buch von
Tuschik und Wolter
vorgestellte angeben.
Wir starten mit 12 sogenannten logischen Axiomen:
Hier sind sieben aussagenlogischen Tautologien, wobei
A, B, C beliebige Formeln sind:
- (1) A
(B A),
- (2) [A
(B C)]
[A B)
(A C)],
- (3) (
A
B)
(B A),
- (4) a) A
B A,
b) A B B
- (5) (A
B)
[(A C)
(A (B C))],
- (6) a) A
A B,
b) B A B,
- (7) (A
C)
[(B C)
((A B) C],
|
Als Nächstes geben wir eine Liste von fünf Axiomen,
die Quantoren enthalten:
- (8)
x A(x) A(t),
wobei t ein beliebiger Term ist,
dessen Variablen in A frei sind wo x frei war,
- (9)
x (A B)
(A
x B),
wobei x in A nicht frei vorkommt,
- (10) a)
x
A
x A,
b) x A
x
A,
- (11)
x (x = x),
- (12)
x y
(x = y
(A A')), wobei A' aus A dadurch entsteht,
daß x an einigen frei vorkommenden Stellen durch y
(frei vorkommend) ersetzt wird.
|
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:
- Ai hat einen Typ wie
(1)-(7) oder
(8)-(12) oben,
- Ai ist Element von Q,
- Ai ist direkte Konsequenz nach
Modus Ponens
zweier vorhergehender Folgenglieder,
- Ai ist direkte Konsequenz nach
Generalisierung
zweier vorhergehender Folgenglieder
Jedes solche Ai heisst aus Q ableitbar
(beweisbar).
Abl(Q) ist die Menge aller aus Q ableitbaren Formeln.
|
"Abl" ist ein Hüllenoperator, d.h.
- Q
Abl(Q),
- Ist Q
Q', so folgt
Abl(Q) Abl(Q'),
- Abl(Abl(Q)) = Abl(Q),
|
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.
|
Weiter zu ...,
oder zurück zur Sprachbeschreibung,
oder zurück zur Semantik
Erich Prisner
erstellt im Juni 2000.