Preuves et tableaux sémantiques

1. Ce qu'est une preuve

Un argument est l'affirmation qu'une conclusion découle de certaines prémisses. Une preuve est ce qui tranche cette affirmation : un objet fini et vérifiable que chacun peut lire ligne à ligne et accepter, sans avoir à vous croire sur parole. L'intérêt d'une preuve n'est pas qu'elle convainc - un bon discours le fait aussi - mais que chacune de ses étapes ne pouvait pas se passer autrement.

C'est une exigence plus stricte qu'il n'y paraît. « Il pleut, donc le sol est mouillé » est une chose raisonnable à dire, mais elle s'appuie sur ce que vous savez de la pluie et du sol. La logique formelle écarte cela et pose une question plus étroite : étant donné la seule forme des phrases, y a-t-il un moyen quelconque que les prémisses soient vraies et la conclusion fausse ? S'il n'y en a aucun, l'argument est valide, et la preuve est le compte rendu de cette absence.

Ce guide porte sur une manière de produire ce compte rendu : la méthode des tableaux sémantiques, aussi appelés arbres de vérité. C'est la méthode qu'utilise ce site dès que vous saisissez un argument dans la calculatrice, et une fois que vous l'avez suivie une fois, vous pouvez vérifier un argument sur papier avec un simple stylo.

2. Valide, et comment le savoir

Écrivez un argument avec un signe de conséquence : les prémisses à gauche, la conclusion à droite. L'affirmation p → q, ¬q ⊨ ¬p dit que d'un conditionnel et de la négation de son conséquent découle la négation de son antécédent. Le signe de conséquence n'est pas un connecteur de plus. C'est une affirmation sur les formules qui l'encadrent, et elle est soit juste, soit fausse.

La définition de la validité indique directement une façon de la tester : parcourir chaque attribution de vrai et de faux aux variables et regarder si l'une d'elles rend toutes les prémisses vraies et la conclusion fausse. C'est ce que fait une table de vérité, et pour deux ou trois variables cela convient très bien. L'ennui est que la table croît en 2ⁿ. Dix variables demandent mille lignes, vingt en demandent un million, et la table ne dit rien de savoir quelles lignes comptaient.

Un tableau aborde la même question par l'autre bout. Au lieu d'énumérer toutes les possibilités pour en chercher une mauvaise, il suppose qu'il en existe une mauvaise et tente de la construire. Si la tentative s'effondre en contradiction sur toutes les routes possibles, aucune attribution de ce genre n'existe et l'argument est valide. Si la tentative réussit, ce qu'elle a construit est un contre-exemple que vous pouvez lire directement.

3. La méthode des tableaux

Un tableau est un arbre de formules signées. Chaque ligne est une formule précédée d'un T ou d'un F, et le signe dit ce que la branche suppose de cette formule - non pas sa valeur de vérité, mais celle qu'il faudrait pour que l'argument échoue. Toute la méthode tient en quatre étapes :

1. Écrivez chaque prémisse avec un T. Vous supposez que toutes les prémisses de l'argument tiennent.
2. Écrivez la conclusion avec un F. Vous supposez qu'elle échoue malgré tout - c'est l'hypothèse que vous cherchez à réfuter.
3. Prenez une ligne qui n'est pas encore un atome et appliquez la règle de son connecteur principal et de son signe, en ajoutant ce que produit cette règle à la fin de chaque branche qui la traverse.
4. Fermez une branche dès qu'elle porte à la fois T A et F A pour une même formule A. Arrêtez quand toutes les branches sont fermées, ou qu'il ne reste plus de ligne à décomposer.

Rien dans cette boucle ne demande d'astuce ni de choix de stratégie. Chaque ligne a exactement une règle, et les appliquer dans n'importe quel ordre donne le même verdict - c'est pourquoi une machine peut le faire, et pourquoi vous pouvez vous fier au résultat quand elle le fait.

4. Les règles

Il y a une règle par connecteur et par signe - dix en tout. Elles se répartissent en deux sortes, et la différence entre ces sortes est toute la raison pour laquelle un tableau est un arbre et non une liste. Une règle α dit que plusieurs choses doivent tenir ensemble : elle empile ses résultats le long de la branche. Une règle β dit que l'une de deux choses doit tenir : elle scinde la branche en deux et laisse chaque cas suivre sa route.

Chaque règle n'est que la condition de vérité de son connecteur, lue à l'envers. Une conjonction n'est vraie que si les deux côtés le sont, donc T (A ∧ B) empile T A et T B. Une conjonction est fausse dès qu'un côté l'est, mais la formule ne dit pas lequel, donc F (A ∧ B) doit essayer les deux : elle scinde. La même asymétrie joue en sens inverse pour la disjonction, et un conditionnel faux signifie que l'antécédent tenait et que le conséquent a échoué - le seul cas où une implication se rompt.

Remarquez ce que les règles ne font jamais : elles n'inventent jamais de formule. Tout ce qu'une règle produit est un morceau de la ligne dont elle provient. Cette propriété - la propriété de la sous-formule - est ce qui rend la méthode finie, et nous y revenons plus bas.

5. Fermer une branche

Une branche est un seul fil de raisonnement : lisez de la racine à une feuille et vous avez un ensemble complet d'hypothèses. Une branche se ferme quand ces hypothèses se contredisent franchement, c'est-à-dire quand elle porte à la fois T A et F A pour une seule et même formule. Peu importe la complexité de A ou la distance entre les deux lignes : si une branche exige qu'une formule soit à la fois vraie et fausse, rien ne la satisfait.

Marquez une branche fermée d'un ×, en nommant les deux lignes qui l'ont fermée, et cessez d'y travailler. On n'apprend plus rien d'une hypothèse qui était déjà impossible.

Quand toutes les branches se ferment, le tableau est fermé, et c'est là la preuve. Elle montre que la supposition de départ - toutes les prémisses vraies, la conclusion fausse - mène à une contradiction sur chacune des routes possibles. Comme aucune route ne subsiste, aucune attribution de ce genre n'existe, et l'argument est valide. C'est une preuve par l'absurde, disposée de sorte qu'aucun cas ne puisse être oublié.

6. Une preuve, ligne à ligne

Prenons le modus tollens : p → q, ¬q ⊨ ¬p. Les lignes 1 et 2 sont les prémisses, supposées vraies. La ligne 3 est la conclusion, supposée fausse - et comme la conclusion est ¬p, la supposer fausse revient à supposer p vraie, ce que consigne la ligne 5. La ligne 4 vient de la règle de négation appliquée à la ligne 2 : si ¬q est vraie, q est fausse. Le conditionnel de la ligne 1 est la seule ligne qui garde un connecteur, et c'est une règle β : l'arbre se scinde donc.

La branche de gauche suppose que le conditionnel tenait parce que son antécédent a échoué - mais la ligne 5 a déjà p vraie, donc la branche se contredit et se ferme. La branche de droite suppose qu'il tenait parce que son conséquent était vrai - mais la ligne 4 a déjà q fausse, donc elle se ferme aussi.

Les deux branches sont fermées : il n'y a donc aucun moyen d'avoir p → q et ¬q vraies avec ¬p fausse. L'argument est valide, et l'arbre en est la raison. Remarquez que la preuve ne parle ni de pluie, ni de sol, ni de ce que désignent p et q. Elle n'en avait pas besoin.

7. Quand une branche reste ouverte

Tous les arguments ne sont pas valides, et c'est là que la méthode fait ses preuves. Si vous travaillez une branche jusqu'à ce que plus rien n'y soit décomposable - il ne reste que des atomes et des atomes niés - et qu'elle ne s'est toujours pas fermée, cette branche est saturée et ouverte. Elle ne s'est pas fermée non parce que vous vous êtes arrêté trop tôt : il n'y a plus rien à essayer.

Une branche ouverte est plus qu'un verdict d'« invalide ». Lisez les signes de ses atomes et vous obtenez une attribution : tout atome marqué T est vrai, tout atome marqué F est faux. Cette attribution rend toutes les prémisses vraies et la conclusion fausse, ce qui est exactement un contre-exemple. Les logiciens l'appellent un contre-modèle, et c'est une réponse concrète à « pourquoi non ? » plutôt qu'un refus.

L'affirmation du conséquent, p → q, q ⊨ p, en est le cas type. Son tableau laisse une branche ouverte avec p faux et q vrai - une situation où le conditionnel tient, où son conséquent tient, et où pourtant l'antécédent ne tient pas. Cette seule attribution réfute l'argument à elle seule.

8. Pourquoi elle se termine toujours

Chaque règle remplace une formule par ses propres sous-formules, et toute sous-formule est strictement plus courte que la formule dont elle vient. Aucune branche ne peut donc croître indéfiniment : chaque étape descend une échelle finie de morceaux de l'argument de départ, et l'échelle a un bas. Tôt ou tard, chaque ligne d'une branche est un atome ou la négation d'un atome, et il n'y a plus rien à faire.

C'est une garantie réelle, pas un espoir. Cela signifie que la méthode est une procédure de décision pour la logique propositionnelle : lancez-la sur n'importe quel argument et elle s'arrêtera, avec soit un arbre fermé, soit une branche ouverte, et jamais sur un haussement d'épaules. Le prouveur de ce site impose en plus un budget de nœuds, mais seulement pour éviter qu'une formule pathologique n'épuise un onglet de navigateur - les mathématiques n'ont besoin d'aucune limite de ce genre.

9. Les autres systèmes de preuve

Les tableaux sont un système de preuve parmi plusieurs, et c'est celui qui a la forme d'une réfutation : ils procèdent en écartant l'échec. La déduction naturelle fait l'inverse et construit la conclusion vers l'avant à partir des prémisses, avec des règles comme le modus ponens et la preuve conditionnelle ; elle ressemble bien davantage à la façon dont un mathématicien argumente en prose. Une preuve en déduction naturelle est en général plus courte ; la trouver demande en général plus d'invention.

Le calcul des séquents formalise le signe de conséquence lui-même et traite les affirmations de conséquence comme des objets, ce qui en fait l'outil de choix pour démontrer des énoncés sur les preuves. La résolution ramène tout à des clauses et à une seule règle, ce qui est ingrat à lire et extrêmement rapide à exécuter - c'est sur elle que reposent la plupart des démonstrateurs automatiques et des solveurs SAT.

Tous s'accordent sur les arguments propositionnels valides ; ils diffèrent par l'allure d'une preuve et par ce qui est facile à trouver. Les tableaux sont les plus accueillants pour apprendre, car une preuve qui échoue n'est pas une impasse : elle vous remet le contre-exemple.

10. S'exercer

Le plus court chemin pour apprendre la méthode est de l'exécuter. Saisissez un argument dans la calculatrice avec ⊨, ⊢ ou |= et le tableau est dessiné à côté de la table de vérité, ce qui vous permet de confronter l'arbre aux lignes. Travaillez ensuite quelques preuves sur papier avant de regarder.