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 (⊨)

Die semantische Fassung des Deduktionstheorems lautet wie folgt:

Eine Formel ${\displaystyle B}$ ist genau dann eine semantische Folgerung der Formelmenge ${\displaystyle T}$ mit ${\displaystyle T=\{A_{1},A_{2},\dots ,A_{n}\}}$, formal ${\displaystyle T\models B}$, wenn die Implikation

${\displaystyle A_{1}\land A_{2}\land \dots \land A_{n}\rightarrow B}$

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 ${\displaystyle B}$ genau dann eine semantische Folgerung der Formelmenge ${\displaystyle T}$, d. h. ${\displaystyle T\models B}$, wenn für jede Interpretation ${\displaystyle I}$, für die alle Formeln der Formelmenge ${\displaystyle T}$ wahr sind, auch die Formel ${\displaystyle B}$ 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 (⊢)

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

${\displaystyle T,A\vdash B,}$

dann

${\displaystyle T\vdash A\rightarrow B.}$

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

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

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

Siehe auch

• Modelltheorie
• Wissensrepräsentation mit Logik
• Negation, zu Logik-Polarität siehe Schaltalgebra
• Metawissenschaft

Literatur

• Franz von Kutschera, Alfred Breitkopf: Einführung in die moderne Logik, 8. Aufl. (2007), ISBN 978-3-495-482711, S. 72–75 (Beweis des Deduktionstheorems)