Fitch-Kalkül

Das Fitch-Kalkül ist eine Methode, um formelle Beweise in Logik erster Ebene durchzuführen. Es wurde von dem amerikanischen Logiker Frederic Brenton Fitch erfunden. Beweise, die mit dem Fitch-Kalkül geführt werden bestehen aus atomaren Aussagen. Besondere atomare Aussagen sind Vorbedingungen und Unterbeweise. Damit ein Beweis korrekt ist, müssen alle Schritte außer den Voraussetzungen und den initalen 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 die Problemstellung bewiesen wurde.

Regeln

Das Fitch-Kalkül basiert auf Logik erster Ebene. Syntaktisch korrekte atomare Aussagen bestehen aus einer Mischung folgender Symbole:

AND → Eine Aussage ist genau dann wahr, wenn alle mit einem AND verbundene Terme wahr sind.

OR → Eine Aussage ist genau dann wahr, wenn mindestens eine der mit einem OR verbundenen Terme wahr ist.

NOT → Eine Aussage ist genau dann wahr, wenn alle mit einem NOT verbundenen Terme nicht wahr sind.

BOTTOM → Ein Widerspruch wurde festgestellt, eine der vorhergehenden Annahmen oder Voraussetzung ist falsch.

IMPLICATION → Eine Aussage ist sowohl dann wahr, wenn der Term nach dem IMPLICATION Zeichen wahr ist, als auch wenn der Term vor dem IMPLICATION Zeichen falsch ist.

BIIMPLICATION → Eine Aussage ist sowohl dann wahr, wenn beide Term vor und nach dem BIIMPLICATION Zeichen wahr sind, als auch wenn beide Terme vor und nach dem BIIMPLICATION Zeichen falsch sind.

EQUALS → Eine Aussage ist genau dann wahr, wenn beide Terme die mit einem EQUALS Zeichen verbunden sind gleich sind.

UNIVERSAL QUANTIFIER(X) → Eine Aussage ist genau dann wahr, wenn sie für alle möglichen Ausprägungen einer Variable X gilt.

EXISTENTIAL QUANTIFIER → Eine Aussage ist genau dann wahr, wenn sie für mindestens eine Ausprägungen einer Variable X gilt.

Aussagen werden aus Termen aufgebaut die durch diese Symbole miteinander in Beziehung stehen. Die syntaktisch korrekte Form dieser Aussagen kann unter Prädikatenlogik nachgelesesen werden.

Beispiel

Das folgende Beispiel ist eine einfache Veranschaulichung, dass eine Aussage wahr oder falsch sein muss. Hierfür werden keine Vorbedingungen benötigt.

  1 NOT(Aussage OR NOT(Aussage))           [Annahme]
    2 Aussage                              [Annahme]
    3 Aussage OR NOT(Aussage)              [OR Intro: 2]
    4 BOTTOM                               [BOTTOM Intro: 1,3]
  5 NOT(Aussage)                           [NOT Intro: 2-4]
  6  Aussage OR NOT(Aussage)               [OR Intro: 5]
  7  BOTTOM                                [BOTTOM Intro: 1,6]
8 NOT NOT(Aussage OR NOT(Aussage))         [NOT Intro: 1-7]
9 Aussage OR NOT(Aussage)                  [NOT Elim: 8]

Anwendungen

Das Fitch-Kalkül kann neben philosophischen Zwecken auch in der Informatik eingesetzt werden. Es hat vor allem in der theoretischen Informatik Bedeutung. Da nur Logik erster Ordnung und keine Logik höherer Stufe verwendet wird, ist dieses Kalkül weniger mächtig als z.B. Fuzzylogik, dennoch aber für einfachere Probleme, auch aufgrund der leichten Nachvollziehbarkeit, praktisch und didaktisch geeignet.

Verwandt

• Anwendung der Stanford University "Fitch".
• Eine online Java Anwendung um Beweise zu führen [1].

Weblinks

• Fitch Calculus
• Fitch's Paradox of Knowability

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.