Logo

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.
Beispiele:

"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.