De auteurs van forall x geven deze definitie van geldigheid (pagina 8):
Een argument is geldig als en alleen als het onmogelijk is dat alle premissen waar zijn en de conclusie onwaar.
Ze noemen dit ook wel “validity in virtue of form” (blz. 21):
De geldigheid van de zojuist besproken argumenten heeft niet veel te maken met de betekenissen van Engelse uitdrukkingen als ‘Jenny is miserable’, ‘Dipan is an avid reader of Tolstoy’, of ‘Jim acted in lots of plays’. Als het al met betekenissen te maken heeft, dan is het met de betekenissen van zinnen als ‘en’, ‘of’, ‘niet,’ en ‘als…, dan…’.
Zulke geldigheid kan automatisch worden gevalideerd met behulp van proof checkers. Ervan uitgaande dat de proof checker niet slecht geconstrueerd is, als het argument dat we in de proof checker invoeren slaagt, dan is het geldig op grond van de vorm.
Overweeg de zin: “Het regent.” De negatie van deze zin zou geschreven kunnen worden als “Het is niet zo dat het regent.” Laten we “Het regent” symboliseren met “P”. Dan zou de negatie “¬P” zijn. Een zelf-contradictoire zin opgebouwd uit deze twee zou zijn “P ∧ ¬P”, dat wil zeggen, zowel “P” als “¬P”.
Kunnen we, als we dit als premisse gebruiken, een geldig argument op grond van vorm construeren? Ja, dat kunnen we. Hier is een voorbeeld waarin ik probeer aan te tonen dat “P ∧ ¬P” “P” impliceert.
De eerste regel is de premisse. De tweede regel krijg ik door gebruik te maken van de eliminatieregel van het voegwoord (∧E), die me toestaat beide zijden van het voegwoord (∧) in mijn argument te gebruiken. Het blijkt dat wat ik gebruikte, “P”, was wat ik wilde laten zien en dus controleerde de bewijscontroleur of ik mijn doel bereikt had.
Het kan vreemd lijken dat gegeven een zelf-contradictoire premisse, ik in staat was om een geldig argument te construeren waaruit bleek dat een van de conjuncten in de zelf-contradictoire premisse volgde. Het kan nog vreemder.
Met een beetje meer werk, kan ik laten zien dat alles volgt uit een zelf-contradictoire premisse. Laat “Q” de symbolisering zijn voor wat dan ook. Dit voorbeeld laat zien dat ik een geldig in deugd van vorm argument voor “Q” kan construeren:
De eerste regel bevat de zelf-contradictoire premisse zoals in het vorige voorbeeld.
Op regel 2 en 3 heb ik voegwoordeliminatie (∧E) toegepast aan beide zijden van de premisse (regel 1) om deze op aparte regels te plaatsen.
Als ik ze eenmaal op aparte regels heb staan, kan ik de regel van tegenspraakinleiding (⊥I) gebruiken om op regel 4 te noteren dat ik een tegenspraak heb (⊥).
Op regel 5 kan ik, omdat ik een tegenspraak heb, alles schrijven wat ik wil. Dat heet de regel van explosie (X). Omdat mijn doel “Q” is en ik volgens de regels alles kan schrijven wat ik wil, schrijf ik “Q”. De proof checker controleert of ik mijn doel heb bereikt.
Voor meer details over deze regels, zie hoofdstuk 15 “Basisregels voor TFL” in forall x.