Deduktionstheorem

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, stellt auf den Begriff der logischen Schlussfolgerung ab. Die andere Variante, die innerhalb von Kalkülen Anwendung findet, macht statt der (semantischen) logischen Folgerung die (syntaktische) Ableitung zum Ausgangspunkt. In beiden Fällen wird eine Beziehung zur materialen Implikation hergestellt.

Das Deduktionstheorem für logische Folgerungen (⊨)

Die semantische Fassung des Deduktionstheorems lautet wie folgt:

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

$A_{1}\land A_{2}\land ...\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 B genau dann eine logische Folgerung der Formelmenge T, d.h. $T\models B$, wenn für jede Interpretation I, für die alle Formeln der Formelmenge T wahr sind, auch die Formel B wahr ist. Das Deduktionstheorem setzt diese allgemeine Definition einer logischen Folgerung in Beziehung zur Implikation. Es bildet damit einen der wesentlichen Mechanismen, um den semantischen Begriff der logischen Folgerung in Computersystemen durch rein formale Manipulationen handhabbar zu machen. Es ist daher eng verwandt mit dem Widerlegungstheorem.

Die für die obige Aussage zentralen Begriffe der Formel und der Interpretation werden im Artikel über Wissensrepräsentation mit Logik ausführlich erläutert.

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) logischen Folgerung die (syntaktische) Ableitung. Diese wird wie im oben beschriebenen Deduktionstheorem in ein Verhältnis zur Implikation gesetzt:

Wenn

$T,A\vdash B,$

dann

$T\vdash A\rightarrow B.$

Hilbert und 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.

Siehe auch

• Negation, zu Logik-Polarität siehe Schaltalgebra
• These, Satz, Deduktion, Induktion (Denken), Abduktion, Fehlschluss, Statistik, Nullhypothese, Rhetorik, Dialektik, Fehler 1. und 2. Art
• Falsch positiv, Metawissenschaft

Literatur

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