Fitch-Kalkül
# 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.

