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, 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} ist genau dann eine semantische Folgerung der Formelmenge Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T} mit $T=\{A_{1},A_{2},\dots ,A_{n}\}$, formal $T\models B$, wenn die Implikation

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} genau dann eine semantische Folgerung der Formelmenge Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T} , d. h. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T \models B} , wenn für jede Interpretation Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle I} , für die alle Formeln der Formelmenge $T$ wahr sind, auch die Formel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T, A \vdash B, }

dann

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\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.

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)