Hilfe zum Fitch-Applet

(dieser Text: Steven DeHaven, Calgary, und Christian Gottschall, Wien)

Dieser Text behandelt nicht den verwendeten Kalkül. Er setzt voraus, dass Sie mit diesem Kalkül vertraut sind. Wenn Sie Hilfe zum Kalkül selbst suchen, lesen Sie bitte die Hilfe zu den Regeln. Benötigen Sie Informationen zur logischen Sprache, lesen Sie bitte die Hilfe zur Sprache. Der einzige Zweck dieses Textes besteht darin, die "Mechanismen" der Verwendung des Beweisbauers darzulegen.

Soferne Sie nicht sein Fenster geschlossen haben, sollte der Beweisbauer in einem eigenen Fenster sichtbar sein. Beachten Sie die vier weißen Bereiche des Applets. Den langen horizontalen Bereich an der Oberseite nennen wir "Oben". Den einzelnen Bereich links darunter nennen wir "Links". Die beiden weißen Bereiche rechts von Links nennen wir "R1" und "R2". Oben ist der Meldungsbereich, in dem z.B. Fehlermeldungen angezeigt werden. Oben erlaubt keine Benutzereingaben. Links ist der Bereich, in dem die Ableitung angezeigt wird, die Sie eingeben. Anklicken einer Zeile der Ableitung wählt diese. Wenn Sie eine bereits gewählte Zeile erneut anklicken, wird die Auswahl rückgängig gemacht. Wählen der Schaltfläche "Markierung aufheben" macht die gesamte getroffene Auswahl rückgängig. Die Schaltfläche "Rückgängig" entfernt die zuletzt zur Ableitung in Links hinzugefügte Zeile. Wir kehren später zur Bedeutung von Links zurück.

R1 ist der Bereich, in dem Prämissen und Annahmen eingegeben werden können. Bewegen Sie Ihre Maus auf R1 und betätigen Sie die Maustaste. Eine blinkende Schreibmarke wird sichtbar. Sie können nun Ihre Eingaben in diesem Bereich vornehmen. Versuchen Sie, eine Formel der logischen Sprache in R1 einzugeben. Sobald Sie dies getan haben, klicken Sie entweder auf "Prämisse" oder auf "A" ("Annahme"). Ihre Eingabe wird nach Links übernommen. Sie wird nummeriert und mit der korrekten Rechtfertigung versehen. Beachten Sie, dass jede Annahme gegenüber der ihr vorangehenden Zeile um eine Spalte eingerückt dargestellt wird. Um ein Theorem zu beweisen, beginnt man natürlich mit einer Annahme. Das Theorem selbst wird in der ersten Spalte (ohne Einrückung) aufscheinen, was einer Herleitung aus der leeren Prämissenmenge entspricht. Dies wird auch in Oben durch Aufscheinen des Theorems rechts vom Herleitungszeichen |- widergespiegelt. Sie können zu jeder Zeit die jeweils letzte Zeile des Beweises durch Klicken von "Rückgängig" entfernen.

Als nächstes müssen wir die Benützung der Regeln erlernen. Geben Sie eine Konjunktion als Prämisse ein, z.B. den Satz "P & Q" (ohne die Anführungszeichen!). Nun wollen wir &B (Und-Beseitigung) auf diese Zeile anwenden. Bewegen Sie zuerst die Maus auf Links und klicken Sie auf den Satz. Er wird dadurch ausgewählt. Sie können die Auswahl durch neuerliches Klicken auf den gewählten Satz oder durch Wahl von "Markierung aufheben" rückgängig machen. Im Allgemeinen werden Sie jedoch jenen Satz oder jene Sätze auswählen, auf die Sie eine Regel anwenden möchten, und anschließend die gewünschte Regelschaltfläche anklicken. Falls Sie einen Ableitungsschritt versuchen, der im formalen System nicht zulässig ist, wird eine entsprechende Fehlermeldung in Oben ausgegeben. In unserem Beispiel klicken Sie nach Wählen der Konjunktionszeile auf die Schaltfläche "&B" (Und-Beseitigung). Beachten Sie, dass sowohl P als auch Q in R2 aufscheinen werden. Dies zeigt an, dass die Anwendung der Regel zu mehr als einem Ergebnis führen könnte. Sie müssen nun entscheiden, welches der möglichen Ergebnisse Sie wünschen. Sie wählen das gewünschte Ergebnis durch Doppelklick darauf in R2. Es wird dann als neue Zeile der Herleitung hinzugefügt, versehen mit einer Zeilennummer und der korrekten Rechtfertigung.

Unser logisches System nach Gentzen und Fitch macht starken Gebrauch von der Regel der Wiederholung (Reiteration, Reit). Um eine Zeile zu wiederholen, wählen Sie sie einfach in Links und klicken Sie auf die Regelschaltfläche "Reit". Falls die versuchte Reiteration unzulässig ist, wird eine entsprechende Fehlermeldung ausgegeben. Sie können z.B. keine Zeile in einer abgeschlossenen Subderivation reiterieren.

Andere Schwierigkeiten, auf die mein beim Ableiten stoßen kann, werden meist dadurch verursacht, dass man mit dem logischen System noch nicht vollends vertraut ist. Grundsätzlich ist das System vollständig, sodass jedes gültige Argument in ihm auch tatsächlich hergeleitet werden kann. Leider ist es in formalen Systemen so, dass nicht jede offensichtliche Wahrheit auch einfach herzuleiten ist.