Les auteurs de forall x donnent cette définition de la validité (page 8):
Un argument est valide si et seulement s’il est impossible que toutes les prémisses soient vraies et la conclusion fausse.
Ils parlent aussi de « validité en vertu de la forme » (page 21):
La validité des arguments que nous venons de considérer n’a pas grand-chose à voir avec le sens d’expressions anglaises comme « Jenny is miserable », « Dipan est un lecteur avide de Tolstoï » ou « Jim a joué dans de nombreuses pièces de théâtre ». Si cela a un rapport avec les significations, c’est avec les significations de phrases comme ‘et’, ‘ou’, ‘pas’ et ‘si…, alors…’.
Cette validité peut être automatiquement validée en utilisant des vérificateurs de preuves. En supposant que le vérificateur de preuve n’est pas mal construit, si l’argument que nous entrons dans le vérificateur de preuve passe, alors il est valide en vertu de la forme.
Considérez la phrase, « Il pleut ». La négation de cette phrase pourrait s’écrire « Il n’est pas le cas qu’il pleuve ». Symbolisons « Il pleut » par « P ». Sa négation serait alors « ¬P ». Une phrase auto-contradictoire construite à partir de ces deux-là serait « P ∧ ¬P », c’est-à-dire à la fois « P » et « ¬P ».
En utilisant ceci comme prémisse pouvons-nous construire un argument valide en vertu de la forme ? Oui, nous le pouvons. Voici un exemple où j’essaie de montrer que « P ∧ ¬P » implique « P ».
La première ligne est la prémisse. J’obtiens la deuxième ligne en utilisant la règle d’élimination des conjonctions (∧E) qui me permet d’utiliser l’un ou l’autre côté de la conjonction (∧) dans mon argument. Il s’avère que ce que j’ai utilisé, « P », était ce que je voulais montrer et donc le vérificateur de preuve a vérifié que j’ai atteint mon objectif.
Il peut paraître étrange que, étant donné une prémisse auto-contradictoire, j’ai pu construire un argument valide montrant qu’une des conjonctions de la prémisse auto-contradictoire suivait. Cela peut devenir encore plus étrange.
Avec un peu plus de travail, je peux montrer que n’importe quoi suit d’une prémisse auto-contradictoire. Soit « Q » la symbolisation de n’importe quoi n’importe comment. Cet exemple montre que je peux construire un argument valide en vertu de la forme pour « Q »:
La première ligne contenait la prémisse auto-contradictoire comme dans l’exemple précédent.
Sur les lignes 2 et 3, j’ai utilisé l’élimination de la conjonction (∧E) des deux côtés de la prémisse (ligne 1) pour les placer sur des lignes séparées.
Une fois que je les ai sur des lignes séparées, je peux utiliser la règle d’introduction de la contradiction (⊥I) pour noter à la ligne 4 que j’ai une contradiction (⊥).
À la ligne 5, parce que j’ai une contradiction, je peux écrire tout ce que je veux. C’est ce qu’on appelle la règle de l’explosion (X). Puisque mon but est « Q » et que selon les règles je peux écrire tout ce que je veux, j’écris « Q ». Le vérificateur de preuve vérifie que j’ai atteint mon but.
Pour plus de détails sur ces règles, voir le chapitre 15 « Règles de base pour TFL » in forall x.
.