Hilfe zum Lemmon-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 Sprachhilfe. 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 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 auf "A" ("Annahme"). Ihre Eingabe wird nach Links übernommen. Sie wird korrekt nummeriert und mit der korrekten Rechtfertigung versehen. 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". 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.

Andere Schwierigkeiten, auf die man 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.