Logique des propositions

Les arbres de Quine

Une méthode pour décider si une formule est une tautologie, une contradiction ou une formule contingente : on remplace une variable par V puis par F, on simplifie aussitôt, et l’on recommence. Le calcul dessine un arbre dont les feuilles donnent le verdict, souvent bien plus vite qu’une table de vérité.

L’arbre de Quine de la transitivité de l’implication, ((p → q) ∧ (q → r)) → (p → r). Quatre feuilles suffisent là où la table de vérité demande huit lignes ; toutes valent V, la formule est une tautologie. Chaque nœud montre la formule obtenue après substitution, puis (⇓) sa forme réduite ; dépliez « réduction » pour voir les règles appliquées.

1.Pourquoi une autre méthode que la table de vérité ?

Pour savoir si une formule de la logique des propositions est vraie dans toutes les situations, on apprend d’abord la table de vérité : on énumère toutes les façons d’attribuer V ou F aux variables, puis on calcule la valeur de la formule ligne par ligne. La méthode est infaillible mais coûteuse : avec n variables, il y a 2n lignes, et chaque ligne exige d’évaluer chaque sous-formule. Trois variables donnent 8 lignes, cinq en donnent 32, dix en donnent 1024.

Beaucoup de ces lignes sont pourtant « jouées d’avance ». Dans la formule (p ∧ q) → p, dès que p vaut V, le conséquent de l’implication est vrai et l’implication tout entière est vraie, quelle que soit la valeur de q : deux lignes de la table sont réglées d’un coup. La méthode que Willard Van Orman Quine présente en 1950 dans Methods of Logic (chapitre « Truth-Value Analysis », analyse par valeurs de vérité) tire parti de cette observation :

  1. on choisit une variable, on la remplace partout par la constante V, et l’on simplifie immédiatement la formule obtenue à l’aide de règles élémentaires (par exemple V ∧ A se réduit à A, et A → V se réduit à V) ;
  2. on fait de même en remplaçant la variable par F ;
  3. on recommence sur chacune des formules obtenues tant qu’elle contient encore une variable.

Le calcul se dessine naturellement comme un arbre binaire : chaque nœud porte une formule, chaque branche porte une substitution (p := V ou p := F), et chaque feuille porte une constante, V ou F. C’est l’arbre de Quine de la formule. Sa lecture est immédiate : si toutes les feuilles valent V, la formule est une tautologie ; si toutes valent F, c’est une contradiction ; s’il y a des feuilles des deux sortes, la formule est contingente, et chaque feuille indique en outre une valuation qui rend la formule vraie ou fausse.

Cette page développe la méthode dans l’ordre suivant : les rappels indispensables (§2), la substitution et le catalogue des règles de réduction avec leur justification (§3), l’algorithme et la construction de l’arbre (§4), des exemples entièrement commentés (§5), la démonstration rigoureuse de la correction de la méthode (§6), les stratégies qui rendent les arbres petits et les erreurs à éviter (§7), la comparaison de coût avec la table de vérité (§8), les extensions et les méthodes voisines à ne pas confondre (§9), un outil interactif qui construit l’arbre de n’importe quelle formule en montrant chaque règle appliquée (§10), et des exercices corrigés (§11).

2.Rappels : syntaxe, sémantique, classification

La méthode de Quine est purement sémantique : elle repose sur la signification des connecteurs, c’est-à-dire sur leurs tables de vérité. Il est donc indispensable de fixer avec précision ce qu’est une formule et comment on la « calcule ».

2.1 Syntaxe

Définition 2.1 (alphabet). Le langage de la logique des propositions utilisé ici comprend :

  • des variables propositionnelles (ou lettres de proposition), notées p, q, r, s, … ;
  • deux constantes, V (le vrai) et F (le faux) ;
  • cinq connecteurs : ¬ (négation, unaire), ∧ (conjonction), ∨ (disjonction), → (implication, ou conditionnel), ↔ (équivalence, ou biconditionnel) ;
  • les parenthèses ( et ).

Définition 2.2 (formules). L’ensemble des formules est le plus petit ensemble d’expressions tel que :

  1. toute variable propositionnelle est une formule ; les constantes V et F sont des formules (on parle de formules atomiques) ;
  2. si A est une formule, alors ¬A est une formule ;
  3. si A et B sont des formules, alors (A ∧ B), (A ∨ B), (A → B) et (A ↔ B) sont des formules.

Les lettres A, B, C, … ne font pas partie du langage : ce sont des métavariables, des noms que nous utilisons pour parler de formules quelconques. Une sous-formule de A est une formule qui apparaît dans la construction de A ; A est sous-formule d’elle-même.

Conventions d’écriture. Comme il est d’usage, on omet les parenthèses extérieures : on écrit (p ∧ q) → p pour ((p ∧ q) → p). Sur cette page, toute autre sous-formule binaire reste parenthésée, ce qui évite toute ambiguïté. L’outil interactif (§10) accepte aussi une écriture allégée fondée sur les priorités décroissantes ¬, ∧, ∨, →, ↔, l’implication associant à droite (p → q → r se lit p → (q → r)) et les autres connecteurs binaires à gauche ; en cas de doute, mettez des parenthèses.

Les constantes sont notées V et F dans la tradition francophone ; d’autres textes écrivent ⊤ et ⊥, 1 et 0, ou T et ⊥ (c’est la notation de Quine). Cela ne change rien à la méthode.

2.2 Sémantique

Définition 2.3 (valuation). Une valuation (ou interprétation, ou distribution de valeurs de vérité) est une fonction v qui associe à chaque variable propositionnelle une valeur de vérité, vrai ou faux, que nous noterons encore V et F. Une valuation s’étend de manière unique à toutes les formules, en une fonction notée v̄ (« v barre »), par les clauses suivantes :

  • v̄(p) = v(p) pour toute variable p ; v̄(V) = V et v̄(F) = F ;
  • v̄(¬A), v̄(A ∧ B), v̄(A ∨ B), v̄(A → B) et v̄(A ↔ B) sont déterminées par v̄(A) et v̄(B) selon les tables de vérité ci-dessous.
AB¬AA ∧ BA ∨ BA → BA ↔ B
VVFVVVV
VFFFVFF
FVVFVVF
FFVFFVV

Deux points de ces tables reviennent sans cesse dans la méthode de Quine et méritent d’être mémorisés : l’implication A → B n’est fausse que dans un seul cas, antécédent vrai et conséquent faux ; l’équivalence A ↔ B est vraie exactement quand A et B ont la même valeur.

Remarque sur la notation V / F. Le même symbole V désigne ici une constante du langage (un signe que l’on peut écrire dans une formule) et une valeur de vérité (un objet sémantique). Cette double lecture, universelle dans les présentations de la méthode de Quine, est sans danger parce que la constante V est interprétée par la valeur vrai dans toute valuation, et de même pour F. Lorsque la distinction importe, nous dirons « la constante V » ou « la valeur V ».

2.3 Classification des formules

Définition 2.4. Soit A une formule.

  • A est une tautologie (ou est valide) si v̄(A) = V pour toute valuation v ; on note ⊨ A.
  • A est une contradiction (ou antilogie, ou formule insatisfaisable) si v̄(A) = F pour toute valuation v.
  • A est contingente (ou neutre, ou indéterminée) si elle n’est ni une tautologie ni une contradiction : il existe une valuation qui la rend vraie et une autre qui la rend fausse.
  • A est satisfaisable s’il existe au moins une valuation v telle que v̄(A) = V ; une telle valuation est un modèle de A. Une valuation qui rend A fausse est un contre-modèle de A.

Toute formule est dans exactement une des trois classes : tautologie, contradiction, contingente. Les formules satisfaisables sont les tautologies et les formules contingentes.

Deux notions dérivées serviront au §9 : deux formules A et B sont logiquement équivalentes, noté A ≡ B, si v̄(A) = v̄(B) pour toute valuation v ; et B est conséquence logique des formules A1, …, Ak, noté A1, …, Ak ⊨ B, si toute valuation qui rend vraies toutes les Ai rend aussi B vraie. On vérifie immédiatement à partir des tables que A ≡ B si et seulement si A ↔ B est une tautologie, et que A1, …, Ak ⊨ B si et seulement si (A1 ∧ … ∧ Ak) → B est une tautologie. Enfin, A est une contradiction si et seulement si ¬A est une tautologie.

Puisque la valeur v̄(A) ne dépend que des valeurs que v attribue aux variables qui apparaissent effectivement dans A (cela se démontre par une induction immédiate sur la construction de A), il suffit, pour classer une formule à n variables, d’examiner les 2n attributions possibles à ces n variables. C’est ce que fait la table de vérité, et c’est cet examen que la méthode de Quine organise plus astucieusement.

3.Substitution et règles de réduction

La méthode repose sur deux opérations syntaxiques dont nous démontrerons au §6 qu’elles respectent la sémantique : la substitution d’une constante à une variable, et la réduction d’une formule contenant des constantes.

3.1 Substitution

Définition 3.1. Soient A une formule, p une variable et c l’une des constantes V ou F. On note A[p := c] la formule obtenue en remplaçant toutes les occurrences de p dans A par c. Formellement, par induction sur A :

  • p[p := c] = c ; q[p := c] = q si q est une variable différente de p ; V[p := c] = V et F[p := c] = F ;
  • (¬A)[p := c] = ¬(A[p := c]) ;
  • (A ∘ B)[p := c] = (A[p := c] ∘ B[p := c]) pour chaque connecteur binaire ∘.

Exemple. Si A est (p → q) ∧ (p ∧ ¬q), alors A[p := V] est (V → q) ∧ (V ∧ ¬q) et A[q := F] est (p → F) ∧ (p ∧ ¬F). La variable substituée ne figure plus dans le résultat : c’est ce qui garantit que la méthode termine.

3.2 Le catalogue des règles de réduction

Une fois une constante introduite, la formule peut être simplifiée grâce aux identités ci-dessous. Chaque ligne se lit « la sous-formule de gauche peut être remplacée par la formule de droite ». La lettre A désigne une sous-formule quelconque. La dernière colonne donne la vérification : on y calcule, d’après les tables du §2.2, la valeur du membre de gauche lorsque A vaut V puis F, et l’on constate qu’elle coïncide avec celle du membre de droite ; les deux membres sont donc logiquement équivalents (lemme 6.2). La numérotation est celle de cette page ; elle n’a rien de canonique.

N°Sous-formuleRemplacée parVérification (cas A = V ; cas A = F)
Négation
N1¬V⇒F¬V = F (table de ¬)
N2¬F⇒V¬F = V
N3¬¬A⇒A¬¬V = ¬F = V ; ¬¬F = ¬V = F. Règle de commodité, non indispensable (voir la remarque plus bas).
Conjonction — V est neutre, F est absorbant
C1V ∧ A⇒AV ∧ V = V ; V ∧ F = F
C2A ∧ V⇒AV ∧ V = V ; F ∧ V = F
C3F ∧ A⇒FF ∧ V = F ; F ∧ F = F
C4A ∧ F⇒FV ∧ F = F ; F ∧ F = F
Disjonction — V est absorbant, F est neutre
D1V ∨ A⇒VV ∨ V = V ; V ∨ F = V
D2A ∨ V⇒VV ∨ V = V ; F ∨ V = V
D3F ∨ A⇒AF ∨ V = V ; F ∨ F = F
D4A ∨ F⇒AV ∨ F = V ; F ∨ F = F
Implication
I1V → A⇒AV → V = V ; V → F = F
I2F → A⇒VF → V = V ; F → F = V
I3A → V⇒VV → V = V ; F → V = V
I4A → F⇒¬AV → F = F = ¬V ; F → F = V = ¬F
Équivalence
E1V ↔ A⇒AV ↔ V = V ; V ↔ F = F
E2A ↔ V⇒AV ↔ V = V ; F ↔ V = F
E3F ↔ A⇒¬AF ↔ V = F = ¬V ; F ↔ F = V = ¬F
E4A ↔ F⇒¬AV ↔ F = F = ¬V ; F ↔ F = V = ¬F

Ces règles se retiennent sans effort si l’on garde en tête leur sens : V est l’élément neutre de ∧ et l’élément absorbant de ∨ ; F est l’élément absorbant de ∧ et l’élément neutre de ∨ ; une implication dont l’antécédent est faux ou dont le conséquent est vrai est vraie ; une implication d’antécédent vrai vaut son conséquent, une implication de conséquent faux vaut la négation de son antécédent ; enfin V ↔ A « dit la même chose » que A, et F ↔ A la même chose que ¬A.

Attention. Les règles ne sont pas symétriques pour l’implication : F → A vaut V (règle I2), mais A → F vaut ¬A (règle I4). Confondre les deux est l’erreur la plus fréquente dans la construction d’un arbre de Quine. De même, ne confondez pas V ∧ A ⇒ A (V neutre) et V ∨ A ⇒ V (V absorbant).

Règles étendues (facultatives). On peut ajouter n’importe quelle équivalence logique valide sans compromettre la méthode, puisque la justification du §6 n’exige que l’équivalence entre le membre de gauche et le membre de droite. Les plus utiles sont l’idempotence A ∧ A ⇒ A et A ∨ A ⇒ A, la réflexivité A → A ⇒ V et A ↔ A ⇒ V, ainsi que A ∧ ¬A ⇒ F et A ∨ ¬A ⇒ V (nous les numérotons X1 à X6 dans l’outil du §10). Elles raccourcissent certains arbres, par exemple en réduisant r → r à V sans avoir à brancher sur r. En revanche, elles ne sont pas nécessaires : les règles N1 à E4 suffisent, et c’est avec elles seules que les exemples de cette page sont traités, sauf mention contraire.

3.3 Réduction d’une formule

Définition 3.2 (réduction). Réduire une formule, c’est lui appliquer les règles de réduction, à n’importe quelle sous-formule et dans n’importe quel ordre, jusqu’à ce qu’aucune règle ne s’applique plus. Une formule à laquelle aucune règle ne s’applique est dite réduite (ou en forme normale pour ces règles). Nous noterons red(A) une formule réduite obtenue à partir de A.

Lemme 3.3 (terminaison). Toute suite d’applications de règles à partir d’une formule A est finie ; la réduction aboutit donc toujours à une formule réduite.

Démonstration. Appelons taille d’une formule le nombre total de symboles autres que les parenthèses (variables, constantes et connecteurs). Chaque règle du catalogue remplace une sous-formule par une formule strictement plus petite : N1 et N2 remplacent 2 symboles par 1 ; N3 supprime 2 symboles ; C1 à C4, D1 à D4, I1 à I3, E1 et E2 remplacent une formule de taille |A| + 2 par une formule de taille |A| ou 1 ; I4, E3 et E4 remplacent une formule de taille |A| + 2 par ¬A, de taille |A| + 1. Comme la taille est un entier positif qui décroît strictement à chaque étape, il n’y a qu’un nombre fini d’étapes. (Les règles étendues X1 à X6 font elles aussi décroître la taille.) ∎

Lemme 3.4 (forme d’une formule réduite). Une formule réduite est soit une constante (V ou F), soit une formule dans laquelle n’apparaît aucune constante. En particulier, une formule sans variable se réduit toujours à une constante.

Démonstration. Soit B une formule réduite contenant une occurrence d’une constante c. Si B est cette constante, c’est terminé. Sinon, cette occurrence est l’argument immédiat d’un connecteur de B, c’est-à-dire que B possède une sous-formule de l’une des formes ¬c, c ∘ D ou D ∘ c, avec ∘ un connecteur binaire. Or le catalogue contient une règle pour chacune de ces formes : N1 ou N2 pour ¬c ; C1, C3, D1, D3, I1, I2, E1, E3 pour c ∘ D selon la constante et le connecteur ; C2, C4, D2, D4, I3, I4, E2, E4 pour D ∘ c. Une règle s’applique donc à B, ce qui contredit l’hypothèse que B est réduite. Ainsi, une formule réduite qui n’est pas une constante ne contient aucune constante. Enfin, si A ne contient aucune variable, red(A) n’en contient pas non plus (aucune règle n’introduit de variable) ; n’étant faite que de connecteurs et de constantes, elle ne peut être réduite qu’en étant une constante. ∎

Remarque (les règles seules ne suffisent pas). La formule p ∨ ¬p est une tautologie, mais elle est déjà réduite : aucune règle du catalogue de base ne s’y applique, faute de constante. La réduction ne décide donc rien à elle seule ; c’est le branchement sur les variables, décrit au §4, qui fait apparaître des constantes et permet aux règles d’agir. Quelques mots aussi sur l’ordre d’application : puisque chaque règle remplace une sous-formule par une formule équivalente, toutes les formules réduites obtenues à partir de A, quel que soit l’ordre choisi, sont logiquement équivalentes à A (c’est le lemme 6.2) ; c’est tout ce dont la méthode a besoin. L’outil du §10 applique toujours la règle possible la plus à gauche et la plus profonde, ce qui rend son calcul reproductible.

4.La méthode de Quine pas à pas

Nous pouvons maintenant énoncer la méthode. Elle s’applique à une formule quelconque A et produit un arbre dont la lecture classe A.

Algorithme (construction de l’arbre de Quine de A)
  1. Réduire. Réduire la formule courante à l’aide des règles du §3.2. Placer la formule réduite dans le nœud courant (au départ, la racine).
  2. Tester. Si la formule réduite est la constante V ou la constante F, le nœud est une feuille ; on s’arrête pour cette branche.
  3. Brancher. Sinon, la formule réduite contient au moins une variable (lemme 3.4). En choisir une, disons p, et créer deux branches : la branche de gauche, étiquetée p := V, mène à la formule B[p := V] ; la branche de droite, étiquetée p := F, mène à B[p := F], où B est la formule réduite du nœud courant.
  4. Recommencer à l’étape 1 sur chacune des deux nouvelles formules.

Lecture du résultat. Toutes les feuilles portent V : A est une tautologie. Toutes portent F : A est une contradiction. Il y a des feuilles V et des feuilles F : A est contingente.

Définition 4.1 (arbre de Quine). Un arbre de Quine de la formule A est un arbre binaire fini dont chaque nœud est étiqueté par une formule réduite, et qui satisfait les conditions suivantes :

  • la racine est étiquetée par une forme réduite de A ;
  • un nœud étiqueté par une constante est une feuille ;
  • un nœud étiqueté par une formule B qui n’est pas une constante possède exactement deux enfants, associés à une variable p de B : l’enfant de gauche, relié par l’arête p := V, est étiqueté par une forme réduite de B[p := V] ; l’enfant de droite, relié par l’arête p := F, est étiqueté par une forme réduite de B[p := F].

Le chemin qui mène de la racine à un nœud définit une valuation partielle : la liste des substitutions rencontrées, par exemple p := V, q := F. Une formule peut avoir plusieurs arbres de Quine, selon les variables choisies ; nous verrons (corollaire 6.5) qu’ils donnent tous le même verdict.

4.1 Un premier exemple, entièrement détaillé

Prenons A = (p ∧ q) → p. La formule ne contient aucune constante : elle est déjà réduite, et c’est la racine. Elle contient deux variables ; p apparaît deux fois et q une fois, choisissons p (le §7 explique pourquoi ce choix est judicieux).

  • Branche p := V. La substitution donne (V ∧ q) → V. On réduit : la sous-formule V ∧ q devient q (règle C1), d’où q → V ; puis q → V devient V (règle I3). La branche aboutit à la feuille V. Remarquez que l’on n’a jamais eu à se prononcer sur q.
  • Branche p := F. La substitution donne (F ∧ q) → F. La sous-formule F ∧ q devient F (règle C3), d’où F → F, qui devient V (règle I2). Feuille V.

Les deux feuilles portent V : (p ∧ q) → p est une tautologie. L’arbre a deux feuilles alors que la table de vérité aurait quatre lignes.

Arbre de Quine de (p ∧ q) → p. Sous chaque formule substituée, le symbole ⇓ introduit la formule réduite ; « réduction » déplie la liste des règles appliquées.

4.2 Comment présenter un arbre sur papier

La présentation manuscrite habituelle est la suivante, et c’est aussi celle des figures de cette page :

  • la racine, en haut, porte la formule de départ (réduite si nécessaire) ;
  • sous un nœud à développer, on trace deux branches et l’on écrit sur chacune la substitution, p := V à gauche et p := F à droite (certains auteurs écrivent p = V, ou p et ¬p, ou encore 1 et 0) ;
  • au bout de chaque branche, on écrit la formule obtenue après substitution, puis, en dessous ou à côté, les étapes de réduction, en indiquant la règle utilisée si le contexte l’exige ; on peut aussi n’écrire que la formule réduite lorsque la réduction est évidente ;
  • on encadre ou l’on souligne les feuilles V et F, et l’on conclut par une phrase : « toutes les feuilles valent V, donc … ».

Les feuilles sont aussi une source d’information supplémentaire : la valuation partielle lue le long d’une branche qui aboutit à F est un contre-modèle de la formule (toute façon de compléter cette valuation partielle rend la formule fausse), et la valuation partielle d’une branche qui aboutit à V en est un modèle. C’est l’objet du corollaire 6.6.

5.Exemples commentés

Chaque exemple est présenté en deux temps : le raisonnement écrit comme on le ferait sur papier, puis l’arbre calculé par l’outil de cette page (mêmes règles, même stratégie : à chaque nœud, la variable la plus fréquente est choisie ; la règle appliquée est toujours la plus profonde et la plus à gauche possible). Dans chaque nœud, dépliez « réduction » pour voir la liste des règles.

5.1 Une contradiction : (p → q) ∧ (p ∧ ¬q)

Aucune constante : la formule est réduite. Les variables p et q apparaissent deux fois chacune ; prenons p.

  • p := V. On obtient (V → q) ∧ (V ∧ ¬q). Par I1, V → q devient q ; par C1, V ∧ ¬q devient ¬q. Il reste q ∧ ¬q, qui est réduite mais n’est pas une constante : il faut brancher sur q.
    • q := V : V ∧ ¬V ; par N1, ¬V devient F, puis V ∧ F devient F (C1). Feuille F.
    • q := F : F ∧ ¬F ; par N2, ¬F devient V, puis F ∧ V devient F (C2). Feuille F.
  • p := F. On obtient (F → q) ∧ (F ∧ ¬q). Par I2, F → q devient V ; par C3, F ∧ ¬q devient F ; enfin V ∧ F devient F (C1). Feuille F, sans avoir touché à q.

Trois feuilles, toutes F : la formule est une contradiction. On le comprend : elle affirme à la fois « si p alors q » et « p et non q », ce qui est impossible.

Arbre de Quine de (p → q) ∧ (p ∧ ¬q) : trois feuilles F, contre quatre lignes de table de vérité.

5.2 Une formule contingente : p → q

  • p := V. V → q devient q (I1) ; il faut brancher sur q : q := V donne la feuille V, q := F donne la feuille F.
  • p := F. F → q devient V (I2). Feuille V.

Il y a des feuilles des deux sortes : la formule est contingente. La branche qui aboutit à F porte la valuation partielle p := V, q := F : c’est l’unique contre-modèle de p → q. Les deux branches qui aboutissent à V décrivent ses modèles : p := V, q := V, et p := F avec q quelconque, soit trois valuations en tout, comme l’indique la table de vérité de l’implication.

Arbre de Quine de p → q : feuilles V, F, V ; la formule est contingente.

5.3 Trois variables : la transitivité de l’implication

Reprenons la formule de l’en-tête, A = ((p → q) ∧ (q → r)) → (p → r). Chaque variable apparaît deux fois ; nous prenons p, la première rencontrée.

  • p := V. ((V → q) ∧ (q → r)) → (V → r). Deux applications de I1 (V → q ⇒ q, puis V → r ⇒ r) donnent (q ∧ (q → r)) → r, réduite. On branche sur q.
    • q := V : (V ∧ (V → r)) → r ; par I1, V → r ⇒ r, puis par C1, V ∧ r ⇒ r : il reste r → r. Avec les règles de base, cette formule est réduite, et l’on branche sur r : V → V ⇒ V (I1) et F → F ⇒ V (I2). Deux feuilles V. (La règle étendue X3 aurait donné V directement.)
    • q := F : (F ∧ (F → r)) → r ; par I2, F → r ⇒ V ; par C2, F ∧ V ⇒ F ; par I2, F → r ⇒ V. Feuille V.
  • p := F. ((F → q) ∧ (q → r)) → (F → r). Par I2, F → q ⇒ V ; par C1, V ∧ (q → r) ⇒ q → r ; par I2, F → r ⇒ V ; il reste (q → r) → V, qui vaut V par I3. Feuille V. Ni q ni r n’ont eu à être examinées.

Quatre feuilles V : la formule est une tautologie. La table de vérité aurait exigé huit lignes de trois sous-formules chacune. L’arbre figure en tête de page.

5.4 La loi de Peirce : ((p → q) → p) → p

La variable p apparaît trois fois, q une seule : on branche sur p.

  • p := V. ((V → q) → V) → V. On peut conclure d’un coup : le conséquent de l’implication principale est V, donc la formule vaut V (I3). En procédant de l’intérieur vers l’extérieur, comme l’outil : V → q ⇒ q (I1), q → V ⇒ V (I3), V → V ⇒ V (I1). Feuille V.
  • p := F. ((F → q) → F) → F. Par I2, F → q ⇒ V ; par I1, V → F ⇒ F ; par I2, F → F ⇒ V. Feuille V.

Deux feuilles V : la loi de Peirce est une tautologie, et la variable q n’a jamais eu à être valuée. C’est un cas où le bon choix de variable divise le travail par deux.

Arbre de Quine de la loi de Peirce : deux feuilles suffisent.

5.5 Vérifier une équivalence : une loi de De Morgan

Pour établir ¬(p ∧ q) ≡ ¬p ∨ ¬q, il suffit (§2.3) de montrer que ¬(p ∧ q) ↔ (¬p ∨ ¬q) est une tautologie.

  • p := V. ¬(V ∧ q) ↔ (¬V ∨ ¬q). Par C1, V ∧ q ⇒ q ; par N1, ¬V ⇒ F ; par D3, F ∨ ¬q ⇒ ¬q. Il reste ¬q ↔ ¬q, réduite : on branche sur q.
    • q := V : ¬V ↔ ¬V ; deux applications de N1 donnent F ↔ F, puis E3 donne ¬F et N2 donne V.
    • q := F : ¬F ↔ ¬F ; deux applications de N2 donnent V ↔ V, puis E1 donne V.
  • p := F. ¬(F ∧ q) ↔ (¬F ∨ ¬q). Par C3, F ∧ q ⇒ F ; par N2, ¬F ⇒ V (deux fois) ; par D1, V ∨ ¬q ⇒ V ; il reste V ↔ V, qui vaut V (E1).

Trois feuilles V : l’équivalence est établie.

Arbre de Quine de ¬(p ∧ q) ↔ (¬p ∨ ¬q).

5.6 Vérifier une conséquence logique : le modus ponens

Pour établir que p → q, p ⊨ q, on montre (§2.3) que ((p → q) ∧ p) → q est une tautologie. La variable p apparaît deux fois, q deux fois ; prenons p.

  • p := V. ((V → q) ∧ V) → q ; par I1 puis C2, on obtient q → q, et l’on branche sur q : V → V ⇒ V, F → F ⇒ V.
  • p := F. ((F → q) ∧ F) → q ; par I2, F → q ⇒ V ; par C1, V ∧ F ⇒ F ; par I2, F → q ⇒ V. Feuille V.
Arbre de Quine de ((p → q) ∧ p) → q : le modus ponens est une règle valide.

6.Justification : pourquoi la méthode est correcte

Une méthode de décision doit être correcte (si elle répond « tautologie », la formule en est vraiment une, et de même pour les autres verdicts) et complète (elle répond toujours, et toujours par le bon verdict). Les deux propriétés découlent de trois lemmes élémentaires et d’un théorème.

Lemme 6.1 (substitution). Soient A une formule, p une variable, c ∈ {V, F} et v une valuation telle que v(p) = c. Alors v̄(A[p := c]) = v̄(A).

Démonstration. Par induction sur la construction de A.

  • Si A est la variable p : A[p := c] = c et v̄(c) = c = v(p) = v̄(A). Si A est une variable q ≠ p ou une constante, A[p := c] = A et il n’y a rien à démontrer.
  • Si A = ¬B : v̄((¬B)[p := c]) = v̄(¬(B[p := c])), qui est la négation de v̄(B[p := c]), c’est-à-dire, par hypothèse d’induction, la négation de v̄(B), soit v̄(¬B).
  • Si A = B ∘ C avec ∘ binaire : v̄((B ∘ C)[p := c]) = v̄(B[p := c] ∘ C[p := c]) est obtenue en appliquant la table de ∘ à v̄(B[p := c]) et v̄(C[p := c]), qui valent v̄(B) et v̄(C) par hypothèse d’induction ; le résultat est donc v̄(B ∘ C). ∎

Lemme 6.2 (les réductions préservent la valeur). Si B est obtenue à partir de A par une ou plusieurs applications des règles de réduction, alors A ≡ B, c’est-à-dire v̄(A) = v̄(B) pour toute valuation v. En particulier A ≡ red(A).

Démonstration. Il suffit de traiter une seule application, le cas général s’obtenant par transitivité de ≡. La colonne « vérification » du tableau du §3.2 montre que, pour chaque règle L ⇒ R et pour chaque valeur de A, les deux membres prennent la même valeur ; comme la valeur d’une sous-formule ne dépend que des valeurs de ses composants, on a v̄(L) = v̄(R) pour toute valuation v. Reste à voir que remplacer une sous-formule par une formule équivalente ne change pas la valeur de la formule entière : c’est une induction sur la position de la sous-formule remplacée. Si la sous-formule remplacée est la formule entière, c’est immédiat. Sinon elle se trouve dans un argument immédiat de la formule, disons dans B pour une formule B ∘ C ; par hypothèse d’induction, la valeur de B n’est pas modifiée, donc celle de B ∘ C, calculée par la table de ∘ à partir des valeurs de B et C, ne l’est pas non plus ; le cas de ¬B est identique. ∎

Lemme 6.3 (finitude de l’arbre). Soit A une formule à n variables. Tout arbre de Quine de A est fini : sa hauteur est au plus n, il a au plus 2n feuilles, et, le long d’un chemin, chaque variable est substituée au plus une fois.

Démonstration. Si un nœud porte la formule B et que l’on branche sur p, la variable p n’apparaît plus dans B[p := V] ni dans B[p := F] (définition 3.1), et aucune règle de réduction n’introduit de variable ; les formules des descendants ne contiennent donc plus p, ce qui interdit de rebrancher sur elle. Chaque niveau de l’arbre fait ainsi disparaître une variable : après n branchements au plus, la formule n’a plus de variable et, par le lemme 3.4, sa forme réduite est une constante, donc une feuille. Un arbre binaire de hauteur au plus n a au plus 2n feuilles. ∎

Théorème 6.4 (correction et complétude de la méthode de Quine). Soient A une formule et T un arbre de Quine quelconque de A. Alors :

  1. A est une tautologie si et seulement si toutes les feuilles de T portent V ;
  2. A est une contradiction si et seulement si toutes les feuilles de T portent F ;
  3. A est contingente si et seulement si T possède au moins une feuille V et au moins une feuille F.

Démonstration. Pour un nœud N de T, notons BN la formule qui l’étiquette et σN la valuation partielle lue sur le chemin de la racine à N ; disons qu’une valuation v prolonge σN si v(p) = c pour chaque substitution p := c de σN. Par le lemme 6.3, σN n’attribue jamais deux valeurs à une même variable, de sorte que toute valuation partielle σN se prolonge en au moins une valuation.

Affirmation. Pour tout nœud N et toute valuation v qui prolonge σN, on a v̄(A) = v̄(BN).

On raisonne par induction sur la profondeur de N. Si N est la racine, σN est vide, toute valuation la prolonge, et BN = red(A) ≡ A par le lemme 6.2. Sinon, N est l’enfant d’un nœud M par une arête p := c, et BN est une forme réduite de BM[p := c]. Soit v prolongeant σN ; alors v prolonge σM et v(p) = c. On calcule : v̄(BN) = v̄(BM[p := c]) (lemme 6.2), = v̄(BM) (lemme 6.1, car v(p) = c), = v̄(A) (hypothèse d’induction appliquée à M). L’affirmation est démontrée.

Toute valuation aboutit à une feuille. Soit v une valuation. Partons de la racine ; à chaque nœud interne, dont le branchement porte sur une variable p, suivons l’arête p := v(p). Le chemin suivi est tel que v prolonge chaque σN rencontrée ; l’arbre étant fini, il aboutit à une feuille L, étiquetée par une constante cL. Par l’affirmation, v̄(A) = v̄(cL) = cL. Autrement dit, la valeur de A sous v est la constante de la feuille que v atteint.

Toute feuille est atteinte. Soit L une feuille. Une valuation v prolongeant σL existe ; en suivant les arêtes p := v(p) depuis la racine, on suit exactement le chemin de L, donc v atteint L et v̄(A) = cL.

Conclusion. (1) Si toutes les feuilles portent V, toute valuation atteint une feuille V, donc v̄(A) = V pour toute v : A est une tautologie. Réciproquement, si une feuille porte F, une valuation l’atteint et rend A fausse : A n’est pas une tautologie. (2) se démontre de même en échangeant V et F. (3) résulte de (1), de (2) et du fait que les trois classes forment une partition. ∎

Corollaire 6.5 (indépendance du choix des variables). Le verdict lu sur un arbre de Quine de A ne dépend ni des variables choisies pour brancher ni de l’ordre d’application des règles ; seule la taille de l’arbre en dépend.

Démonstration. Le théorème 6.4 vaut pour tout arbre de Quine de A, et le verdict est une propriété de A seule. ∎

Corollaire 6.6 (lecture des modèles et des contre-modèles). Toute valuation qui prolonge la valuation partielle d’une feuille V est un modèle de A ; toute valuation qui prolonge celle d’une feuille F est un contre-modèle. L’ensemble des modèles de A est exactement l’ensemble des valuations qui prolongent la valuation partielle d’une feuille V.

Démonstration. La première phrase est l’affirmation de la démonstration précédente appliquée à une feuille. Pour la seconde, si v est un modèle, la feuille qu’elle atteint porte v̄(A) = V, et v prolonge sa valuation partielle. ∎

Corollaire 6.7 (arrêt anticipé). Dès qu’une feuille F apparaît, A n’est pas une tautologie ; dès qu’une feuille V apparaît, A n’est pas une contradiction ; dès que l’on a vu une feuille de chaque sorte, A est contingente et l’exploration peut cesser. En revanche, conclure « tautologie » ou « contradiction » exige d’avoir développé toutes les branches.

Remarque (le théorème de développement). Le cœur algébrique de la méthode est l’identité, valable pour toute formule A et toute variable p :

A ≡ (p ∧ A[p := V]) ∨ (¬p ∧ A[p := F])

appelée théorème de développement de Boole, ou développement de Shannon en théorie des circuits. Elle se démontre par le lemme 6.1 : sous une valuation où p vaut V, le membre de droite vaut v̄(A[p := V]) = v̄(A) ; sous une valuation où p vaut F, il vaut v̄(A[p := F]) = v̄(A). On en tire aussitôt que A est une tautologie si et seulement si A[p := V] et A[p := F] le sont toutes deux, ce qui est précisément l’étape de branchement, la réduction servant à reconnaître au plus vite les cas triviaux.

7.Stratégies, heuristiques et erreurs fréquentes

7.1 Bien choisir la variable de branchement

Le corollaire 6.5 garantit que n’importe quel choix conduit au bon verdict ; mais la taille de l’arbre, donc la longueur du calcul et le risque d’erreur, en dépend fortement. Deux principes guident le choix.

  • La variable la plus fréquente. Chaque occurrence remplacée par une constante déclenche une règle de réduction ; plus il y a d’occurrences, plus la formule fond. Dans la loi de Peirce (§5.4), brancher sur p (trois occurrences) donne deux feuilles ; brancher sur q (une occurrence) en donne quatre. Dans (p ∧ q) → p, brancher sur q d’abord donne trois feuilles au lieu de deux : essayez-le dans l’outil du §10 en imposant l’ordre q, p.
  • La variable « décisive ». Une variable dont l’une des valeurs fixe d’un coup la valeur de la formule est un bon choix : dans B → C, une variable qui rend B faux ou C vrai clôt immédiatement l’une des deux branches (I2 ou I3) ; dans une conjonction, une variable qui rend faux l’un des conjoints (C3, C4) ; dans une disjonction, une variable qui rend vrai l’un des disjoints (D1, D2). L’autre branche concentre alors tout le travail, mais sur une formule déjà réduite.

Ces deux principes coïncident souvent. Quand ils divergent, on peut simplement essayer les deux : un arbre trop volumineux est le signe d’un choix perfectible, jamais d’une erreur logique.

7.2 Réduire complètement avant de brancher

Brancher sur une formule contenant encore des constantes n’est pas faux (le théorème 6.4 s’applique dès lors que chaque étiquette est équivalente à la formule substituée), mais c’est inutile et dangereux : la réduction aurait peut-être révélé une constante, et l’on développe pour rien deux sous-arbres identiques. Réduisez toujours jusqu’au bout, en vérifiant à la fin que la formule est soit une constante, soit sans aucune constante (lemme 3.4).

7.3 Règles étendues et arrêt anticipé

Si votre cours l’autorise, les règles étendues X1 à X6 (§3.2) évitent quelques branchements : r → r ou ¬q ↔ ¬q se réduisent directement à V. Souvenez-vous seulement que toute règle ajoutée doit être une équivalence logique, sous peine de fausser le verdict. Par ailleurs, lorsque la question posée est seulement « est-ce une tautologie ? », la première feuille F rencontrée permet de répondre non sans terminer l’arbre (corollaire 6.7) ; sur papier, on indique alors la valuation partielle de cette feuille comme contre-exemple.

7.4 Les erreurs les plus fréquentes

  • Oublier une occurrence. La substitution porte sur toutes les occurrences de la variable, y compris celles qui se cachent sous une négation ou dans un conséquent. Une occurrence oubliée réapparaît plus bas et fausse la valuation partielle.
  • Confondre I2 et I4. F → A vaut V ; A → F vaut ¬A. L’implication n’est pas symétrique.
  • Confondre neutre et absorbant. V ∧ A ⇒ A mais V ∨ A ⇒ V ; F ∨ A ⇒ A mais F ∧ A ⇒ F.
  • Réduire V ↔ A en V. C’est A (E1) ; et F ↔ A est ¬A (E3), non F.
  • S’arrêter à une formule qui n’est pas une constante. Une feuille porte V ou F, jamais q ∧ ¬q ni r → r, même si l’on « voit » leur valeur : il faut brancher (ou invoquer explicitement une règle étendue).
  • Conclure trop tôt. Une branche V ne prouve pas la tautologie ; il faut toutes les branches. Symétriquement, une branche F prouve seulement que la formule n’est pas une tautologie, pas qu’elle est une contradiction.
  • Mal lire un contre-modèle. La valuation partielle d’une feuille ne fixe que les variables rencontrées sur le chemin ; les autres sont libres, et n’importe quelle valeur leur convient.
  • Mélanger les méthodes. Dans un arbre de Quine on ne « décompose » jamais une formule selon son connecteur principal (cela relève des tableaux sémantiques, §9.4) : on substitue et l’on réduit, rien d’autre.

8.Arbre de Quine ou table de vérité ? Coût et complexité

Table de véritéArbre de Quine
Nombre de cas examinésToujours 2n lignes.Entre 1 et 2n feuilles ; souvent bien moins que 2n.
Travail par casÉvaluation de toutes les sous-formules.Quelques réductions sur une formule qui rétrécit à chaque niveau.
Meilleur casAucun : le coût est fixe.Une seule feuille (formule contenant une constante décisive) ou deux (Peirce, §5.4).
Pire cas2n lignes.2n feuilles, atteint par exemple par les formules de parité (ci-dessous).
Information obtenueLa valeur sous chaque valuation.Le verdict, et une description compacte des modèles et contre-modèles par valuations partielles.
Erreurs typiquesFautes de recopie dans les grandes tables.Mauvaise règle de réduction, occurrence oubliée.
Choix à faireAucun.L’ordre des variables ; il influe sur la taille, pas sur le verdict.

8.1 Un cas où l’arbre ne fait pas mieux que la table

Considérons (p ↔ q) ↔ r. Cette formule est vraie exactement quand le nombre de variables fausses est pair : c’est une formule de parité. Son arbre de Quine a huit feuilles, autant que la table a de lignes, et ce quel que soit l’ordre des variables.

Arbre de Quine de (p ↔ q) ↔ r : huit feuilles, aucune branche ne se ferme avant d’avoir valué les trois variables.

Proposition 8.1. Soit A une formule à n variables dont la valeur change chaque fois que l’on change la valeur d’une seule variable (c’est le cas de (p ↔ q) ↔ r, et plus généralement des formules de parité p1 ↔ p2 ↔ … ↔ pn). Alors tout arbre de Quine de A a exactement 2n feuilles, quelles que soient les variables choisies et les règles (correctes) utilisées.

Démonstration. Soit L une feuille de valuation partielle σL. Par l’affirmation de la démonstration du théorème 6.4, A prend la même valeur sous toutes les valuations qui prolongent σL. Si σL laissait une variable q libre, deux prolongements ne différant que par la valeur de q donneraient à A des valeurs différentes, contradiction. Donc chaque feuille est à profondeur exactement n, et un arbre binaire dont toutes les feuilles sont à profondeur n a 2n feuilles. ∎

8.2 Ce que dit la théorie de la complexité

On ne connaît aucune méthode qui décide si une formule quelconque est une tautologie en un temps borné par un polynôme en la taille de la formule. Le problème de la satisfaisabilité est NP-complet (théorème de Cook, 1971), et celui de la validité est son dual, coNP-complet ; une méthode polynomiale pour l’un ou l’autre entraînerait P = NP. Toutes les méthodes connues, arbres de Quine compris, ont un pire cas exponentiel. L’intérêt de la méthode de Quine est donc double : elle est très efficace sur la plupart des formules que l’on rencontre en pratique, où beaucoup de branches se ferment tôt ; et elle est transparente, chaque étape étant une règle élémentaire que l’on peut vérifier.

9.Extensions, variantes et méthodes voisines

9.1 Ce que l’arbre permet aussi de décider

  • Équivalence logique. A ≡ B si et seulement si A ↔ B est une tautologie (§5.5).
  • Conséquence logique. A1, …, Ak ⊨ B si et seulement si (A1 ∧ … ∧ Ak) → B est une tautologie (§5.6). Chaque feuille F de l’arbre fournit un contre-exemple : une situation où les prémisses sont vraies et la conclusion fausse.
  • Satisfaisabilité et énumération des modèles. A est satisfaisable si et seulement si son arbre a une feuille V ; l’ensemble de ses modèles est décrit par les valuations partielles de ses feuilles V (corollaire 6.6), ce qui en donne une forme normale disjonctive : la disjonction, sur les feuilles V, des conjonctions de littéraux lues sur les chemins. Pour p → q (§5.2), on obtient (p ∧ q) ∨ ¬p.
  • Formules contenant déjà des constantes. Il suffit de commencer par réduire : l’algorithme du §4 le prévoit.

9.2 Deux descendantes directes

  • La procédure DPLL (Davis et Putnam, 1960 ; Davis, Logemann et Loveland, 1962) applique la même idée de branchement sur la valeur d’une variable, mais à des ensembles de clauses (formules en forme normale conjonctive), en y ajoutant la propagation unitaire et l’élimination des littéraux purs. C’est l’ancêtre des solveurs SAT modernes.
  • Les diagrammes de décision binaire (Lee, 1959 ; Akers, 1978 ; Bryant, 1986) sont des arbres de Quine dans lesquels on impose un ordre fixe des variables et l’on fusionne les sous-arbres identiques ; on obtient une représentation canonique de chaque fonction booléenne, très utilisée en vérification de circuits.

9.3 Une reformulation logique

Comme le montre la remarque qui suit le corollaire 6.7, brancher sur p revient à utiliser l’équivalence A ≡ (p ∧ A[p := V]) ∨ (¬p ∧ A[p := F]). En termes de démonstration, prouver A à partir de A[p := V] et A[p := F] est une forme de raisonnement par cas sur le tiers exclu p ∨ ¬p. C’est aussi ce que Quine appelle « résoudre » un schéma ; ce mot n’a aucun rapport avec la résolution de Robinson (1965), une règle d’inférence sur les clauses.

9.4 À ne pas confondre

Les tableaux sémantiques, ou « méthode des arbres »
Introduits par Beth (1955) et Hintikka (1955), popularisés par Smullyan (1968) et par Jeffrey (1967, sous le nom de truth trees), ils sont eux aussi des arbres, ce qui prête à confusion. Mais on n’y substitue jamais de constante : on part de la négation de la formule à prouver et l’on décompose les formules selon leur connecteur principal (une conjonction vraie s’écrit sur une même branche, une disjonction vraie ouvre deux branches) jusqu’à ce que chaque branche contienne un littéral et sa négation (branche fermée) ou ne puisse plus être développée. Un arbre de Quine branche sur les valeurs des variables ; un tableau branche sur la structure des formules. Certains cours francophones appellent « arbres de Beth » les tableaux et réservent « méthode de Quine » ou « algorithme de Quine » à la méthode de cette page.
L’algorithme de Quine–McCluskey
Décrit par Quine (1952) puis McCluskey (1956), il sert à minimiser une fonction booléenne, c’est-à-dire à trouver une forme normale disjonctive la plus courte possible à partir de ses implicants premiers. Il ne décide pas de la validité et ne construit pas d’arbre.
Les tables de Karnaugh
Autre outil de minimisation, graphique, limité à quelques variables ; sans rapport avec la décision par substitution.

10.Outil interactif : construire l’arbre de Quine d’une formule

Saisissez une formule, choisissez éventuellement la stratégie de branchement, puis construisez l’arbre. Chaque nœud montre la formule après substitution, sa forme réduite et, dans « réduction », la liste des règles appliquées avec leur numéro (§3.2). Le verdict, le nombre de feuilles, les modèles et les contre-modèles lus sur les feuilles, et, si vous le souhaitez, la table de vérité complète pour comparaison, s’affichent sous l’arbre.

Saisie acceptée : ¬ (ou ~, !), ∧ (ou &, ^), ∨ (ou |, +), → (ou ->, =>), ↔ (ou <->, <=>), constantes V/F (ou ⊤/⊥, 1/0). Les variables sont des lettres, éventuellement suivies de chiffres (p, q1, P), V et F exceptées. Priorités décroissantes ¬, ∧, ∨, →, ↔ ; → associe à droite, les autres à gauche. Au plus 10 variables pour l’arbre, 6 pour la table de vérité.

Pour s’exercer avec l’outil. Comparez, sur une même formule, l’arbre obtenu avec « la plus fréquente » et celui obtenu en imposant un mauvais ordre : le verdict ne change pas (corollaire 6.5), la taille si. Activez ensuite les règles étendues et observez quels branchements disparaissent. Enfin, affichez la table de vérité et vérifiez que chaque feuille F correspond bien aux lignes où la formule est fausse.

11.Exercices corrigés

Construisez l’arbre de Quine de chaque formule avec les règles de base seulement, en choisissant à chaque nœud la variable la plus fréquente (la première rencontrée en cas d’égalité), puis comparez avec la solution. Les solutions sont calculées par l’outil du §10 ; les formules réduites intermédiaires y sont donc exactement celles que vous devez obtenir.

Exercice 1 — p ∨ ¬p (tiers exclu)

Déterminez la nature de la formule.

Solution

Branche p := V : V ∨ ¬V ; ¬V ⇒ F (N1), puis V ∨ F ⇒ V (D1). Branche p := F : F ∨ ¬F ; ¬F ⇒ V (N2), puis F ∨ V ⇒ V (D2). Deux feuilles V : tautologie. Notez que la formule était réduite au départ : sans branchement, les règles seules n’auraient rien donné.

Arbre de p ∨ ¬p.
Exercice 2 — (p → q) → (¬q → ¬p) (contraposition)

Déterminez la nature de la formule et comptez les feuilles.

Indice

Les deux variables apparaissent deux fois ; on branche donc sur p. Sur la branche p := V, une double négation apparaît.

Solution

Branche p := V : (V → q) → (¬q → ¬V) ; I1 donne q → (¬q → ¬V), N1 donne q → (¬q → F), I4 donne q → ¬¬q, N3 donne q → q. On branche sur q : V → V ⇒ V (I1) et F → F ⇒ V (I2). Branche p := F : (F → q) → (¬q → ¬F) ; I2 donne V → (¬q → ¬F), N2 donne V → (¬q → V), I3 donne V → V, I1 donne V. Trois feuilles V : tautologie. Avec la règle étendue X3, la sous-formule q → q se serait réduite en V et l’arbre n’aurait eu que deux feuilles.

Arbre de (p → q) → (¬q → ¬p).
Exercice 3 — (p ∨ q) → p

Déterminez la nature de la formule ; si elle est contingente, donnez tous ses contre-modèles.

Solution

Branche p := V : (V ∨ q) → V ; D1 donne V → V, I1 donne V. Branche p := F : (F ∨ q) → F ; D3 donne q → F, I4 donne ¬q ; on branche sur q : ¬V ⇒ F (N1) et ¬F ⇒ V (N2). Feuilles V, F, V : la formule est contingente. L’unique feuille F porte la valuation p := F, q := V, qui est donc l’unique contre-modèle : « p ou q » ne permet pas de conclure « p ».

Arbre de (p ∨ q) → p.
Exercice 4 — (p ↔ q) ∧ (p ↔ ¬q)

Déterminez la nature de la formule. L’arbre est-il plus petit que la table de vérité ?

Solution

Branche p := V : (V ↔ q) ∧ (V ↔ ¬q) ; E1 deux fois donne q ∧ ¬q ; branchement sur q : V ∧ ¬V se réduit en F (N1 puis C1), F ∧ ¬F se réduit en F (N2 puis C2). Branche p := F : (F ↔ q) ∧ (F ↔ ¬q) ; E3 deux fois donne ¬q ∧ ¬¬q, N3 donne ¬q ∧ q ; branchement sur q : ¬V ∧ V ⇒ F (N1 puis C2) et ¬F ∧ F ⇒ F (N2 puis C1). Quatre feuilles F : contradiction. Ici l’arbre a autant de feuilles que la table a de lignes : la formule impose à p d’être à la fois équivalente à q et à ¬q, et aucune branche ne se ferme avant d’avoir valué les deux variables. (Avec la règle étendue X5, chaque sous-formule q ∧ ¬q se réduirait en F et l’arbre n’aurait que deux feuilles.)

Arbre de (p ↔ q) ∧ (p ↔ ¬q).
Exercice 5 — le syllogisme disjonctif : p ∨ q, ¬p ⊨ q ?

Traduisez la question en une formule, puis décidez-la par un arbre de Quine.

Indice

D’après le §2.3, il s’agit de savoir si ((p ∨ q) ∧ ¬p) → q est une tautologie.

Solution

Branche p := V : ((V ∨ q) ∧ ¬V) → q ; D1 donne (V ∧ ¬V) → q, N1 donne (V ∧ F) → q, C1 donne F → q, I2 donne V. Branche p := F : ((F ∨ q) ∧ ¬F) → q ; D3 donne (q ∧ ¬F) → q, N2 donne (q ∧ V) → q, C2 donne q → q ; branchement sur q : deux feuilles V. Trois feuilles V : la formule est une tautologie, donc la conséquence logique est valide.

Arbre de ((p ∨ q) ∧ ¬p) → q.
Exercice 6 — (p → q) ∨ (q → p)

Cette formule surprend souvent : de deux propositions quelconques, l’une implique toujours l’autre. Vérifiez-le.

Solution

Branche p := V : (V → q) ∨ (q → V) ; I1 donne q ∨ (q → V), I3 donne q ∨ V, D2 donne V. Branche p := F : (F → q) ∨ (q → F) ; I2 donne V ∨ (q → F), I4 donne V ∨ ¬q, D1 donne V. Deux feuilles V : tautologie, et q n’a jamais été valuée. La surprise vient de la lecture de → comme implication matérielle : si p est vrai, alors q → p est vrai ; si p est faux, alors p → q est vrai.

Arbre de (p → q) ∨ (q → p).
Exercice 7 — (p → (q → r)) → ((p → q) → (p → r))

Décidez cette formule à trois variables (l’un des axiomes de Frege pour l’implication) et comparez le nombre de feuilles au nombre de lignes de la table.

Indice

p apparaît trois fois : c’est elle qu’il faut substituer en premier. Sur la branche p := F, tout se réduit sans autre branchement.

Solution

Branche p := V : trois applications de I1 donnent (q → r) → (q → r). On branche sur q. Pour q := V, I1 deux fois donne r → r, puis le branchement sur r donne deux feuilles V. Pour q := F, (F → r) → (F → r) se réduit en V (I2, I2, I1). Branche p := F : (F → (q → r)) → ((F → q) → (F → r)) ; trois applications de I2 donnent V → (V → V), et deux applications de I1 donnent V. Quatre feuilles V au lieu de huit lignes : tautologie.

Arbre de (p → (q → r)) → ((p → q) → (p → r)).
Exercice 8 — questions de réflexion
  1. Donnez une formule à trois variables dont l’arbre de Quine n’a que deux feuilles, et une autre dont tout arbre de Quine a huit feuilles.
  2. Une formule dont l’arbre a une feuille V à profondeur 1 et une feuille F à profondeur 1 peut-elle être une tautologie ?
  3. Peut-on brancher deux fois sur la même variable le long d’un même chemin ?
  4. Si l’on ajoute au catalogue la « règle » A → B ⇒ B → A, que se passe-t-il ?
Solution
  1. ((p ∧ q) ∧ r) → p a deux feuilles : pour p := V, C1 puis I3 donnent V ; pour p := F, C3, C3 puis I2 donnent V. La formule de parité (p ↔ q) ↔ r a huit feuilles dans tout arbre de Quine (proposition 8.1).
  2. Non : par le théorème 6.4, une feuille F suffit à exclure la tautologie (et une feuille V à exclure la contradiction) ; la formule est contingente. La profondeur des feuilles ne joue aucun rôle dans le verdict.
  3. Non : après la substitution p := c, la variable p ne figure plus dans aucune formule du sous-arbre (lemme 6.3), et l’on ne branche que sur des variables présentes.
  4. Le verdict peut devenir faux, car A → B et B → A ne sont pas équivalentes : appliquée à p → q on obtiendrait q → p, et les contre-modèles lus sur l’arbre seraient ceux d’une autre formule. Seules des équivalences logiques peuvent être ajoutées au catalogue (lemme 6.2).

12.Références et notes

  1. W. V. O. Quine, Methods of Logic, Henry Holt, New York, 1950 ; éditions révisées 1959 et 1972, 4e édition Harvard University Press, 1982. La méthode est exposée dans la première partie, au chapitre « Truth-Value Analysis ». Traduction française : Méthodes de logique, Armand Colin, 1972.
  2. P. Gochet et P. Gribomont, Logique. Volume 1 : Méthodes pour l’informatique fondamentale, Hermès, Paris, 1990 — présentation de la « méthode de Quine » dans l’enseignement francophone de la logique propositionnelle.
  3. M. Davis et H. Putnam, « A Computing Procedure for Quantification Theory », Journal of the ACM, 7 (3), 1960 ; M. Davis, G. Logemann et D. Loveland, « A Machine Program for Theorem-Proving », Communications of the ACM, 5 (7), 1962.
  4. R. E. Bryant, « Graph-Based Algorithms for Boolean Function Manipulation », IEEE Transactions on Computers, C-35 (8), 1986.
  5. S. A. Cook, « The Complexity of Theorem-Proving Procedures », Proceedings of the 3rd ACM Symposium on Theory of Computing, 1971.
  6. E. W. Beth, « Semantic Entailment and Formal Derivability », Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 1955 ; R. M. Smullyan, First-Order Logic, Springer, 1968 ; R. C. Jeffrey, Formal Logic: Its Scope and Limits, McGraw-Hill, 1967 — pour la méthode des tableaux, à ne pas confondre avec celle de cette page.
  7. W. V. Quine, « The Problem of Simplifying Truth Functions », American Mathematical Monthly, 59 (8), 1952 ; E. J. McCluskey, « Minimization of Boolean Functions », Bell System Technical Journal, 35 (6), 1956 — l’algorithme de Quine–McCluskey, homonyme mais distinct.
  8. D. van Dalen, Logic and Structure, Springer, 5e édition, 2013 — pour les définitions générales de la logique des propositions (syntaxe, sémantique, induction sur les formules) utilisées au §2 et au §6.

Notes sur cette page. La numérotation des règles (N1 … E4, X1 … X6), des définitions et des énoncés est propre à cette page. Le moteur de l’outil du §10 applique exactement le catalogue du §3.2 (avec, sur demande, les règles étendues), la règle la plus profonde et la plus à gauche d’abord ; il a été vérifié sur des milliers de formules aléatoires que le verdict de l’arbre coïncide avec celui de la table de vérité et que chaque feuille donne bien la valeur de la formule sous toute valuation prolongeant son chemin, ce qui est précisément le contenu du théorème 6.4. Cette page fonctionne hors ligne ; seules les polices de caractères sont chargées depuis Internet, et des polices de substitution sont utilisées en leur absence.