Die Autoren von forall x geben diese Definition von Gültigkeit (Seite 8):
Ein Argument ist gültig, wenn und nur wenn es unmöglich ist, dass alle Prämissen wahr und die Schlussfolgerung falsch ist.
Sie bezeichnen dies auch als „Gültigkeit kraft der Form“ (Seite 21):
Die Gültigkeit der soeben betrachteten Argumente hat nicht viel mit den Bedeutungen englischer Ausdrücke wie „Jenny is miserable“, „Dipan is an avid reader of Tolstoy“ oder „Jim acted in lots of plays“ zu tun. Wenn es überhaupt mit Bedeutungen zu tun hat, dann mit den Bedeutungen von Ausdrücken wie ‚und‘, ‚oder‘, ’nicht‘ und ‚wenn…, dann…‘.
Solche Gültigkeiten können automatisch mit Hilfe von Proof Checkern überprüft werden. Unter der Annahme, dass der Beweisprüfer nicht schlecht konstruiert ist, wenn das Argument, das wir in den Beweisprüfer eingeben, besteht, dann ist es kraft der Form gültig.
Betrachten Sie den Satz: „Es regnet.“ Die Negation dieses Satzes könnte geschrieben werden als „Es ist nicht der Fall, dass es regnet.“ Wir symbolisieren „Es regnet“ mit „P“. Dann wäre seine Negation „¬P“. Ein aus diesen beiden gebildeter selbstwidersprüchlicher Satz wäre „P ∧ ¬P“, also sowohl „P“ als auch „¬P“.
Können wir mit dieser Prämisse ein gültiges Argument kraft der Form konstruieren? Ja, das können wir. Hier ist ein Beispiel, in dem ich zu zeigen versuche, dass „P ∧ ¬P“ „P“ impliziert.
Die erste Zeile ist die Prämisse. Die zweite Zeile erhalte ich, indem ich die Konjunktionsauslöschungsregel (∧E) verwende, die es mir erlaubt, beide Seiten der Konjunktion (∧) in meinem Argument zu verwenden. Es stellt sich heraus, dass das, was ich verwendet habe, „P“, das war, was ich zeigen wollte, und so hat der Proof Checker überprüft, dass ich mein Ziel erreicht habe.
Es mag seltsam erscheinen, dass ich in der Lage war, bei einer selbstwidersprüchlichen Prämisse ein gültiges Argument zu konstruieren, das zeigt, dass eine der Konjunktionen in der selbstwidersprüchlichen Prämisse folgte. Es kann sogar noch seltsamer werden.
Mit ein wenig mehr Arbeit kann ich zeigen, dass aus einer selbstwidersprüchlichen Prämisse irgendetwas folgt. Lassen Sie „Q“ die Symbolisierung für irgendetwas sein. Dieses Beispiel zeigt, dass ich ein gültiges formelles Argument für „Q“ konstruieren kann:
Die erste Zeile enthält die selbstwidersprüchliche Prämisse wie im vorherigen Beispiel.
In den Zeilen 2 und 3 habe ich die Konjunktion (∧E) auf beiden Seiten der Prämisse (Zeile 1) eliminiert, um sie auf separate Zeilen zu setzen.
Sobald ich sie auf getrennten Zeilen habe, kann ich die Regel der Widerspruchseinleitung (⊥I) anwenden, um in Zeile 4 zu vermerken, dass ich einen Widerspruch (⊥) habe.
In Zeile 5, weil ich einen Widerspruch habe, kann ich schreiben, was ich will. Das nennt man die Regel der Explosion (X). Da mein Ziel „Q“ ist und ich nach den Regeln alles schreiben kann, was ich will, schreibe ich „Q“. Der Proof Checker prüft, ob ich mein Ziel erreicht habe.
Weitere Details zu diesen Regeln finden Sie in Kapitel 15 „Grundregeln für TFL“ in forall x.