Deduktionstheorem

mathematischer Satz
(Weitergeleitet von Folgerungstheorem)

Unter dem Begriff Deduktionstheorem sind zwei eng verwandte Theoreme bekannt, die in der mathematischen Logik von Bedeutung sind. Eine Variante des Theorems, auch als Folgerungstheorem bekannt, zielt auf den Begriff der semantischen Folgerung ab. Die andere Variante, die innerhalb von Kalkülen Anwendung findet, macht statt der (semantischen) Folgerung die (syntaktische) Ableitung zum Ausgangspunkt. In beiden Fällen wird eine Beziehung zur materialen Implikation hergestellt.

Das Deduktionstheorem für semantische Folgerungen (⊨)

Bearbeiten

Die semantische Fassung des Deduktionstheorems lautet wie folgt:

Eine Formel   ist genau dann eine semantische Folgerung der Formelmenge   mit  , formal  , wenn die Implikation

 

allgemeingültig, d. h. eine Tautologie, ist (in klassischer Logik ist das genau dann der Fall, wenn die Implikation für jede mögliche Interpretation wahr ist).

Allgemein ist in klassischer Logik eine Formel   genau dann eine semantische Folgerung der Formelmenge  , d. h.  , wenn für jede Interpretation  , für die alle Formeln der Formelmenge   wahr sind, auch die Formel   wahr ist. Das Deduktionstheorem setzt diese allgemeine Definition einer semantischen Folgerung in Beziehung zur Implikation. Es bildet damit einen der wesentlichen Mechanismen, um den semantischen Begriff der Folgerung in Computersystemen durch rein formale Manipulationen handhabbar zu machen (siehe Ableitung in der Informatik). Es ist daher eng verwandt mit dem Widerlegungstheorem.

Das Deduktionstheorem für Ableitungen (⊢)

Bearbeiten

Im Bereich der Kalküle wird eine andere Definition des Deduktionstheorems verwendet, die sich rein auf der syntaktischen Ebene bewegt. Diese Variante des Deduktionstheorems wurde bereits um 1930 von Jacques Herbrand und (unabhängig von diesem und nahezu gleichzeitig) von Alfred Tarski gefunden und bewiesen. Im Zentrum dieser Definition steht im Gegensatz zur semantischen Folgerung die (syntaktische) Ableitung. Diese wird wie im oben beschriebenen Deduktionstheorem in ein Verhältnis zur Implikation gesetzt:

Wenn

 

dann

 

David Hilbert und Paul Bernays formulieren dies so: „Wenn aus einer Formel A eine Formel B in solcher Weise ableitbar ist [...], dann ist die Formel A → B ohne Benutzung der Formel A ableitbar.“[1]

In vielen Kalkülen gilt auch die Umkehrung. Das heißt, ist aus einer Menge die Formel A → B ableitbar, so auch die Formel B unter Zuhilfenahme der zusätzlichen Hypothese A. Gilt in einem Kalkül der Modus ponens, so ist diese Schlussrichtung trivial.

Einzelnachweise

Bearbeiten
  1. David Hilbert, Paul Bernays: Grundlagen der Mathematik, Band 2, Berlin: 1939, Seite 387.

Siehe auch

Bearbeiten

Literatur

Bearbeiten