~2026-40679-8 am 19. Januar 2026 um 12:42 Uhr

2026-01-19T12:42:37Z

Neue Seite

{{Überarbeiten}}

Unter dem Begriff '''Deduktionstheorem''' sind zwei eng verwandte [[Theorem]]e bekannt, die in der [[Mathematische Logik|mathematischen Logik]] von Bedeutung sind. Eine Variante des Theorems, auch als '''Folgerungstheorem''' bekannt, zielt auf den Begriff der [[Semantische Folgerung|''semantischen Folgerung'']] ab. Die andere Variante, die innerhalb von [[Kalkül]]en Anwendung findet, macht statt der ([[Semantik|semantischen]]) Folgerung die ([[Syntax|syntaktische]]) [[Ableitung (Logik)|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 <math>B</math> ist genau dann eine [[semantische Folgerung]] der Formelmenge <math>T</math> mit <math>T = \{ A_1, A_2, \dots, A_n \}</math>, formal <math>T \models B</math>, wenn die Implikation

:<math> A_1 \land A_2 \land \dots \land A_n \rightarrow B</math>

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

Allgemein ist in [[Klassische Logik|klassischer Logik]] eine Formel <math>B</math> genau dann eine semantische Folgerung der Formelmenge <math>T</math>, d. h. <math>T \models B</math>, wenn für jede Interpretation <math>I</math>, für die alle Formeln der Formelmenge <math>T</math> wahr sind, auch die Formel <math>B</math> 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 (Informatik)|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 (Logik)|Ableitung]]. Diese wird wie im oben beschriebenen Deduktionstheorem in ein Verhältnis zur Implikation gesetzt:

Wenn
:<math> T, A \vdash B, </math>
dann
:<math> T \vdash A \rightarrow B.
</math>

[[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.“<ref>David Hilbert, Paul Bernays: ''Grundlagen der Mathematik'', Band 2, Berlin: 1939, Seite 387.</ref>

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 ==
<references />

== Siehe auch ==
* [[Modelltheorie]]
* [[Wissensrepräsentation mit Logik]]
* [[Negation#Negation im Sinne der philosophischen Dialektik (Hegels)|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)

[[Kategorie:Mathematische Logik]]

Deduktionstheorem - Versionsgeschichte

~2026-40679-8 am 19. Januar 2026 um 12:42 Uhr