Fitch-Kalkül

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.

Regeln

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 $\vdash$ ist der Ableitungsoperator (z. B. $p\vdash q$ , 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: $p\rightarrow q,p\rightarrow \neg q\vdash \neg p$
Negations-Beseitigung: Ist NICHT NICHT p gegeben (oder jede andere gerade Anzahl von Negationen), dann auch p (s. Gesetz der doppelten Negation). Beispiel: $\neg \neg p\vdash p$
Konjunktions-Einführung: Sind p, q, r,… gegeben, dann auch p UND q UND r UND …. Beispiel: $p,q\vdash p\wedge q$
Konjunktions-Beseitigung: Ist p UND q UND r UND … gegeben, dann auch p, q, r,…. Beispiel: $p\wedge q\vdash p$
Disjunktions-Einführung: Ist p gegeben, dann auch p ODER q ODER r ODER …. Beispiel: $p\vdash p\lor q$
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\lor q,p\to z,q\to z\vdash z$
Äquivalenz-Einführung: Sind p IMPLIZIERT q sowie q IMPLIZIERT p gegeben, dann auch p ÄQUIVALENT q. Beispiel: $p\to q,q\to p\vdash p\leftrightarrow q$
Äquivalenz-Beseitigung: Ist p ÄQUIVALENT q gegeben, dann auch p IMPLIZIERT q sowie q IMPLIZIERT p. Beispiel: $p\leftrightarrow q\vdash p\to q$
Subjunktions-Einführung: Ist gezeigt worden, dass q durch Fitch-Ableitungsregeln aus p bewiesen werden kann (Notation: p $\vdash$ q), dann gilt auch p IMPLIZIERT q. Durch Subjunktions-Einführung beendet man einen Unterbeweis. Beispiel: $(p\vdash q)\vdash (p\to q)$
Subjunktionsbeseitigung: Sind p gegeben sowie p IMPLIZIERT q, dann auch q. Beispiel: $p,p\to q\vdash q$

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: $\operatorname {ungerade} (x)\vdash \forall x.\operatorname {ungerade} (x)$

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: $\forall x.\operatorname {ungerade} (x)\vdash \operatorname {ungerade} (3)$

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

Das folgende Beispiel beweist den Kettenschluss: Aus $(p\to q)$ und $(q\to r)$ folgt $(p\to r)$ . 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 $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ :

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

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

Weblinks

Eintrag „Fitch Calculus“ In: John Halleck's Logic Systems
Übungen und Beweisrechner für den Fitch-Kalkül auf den Seiten der Stanford University.
Java-Anwendung für Fitch-Beweise von Christian Gottschall (Universität Wien).

Literatur

Jon Barwise und John Etchemendy: Sprache, Beweis und Logik, Band 1: Aussagen- und Prädikatenlogik. 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. Übers. von Language proof and logic, Seven Bridges Press and CSLI, 1999.
- engl. Original als pdf