Fitch-Kalkül

Methode für Beweise in Prädikatenlogik erster Stufe

Der Fitch-Kalkül ist eine von dem amerikanischen Logiker Frederic Brenton Fitch erfundene Methode für Beweise in Prädikatenlogik erster Stufe. Der Beweis wird lediglich aufgrund syntaktischer Regeln geführt, ohne Berücksichtigung inhaltlicher Bedeutungen der vorkommenden Sätze, also formal. Der Fitch-Kalkül ist sowohl korrekt als auch vollständig und daher auch als Interaktives Beweissystem geeignet. Im Fitch-Kalkül ist zusätzlich zu den Prämissen des Hauptbeweises die Einführung beliebiger weiterer Annahmen erlaubt, aber nur innerhalb von Unterbeweisen. Damit ein Beweis korrekt ist, müssen alle Schritte außer den Voraussetzungen und den initialen Annahmen der Unterbeweise durch Logikregeln erster Ordnung belegt werden. Nachdem eine atomare Aussage bewiesen wurde, darf diese zur Begründung einer neuen Aussage herangezogen werden, bis der Beweis geführt wurde.

Der Fitch-Kalkül verwendet die Sprache der Prädikatenlogik 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   ist der Ableitungsoperator (z. B.  , lies: „p beweist q“ oder „q ist ableitbar aus p“). Im Fitch-Kalkül gibt es folgende Ableitungsregeln:

Negations-Einführung
Sind p IMPLIZIERT q sowie p IMPLIZIERT NICHT q gegeben, dann auch NICHT p (s. Reductio ad absurdum). Beispiel:  
Negations-Beseitigung
Ist NICHT NICHT p gegeben (oder jede andere gerade Anzahl von Negationen), dann auch p (s. Gesetz der doppelten Negation). Beispiel:  
Konjunktions-Einführung
Sind p, q, r,… gegeben, dann auch p UND q UND r UND …. Beispiel:  
Konjunktions-Beseitigung
Ist p UND q UND r UND … gegeben, dann auch p, q, r,…. Beispiel:  
Disjunktions-Einführung
Ist p gegeben, dann auch p ODER q ODER r ODER …. Beispiel:  
Disjunktions-Beseitigung
Sind p ODER q ODER r ODER … sowie p IMPLIZIERT z, q IMPLIZIERT z, r IMPLIZIERT z,… gegeben, dann auch z. Beispiel:  
Äquivalenz-Einführung
Sind p IMPLIZIERT q sowie q IMPLIZIERT p gegeben, dann auch p ÄQUIVALENT q. Beispiel:  
Äquivalenz-Beseitigung
Ist p ÄQUIVALENT q gegeben, dann auch p IMPLIZIERT q sowie q IMPLIZIERT p. Beispiel:  
Subjunktions-Einführung
Ist gezeigt worden, dass q durch Fitch-Ableitungsregeln aus p bewiesen werden kann (Notation: p   q), dann gilt auch p IMPLIZIERT q. Durch Subjunktions-Einführung beendet man einen Unterbeweis. Beispiel:  
Subjunktionsbeseitigung
Sind p gegeben sowie p IMPLIZIERT q, dann auch q. Beispiel:  

Enthält die Sprache Quantoren, kommen vier weitere Regeln hinzu:

Allquantor-Einführung
Ist ein Satz mit freien Variablen gegeben, lässt sich die Tatsache, dass diese jeden beliebigen Wert der Grundmenge annehmen können, als Allquantifizierung schreiben. Beispiel:  
Allquantor-Beseitigung
Ist ein allquantifizierter Satz gegeben, lässt sich von diesem allgemeinen Fall auf einen beliebigen Einzelfall schließen; die vom Allquantor gebundene Variable kann also durch jedes Element der Grundmenge ersetzt werden. Beispiel:  
Existenzquantor-Einführung
Ist ein konkreter Einzelfall gegeben, lässt 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) „für 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 Prädikat r“) lässt sich auf das Sukzedens (hier: y) schließen. Beispiel: Aus den beiden Prämissen 1. ∀x.(x erhält die Mehrheit der abgegebenen Stimmen → x ist gewählt) und 2. ∃x.(x hat die Mehrheit der Stimmen erhalten) lässt sich schließen: x ist gewählt.

Beispiele

Bearbeiten

Das folgende Beispiel beweist den Kettenschluss: Aus   und   folgt  . Der Pfeil → bedeutet IMPLIZIERT, IE ist kurz für Implication Elimination (Subjunktionsbeseitigung), II für Implication Introduction (Subjunktionseinführung).

1 p → q [Prämisse]
2 q → r [Prämisse]
   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 für die Distribution der Implikation  :

1 p → (q → r) [Prämisse]
   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 Prämisse ∃y.∀x.r(x,y) – „es existiert ein y, sodass r(x,y) für 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) [Prämisse]
   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]

Abkürzungen: UE: Universal Elimination = Allquantor-Beseitigung, UI: Universal Introduction = Allquantor-Einführung, EI: Existential Introduction = Existenzquantor-Einführung, EE: Existential Eliminitation = Existenzquantor-Beseitigung

Anwendungen

Bearbeiten

Der Fitch-Kalkül kann neben philosophischen Zwecken auch in der Informatik eingesetzt werden. Er hat vor allem in der theoretischen Informatik Bedeutung.

Bearbeiten

Literatur

Bearbeiten