Diskussion:Deduktionstheorem

ich versteh kein wort

Siehe auch

Das "Siehe auch"-Kapitel scheint mir ein bisschen zu viele bzw. nicht die richtigen Querverweise zu enthalten. --GottschallCh 22:35, 22. Dez 2005 (CET)

Implikation vs. Äquivalenz

Gilt das Deduktionstheorem nicht in beide Richtungen? Das „Wenn ... dann ... ” suggeriert, dass nur folgendes gilt:

$T,A\vdash B~\Rightarrow ~T\vdash A\rightarrow B$

Jedoch gilt meines wissens sogar:

$T,A\vdash B~\Leftrightarrow ~T\vdash A\rightarrow B$

Falls das wer bestätigen kann, bitte korrigieren. 84.56.16.129 23:15, 9. Jan 2006 (CET)

Das Deduktionstheorem sagt lediglich aus, dass, wenn $\psi$ aus $\Gamma \cup \varphi$ herleitbar ist, aus $\Gamma$ alleine $\varphi \rightarrow \psi$ herleitbar ist.

Es stimmt schon, dass, wenn aus $\Gamma$ der Satz $\varphi \rightarrow \psi$ herleitbar ist, dann aus $\Gamma \cup \varphi$ der Satz $\psi$ herleitbar ist; das ist aber nicht eine Folgerung oder Aussage des Deduktionstheorems, sondern der Abtrennungsregel (Modus ponendo ponens). --GottschallCh 23:29, 9. Jan 2006 (CET)

Überarbeitung des Artikels

Hallo liebe Freunde, ich habe mir erlaubt, den Artikel zum einen vereinfachend umzuformulieren, zum anderen das Wesentliche des Deduktionstheorems besser herauszuarbeiten. Artikel im Stil einer Formelsammlung bringen imho nur wenig, und der zentrale Zweck des Deduktionstheorems, nämlich den semantischen Begriff der logischen Folgerung syntaktisch handhabbar zu machen, ging aus dem bisherigen Artikel überhaupt nicht hervor. Sollte jemandem an der bisherigen Formulierung sehr gelegen sein, bin ich zur Findung einer gemeinsamen Artikelfassung jederzeit bereit. Grüße Mkleine 16:16, 22. Jan 2006 (CET)

Des weiteren habe ich soeben den als Duplikat anzusehenden Artikel Folgerungstheorem zu einem Redirect auf diesen Artikel gemacht. Mkleine 16:36, 22. Jan 2006 (CET)

Hallo!

Deduktionstheorem und Folgerungstheorem (im Sinn des alten Artikels Folgerungstheorem) in ein und demselben Artikel zu behandeln ist sicher eine diskussionswürdige Idee, es sollte aber doch klarer herausgehen, was beide behandeln. Der wesentliche Unterschied ist der, dass das Deduktionstheorem eine Aussage über rein syntaktische Sachverhalte ist ("Wenn aus Γ gemeinsam mit A ein Satz B hergeleitet werden kann, dann kann aus Γ alleine ein Satz A → B hergeleitet werden"). Im Gegensatz dazu ist das Folgerungstheorem, wie es in dem gleichnamigen Artikel stand, (a) eine semantische Aussage und (b) ein Bikonditional ("genau dann wenn") (das Deduktionstheorem ist wirklich nur ein Konditional).

Viele Grüße, --GottschallCh 22:48, 23. Jan 2006 (CET)

Ich habe hierzu auf meiner Benutzer-Diskussion Stellung genommen, da du mir dort eine Nachricht hinterlassen hast. Gerne können wir die Diskussion hier fortsetzen, weshalb ich meinen Kommentar hier einfüge:

Hallo, meines Erachtens ist deine Darstellung nicht korrekt. Der Begriff des Ableitens oder Herleitens kommt eigentlich erst in einem Kalkül zum Tragen, und ohne mich nun im einzelnen durch das von dir angegebene Skript arbeiten zu können (die Symbolik dort ist doch sehr eigenwillig), gehe ich stark davon aus, dass hier bereits der Kalkülbegriff eingeführt wurde. Ein Kalkül verfügt im Gegensatz zu einer Logik zusätzlich über Schlussregeln (wie modus ponens usw.), denn ohne diese könnte man ja gar keine Ableitungen bilden. Das Deduktionstheorem funktioniert jedoch bereits in Aussagenlogik und PL1 (ohne Schlussregeln) und basiert dort auf dem Begriff der logischen Folgerung (als Symbol |=) im Gegensatz zum syntaktischen Ableiten (Symbol |-) in einem Kalkül.

Logisches Folgern ist jedoch in jedem Fall eine semantische Angelegenheit, denn eine Formel B folgt aus einer Formel A (symbolisch: A |= B), wenn alle Modelle von A auch Modelle von B sind. Modelle aber basieren auf Interpretationen, und die sind unzweifelhaft Teil der semantischen Ebene.

Bitte schau doch nochmal durch dein Skript und prüfe, ob hier bereits der Kalkülbegriff im Spiel ist - der Professor hat dann offenbar das Deduktionstheorem auf einen Kalkül angewandt, und dann kann es natürlich sein, dass daraus eine rein syntaktische Angelegenheit wird. (Zur Erinnerung sei angefügt, dass |= und |- äquivalent sind, wenn es sich um einen korrekten und vollständigen Kalkül handelt.) Es handelt sich dann in diesem Skript gewissermaßen um ein "spezielleres" Deduktionstheorem. Daraus könnte man sicher ein interessante Diskussion in der Vorlesung führen ;-).

Gerne können wir diese Differenzierung in den Artikel einarbeiten, wenn hierzu eine passende Formulierung gefunden wird. Viele Grüße Mkleine 23:08, 23. Jan 2006 (CET)

Viele Grüße Mkleine 13:37, 24. Jan 2006 (CET)

Hallo! Wie gesagt, kein inhaltlicher Widerspruch von meiner Seite, es scheint mir nur das Theorem, das ich unter dem Titel "Deduktionstheorem" kenne, das häufiger so bezeichnete zu sein. Dass es relativ zu einem Kalkül definiert ist (und nicht zu einem semantischen Konzept) ist durchaus Absicht. Ich kann mir ohne weiteres vorstellen, dass auch das semantische Theorem öfters als Deduktionstheorem bezeichnet wird, nur - wie gesagt - mir ist es in dieser Bezeichnung noch nicht untergekommen, und ich bin mir relativ sicher, dass es die statistisch seltenere Verwendung dieses Begriffs sein müsste.

Das Skriptum, das ich zitiert habe, war nur rasch mit Google herausgesucht, weil ich gern dazu neige, im Lauf der Jahre einzelne Theoreme zu verwechseln und weil ich keinen Unsinn sagen wollte. ;-) Es sieht aber wirklich so aus, als könnte man ziemlich willkürlich nach "Deduktionstheorem" suchen und würde man immer auf eine syntaktische Formulierung gestoßen, z.B. auch [1].

Ein mehr rhetorisches, aber vielleicht auch nicht schlechtes Argument: Die semantische Formulierung des Theorems ist (in klassischer Logik) ganz trivial zu beweisen und ergibt sich schon aus der Definition des Folgerungsbegriffs und des Konditionals. Das (syntaktische) Deduktionstheorem bedarf schon eines nicht ganz trivialen Induktionsbeweises. Wo (mir) in der Literatur das Deduktionstheorem untergekommen ist, stand aber immer der Induktionsbeweis dabei (auch im zuletzt genannten Stuttgarter Skriptum).

Ich habe im Hinterkopf, dass das (syntaktische) Deduktionstheorem 1930 von Herbrand bewiesen wurde, habe aber im Büro nicht die Mittel, das zu klären - erfahrungsgemäß liegen meine Erinnerungen bezüglich den Quellen von Theoremen sehr oft daneben. ;-)

Viele Grüße, --GottschallCh 18:44, 24. Jan 2006 (CET)

Hallo, ich habe jetzt einen zusätzlichen Abschnitt über das Deduktionstheorem in Kalkülen in den Artikel aufgenommen, der auf der vorherigen Artikelfassung beruht. Wenn du Präziseres zu Hilberts Beweis zur Verfügung hast, wäre es prima, wenn das noch in den Artikel einfließen könnte. Ich denke, dass in der Literatur generell nicht präzise zwischen diesen beiden Definitionen unterschieden wird, insofern gefällt mir das Ergebnis dieser Diskussion wirklich sehr gut! Grüße Mkleine 19:20, 24. Jan 2006 (CET)

Hallo! Ich bin inzwischen zu Hause und habe Zugriff auf etwas mehr Literatur. ;-) Hier habe ich auf die Schnelle folgende drei Verweise auf den Ausdruck "Deduktionstheorem" gefunden:

Hilbert/Bernays: Grundlagen der Mathematik, Band 2, Berlin: 1939, Seite 387: "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"

Henkin: The completeness of the first-order functional calculus, in: JSL 14, 1949, Seite 161: "Wenn Γ, A |- B, so Γ |- A→B (für irgendwelche Ausdrücke A, B und Ausdrucksmengen Γ)".

Kreiser/Gottwald/Stelzner: Nichtklassische Logik, Berlin: Akademie 1990, Seite 37 f.: "D|-: Für beliebige Ausdrücke H1, H2 und Ausdrucksmengen Σ gilt: Σ ∪ {H1} |- H2 gdw. Σ |- H1 → H2 (2.12). [...] Eigenschaft D|- ist wieder eine Kalküleigenschaft, deren Erfülltsein Bedingungen an das Ableiten im Kalkül und an formale Eigenschaften der betrachteten Implikation stellt. Gillt stets (2.13) für einen Kalkül, so sagen wir, daß für ihn das Deduktionstheorem gilt".

Bezüglich der Frage, ob syntaktisch oder semantisch, sind sich zumindest diese Quellen zugunsten der Syntax einig, und bezüglich der Frage, ob in der gebräuchlichsten Verwendung die Bedingung von links nach rechts geht (wie ich mich zu erinnern glaubte) oder ob es eine gdw-Bedingung ist, sind sie sogar untereinander uneinig. Logik ist auch nicht mehr das, was sie einmal war. :-) Viele Grüße, --GottschallCh 19:48, 24. Jan 2006 (CET)

Hier auch noch eine Quelle für die semantische Version: "Für alle Formeln F, G ohne freie Variablen gilt F |= G genau dann, wenn die Formel F -> G allgemeingültig ist." (Görz, Handbuch der Künstlichen Intelligenz). Eine ähnliche Formulierung (ebenfalls mittels gdw.) findet sich in Künstliche Intelligenz und automatische Wissensverarbeitung von Prof. Helbig: "Formel Q ist genau dann eine logische Folgerung der Formeln $P_{1},P_{2},...,P_{n}$, wenn die Implikation $P_{1},P_{2},...,P_{n}\rightarrow Q$ wahr ist." In beiden Fällen geht es nicht um Kalküle, sondern um die PL1. Mkleine 20:41, 24. Jan 2006 (CET)

Ich glaube, damit haben wir die Erklärung gefunden: In der Logik wird der Begriff "Deduktionstheorem" wohl im syntaktischen Sinn verwendet, in der Informatik im semantischen Sinn. Ich habe zur Stützung dieser Vermutung noch in Bibel: Deduktion. Automatisierung der Logik nachgesehen, also einem Informatikbuch, und dort wird es semantisch definiert.

Ein bisschen stört das Bild Melvin Fitting: First-Order Logic and Automated Theorem Proving, wo es - obwohl ein ATP-Buch - doch auch wieder syntaktisch definiert ist (Seite 80), aber andererseits ist Fitting meines Wissens Logiker, sodass es dann doch ins Schema passt.

Ich finde es faszinierend, dass sich sogar zwei formale Wissenschaften in der Terminologie unterscheiden...

Viele Grüße, --GottschallCh 00:24, 25. Jan 2006 (CET)

Was denkst du, wie der Artikel unter diesem Aspekt aussehen sollte? Meine Recherche hat mich an einigen wenigen Stellen zu dem Begriff "schwaches Deduktionstheorem" geführt. Leider gibt es da im Web nur sehr wenige Treffer. Etwas mehr findet man unter "weak deduction theorem". Vielleicht kommen wir über diese Unterscheidung weiter? Wobei mir noch nicht klar ist, ob unter dem "schwachen Deduktionstheorem" nun die rein syntaktische Version verstanden wird, aber das ist meine Vermutung. Denn zu einer formalen Logik gehört eben auch die semantische Ebene (erst durch sie kommen überhaupt Wahrheitswerte für konkrete Formeln ins Spiel, und was ist eine Logik ohne Wahrheitswerte ...). Mir erscheint daher die syntaktische Fassung "schwächer". Falls sich diese Vermutung bestätigt, könnte man im Artikel diese Unterscheidung hervorheben.

Ganz so deutlich wie du würde ich übrigens die Trennung zwischen Informatik/KI und Logik nicht ziehen. In der KI gilt das Interesse eben im wesentlichen dem Begriff der (semantischen) logischen Folgerung, und hier bildet das Deduktionstheorem eben die Brücke zu den rein formalen Mechanismen. Nichtsdestoweniger steht die KI auf dem Boden der formalen Logik und benutzt diese nur, um etwa automatisches Schließen zu realisieren. Aber du hast recht, die Perspektiven sind da anders, und das führt offenbar dazu, dass derselbe Begriff in zwei (wenn auch eng verwandten) Varianten benutzt wird. Übrigens könnte man auch mal untersuchen, inwieweit der Begriff Konditionalbeweis sich mit dem Deduktionstheorem verbinden ließe. Jedenfalls ist dieser ebenfalls sehr eng verwandt. Grüße Mkleine 11:52, 25. Jan 2006 (CET)

Nachdem beide Fassungen des Deduktionstheorems recht prominent zu sein scheinen, würde ich fast versuchen, in der Einleitung eine vereinheitlichte Fassung zu geben, so in dem Sinn von: "Das Deduktionstheorem stellt eine Beziehung zwischen entweder der Folgerung oder der Herleitbarkeit einer Aussage B aus einer Aussage A auf der einen Seite und der Gültigkeit oder der Herleitbarkeit des Konditionals A→B auf der anderen Seite her". Für die nähere Erläuterung würde ich die Unterteilung in zwei Kapitel belassen, allerdings gefiele mir als Wortlaut für die Überschriften "Semantische Formulierung" und "Syntaktische Formulierung" oder auch "Folgerung" und "Herleitung" besser als "stark" und "schwach": Diese Bezeichnungen sind mir selber nur im Bereich mehrwertiger Logiken untergekommen, für die das Deduktionsthorem unter dem gewöhnlichen Folgerungsbegriff nicht gilt und wo man sich dann mit einer schwächeren Variante behilft, die einen schwächeren Folgerungsbegriff zugrunde legt.

Inhaltlich stimme ich natürlich zu, dass die Semantik wichtig ist und auch wichtiger sein kann. Die Gültigkeit des (syntakt.) Deduktionstheorems wird aber auch schon dann für einen Kalkül thematisiert und u.U. bewiesen oder widerlegt, wenn es dafür noch gar keine ausgearbeitete Semantik gibt (heute kommt das wohl nicht mehr so häufig vor); z.B. hat man Modallogik oder auch intuitionistische Logik syntaktisch betrieben und sich nach der Gültigkeit des Deduktionstheorems für einzelne Kalküle dieser Systeme gefragt, bevor es noch formale Semantiken dafür gab (auch wenn man sich natürlich - informell - etwas Inhaltliches dabei gedacht hat). Insofern sehe ich nicht eines der beiden als primäre Formulierung.

Viele Grüße, --GottschallCh 19:54, 25. Jan 2006 (CET)

syntaktische oder semantische Version?

Bezug nehmend auf die obige Expertendiskussion: Zum Teil wird schlicht zwischen einer semantischen und einer syntaktischen Version des Deduktionstheorems unterschieden, so in Martin Gessmann (Hg.): Philosophisches Wörterbuch. 23. Auflage. Kröner, Stuttgart 2009, ISBN 978-3-520-01323-1: Deduktionsproblem.

--Karl-Hagemann (Diskussion) 18:03, 15. Dez. 2012 (CET)