Die Regeln des Lemmon-Systems

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

Dieser Hilfetext ist eine kurze Übersicht über die Schlussregeln des Systems. Wenn Sie Hilfe mit dem Applet benötigen, lesen Sie bitte die Hilfe zum Applet. Benötigen Sie Hilfe zur logischen Sprache, lesen Sie bitte die Sprachhilfe. Bitte beachten Sie, dass dieser Text nur eine Übersicht über die angebotenen Schlussregeln ist und keine Einführung in deduktive Systeme bieten kann. Falls Sie noch nicht mit Kalkülen des natürlichen Schließens oder zumindest anderen formalen Systemen vertraut sind, sollten Sie zunächst die Vorlesung "Einführung in die Logik" bei Dr. Klaus Dethloff oder die Nachfolgevorlesung bei Dr. Esther Ramharter besuchen oder die einführenden Kapitel in E.J. Lemmons Buch "Beginning Logic" lesen.

&B (Und-Beseitigung) erlaubt es, auf p oder auf q zu schließen, soferne p & q eine verfügbare Zeile ist.
&E (Und-Einführung) erlaubt es, von p und von q als einzelnen Zeilen auf p & q oder auf q & p zu schließen.
->B (Pfeil-Beseitigung) erlaubt es, von p und von p -> q auf q zu schließen. Dieser Schritt wird oft "modus ponens" oder -korrekter- "modus ponendo ponens" genannt.
~~B (Doppelte Negationsbeseitigung) erlaubt es, von ~~p auf p zu schließen.
vE (Oder-Einführung) erlaubt es, von p auf p v q oder auf q v p zu schließen. Beachten Sie, dass Sie das Disjunkt q in R1 angeben müssen.
vB (Oder-Beseitigung) erlaubt es, von p v q auf r zu schließen, soferne unabhängig voneinander zuerst aus der Annahme von p auf r und hernach von der Annahme von q auf r geschlossen wurde. Zum Ausführen der vB muss vor dem Klicken auf "vB" die Disjunktion, die Annahme von p, das aus p hergeleitete r, die Annahme von q und das aus q hergeleitete r mit der Maus gewählt werden.
D<-> (Definition des Doppelpfeils) erlaubt es, ein Bikonditional einzuführen oder aufzulösen.
->E (Pfeil-Einführung) führt ein Konditional ein. Beachten Sie, dass Sie die Annahme (das werdende Antecedens) und die letzte Zeile (das werdende Konsequens) mit der Maus wählen müssen, ehe Sie auf "->E" klicken.
~E (Nicht-Einführung) wird verwendet, einen indirekten Beweis abzuschließen. Die letzte Zeile muss ein expliziter Widerspruch sein.

Die übrigen Regeln beziehen sich auf die Prädikatenlogik und sollen zu einem späteren Zeitpunkt erläutert werden.