§ 1Deux arbres à ne pas confondre
En logique, le mot arbre désigne couramment deux objets très différents. Les confondre rend la suite incompréhensible, alors commençons par les séparer.
L'arbre syntaxique : comment une formule est fabriquée
Une formule n'est pas une simple suite de symboles : elle a été construite, étape par étape, à partir de variables et de connecteurs. L'arbre syntaxique rend cette construction visible. À la racine se trouve la formule entière, aux feuilles les variables, et chaque nœud porte le connecteur principal de la sous-formule correspondante.
L'arbre de réfutation : comment on décide
Le second arbre ne décrit pas une formule : il décrit une recherche. On part d'un ensemble de formules et on essaie systématiquement de construire une valuation qui les rende toutes vraies. Chaque branche est une tentative ; chaque bifurcation est un choix qu'on ne sait pas trancher ; chaque croix marque une tentative qui a échoué. Si toutes les tentatives échouent, c'est qu'il n'y avait rien à trouver.
Comment lire un arbre de réfutation
Tous les arbres de ce site suivent la même convention de tracé :
| Élément | Sens |
|---|---|
| 3. | numéro de ligne, attribué dans l'ordre où la formule est écrite |
| ✓ | la formule a été décomposée ; il est inutile d'y revenir sur cette branche |
| α∧ 1 | justification : obtenue de la ligne 1 par la règle non ramifiante du ∧ |
| β∨ 2 | justification : obtenue de la ligne 2 par la règle ramifiante du ∨ |
| ✗ | branche close : elle contient une formule et sa négation ; les deux lignes fautives sont indiquées |
| ○ | branche ouverte et saturée : les littéraux qu'elle porte définissent un modèle |
Les deux arbres sont liés : la règle qu'on applique à une formule est déterminée par son connecteur principal, c'est-à-dire par la racine de son arbre syntaxique — éventuellement précédée d'une négation. C'est pourquoi le § 2 commence par la syntaxe.
§ 2Le langage : écrire
Tout ce qui suit porte d'abord sur la logique propositionnelle : le fragment où l'on ne décompose pas les énoncés au-delà de leur structure en « et », « ou », « non », « si… alors ». Le premier ordre viendra au § 14.
On se donne un ensemble infini dénombrable de variables propositionnelles p, q, r, p₁, p₂, …, cinq connecteurs ¬ (négation), ∧ (conjonction), ∨ (disjonction), → (conditionnel), ↔ (biconditionnel), et deux parenthèses.
L'ensemble FORM des formules est le plus petit ensemble de suites de symboles tel que :
- toute variable propositionnelle est une formule ;
- si A est une formule, ¬A en est une ;
- si A et B sont des formules et ∘ l'un des connecteurs ∧ ∨ → ↔, alors (A ∘ B) en est une.
Rien d'autre n'est une formule. C'est cette clause de clôture qui autorise les raisonnements par récurrence.
La lecture est unique
Une propriété discrète mais capitale : la syntaxe ci-dessus ne permet aucune ambiguïté.
Toute formule relève d'exactement un des trois cas de la définition, et de façon unique : ou bien elle est une variable, ou bien elle s'écrit ¬A pour une unique formule A, ou bien elle s'écrit (A ∘ B) pour un unique connecteur ∘ et un unique couple (A, B).
La démonstration usuelle compte les parenthèses : dans toute formule, le nombre de parenthèses ouvrantes égale celui des fermantes, et dans tout préfixe strict non vide le premier l'emporte strictement sur le second. On en déduit qu'aucun préfixe strict d'une formule n'est une formule, ce qui interdit deux découpages concurrents.
Conséquence pratique : l'arbre syntaxique d'une formule est unique, le connecteur principal est bien défini, et l'on peut définir sans ambiguïté des fonctions par récursion sur la structure — la valeur de vérité, le degré, l'ensemble des sous-formules. Sans lecture unique, la règle « on applique la règle du connecteur principal » n'aurait pas de sens. ∎
Les parenthèses qu'on s'autorise à ne pas écrire
Écrire toutes les parenthèses est illisible. On convient donc d'un ordre de priorité, du plus liant au moins liant :
| Priorité | Connecteur | Associativité | Exemple abrégé | Lecture officielle |
|---|---|---|---|---|
| 1 (le plus liant) | ¬ | — | ¬p ∧ q | (¬p) ∧ q |
| 2 | ∧ | à gauche | p ∧ q ∧ r | (p ∧ q) ∧ r |
| 3 | ∨ | à gauche | p ∧ q ∨ r | (p ∧ q) ∨ r |
| 4 | → | à droite | p → q → r | p → (q → r) |
| 5 (le moins liant) | ↔ | à droite | p → q ↔ r | (p → q) ↔ r |
Deux mesures utiles
Le degré d'une formule est le nombre d'occurrences de connecteurs qu'elle contient. Ses sous-formules sont les formules qui étiquettent les nœuds de son arbre syntaxique, elle-même comprise.
Ces deux notions serviront au § 12 : les règles de l'arbre ne produisent jamais que des sous-formules de l'ensemble de départ, ou leurs négations, et elles font toujours baisser une mesure de complexité. C'est ce qui garantit que la méthode s'arrête.
§ 3Le langage : évaluer
La syntaxe dit ce qu'on a le droit d'écrire. La sémantique dit ce que cela veut dire. Toute la méthode des arbres n'est qu'un moyen efficace de répondre à des questions sémantiques.
Une valuation est une fonction v qui attribue à chaque variable propositionnelle une valeur dans {V, F}. Par lecture unique, elle s'étend de manière unique en une fonction v̄ définie sur toutes les formules par :
- v̄(¬A) = V si et seulement si v̄(A) = F ;
- v̄(A ∧ B) = V si et seulement si v̄(A) = v̄(B) = V ;
- v̄(A ∨ B) = V si et seulement si v̄(A) = V ou v̄(B) = V ;
- v̄(A → B) = F si et seulement si v̄(A) = V et v̄(B) = F ;
- v̄(A ↔ B) = V si et seulement si v̄(A) = v̄(B).
On écrit désormais v pour v̄.
| A | B | ¬A | A ∧ B | A ∨ B | A → B | A ↔ B |
|---|---|---|---|---|---|---|
| V | V | F | V | V | V | V |
| V | F | F | F | V | F | F |
| F | V | V | F | V | V | F |
| F | F | V | F | F | V | V |
Les quatre notions à distinguer
- Une valuation v satisfait un ensemble Γ de formules si elle rend vraies toutes les formules de Γ ; on dit alors que v est un modèle de Γ.
- Γ est satisfiable s'il admet au moins un modèle, insatisfiable sinon.
- Une formule A est valide (une tautologie, noté ⊨ A) si toute valuation la rend vraie.
- A est conséquence logique de Γ, noté Γ ⊨ A, si toute valuation qui satisfait Γ rend A vraie.
- A et B sont logiquement équivalentes si A ⊨ B et B ⊨ A, c'est-à-dire si A ↔ B est valide.
Le théorème qui rend la méthode possible
Tester la validité d'un raisonnement, c'est vérifier une infinité de valuations — ou, en propositionnel, 2ⁿ d'entre elles, ce qui est fini mais vite énorme. Le théorème suivant convertit ce problème universel en un problème d'existence, beaucoup plus facile à attaquer : chercher un modèle et échouer.
Pour tout ensemble fini de formules Γ et toute formule A :
Γ ⊨ A si et seulement si Γ ∪ {¬A} est insatisfiable.
En particulier A est valide si et seulement si {¬A} est insatisfiable.
Supposons Γ ⊨ A et soit v une valuation satisfaisant Γ ∪ {¬A}. Alors v satisfait Γ, donc v(A) = V par hypothèse ; mais v(¬A) = V donne v(A) = F : contradiction. Donc Γ ∪ {¬A} n'a pas de modèle.
Réciproquement, supposons Γ ∪ {¬A} insatisfiable et soit v une valuation satisfaisant Γ. Si l'on avait v(A) = F, alors v satisferait ¬A, donc Γ ∪ {¬A}, ce qui est exclu. Donc v(A) = V, et Γ ⊨ A. ∎
Tout le reste du site consiste à répondre à une seule question : cet ensemble fini de formules est-il satisfiable ? — et à le faire mieux qu'en dressant une table de 2ⁿ lignes.
§ 4L'idée de la méthode
On ne cherche pas à démontrer la conclusion. On cherche à construire un contre-exemple, méthodiquement, et l'on regarde si la recherche échoue partout.
Une branche est une tentative de modèle
Partons d'un ensemble de formules qu'on voudrait toutes vraies. Chaque formule impose des contraintes sur la valuation cherchée, et ces contraintes sont de deux espèces seulement :
- Des exigences cumulées. Si A ∧ B doit être vraie, alors A doit être vraie et B doit être vraie. Rien à décider : on ajoute les deux à la tentative en cours.
- Des alternatives. Si A ∨ B doit être vraie, alors A est vraie ou B l'est — et l'information disponible ne dit pas laquelle. On n'a pas le droit de choisir : on explore les deux possibilités en parallèle, en dédoublant la tentative.
Une branche de l'arbre est donc une tentative de modèle en cours de construction : la liste des formules dont on a supposé, le long de ce chemin, qu'elles étaient vraies. Deux cas peuvent se produire.
Si une branche finit par contenir à la fois une formule et sa négation, la tentative est contradictoire : aucune valuation ne peut la réaliser. On la barre d'une croix — on dit qu'elle est close. Si au contraire une branche est entièrement déployée sans jamais se contredire, elle décrit un modèle, qu'il suffit de lire sur ses littéraux.
Un exemple minuscule, commenté
Testons la satisfaisabilité de p ∧ (q ∨ r), ¬q, ¬r.
Aucune branche ne survit : l'ensemble est insatisfiable. Remarquez que nous n'avons jamais eu à envisager les 8 lignes d'une table de vérité — et que nous n'avons jamais eu à deviner quoi que ce soit.
Changeons une hypothèse : remplaçons ¬r par r → r, qui n'apporte aucune information.
Et pour un raisonnement ?
Grâce au théorème du § 3, rien ne change : pour tester Γ ⊨ A, on met dans l'arbre les prémisses et la négation de la conclusion. Si tout se ferme, le raisonnement est valide ; sinon, une branche ouverte livre directement le contre-exemple qui l'invalide.
Oublier de nier la conclusion. On se retrouve alors à tester la satisfaisabilité de Γ ∪ {A}, ce qui ne répond à aucune question intéressante — et l'arbre reste obstinément ouvert.
§ 5Les neuf règles
Il y a une règle par forme de formule non littérale : cinq connecteurs, chacun sous sa forme affirmée et sous sa forme niée, plus la double négation. Chacune se lit directement dans la table des connecteurs du § 3.
La notation uniforme de Smullyan
Ces règles se regroupent naturellement en deux familles, ce qui permet d'énoncer les théorèmes une seule fois au lieu de neuf. Une formule de type α se comporte comme une conjonction ; une formule de type β se comporte comme une disjonction.
| α (non ramifiantes) | α₁ | α₂ |
|---|---|---|
| ¬¬A | A | A |
| A ∧ B | A | B |
| ¬(A ∨ B) | ¬A | ¬B |
| ¬(A → B) | A | ¬B |
| β (ramifiantes) | β₁ | β₂ |
|---|---|---|
| A ∨ B | A | B |
| ¬(A ∧ B) | ¬A | ¬B |
| A → B | ¬A | B |
Le tableau strict de Smullyan couvre ¬ ∧ ∨ →. Le biconditionnel n'y rentre pas tel quel, car chacune de ses deux alternatives comporte deux composantes à écrire, et non une. Deux traitements sont possibles, tous deux corrects : le considérer comme abréviation de (A → B) ∧ (B → A) et n'utiliser que les sept règles précédentes, ou lui donner une règle β étendue, comme nous le faisons ici. La seconde solution donne des arbres nettement plus courts.
Pourquoi ces règles sont légitimes
Une règle d'arbre n'est pas une règle d'inférence ordinaire : elle ne prétend pas conserver la vérité, mais la possibilité d'être vraie. C'est l'énoncé suivant, qui sera la clé de la correction (§ 12).
Soit S l'ensemble des formules d'une branche.
- Si α ∈ S, alors S est satisfiable si et seulement si S ∪ {α₁, α₂} l'est.
- Si β ∈ S, alors S est satisfiable si et seulement si S ∪ {β₁} ou S ∪ {β₂} l'est.
Le sens « si » est immédiat dans les deux cas puisque les ensembles augmentés contiennent S. Pour le sens « seulement si », soit v un modèle de S. Dans le cas α, v(α) = V ; or les tables du § 3 donnent, forme par forme, v(α₁) = v(α₂) = V — par exemple pour α = ¬(A → B) : A → B est fausse, donc A est vraie et B fausse, c'est-à-dire v(A) = v(¬B) = V. Donc v satisfait S ∪ {α₁, α₂}. Dans le cas β, les mêmes tables donnent v(β₁) = V ou v(β₂) = V, donc v satisfait l'un au moins des deux ensembles augmentés. ∎
Une propriété remarquable : l'analyticité
Regardez les colonnes α₁, α₂, β₁, β₂ : elles ne contiennent que des sous-formules de la formule décomposée, ou leurs négations. Jamais une formule nouvelle n'apparaît, jamais on n'a besoin d'inventer une idée ingénieuse.
C'est ce qu'on appelle la propriété de la sous-formule, et c'est ce qui fait des tableaux une méthode analytique : purement mécanique, sans invention. On le paiera au § 12 en termes de taille de preuve.
§ 6Le vocabulaire exact
Les conclusions qu'on tire d'un arbre dépendent de définitions précises. Trois mots méritent une attention particulière : close, saturée, achevé.
Un arbre de réfutation pour un ensemble fini S est un arbre dont les nœuds portent des formules, obtenu en écrivant d'abord les éléments de S les uns sous les autres, puis en appliquant un nombre fini de fois les règles du § 5. Une branche est un chemin de la racine à une feuille ; on l'identifie à l'ensemble des formules qu'elle porte.
Une branche est close si elle contient une formule A et sa négation ¬A (ou la constante ⊥). Elle est ouverte sinon. Un arbre est clos si toutes ses branches le sont.
Une branche ouverte est saturée (on dit aussi complète) si, pour chacune de ses formules :
- si c'est une formule de type α, alors α₁ et α₂ figurent aussi sur la branche ;
- si c'est une formule de type β, alors β₁ ou β₂ y figure.
Un arbre est achevé si chacune de ses branches est close ou saturée. C'est le point d'arrêt de la construction : plus aucune règle n'a d'effet.
Une branche ouverte n'autorise aucune conclusion tant qu'elle n'est pas saturée : il reste peut-être une formule dont la décomposition la fermerait. Seule une branche ouverte et saturée prouve la satisfaisabilité.
Ce qu'on peut dire, et quand
| État de l'arbre | Sur l'ensemble de départ S | Si S = Γ ∪ {¬A} |
|---|---|---|
| clos | S est insatisfiable | Γ ⊨ A : le raisonnement est valide |
| achevé, au moins une branche ouverte | S est satisfiable ; le modèle se lit sur la branche | Γ ⊭ A ; la branche donne un contre-exemple |
| ni clos ni achevé | on ne sait encore rien : il faut continuer | idem |
§ 7La méthode pas à pas
La procédure complète tient en huit lignes. Tout le reste est affaire d'ordre — un ordre qui ne change jamais le verdict, mais qui peut diviser par dix la taille de ce que vous écrivez.
La procédure
- Écrire les prémisses, puis la négation de la conclusion, une par ligne, numérotées.
- S'il existe sur une branche ouverte une formule non littérale non encore décomposée, en choisir une. Préférer une formule de type α. Sinon, l'arbre est achevé : aller à 7.
- Appliquer sa règle au bas de chaque branche ouverte qui passe par cette formule.
- Cocher la formule décomposée sur ces branches.
- Fermer par ✗ toute branche contenant désormais une formule et sa négation.
- Revenir à 2.
- Si toutes les branches sont closes : l'ensemble est insatisfiable, le raisonnement est valide.
- Sinon, choisir une branche ouverte : ses littéraux définissent un modèle. Le vérifier.
Quand on décompose une formule écrite avant une bifurcation, le résultat doit être recopié au bas de toutes les branches ouvertes issues de cette bifurcation, pas seulement de celle où l'on travaille. Les arbres affichés ici le font automatiquement : c'est pourquoi une même formule peut apparaître deux fois avec deux numéros de ligne différents.
Quatre habitudes qui font gagner du temps
- Les α avant les β. Un travail effectué avant une bifurcation n'est fait qu'une fois ; après, il doit être refait dans chaque branche. C'est de loin la règle la plus rentable.
- Les β qui ferment d'abord. Si une disjonction a un membre dont la négation est déjà sur la branche, la décomposer ferme immédiatement une des deux branches nouvelles.
- Ne jamais décomposer un littéral. Il n'y a rien à en tirer : c'est déjà l'information finale.
- Abandonner une branche close. Elle est morte ; y écrire quoi que ce soit est du travail perdu.
La différence, en images
Même problème, deux stratégies. On teste la satisfaisabilité de p ∨ q, p ∨ r, ¬p ∧ ¬q ∧ ¬r.
Le verdict est identique — c'est la propriété de confluence du § 12 — mais l'arbre a plus que doublé. Sur des formules de taille réelle, l'écart devient rédhibitoire.
§ 8Laboratoire
Tapez un raisonnement et regardez l'arbre se construire. Le même problème est présenté de trois façons : l'arbre, la structure des formules, et la table de vérité qui sert d'étalon.
La case « ne fermer que sur un couple de littéraux » mérite un essai. La fermeture sur des formules composées est parfaitement correcte — si A et ¬A sont sur une branche, aucune valuation ne la satisfait, quelle que soit la complexité de A — et elle raccourcit souvent beaucoup l'arbre. Beaucoup de manuels ne l'autorisent pourtant pas, afin de garder une définition plus simple. Les deux conventions donnent le même verdict.
§ 9Lire le résultat
Un arbre achevé répond toujours, et sa réponse est de deux natures très différentes : une impossibilité, ou un objet concret qu'on peut vérifier soi-même.
Arbre clos : une démonstration
Toutes les branches closes signifient : toute tentative de modèle a échoué, donc il n'y en a pas. Selon ce qu'on avait mis à la racine, on conclut :
- on y avait mis ¬A seule → A est une tautologie ;
- on y avait mis Γ ∪ {¬A} → Γ ⊨ A ;
- on y avait mis un ensemble Γ → Γ est contradictoire ;
- on y avait mis {A, ¬B} et {¬A, B} (deux arbres) → A et B sont équivalentes.
L'arbre lui-même est la démonstration : il se relit ligne à ligne, chaque justification étant vérifiable mécaniquement.
Branche ouverte saturée : un contre-exemple
On lit la valuation sur les littéraux de la branche : si p y figure, poser v(p) = V ; si ¬p y figure, poser v(p) = F. La branche étant ouverte, ces deux cas s'excluent, donc v est bien définie.
La vérification est indépendante de l'arbre et coûte trente secondes : on calcule la valeur de chaque prémisse et de la conclusion sous la valuation trouvée. Si toutes les prémisses valent V et la conclusion F, le contre-exemple est bon — et il l'est quoi qu'on ait pu se tromper en construisant l'arbre. C'est le grand avantage d'un verdict négatif : il est auto-certifiant. Le laboratoire du § 8 fait cette vérification à chaque fois.
Un arbre peut avoir plusieurs branches ouvertes
Elles donnent des contre-exemples différents, parfois redondants. Un seul suffit à réfuter le raisonnement. En revanche, si l'on cherche tous les modèles d'un ensemble, il faut les collecter sur toutes les branches ouvertes, sans oublier les variables laissées libres.
§ 10Exemples travaillés
Cinq arbres commentés, du plus simple au plus retors. Chacun peut être rouvert dans le laboratoire pour être reconstruit pas à pas.
1. Le modus tollens
Reconstruire cet arbre pas à pas
2. Un raisonnement invalide : l'affirmation du conséquent
Reconstruire cet arbre pas à pas
3. La loi de Peirce
Reconstruire cet arbre pas à pas
4. Une équivalence : la loi de De Morgan
Reconstruire cet arbre pas à pas
5. Un ensemble satisfiable, avec plusieurs modèles
§ 11Les pièges
Huit erreurs qui expliquent la quasi-totalité des arbres faux rendus en examen.
La méthode teste une insatisfaisabilité. Sans la négation de la conclusion, on teste autre chose.
Dans ¬(p ∨ q), le connecteur principal est la négation, et la règle est α¬∨ : on écrit ¬p et ¬q sur la même branche. Appliquer la règle du ∨ et ramifier en p et q est une faute grossière — et donne un verdict faux. Repérez toujours le connecteur principal, au besoin en dessinant l'arbre syntaxique.
Le moyen mnémotechnique : on ramifie quand il y a un choix à faire. « Et » n'offre aucun choix, « ou » en offre un. Et tout se renverse sous une négation.
Une formule située au-dessus d'une bifurcation appartient à toutes les branches qui passent par elle. Sa décomposition doit être écrite au bas de chacune.
p → q et ¬(¬q → ¬p) sont contradictoires, mais ne ferment rien telles quelles. La règle de fermeture demande A et ¬A, au caractère près.
Tant qu'il reste une formule cochable, la branche peut encore mourir. Voir le § 6.
Une valuation attribue des valeurs à des variables. On la lit donc sur les littéraux de la branche, pas sur p → q qui s'y trouverait encore.
Deux arbres corrects du même problème peuvent avoir des tailles très différentes et donnent pourtant toujours le même verdict. Un arbre inutilement long n'est pas faux — seulement fatigant.
§ 12Pourquoi la méthode est correcte
Deux choses restent à démontrer : que la construction s'arrête toujours, et qu'un arbre clos ne ment pas. Les deux démonstrations sont courtes et entièrement vérifiables.
La construction s'arrête toujours
Pour tout ensemble fini S de formules propositionnelles, toute construction d'arbre à partir de S se termine après un nombre fini d'étapes, et l'arbre obtenu est fini.
Attribuons à chaque formule le poids
w(F) = 2 × (nombre de connecteurs binaires de F) + (nombre de négations de F).
Ce poids est un entier positif, et l'on a immédiatement w(¬F) = w(F) + 1 et w(A ∘ B) = w(A) + w(B) + 2 pour ∘ binaire.
Associons à chaque branche la somme des poids de ses formules non encore décomposées. Le tableau ci-dessous vérifie, règle par règle, que cette somme diminue strictement à chaque application : on retire la formule décomposée et l'on ajoute ce que la règle produit.
| Règle | poids retiré | poids ajouté (par branche) | variation |
|---|---|---|---|
| α ¬¬A | w(A)+2 | w(A) | −2 |
| α A ∧ B | w(A)+w(B)+2 | w(A)+w(B) | −2 |
| α ¬(A ∨ B) | w(A)+w(B)+3 | w(A)+w(B)+2 | −1 |
| α ¬(A → B) | w(A)+w(B)+3 | w(A)+w(B)+1 | −2 |
| β A ∨ B | w(A)+w(B)+2 | w(A) ou w(B) | ≤ −2 |
| β ¬(A ∧ B) | w(A)+w(B)+3 | w(A)+1 ou w(B)+1 | ≤ −2 |
| β A → B | w(A)+w(B)+2 | w(A)+1 ou w(B) | ≤ −1 |
| β A ↔ B | w(A)+w(B)+2 | w(A)+w(B) | −2 |
| β ¬(A ↔ B) | w(A)+w(B)+3 | w(A)+w(B)+1 | −2 |
Chaque branche est donc finie ; comme l'arbre est binaire, il est fini par le lemme de König — ou, plus simplement ici, parce que le nombre total d'applications de règles est borné par le poids initial. ∎
Une seconde démonstration, plus qualitative, mérite d'être connue : par la propriété de la sous-formule (§ 5), toute formule apparaissant dans l'arbre est une sous-formule d'un élément de S, ou la négation d'une telle sous-formule. Cet ensemble est fini ; aucune branche ne décompose deux fois la même formule ; donc les branches sont de longueur bornée.
Un arbre clos ne ment pas
Si un arbre de réfutation pour S est clos, alors S est insatisfiable.
Appelons une branche satisfiable si l'ensemble des formules qu'elle porte l'est. Montrons par récurrence sur le nombre d'applications de règles la propriété :
si S est satisfiable, alors l'arbre construit contient à chaque étape au moins une branche satisfiable.
Initialisation. L'arbre initial a une seule branche, qui porte exactement S : elle est satisfiable par hypothèse.
Hérédité. Soit b une branche satisfiable à une étape donnée. Si la règle appliquée ne concerne pas b, la branche subsiste inchangée. Sinon, le lemme de préservation (§ 5) s'applique : dans le cas α, la branche prolongée reste satisfiable ; dans le cas β, l'une au moins des deux branches filles l'est. Dans tous les cas il reste une branche satisfiable.
Conclusion. Une branche close contient A et ¬A : aucune valuation ne peut la satisfaire, donc une branche close n'est jamais satisfiable. Si toutes les branches sont closes, aucune n'est satisfiable ; par contraposée de la propriété ci-dessus, S est insatisfiable. ∎
Si votre arbre est clos et que chaque ligne est correctement justifiée, alors le raisonnement est valide — indépendamment de toute intuition, et sans qu'il soit besoin de faire confiance à qui que ce soit. La vérification d'un arbre est purement mécanique : on contrôle ligne par ligne que la règle invoquée est bien celle du connecteur principal de la ligne source, et que les couples de fermeture sont bien complémentaires.
§ 13Pourquoi elle est complète
La correction dit que la méthode ne se trompe pas. La complétude dit qu'elle ne rate rien : si l'ensemble de départ est insatisfiable, l'arbre se fermera. La démonstration passe par un détour élégant, dû à Hintikka.
Un ensemble H de formules est un ensemble de Hintikka si :
- pour toute variable p, H ne contient pas à la fois p et ¬p ;
- si une formule de type α appartient à H, alors α₁ ∈ H et α₂ ∈ H ;
- si une formule de type β appartient à H, alors β₁ ∈ H ou β₂ ∈ H.
Tout ensemble de Hintikka est satisfiable.
Soit H un ensemble de Hintikka. Définissons la valuation v par : v(p) = V si p ∈ H, et v(p) = F sinon. La condition 1 garantit la cohérence de ce choix : si ¬p ∈ H, alors p ∉ H, donc v(p) = F.
Montrons par récurrence sur le poids w (§ 12) que toute formule de H est vraie sous v.
- Poids 0 : la formule est une variable p, et v(p) = V par construction.
- Littéral négatif ¬p : alors p ∉ H, donc v(p) = F et v(¬p) = V.
- Formule de type α : par la condition 2, α₁ et α₂ sont dans H, et leurs poids sont strictement inférieurs (tableau du § 12). Par hypothèse de récurrence elles sont vraies ; or par définition de la famille α, α est vraie dès que α₁ et α₂ le sont.
- Formule de type β : par la condition 3, l'une des deux composantes est dans H, de poids strictement inférieur, donc vraie par hypothèse de récurrence ; et β est vraie dès que l'une de ses composantes l'est.
Donc v satisfait H. ∎
Si S est insatisfiable, alors tout arbre achevé pour S est clos.
Par contraposée. Supposons qu'un arbre achevé pour S possède une branche ouverte b. Cette branche est nécessairement saturée, puisque l'arbre est achevé. L'ensemble des formules de b vérifie alors les trois conditions de la définition : la condition 1 parce que la branche est ouverte, les conditions 2 et 3 parce qu'elle est saturée. C'est donc un ensemble de Hintikka, et il est satisfiable par le lemme. Comme S est inclus dans b, tout modèle de b est un modèle de S : S est satisfiable. ∎
L'ordre des règles ne change pas le verdict
Deux arbres achevés pour le même ensemble S sont soit tous deux clos, soit tous deux ouverts, quelles que soient les stratégies employées pour les construire.
En effet, « être clos » équivaut, par correction et complétude, à « S est insatisfiable », propriété qui ne dépend que de S. ∎
C'est ce qui autorise les heuristiques du § 7 : on peut choisir l'ordre le plus économique sans jamais risquer de fausser le résultat. On dit que le non-déterminisme de la méthode est « sans conséquence ».
Décidabilité et coût
Terminaison, correction et complétude réunies donnent un algorithme de décision pour la validité propositionnelle : construire un arbre achevé et regarder s'il est clos. Cet algorithme termine toujours et répond toujours juste.
Reste la question du coût. Elle n'est pas anecdotique :
- Le problème de la satisfaisabilité propositionnelle est NP-complet (Cook 1971, Levin 1973) ; la validité est donc coNP-complète. Il n'existe pas, sauf si NP = coNP, de système de preuve donnant à toute tautologie une preuve de taille polynomiale. Aucune méthode n'échappera à l'explosion, et les arbres non plus.
- Les tableaux analytiques sont même, en tant que système de preuve, relativement faibles. D'Agostino (1992) a exhibé des familles de formules pour lesquelles ils sont exponentiellement plus coûteux que la simple table de vérité ; Urquhart (1995) a établi une séparation exponentielle entre les systèmes de Gentzen sans coupure — dont les tableaux sont proches parents — et la résolution.
- La cause est précisément ce qui fait leur charme pédagogique : l'absence de coupure. Une preuve analytique n'introduit jamais de lemme intermédiaire ; elle ne peut donc pas factoriser un raisonnement répétitif.
En pratique, la méthode reste excellente sur les formules de taille humaine — celles qu'on rencontre en cours, en philosophie ou en spécification — et c'est pour cela qu'elle s'enseigne.
§ 14Le premier ordre
On passe des propositions aux prédicats : ∀x (Homme(x) → Mortel(x)). La méthode survit presque intacte — deux règles s'ajoutent — mais elle perd la terminaison, et c'est une perte de principe, non un défaut de la méthode.
Ce qui change dans le langage
Les formules atomiques ne sont plus des variables mais des énoncés P(t₁, …, tₙ) où les tᵢ sont des termes : variables, constantes, ou applications de symboles de fonction. Deux quantificateurs s'ajoutent aux connecteurs. Une valuation est remplacée par une structure : un domaine non vide, plus une interprétation de chaque symbole.
Les définitions de satisfaisabilité, de validité et de conséquence logique se transposent mot pour mot, et le théorème de réduction du § 3 reste vrai à l'identique. Les neuf règles propositionnelles s'appliquent sans modification.
Les deux règles nouvelles
| Type γ — universelles | on écrit | condition |
|---|---|---|
| ∀x A(x) | A(t) | t est un terme clos quelconque du langage de la branche. La formule n'est jamais épuisée : on peut y revenir avec un autre terme. |
| ¬∃x A(x) | ¬A(t) |
| Type δ — existentielles | on écrit | condition |
|---|---|---|
| ∃x A(x) | A(c) | c est une constante nouvelle, n'apparaissant nulle part sur la branche. La formule est alors épuisée. |
| ¬∀x A(x) | ¬A(c) |
Si la branche ne contient aucun terme clos au moment d'appliquer une règle γ, on en introduit un : les structures ont, par convention, un domaine non vide.
Un premier arbre
Pourquoi la constante de δ doit être nouvelle
C'est la condition la plus importante du premier ordre, et celle qu'on oublie le plus souvent. Considérons {∃x P(x), ∃x ¬P(x)} : cet ensemble est manifestement satisfiable — prenez un domaine à deux éléments dont l'un vérifie P et l'autre non.
∃x P(x) affirme qu'un objet vérifie P, sans dire lequel. Lui donner un nom déjà utilisé, c'est ajouter l'information — nullement contenue dans l'hypothèse — que cet objet est précisément celui qu'on a déjà nommé. Une constante neuve est un nom arbitraire, qui n'engage à rien d'autre.
Pourquoi la règle γ n'est jamais épuisée
∀x A(x) vaut pour tous les objets : chaque instance A(t) en est une conséquence légitime. Mais on ne sait pas d'avance quelle instance fera fermer la branche. Il faut donc pouvoir y revenir.
Ce qu'on perd : la terminaison
La règle γ peut engendrer indéfiniment de nouveaux termes, et la règle δ de nouvelles constantes, dont γ se ressert aussitôt. Certaines branches sont infinies.
Un arbre clos pour S garantit que S est insatisfiable. Réciproquement, si S est insatisfiable, toute construction menée selon une stratégie équitable produit un arbre clos en un nombre fini d'étapes.
Une stratégie est équitable si toute application de règle possible finit par être effectuée : aucune formule n'est indéfiniment ignorée, et chaque formule γ est instanciée, tôt ou tard, sur chaque terme clos apparu sur la branche. Une mise en œuvre classique traite les formules en attente dans une file, et réinsère les formules γ après usage.
On raisonne de nouveau par contraposée. Si une construction équitable ne se ferme pas, l'arbre obtenu est infini ; comme il est à branchement fini, le lemme de König fournit une branche infinie b. L'équité de la stratégie garantit que l'ensemble des formules de b satisfait les conditions de Hintikka, étendues aux quantificateurs : si ∀x A(x) ∈ b alors A(t) ∈ b pour tout terme clos t de la branche ; si ∃x A(x) ∈ b alors A(c) ∈ b pour une certaine constante. La version premier ordre du lemme de Hintikka construit alors un modèle dont le domaine est l'ensemble des termes clos eux-mêmes — un modèle de Herbrand. Donc S est satisfiable. ∎
Cette démonstration donne davantage que la complétude. Le modèle construit a pour domaine un ensemble de termes, donc dénombrable : on retrouve le théorème de Löwenheim–Skolem. Et comme un arbre clos n'utilise qu'un nombre fini de formules de départ, on obtient le théorème de compacité : si tout sous-ensemble fini de Γ est satisfiable, Γ l'est. C'est aussi, sous une autre forme, le théorème de complétude de Gödel (1930).
La méthode des arbres au premier ordre est une procédure de semi-décision. Si la formule est valide, elle le prouve en temps fini. Si elle ne l'est pas, la construction peut se terminer sur une branche ouverte saturée — et l'on a un contre-modèle — ou bien ne jamais s'arrêter, sans qu'on puisse savoir laquelle des deux situations on est en train de vivre.
§ 15Ouvertures
La méthode des arbres n'est pas une curiosité pédagogique : c'est le socle d'une famille entière de procédures de preuve automatique.
Tableaux à variables libres
Le point faible du premier ordre est le choix du terme dans la règle γ : instancier au hasard fait exploser l'arbre. L'idée, due notamment à Fitting, consiste à instancier avec une variable libre laissée indéterminée, puis à laisser l'unification découvrir après coup la substitution qui ferme la branche. C'est ce que font les prouveurs réels.
Égalité, et au-delà
Traiter = demande des règles supplémentaires (réflexivité, remplacement), ou un mécanisme dédié comme la paramodulation. Le même canevas s'étend aux logiques modales par les tableaux préfixés, où chaque formule est étiquetée par le monde possible où on l'évalue, ainsi qu'aux logiques temporelles, intuitionnistes ou de description — celles qui sous-tendent les ontologies du web sémantique.
Cousins et voisins
- Le calcul des séquents (Gentzen, 1935) : même contenu, présentation différente. La propriété de la sous-formule y porte le nom de théorème d'élimination des coupures.
- La résolution (Robinson, 1965) : travaille sur des clauses plutôt que sur des formules quelconques, et se prête mieux à l'implantation.
- DPLL (Davis, Putnam, Logemann, Loveland, 1962) : c'est essentiellement un tableau restreint aux clauses, augmenté de la propagation unitaire. Les solveurs SAT modernes y ajoutent l'apprentissage de clauses, qui les fait sortir du cadre purement analytique — et c'est précisément pour cela qu'ils sont si efficaces.
§ 16Exercices
Faites-les d'abord sur papier. Chaque lien ouvre la correction dans le laboratoire, où vous pourrez la faire défiler étape par étape.
Série A — reconnaître la règle
Pour chaque formule, dire s'il s'agit d'un littéral, d'une formule de type α ou de type β, et écrire ce que la règle produit.
- ¬(p → q)
- ¬¬(p ∨ q)
- ¬(p ∧ ¬q)
- (p → q) → r
- ¬(p ↔ ¬q)
Série B — tautologie ou non ?
- (p → q) → ((q → r) → (p → r))
- (p ∧ q) ∨ (¬p ∧ ¬q)
- ((p ∨ q) ∧ ¬p) → q
- (p → q) ↔ (¬q → ¬p)
- (p → q) ↔ (q → p)
Série C — raisonnements
- Disjonction des cas : de p ∨ q, p → r et q → r, conclure r.
- Dilemme destructif.
- De ¬(p ∧ q) et p, conclure ¬q.
- Transitivité du biconditionnel.
- Une variante du modus tollens.
Série D — cohérence et modèles
Ces ensembles sont-ils satisfiables ? Si oui, donner tous leurs modèles.
Série E — premier ordre, sur papier
- Montrer que ∀x (P(x) → Q(x)) et ∃x P(x) entraînent ∃x Q(x). Combien d'applications de γ et de δ, et dans quel ordre ?
- Montrer que ∃x ∀y R(x, y) → ∀y ∃x R(x, y) est valide, et que la réciproque ne l'est pas. Quel rôle joue exactement la condition de fraîcheur ?
- Construire les cinq premières lignes de l'arbre de {∀x ∃y R(x,y), ∀x ¬R(x,x)} et expliquer pourquoi il ne se fermera jamais.
Quiz de vérification
Douze questions sur les points où l'on se trompe le plus. Chaque réponse est commentée.
Aucune réponse donnée pour l'instant.
§ 17Aide-mémoire et glossaire
À garder sous les yeux
Règles α — on écrit à la suite
- ¬¬A → A
- A ∧ B → A, B
- ¬(A ∨ B) → ¬A, ¬B
- ¬(A → B) → A, ¬B
Règles γ — réutilisables
- ∀x A(x) → A(t), t quelconque
- ¬∃x A(x) → ¬A(t), t quelconque
Règles β — on ramifie
- A ∨ B → A | B
- ¬(A ∧ B) → ¬A | ¬B
- A → B → ¬A | B
- A ↔ B → A, B | ¬A, ¬B
- ¬(A ↔ B) → A, ¬B | ¬A, B
Règles δ — constante neuve
- ∃x A(x) → A(c), c neuve
- ¬∀x A(x) → ¬A(c), c neuve
Les trois réflexes
- Nier la conclusion avant de commencer.
- Épuiser les α avant de toucher aux β.
- Ne conclure à la satisfaisabilité que sur une branche ouverte et saturée.
Cette page s'imprime : seuls le texte et les arbres sont conservés.
Glossaire
- Arbre achevé
- Arbre dont chaque branche est close ou saturée : plus aucune règle n'a d'effet.
- Branche
- Chemin de la racine à une feuille, identifié à l'ensemble des formules qu'il porte. Une tentative de modèle.
- Branche close
- Branche contenant une formule et sa négation. Aucune valuation ne la satisfait.
- Branche saturée
- Branche ouverte où toute formule de type α a ses deux composantes présentes, et toute formule de type β au moins une. Un ensemble de Hintikka.
- Confluence
- Propriété selon laquelle le verdict d'un arbre achevé ne dépend pas de l'ordre d'application des règles.
- Correction
- Un arbre clos garantit l'insatisfaisabilité de l'ensemble de départ. La méthode ne prouve rien de faux.
- Complétude
- Tout ensemble insatisfiable a un arbre clos. La méthode ne rate rien de vrai.
- Ensemble de Hintikka
- Ensemble de formules cohérent au niveau des variables et clos par les composantes α et β. Tout ensemble de Hintikka est satisfiable : c'est le cœur de la démonstration de complétude.
- Littéral
- Variable propositionnelle ou négation d'une variable. Ne se décompose pas.
- Modèle
- Valuation (ou structure, au premier ordre) rendant vraies toutes les formules considérées.
- Propriété de la sous-formule
- Toute formule apparaissant dans un arbre est une sous-formule de l'ensemble de départ, ou la négation d'une telle sous-formule. C'est ce qui rend la méthode mécanique — et ce qui la rend coûteuse.
- Règle α / β / γ / δ
- Classification de Smullyan : conjonctive (non ramifiante), disjonctive (ramifiante), universelle (réutilisable), existentielle (à constante neuve).
- Semi-décision
- Procédure qui répond « oui » en temps fini quand la réponse est oui, mais peut ne jamais s'arrêter quand la réponse est non. Statut de la méthode au premier ordre.
Pour aller plus loin
- E. W. Beth, « Semantic entailment and formal derivability », 1955 — l'article fondateur des tableaux sémantiques.
- J. Hintikka, « Form and content in quantification theory », 1955 — les model sets, découverts indépendamment, qui portent aujourd'hui son nom.
- R. M. Smullyan, First-Order Logic, Springer, 1968 — la présentation unifiée α/β/γ/δ suivie ici. Court, dense, magnifique.
- R. Jeffrey, Formal Logic: Its Scope and Limits, 1967 — c'est ce livre qui a popularisé les arbres dans l'enseignement, sous le nom de truth trees.
- M. Fitting, First-Order Logic and Automated Theorem Proving, 2ᵉ éd., Springer, 1996 — la référence pour les tableaux à variables libres et l'unification.
- M. D'Agostino, D. Gabbay, R. Hähnle, J. Posegga (dir.), Handbook of Tableau Methods, Kluwer, 1999 — l'état de l'art, toutes logiques confondues.
- R. Cori et D. Lascar, Logique mathématique, tomes 1 et 2, Dunod — le cours français standard, pour la sémantique et la complétude.
- G. Gentzen, « Untersuchungen über das logische Schließen », 1935 — le calcul des séquents et l'élimination des coupures, ancêtre commun.