Der Fitch Kalkul ist eine von dem amerikanischen Logiker Frederic Brenton Fitch erfundene Methode fur Beweise in Pradikatenlogik erster Stufe Der Beweis wird lediglich aufgrund syntaktischer Regeln gefuhrt ohne Berucksichtigung inhaltlicher Bedeutungen der vorkommenden Satze also formal Der Fitch Kalkul ist sowohl korrekt als auch vollstandig und daher auch als Interaktives Beweissystem geeignet Im Fitch Kalkul ist zusatzlich zu den Pramissen des Hauptbeweises die Einfuhrung beliebiger weiterer Annahmen erlaubt aber nur innerhalb von Unterbeweisen Damit ein Beweis korrekt ist mussen alle Schritte ausser den Voraussetzungen und den initialen Annahmen der Unterbeweise durch Logikregeln erster Ordnung belegt werden Nachdem eine atomare Aussage bewiesen wurde darf diese zur Begrundung einer neuen Aussage herangezogen werden bis der Beweis gefuhrt wurde Inhaltsverzeichnis 1 Regeln 2 Beispiele 3 Anwendungen 4 Weblinks 5 LiteraturRegeln BearbeitenDer Fitch Kalkul verwendet die Sprache der Pradikatenlogik erster Ordnung also deren logische Operatoren zum Beispiel UND ODER IMPLIZIERT NICHT usw angewendet auf atomare Aussagen im Folgenden vertreten durch Kleinbuchstaben p q Das Symbol displaystyle vdash nbsp ist der Ableitungsoperator z B p q displaystyle p vdash q nbsp lies p beweist q oder q ist ableitbar aus p Im Fitch Kalkul gibt es folgende Ableitungsregeln Negations Einfuhrung Sind p IMPLIZIERT q sowie p IMPLIZIERT NICHT q gegeben dann auch NICHT p s Reductio ad absurdum Beispiel p q p q p displaystyle p rightarrow q p rightarrow neg q vdash neg p nbsp Negations Beseitigung Ist NICHT NICHT p gegeben oder jede andere gerade Anzahl von Negationen dann auch p s Gesetz der doppelten Negation Beispiel p p displaystyle neg neg p vdash p nbsp Konjunktions Einfuhrung Sind p q r gegeben dann auch p UND q UND r UND Beispiel p q p q displaystyle p q vdash p wedge q nbsp Konjunktions Beseitigung Ist p UND q UND r UND gegeben dann auch p q r Beispiel p q p displaystyle p wedge q vdash p nbsp Disjunktions Einfuhrung Ist p gegeben dann auch p ODER q ODER r ODER Beispiel p p q displaystyle p vdash p lor q nbsp Disjunktions Beseitigung Sind p ODER q ODER r ODER sowie p IMPLIZIERT z q IMPLIZIERT z r IMPLIZIERT z gegeben dann auch z Beispiel p q p z q z z displaystyle p lor q p to z q to z vdash z nbsp Aquivalenz Einfuhrung Sind p IMPLIZIERT q sowie q IMPLIZIERT p gegeben dann auch p AQUIVALENT q Beispiel p q q p p q displaystyle p to q q to p vdash p leftrightarrow q nbsp Aquivalenz Beseitigung Ist p AQUIVALENT q gegeben dann auch p IMPLIZIERT q sowie q IMPLIZIERT p Beispiel p q p q displaystyle p leftrightarrow q vdash p to q nbsp Subjunktions Einfuhrung Ist gezeigt worden dass q durch Fitch Ableitungsregeln aus p bewiesen werden kann Notation p displaystyle vdash nbsp q dann gilt auch p IMPLIZIERT q Durch Subjunktions Einfuhrung beendet man einen Unterbeweis Beispiel p q p q displaystyle p vdash q vdash p to q nbsp Subjunktionsbeseitigung Sind p gegeben sowie p IMPLIZIERT q dann auch q Beispiel p p q q displaystyle p p to q vdash q nbsp Enthalt die Sprache Quantoren kommen vier weitere Regeln hinzu Allquantor Einfuhrung Ist ein Satz mit freien Variablen gegeben lasst sich die Tatsache dass diese jeden beliebigen Wert der Grundmenge annehmen konnen als Allquantifizierung schreiben Beispiel ungerade x x ungerade x displaystyle operatorname ungerade x vdash forall x operatorname ungerade x nbsp Allquantor Beseitigung Ist ein allquantifizierter Satz gegeben lasst sich von diesem allgemeinen Fall auf einen beliebigen Einzelfall schliessen die vom Allquantor gebundene Variable kann also durch jedes Element der Grundmenge ersetzt werden Beispiel x ungerade x ungerade 3 displaystyle forall x operatorname ungerade x vdash operatorname ungerade 3 nbsp Existenzquantor Einfuhrung Ist ein konkreter Einzelfall gegeben lasst sich dies als Existenzaussage formalisieren Beispiel Rom ist die Hauptstadt Italiens impliziert drei Existenzaussagen 1 Es existiert etwas das die Hauptstadt Italiens ist 2 es existiert etwas von dem Rom die Hauptstadt ist 3 es existiert etwas das die Hauptstadt von etwas ist Existenzquantor Beseitigung Aus einer allquantifizierten Implikation zum Beispiel x r x y fur alle x gilt Hat x die Eigenschaft r so folgt y und dem Wissen um die Existenz eines solchen Individuums im Beispiel x r x es existiert ein x mit dem Pradikat r lasst sich auf das Sukzedens hier y schliessen Beispiel Aus den beiden Pramissen 1 x x erhalt die Mehrheit der abgegebenen Stimmen x ist gewahlt und 2 x x hat die Mehrheit der Stimmen erhalten lasst sich schliessen x ist gewahlt Beispiele BearbeitenDas folgende Beispiel beweist den Kettenschluss Aus p q displaystyle p to q nbsp und q r displaystyle q to r nbsp folgt p r displaystyle p to r nbsp Der Pfeil bedeutet IMPLIZIERT IE ist kurz fur Implication Elimination Subjunktionsbeseitigung II fur Implication Introduction Subjunktionseinfuhrung 1 p q Pramisse 2 q r Pramisse 3 p Annahme beginnt einen Unterbeweis 4 q IE in Zeilen 3 1 5 r IE in Zeilen 4 2 Unterbeweis abgeschlossen 6 p r II in Zeilen 5 3 Beweis abgeschlossen Hier ein Beweis fur die Distribution der Implikation p q r p q p r displaystyle p to q to r to p to q to p to r nbsp 1 p q r Pramisse 2 p q Annahme 1 beginnt einen Unterbeweis 3 p Annahme 2 beginnt einen Unter Unterbeweis 4 q IE in Zeilen 3 2 5 q r IE in Zeilen 3 1 6 r IE in Zeilen 4 5 Unter Unterbeweis abgeschlossen 7 p r II in Zeilen 6 3 Unterbeweis abgeschlossen 8 p q p r II in Zeilen 7 2 Beweis abgeschlossen Aus der Pramisse y x r x y es existiert ein y sodass r x y fur alle x gilt soll geschlossen werden dass auch x y r x y gilt zu jedem x existiert ein y sodass r x y gilt 1 y x r x y Pramisse 2 x r x y Annahme beginnt einen Unterbeweis 3 r x y UE in Zeile 2 4 y r x y EI in Zeile 3 5 x r x y y r x y II in Zeilen 2 4 Unterbeweis abgeschlossen 6 y x r x y y r x y UI in Zeile 5 7 y r x y EE in Zeilen 1 6 8 x y r x y UI in Zeile 7 Abkurzungen UE Universal Elimination Allquantor Beseitigung UI Universal Introduction Allquantor Einfuhrung EI Existential Introduction Existenzquantor Einfuhrung EE Existential Eliminitation Existenzquantor BeseitigungAnwendungen BearbeitenDer Fitch Kalkul kann neben philosophischen Zwecken auch in der Informatik eingesetzt werden Er hat vor allem in der theoretischen Informatik Bedeutung Weblinks BearbeitenEintrag Fitch Calculus In John Halleck s Logic Systems Ubungen und Beweisrechner fur den Fitch Kalkul auf den Seiten der Stanford University Java Anwendung fur Fitch Beweise von Christian Gottschall Universitat Wien Literatur BearbeitenJon Barwise und John Etchemendy Sprache Beweis und Logik Band 1 Aussagen und Pradikatenlogik Mentis 2005 ISBN 3 89785 440 6 dort S 59ff 117ff et passim Band 2 Anwendungen und Metatheorie Mentis 2006 ISBN 3 89785 441 4 dt Ubers von Language proof and logic Seven Bridges Press and CSLI 1999 engl Original als pdf Abgerufen von https de wikipedia org w index php title Fitch Kalkul amp oldid 223849619
