0. Einführung
Die Verarbeitung Beweisprüfungsverfahren erlaubt es, die Lösungen von Übungsbeispielen auf ihre Korrektheit zu prüfen. Ist diese Verarbeitungsart gewählt, muss daher im Eingabebereich die Herleitung eines Arguments eingegeben werden. Die Syntax einer Herleitung entspricht im wesentlichen der im weiland Logiktutorium und im Skriptum verwendeten, diese wiederum der aus E.J. Lemmon: ,,Beginning Logic'' und Colin Allen: ,,Logic Primer''.
1. Syntax
Aussagen setzen sich aus Prädikaten, Individuenkonstanten und beliebigen Namen, Individuenvariablen, Konnektiven und Klammern zusammen. Für diese Bestandteile gelten folgende Konventionen:
1.1. Prädikate
Ein Prädikat besteht aus genau einem Großbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben oder Ziffern. Beispiele für Prädikate sind ,,P'', ,,Q'', ,,P1'', ,,Q42'', aber auch ,,Hugo'' oder ,,Blubb37''. Hat das Prädikat Argumente, werden sie - durch Beistriche getrennt - in runden Klammern ans Prädikat angeschlossen, z.B. ,,Mensch(Sokrates)'' oder ,,Groesser(Eins,Zwei)''.
1.2. Individuenkonstanten und beliebige Namen
Individuenkonstanten und beliebige Namen bestehen wie Prädikate aus genau einem Großbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben und Ziffern. Beispiele sind ,,Sokrates'' oder ,,Platon''. Die Beweisprüfung erkennt aus dem Zusammenhang, ob es sich um eine Individuenkonstante oder um einen beliebigen Namen handelt.
1.3. Individuenvariablen
Individuenvariablen beginnen mit einem Kleinbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben und Ziffern. Beispiele sind ,,x'', ,,x42'' und ,,hugo''.
1.4. Konnektive
Aussagen sind aus Negationen, Konjunktionen, Disjunktionen, Konditionalen und Bikonditionalen aufgebaut. Da eine gewöhnliche Computertastatur nicht über die üblicherweise benützten logischen Zeichen verfügt, verwenden Sie bitte folgende Annäherungen:
,,~'', ,,&'', ,,v'', ,,->'', ,,<->''
Alternativ können Sie auch die Wörter ,,nicht'', ,,und'', ,,oder'', ,,dann'' und ,,gdw'' verwenden.
1.5. Quantoren
Als All- bzw. Existenzquantor werden die Wörter ,,alle'' bzw. ,,ein'' verwendet. Dem Quantor folgt in Klammern die durch ihn gebundene Variable und der quantifizierte Ausdruck, voneinander getrennt durch einen Beistrich.
Beispiele:
alle(x,Mensch(x)->Sterblich(x)) ein(x,Unsterblich(x)) alle(x,ein(y,Liebt(x,y)))
1.6. Klammern
Für die Klammerung verwenden Sie bitte die üblichen runden Klammern, ,,('' und ,,)''. Wenn Sie Klammern weglassen, gilt folgende Auswertungsreihenfolge:
- Negationen
- Konjunktionen
- Disjunktionen
- Konditionale
- Bikonditionale
Die zweistelligen Konditionale sind linksassoziativ.
2. Schlussregeln
- Annahme: ,,A''
- Und-Einführung: ,,&E'', ,,^E''
- Und-Beseitigung: ,,&B'', ,,^B''
- Oder-Einführung: ,,vE''
- Oder-Beseitigung: ,,vB''
- Pfeil-Einführung: ,,->E'', ,,CP'' (conditional proof)
- Pfeil-Beseitigung: ,,->B'', ,,MPP'' (modus ponendo ponens)
- Nicht-Einführung (,,indirekter Beweis''): ,,~E'', ,,RAA'' (reductio ad absurdum)
- Doppelte Negation: ,,~~B'', ,,DN''
- Allquantor-Einführung (,,Generalisierung''): ,,AE'', ,,UE'', ,,GEN''
- Allquantor-Beseitigung: ,,AB'', ,,UB''
- Existenzquantor-Einführung: ,,EE''
- Existenzquantor-Beseitigung: ,,EB''
- Identitätseinführung: ,,=E'', ,,IE''
- Identitätsbeseitigung: ,,=B'', ,,IB''