Introduction à la logique formelle
Introduction à la logique formelle
P. Gribomont
2006-2014
i
Table des matières
1 Introduction 5
ii
3.4 Le raisonnement automatique . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.4.2 Digression : Leibniz et le raisonnement automatisable . . . . . . . . . 59
3.4.3 Automatiser la logique . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.4.4 Cubes, clauses et formes normales . . . . . . . . . . . . . . . . . . . . 60
3.4.5 Clauses de Horn et ensembles de Horn . . . . . . . . . . . . . . . . . . 61
3.4.6 L’algorithme de résolution unitaire . . . . . . . . . . . . . . . . . . . . 62
3.4.7 La programmation logique propositionnelle . . . . . . . . . . . . . . . 65
3.4.8 Prolog propositionnel . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
3.5 Quelques exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.1 Argumentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.2 Analyse de formules . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
3.5.3 Problèmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
3.6 La méthode de résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.6.1 Formes normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.6.2 La règle de résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.6.3 Complétude de la méthode de résolution . . . . . . . . . . . . . . . . . 81
3.6.4 Procédure de résolution . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.7 Exercice de récapitulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
3.7.1 Méthode directe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
3.7.2 Méthode algébrique . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
3.7.3 Tableau sémantique (notation réduite) . . . . . . . . . . . . . . . . . . 87
3.7.4 Réduction à la forme conjonctive . . . . . . . . . . . . . . . . . . . . 87
3.7.5 Résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
3.7.6 Résolution généralisée . . . . . . . . . . . . . . . . . . . . . . . . . . 88
3.7.7 Méthode ad-hoc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
iii
5 Logique prédicative : syntaxe et sémantique 102
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.2 Syntaxe du calcul des prédicats simplifié . . . . . . . . . . . . . . . . . . . . . 104
5.2.1 Lexique, termes et formules . . . . . . . . . . . . . . . . . . . . . . . 104
5.2.2 Portée des quantificateurs, variable libre, variable liée . . . . . . . . . . 105
5.2.3 Fermetures universelle et existentielle . . . . . . . . . . . . . . . . . . 107
5.3 Sémantique du calcul des prédicats . . . . . . . . . . . . . . . . . . . . . . . . 107
5.3.1 Interprétations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.3.2 Règles d’interprétation . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.3.3 Capture de variable . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.3.4 Satisfaction, modèle . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3.5 Quelques formules valides importantes . . . . . . . . . . . . . . . . . 109
5.3.6 Conséquence logique, équivalence logique . . . . . . . . . . . . . . . 110
5.4 Le théorème de compacité . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
iv
7.3.6 Forme clausale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
7.4 Théorie de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
7.4.1 Domaines de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . 139
7.4.2 Interprétations, bases et modèles de Herbrand . . . . . . . . . . . . . . 139
7.4.3 Simplification de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . 140
7.4.4 Théorèmes de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . 140
7.4.5 Analyse de formes clausales . . . . . . . . . . . . . . . . . . . . . . . 142
7.4.6 Analyse de règles d’inférence . . . . . . . . . . . . . . . . . . . . . . 143
7.5 Résolution fondamentale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
7.5.1 Procédure de résolution fondamentale . . . . . . . . . . . . . . . . . . 145
7.5.2 Preuve du théorème de compacité . . . . . . . . . . . . . . . . . . . . 145
v
Avant-propos
1
Soient A, B , X et Y des formules quelconques.
On pose A′ =def (X ⇒ (A ⇒ Y )) et B ′ =def (X ⇒ (B ⇒ Y )).
Si A ⇒ B est vrai, que peut-on dire de B ⇒ A, de A′ ⇒ B ′ et B ′ ⇒ A′ ?
et
Quel lien logique y a-t-il entre les formules
∀x ∀y (P (x) ⇒ Q(y)) et ∃x P (x) ⇒ ∀x Q(x) ?
Nous n’avons naturellement pas d’explication définitive à ce problème, et encore moins
de remède infaillible, mais on peut néanmoins explorer quelques pistes. Tout d’abord, les trois
points cités plus haut, bien qu’objectivement favorables, ne sont pas dépourvus d’effets pervers.
– La facilité de la matière peut susciter trois types de réactions négatives. Tout d’abord,
“si c’est trop simple, ce n’est pas utile”. Les applications non triviales de la logique
sont pourtant nombreuses, mais le temps manque parfois pour les aborder. Ensuite, et
cela surtout à propos de la logique propositionnelle, “pourquoi vouloir formaliser et
théoriser à propos d’une arithmétique simpliste, limitée à 0 (faux) et 1 (vrai) ?”. Enfin,
la facilité conduit à l’imprudence, qui elle-même mène à l’erreur ! La logique renferme
quand même quelques pièges . . .
– Les bons livres existent, sans aucun doute, mais ne correspondent pas toujours aux
attentes et besoins du lecteur. Un simple exposé du type “hypothético-déductif”
habituellement utilisé en mathématique ne convient pas, même si paradoxalement la
logique élémentaire s’y prête très bien. Ce genre d’exposé se lit avec peu d’effort mais
conduit seulement à une compréhension passive des concepts, et non à une maı̂trise
active de l’outil qu’est la logique pour un informaticien. En outre, un tel exposé ne
donne pas de justification à l’existence même de la logique mathématique et ne fera
qu’amplifier les réactions négatives évoquées plus haut.
– Notons enfin que la maturité mathématique de l’apprenant ne s’accompagne pas toujours
d’une motivation pour aborder une nouvelle branche des mathématiques . . .
Quelques solutions. Les remèdes existent. Une approche historique et philosophique des
concepts [L1] est un excellent moyen de contrer les réactions négatives, en montrant que
beaucoup d’efforts ont été nécessaires pour aboutir aux concepts simples et épurés sur lesquels
se base la logique moderne. Elle montre aussi que les progrès réalisés au cours des siècles
l’ont souvent été à l’occasion de problèmes concrets ; on voit enfin que la formalisation de
l’expression des raisonnements a été la voie royale conduisant à une meilleure compréhension
de ceux-ci. L’inconvénient de cette approche est qu’elle allonge grandement la taille de
l’exposé, surtout si on le complète d’une introduction à des problèmes de nature informatique
[L2] auxquels la logique apporte une solution partielle ou complète. Tout en restant persuadé
de l’intérêt pédagogique d’une approche historique et philosophique de cette matière, nous
devons admettre qu’elle est peu compatible avec la durée maximale de 30 heures prévue au
programme (travaux pratiques non compris), surtout pour des auditeurs fortement sollicités par
ailleurs.
Un moyen radical de balayer les objections de simplicité et d’inutilité est de dépasser
quelque peu la matière reconnue comme indispensable à l’informaticien, et d’aborder
quelques grands problèmes tels l’incomplétude et l’indécidabilité de l’arithmétique, ou
l’indécidabilité de la logique prédicative, conduisant à de sévères limitations dans les domaines
2
de l’algorithmique, de la démonstration automatique et des systèmes experts, notamment. On
obtient alors un cours de mathématique plutôt volumineux et difficile, dont l’introduction dans
un curriculum de sciences appliquées serait malaisée à justifier. (Recommandons néanmoins
[CL] et [BM] à l’amateur.) L’effort à fournir par l’étudiant peu habitué à l’algèbre et aux
mathématiques abstraites devient alors lourd, même quand l’auteur s’ingénie avec succès à
motiver tout résultat et à en donner une bonne intuition avant d’en exposer une démonstration
rigoureuse [S].
Il semble donc que les problèmes liés à l’enseignement de la logique se résolvent surtout
par des développements supplémentaires, dont le simple volume peut rebuter l’étudiant.
Signalons quand même que peu de domaines progressent aussi rapidement que la logique pour
l’informatique ; le “Handbook of Logic in Computer Science” comporte six volumes, dont le
premier contient plus de 800 pages [AGM].
En dépit de cette inquiétante inflation, on constate que la partie de la logique mathématique
réellement nécessaire à l’informaticien est plutôt réduite, et peut aisément s’exposer en
30 heures et s’assimiler concrètement et pratiquement en 30 heures supplémentaires . . . à
condition de respecter une stricte discipline. Une double comparaison va nous permettre de
préciser ce point. L’étudiant en sciences appliquées apprend, assimile et utilise une grande
quantité de théorèmes d’analyse mathématique, à propos de fonctions réelles et complexes,
d’intégrales et d’équations différentielles, de transformées de Laplace et de Fourier, etc. En
contrepartie, si l’on peut dire, l’assimilation n’est pas toujours très profonde. On mémorise,
ou on sait où retrouver, les formules d’intégration et de transformation de fonctions, mais on
s’interroge moins, ou avec moins de succès, sur les conditions de validité de ces formules.
Le plus souvent, il n’y a pas de conséquences fâcheuses, mais parfois un résultat aberrant
sera admis sans hésitation. A l’opposé, l’étudiant n’utilise que peu de résultats d’arithmétique,
et presque exclusivement des résultats élémentaires ; cependant, il est parfaitement “à l’aise”
dans ce petit domaine ; en particulier, sa perception intuitive des nombres lui permettra le plus
souvent de détecter un résultat aberrant (dû à une erreur de signe, d’un facteur 10, etc.).
Le point crucial est que l’étudiant doit assimiler la logique élémentaire comme
l’arithmétique élémentaire ; il doit pouvoir “doubler” le raisonnement méthodique et rigoureux
par une compréhension intuitive des formules. Il doit arriver, par exemple, à rejeter l’énoncé
de logique (incorrect !)
Si A ⇒ B est vrai, alors (X ⇒ (A ⇒ Y )) ⇒ (X ⇒ (B ⇒ Y )) est vrai.
aussi rapidement que l’énoncé algébrique (incorrect !)
Si a ≤ b est vrai, alors (y − a) − x ≤ (y − b) − x est vrai.
En mathématique, il est extrêmement pénible de mémoriser des démonstrations vues comme
des textes linéaires dont tous les mots ont la même importance. Il est de loin préférable
d’associer à un théorème un objet concret (au sens large) à partir duquel on peut reconstituer
aisément la démonstration du théorème.
Le dessin de gauche de la figure 1 comporte deux carrés intérieurs dont les dimensions
sont a et b ainsi que deux rectangles de côtés a et b. Ce dessin illustre notamment la formule
(a + b)2 = a2 + 2ab + b2 . Le dessin de droite comporte un carré intérieur de dimension c, ainsi
que quatre triangles rectangles de petits côtés a et b et d’hypoténuse c. L’aire totale des deux
rectangles étant égale à celle des quatre triangles, l’aire totale a2 + b2 des deux carrés intérieurs
3
✟✟❆
✟✟ ❆
a a
✟✟ ❆
✟✟ ❆
❆ ❆
❆ ❆
❆ ❆
b ❆c ❆
b ❆ ✟ ✟
✟
❆ ✟✟
❆ ✟✟
a ❆✟
F IG . 1 – Clef du théorème de Pythagore.
à gauche est égale à l’aire c2 du carré intérieur à droite. Cette dernière égalité est le théorème
de Pythagore.
Deux pistes prometteuses . . . Ce genre d’objet (ici, une paire de dessins) est naturellement
très utile, mais il n’est pas évident de le découvrir. C’est cependant moins difficile en logique
formelle qu’en algèbre ou en analyse, et notre principal objectif, en écrivant ce texte, est de
montrer comment ces objets peuvent être découverts et utilisés ; ce seront souvent des objets
bien connus de l’informaticien, tels les tableaux, les listes et les arbres. Nous essayerons
aussi d’arithmétiser la logique, ce qui permet d’importer en logique l’expérience et l’intuition
acquises en arithmétique élémentaire. En particulier, les démonstrations paraı̂tront simples au
lecteur qui observera leur caractère constructif et inductif. Le plus souvent, une démonstration
donne lieu à un programme (récursif) construisant l’objet dont le théorème démontré affirme
l’existence.
4
1 Introduction
Dans ce bref chapitre, on présente les objectifs de la logique. On montre certaines analogies
existant entre la logique et l’arithmétique. On montre l’utilité de la logique pour une meilleure
compréhension des théorèmes et des programmes, et aussi pour l’écriture même de certains
programmes.
Raisonnement et calcul. Le raisonnement est proche du calcul, qui lui aussi transforme
l’information. Etant donné un triangle dont la base et la hauteur sont de 6 cm (information
préexistante), on sait que l’aire du triangle est de 18 cm2 (“nouvelle” information). Le
mécanisme de production est la règle classique S = (B × H)/2.
La logique la plus simple est celle des propositions. Il s’agit bien d’un calcul, dans lequel
les objets ne sont pas les nombres et les expressions numériques, mais les valeurs de vérité
(“vrai” et “faux”) et les propositions et formules susceptibles d’être vraies ou fausses. Voici un
exemple typique de ce calcul. L’information préexistante comporte deux énoncés :
Pour sortir sous la pluie, je prends mon parapluie.
Je suis dehors sans parapluie.
Le mécanisme de calcul, ou plutôt de déduction, est le suivant
A ⇒ B , ¬B
¬A
“Si A implique B est vrai, et si B est faux, alors A est faux.” L’information nouvelle que l’on
peut obtenir ici est “Il ne pleut pas”. On a instancié A en “il pleut” et B en “je sors muni d’un
parapluie”.
On notera l’emploi de la convention habituelle : la ligne horizontale sépare les prémisses d’un
raisonnement (au-dessus de la ligne) et sa conclusion (au-dessous de la ligne).
5
de ce type peut rapidement devenir douteuse.1 Toutefois, ce problème est du ressort de la
linguistique et nous ne l’aborderons pas ici. Plus précisément, nous ne considérerons pas de
raisonnement dont la formalisation ne soit élémentaire, voire même déjà faite. L’objet de la
logique mathématique sera donc la représentation et l’analyse des raisonnements formalisés. A
titre d’exemple, considérons les tables de la négation et de l’implication :
x y x⇒y
x ¬x V V V
V F V F F
F V F V V
F F V
A B A⇒B ¬B ¬A
V V V F F
V F F V F
F V V F V
F F V V V
Valider le mécanisme de raisonnement utilisé dans notre exemple (c’est le “Modus Tollens”)
consiste à vérifier que, dans tous les cas où les deux prémisses A ⇒ B et ¬B sont vraies,
la conclusion ¬A est également vraie. Dans les trois premières lignes du tableau, l’une des
prémisses est fausse. Ces lignes correspondent à des cas où le Modus Tollens ne s’applique
pas. La quatrième ligne correspond au cas où les deux prémisses sont vraies, c’est-à-dire au
cas où le mécanisme de raisonnement étudié s’applique ; on observe que la conclusion est
également vraie, ce qui achève la vérification.
Trop simple, la logique ? On peut se demander à quoi sert la logique en tant que science,
puisqu’elle ne recouvre, dans le contexte élémentaire dont nous ne sortirons pas, que des
connaissances évidentes. Nous aurons amplement l’occasion de souligner plus loin qu’il est
certaines évidences méritant d’être soulignées mais, pour l’informaticien en particulier, l’utilité
de la logique est du même ordre que celle de l’arithmétique. Cette utilité est liée à la dimension
des problèmes traités, et à l’intérêt, au delà d’une certaine taille très vite atteinte, d’automatiser
la résolution de ces problèmes. On “produit” (6 × 6)/2 = 18 sans effort, mais il n’en va
pas de même pour 345 234 × 765 864 = 264 402 292 176 ; on utilisera ici une calculatrice, ou
un ordinateur dont la programmation a requis la mise en œuvre de règles arithmétiques bien
formalisées. Plus peut-être que la taille des problèmes, c’est leur généralisation qui requiert
Pn L’égalité 1 + 2 + · · · + 10 = 55 présente un intérêt nettement
l’élaboration d’une science.
moindre que l’égalité i=1 i = (n × (n + 1))/2. Cette égalité ne se déduit pas seulement
de tables arithmétiques, si détaillées soient-elles ; une “science” arithmétique est nécessaire. Il
1
Même dans notre exemple, certains problèmes surgissent. En particulier, il peut avoir commencé à pleuvoir
après que je sois sorti (sans parapluie) ; je peux aussi égarer mon parapluie en cours de route.
6
en va de même en logique, où l’on formalise des règles générales, telle la classique règle de
récurrence :
P (0) , ∀n [P (n) ⇒ P (n + 1)]
∀n P (n)
L’effet de dimension est également présent en logique, comme en témoignent deux petites
énigmes amusantes.
1. Les étudiants ayant participé à l’examen de logique diffèrent par le le prénom, la
nationalité et le sport favori pratiqué par chacun d’eux. On demande de reconstituer
le classement et de déterminer qui est le Français et quel est le sport pratiqué par
Richard, sur base des indices suivants.
1. Il y a trois étudiants.
2. Michel joue au football.
3. Michel est mieux classé que l’Américain.
4. Simon est Belge.
5. Simon a surclassé le joueur de tennis.
6. Le nageur s’est classé premier.
Mieux comprendre les théorèmes. La logique formelle a été au départ développée par
des mathématiciens, pour éclairer divers problèmes délicats survenant en algèbre, en analyse,
en géométrie, etc. Ce point n’a pas tellement d’intérêt pour l’informaticien, mais il importe
2
Si on n’est pas habitué à résoudre ce type d’énigme, on peut s’attendre à une demi-heure de tâtonnement
avant de découvrir la solution de la seconde, même si une minute suffit pour la première . . .
7
de reconnaı̂tre d’emblée le statut acquis par la logique mathématique : elle contribue au
développement d’autres branches des mathématiques et favorise une meilleure compréhension
de celles-ci. Inversement, une certaine maturité mathématique favorise l’apprentissage de la
logique.
Nous ne donnerons ici qu’un exemple de la symbiose entre logique et mathématique, mais
il est capital. Dans n’importe quelle branche des mathématiques, un théorème évoque une
catégorie d’objets et affirme que tout objet vérifiant l’hypothèse vérifie aussi la thèse. Ceci est
un exemple typique d’évidence qu’il est opportun de souligner. Dans le domaine Z des entiers
relatifs, on a le théorème suivant :
Tout carré est positif.
La paraphrase suivante donne lieu à une traduction immédiate :
Pour tout n, n est un carré implique n est positif.
On peut en effet formaliser l’énoncé en
∀n [C(n) ⇒ P (n)] .
C-P 0, 1, 4, . . . , 100, . . .
C-nP
nC-P 2, 3, 5, . . . , 99, 101, . . .
nC-nP −1, −2, −3, . . . , −100, . . .
Cela illustre la règle logique disant qu’une implication p ⇒ q est fausse si et seulement
si l’antécédent p est vrai et le conséquent q est faux.3 En particulier, une implication dont
l’antécédent est faux est toujours vraie. Par exemple, l’énoncé “si 2+2=5, alors 2+2=6” est
vrai, ce qui ne l’empêche pas d’être sans intérêt pratique.
Cette écriture exprime une relation utile entre la donnée x0 et le résultat F . La logique permet
aussi de donner un argument de conformité entre le programme et sa spécification, par exemple
un invariant de boucle ; cet invariant est ici
x, x0 , y ∈ N ∧ 0 ≤ x ≤ x0 ∧ y ∗ x! = x0 !
3
Le théorème affirme que la seconde des quatre classes est vide ; il n’interdit pas qu’éventuellement une des
trois autres classes soit vide aussi.
8
Enfin, la logique permet de vérifier la validité de l’argument. Un élément crucial de cette
vérification est le fait que le corps de la boucle, lorsqu’il est exécuté, restaure l’invariant. En
appelant cet invariant I, on doit avoir
ou encore
(I ∧ x > 0) ⇒ I[y, x / y∗x, x−1]
où I[y, x / y∗x, x−1] désigne la formule I dans laquelle on a remplacé les occurrences de y et
de x par y ∗ x et x − 1, respectivement. En définitive, pour établir que le programme est correct,
il faut prouver que la formule
est vraie, ce qui peut se faire en utilisant les propriétés arithmétiques usuelles, notamment
l’associativité de la multiplication et le fait que n ∗ (n − 1)! = n! pour tout entier n strictement
positif. Le fait que la logique soit plutôt simple rend possible l’automatisation du raisonnement,
qui est vu comme un calcul d’un genre particulier. La logique est donc une clef de l’intelligence
artificielle et permet en particulier la programmation de systèmes experts, aptes à la résolution
automatique d’énigmes comme celle du zèbre ou, d’une manière moins ludique, à l’élaboration
de diagnostic de pannes dans les réseaux informatiques, pour ne donner qu’un exemple.
Un algorithme est une recette de calcul permettant de résoudre un problème sans devoir
réfléchir. Toute la réflexion nécessaire a été anticipée par l’auteur de l’algorithme, ce qui
explique la difficulté potentielle de la tâche du concepteur d’algorithme. Un programme de
calcul implique des règles de calcul et la mise en œuvre de ces règles. Dans un programme
classique, tel celui calculant la factorielle, ces deux ingrédients sont intimement mélangés,
et les règles mathématiques de base qui ont été utilisées (l’associativité de la multiplication,
par exemple) n’apparaissent explicitement que lors d’une vérification systématique et détaillée
de l’exactitude de l’algorithme. Dans la mesure où calcul et raisonnement ne sont que deux
facettes d’un même processus, on peut envisager de séparer les deux ingrédients. Un algorithme
de mise en œuvre de règles logico-mathématiques est écrit une fois pour toutes, et cet
algorithme est particularisé à un problème particulier par l’adjonction des règles relatives à ce
problème. Cette technique de “programmation (par la) logique” est très puissante, notamment
dans les cas où la programmation classique est décevante. Dans ce contexte, pour trier un
tableau X en un tableau Y , il suffira de donner deux “indices” :
Y est une permutation de X ;
les éléments de Y forment une suite croissante.
Trier de cette manière sera cependant très inefficace. Dans le même contexte de programmation
logique, il suffira de donner les indices et la question de l’énigme évoquée plus haut pour
résoudre celle-ci. Dans la mesure où on ne connaı̂t pas d’algorithme classique de résolution
d’énigme, l’approche logique est ici très attrayante.
Programmer en logique. Puisque la logique est, dans une certaine mesure, un calcul, elle
peut donner naissance à un langage de programmation. Le langage PROLOG (“PROgrammer
en LOGique”) est le plus utilisé des langages basés sur la logique. En dépit de certaines
9
limitations, il se prête bien à la résolution d’une vaste classe de problèmes. A titre d’exemple,
nous donnons à la page suivante un programme PROLOG pour la résolution de l’énigme du
zèbre donnée plus haut. Ce programme décrit d’une part ce qu’est une énigme et, d’autre part,
les particularités de l’énigme du zèbre. Le système PROLOG calcule la réponse en utilisant les
algorithmes de résolution et d’unification, présentés à la fin de ce cours.
one(A,[A,B,C,D,E]).
three(C,[A,B,C,D,E]).
neighbor(A,B,[A,B,C,D,E]). neighbor(B,C,[A,B,C,D,E]).
neighbor(C,D,[A,B,C,D,E]). neighbor(D,E,[A,B,C,D,E]).
neighbor(B,A,[A,B,C,D,E]). neighbor(C,B,[A,B,C,D,E]).
neighbor(D,C,[A,B,C,D,E]). neighbor(E,D,[A,B,C,D,E]).
nation(h(N,C,A,B,T),N).
color(h(N,C,A,B,T),C).
animal(h(N,C,A,B,T),A).
drink(h(N,C,A,B,T),B).
tobacco(h(N,C,A,B,T),T).
go(X,Y) :- St = [h(N1,C1,A1,B1,T1),h(N2,C2,A2,B2,T2),
h(N3,C3,A3,B3,T3),h(N4,C4,A4,B4,T4),h(N5,C5,A5,B5,T5)],
member(X2,St), nation(X2,english), color(X2,green),
member(X3,St), nation(X3,spanish), animal(X3,dog),
member(X4,St), color(X4,red), drink(X4,coffee),
member(X5,St), nation(X5,ukrainian), drink(X5,tea),
neighbor(X6a,X6b,St), prc(X6b,X6a,St), color(X6a,red), color(X6b,white),
member(X7,St), tobacco(X7,oldgold), animal(X7,snails),
member(X8,St), color(X8,yellow), tobacco(X8,gauloises),
three(X9,St), drink(X9,milk),
one(X10,St), nation(X10,norwegian),
neighbor(X11a,X11b,St), tobacco(X11a,chesterfield), animal(X11b,fox),
neighbor(X12a,X12b,St), tobacco(X12a,gauloises), animal(X12b,horse),
member(X13,St), tobacco(X13,luckystrikes), drink(X13,orangejuice),
member(X14,St), nation(X14,japanese), tobacco(X14,gitanes),
neighbor(X15a,X15b,St), nation(X15a,norwegian), color(X15b,blue),
member(Q,St), animal(Q,zebra), nation(Q,X),
member(R,St), drink(R,water), nation(R,Y).
On observe que ce texte ressemble plus à une variante de l’énoncé du problème qu’à un
programme pour résoudre le problème. Il n’est en fait qu’une donnée pour la version Prolog
des algorithmes de résolution et d’unification.
Le texte est composé de clauses qui décrivent des prédicats. Il y a deux sortes de clauses :
a.
a :- b,c,d.
10
La première exprime un fait (axiome, postulat, définition). Elle peut se lire “On a a” ou
“a est (toujours) vrai”. La seconde clause exprime une règle, la possibilité d’obtenir le fait a à
partir des faits b, c et d. On peut lire “Si b, c et d sont vrais, alors a est vrai”, ou encore “Pour
avoir (établir) a, il suffit d’avoir (d’établir) b, c et d”.
Les clauses préliminaires constituent des définitions auxiliaires, pour les notions de
précédence (une maison précède une autre si le numéro de la première est plus petit que celui
de la seconde), de première maison, de maison du milieu et de maisons voisines. On note par
exemple que, dans une structure de cinq éléments [A,B,C,D,E], les maisons A et B sont
mitoyennes, de même que B et A, B et C, . . . et enfin D et E. On précise aussi qu’une maison
est décrite par cinq attributs qui sont, dans l’ordre, la nationalité du propriétaire, la couleur de
la façade, l’animal familier, la boisson favorite et la marque de tabac.
La clause principale définit le prédicat go. Les cinq premières lignes correspondent à
l’indice 1 ; les lignes suivantes correspondent aux quatorze autres indices, sauf les deux
dernières lignes qui correspondent aux deux questions. A titre d’exemple, voici une paraphrase
du dernier indice : “la structure St comporte deux maisons mitoyennes X15a et X15b telles
que l’occupant de X15a est de nationalité norvégienne, et que X15b est de couleur bleue”.
La première question se traduit en “la structure St comporte une maison (inconnue) Q, dont
l’occupant est de nationalité X et possède un zèbre”.
L’exécution de ce programme est représentée ci-dessous.
?- go(ZebraOwner,WaterDrinker).
ZebraOwner = japanese
WaterDrinker = norwegian ? ;
no
Le “no” indique l’absence d’une seconde solution ; sur base des indices, il est donc certain que
le Japonais possède le zèbre et que le Norvégien boit de l’eau.
Notre but n’est pas ici de présenter Prolog, mais de montrer que les algorithmes logiques
que nous étudierons sont suffisamment puissants pour prendre en charge la résolution d’un
problème non trivial. Ces algorithmes sont préprogrammés efficacement et une fois pour toutes
dans le système Prolog, mais peuvent naturellement être programmés dans n’importe quel
langage ; nous verrons d’ailleurs comment, aux chapitres trois et cinq.
Nous terminons ce chapitre par une très brève introduction aux deux algorithmes utilisés
par Prolog. Considérons le petit programme suivant.
a.
b.
c :- a.
d :- a,f.
d :- b,c.
e :- c,f.
{A , B , A ⇒ C , (A ∧ F ) ⇒ D , (B ∧ C) ⇒ D , (C ∧ F ) ⇒ E} .
11
La dernière formule, par exemple, signifie que si C et F sont vrais, alors E est vrai. Essayons,
sur base de nos six clauses, de voir si D est vrai, et si E est vrai. Pour avoir D, d’après la
cinquième clause,4 il suffit d’avoir B et C. On a B (deuxième clause) et, pour avoir C, il
suffit (troisième clause) d’avoir A, que l’on a par la première clause. La réponse à la première
question est donc “oui”. D’autre part, pour avoir E, il suffit d’avoir C et F . On a bien C (on
a vu comment), mais aucune clause ne permet d’espérer obtenir F . La réponse à la seconde
question est donc “non”. Ces raisonnements, illustrés à la figure 2, sont des exemples typiques
de ce qu’étudie la logique des propositions, abordée aux chapitres deux et trois. Les numéros
des nœuds des arbres de la figure 2 indiquent l’ordre dans lequel ces nœuds sont créés et
exploités.
0♠d 0♠e
✜ ❭
✜ ❭
✜ ❭
✜ ❭
1♠a,f 3♠b,c 1♠c,f
12
0♠append(Xs, Ys, [a, b]) ?
✜ ▲
✜ ▲
✜ ▲
✜
Xs, Ys, Ys 1 ← [ ], [a, b], [a, b]▲ Xs, Ys, X 1 , Zs 1 ← [a|Xs 1 ], Ys 1 , a, [b]
▲
✜ ▲
✜ ▲
✜ ▲
✜ ▲
1♠ 2♠append(Xs 1 , Ys 1 , [b]) ?
✜ ▲
{Xs, Ys = [ ], [a, b]} ✜ ▲
✜ ▲
✜
Xs 1 , Ys 1 , Ys 2 ←✜ [ ], [b], [b] ▲ Xs 1 , Ys 1 , X 2 , Zs 2 ← [b|Xs 2 ], Ys 2 , b, [ ]
▲
✜ ▲
✜ ▲
✜ ▲
✜ ▲
3♠ 4♠append(Xs 2 , Ys 2 , [ ]) ?
✜
{Xs, Ys = [a], [b]} ✜
✜
✜ 2 2 3
✜ Xs , Ys , Ys ← [ ], [ ], [ ]
✜
✜
✜
✜
5♠
{Xs, Ys = [a, b], [ ]}
13
3. π > e.
4. Il n’existe que cinq polyèdres réguliers convexes.
5. Il existe une infinité de nombres premiers x tels que x + 2 est aussi premier.
6. Le procompsognathus est un deutérostomien anamniote.
7. Il fera beau à Liège le 29 avril de l’an 2021.
8. x2 + y 2 = z 2 .
9. Il pleut.
10. Je donne cours de logique le mardi.
11. Je donne cours(matière, jour).
12. Un plus deux égalent trois et la terre tourne autour du soleil.
13. Un plus deux égalent trois parce que la terre tourne autour du soleil.
14. Cette phrase est fausse.
15. La phrase suivante est vraie.
16. La phrase précédente est fausse.
17. Ceci n’est pas une phrase.
18. Cette phrase n’est pas une proposition.
14
Ce phénomène est lié à l’autoréférence : ces phrases parlent d’elles-mêmes. Les exemples 17
et 18 montrent que l’autoréférence n’implique pas toujours le paradoxe : il s’agit bien de deux
propositions, toutes deux fausses.
En arithmétique, on distingue les énoncés valides, qui sont toujours vrais, les énoncés
inconsistants, ou contradictoires, qui sont toujours faux, et les énoncés contingents, ou
simplement consistants, qui sont vrais ou faux selon le contexte, c’est-à-dire selon les valeurs
que l’on attribue aux variables qu’ils contiennent. Un énoncé valide peut contenir des variables,
tel x2 + y 2 ≥ 2xy ou n’évoquer que des constantes, tel 2 + 3 = 5. Il en va de même pour les
énoncés inconsistants (x2 +y 2 < 2xy, 2+3 = 6). En revanche, un énoncé contingent comporte
toujours une variable au moins (x < 3).
La même classification sera adoptée en logique propositionnelle. Les énoncés true et
false ⇒ p sont valides ; seul le second comporte une variable propositionnelle. L’énoncé p ⇒ q
est contingent, tandis que l’énoncé true ⇒ false est contradictoire.
Deux différences essentielles existent entre la logique et l’arithmétique. Tout d’abord, il
n’existe que deux valeurs en logique, contre une infinité en arithmétique ; de plus, la notion
de proposition existe en arithmétique (les énoncés arithmétiques sont des propositions, au
même titre que les énoncés de mécanique des fluides, par exemple), alors que la notion de
nombre n’apparaı̂t pas en logique propositionnelle. En fait, la logique “précède” l’arithmétique,
car on ne peut pas faire d’arithmétique sans faire, consciemment ou non, de la logique. En
contrepartie, l’arithmétique est “plus riche” que la logique ; on pourra identifier le calcul des
propositions à un calcul numérique particulier, mais on ne pourra pas identifier le calcul sur les
nombres à une logique propositionnelle particulière.
5
D’après Larousse, la logique est la “science du raisonnement en lui-même, abstraction faite de la matière à
laquelle il s’applique et de tout processus psychologique”.
15
2.1.2 Généralités sur les connecteurs
Les opérateurs combinant les propositions sont appelés connecteurs. La logique des
propositions est en fait la logique des connecteurs, comme l’arithmétique est plus la science
des opérations (addition et multiplication surtout) que celle des nombres proprement dits.
Les opérations de l’arithmétique (au sens large) sont des fonctions dont les arguments (en
général, un ou deux) prennent des valeurs numériques ; la valeur du résultat est numérique, ou
une valeur de vérité. Voici quelques opérations courantes :
– L’addition : + : Z × Z −→ Z : (x, y) 7→ x + y.
– Le passage à l’opposé : − : Z −→ Z : x 7→ −x.
– La divisibilité : | : Z × Z0 −→ {V, F} : (x, y) 7→ x|y.
– La primarité : Pr : N0,1 −→ {V, F} : x 7→ Pr(x).
Rappelons que, si x est un nombre entier plus grand que 1, Pr(x) est vrai si x est premier,
c’est-à-dire n’est divisible que par lui-même et par 1.
Il existe une infinité d’opérations arithmétiques, et le mathématicien s’autorisera à en créer une
nouvelle, qu’il nommera et notera de manière appropriée, dès que le besoin s’en fera sentir.
Toutefois, quand on étudie l’arithmétique, on se limite généralement à une demi-douzaine
d’opérations. On retient, d’une part, celles dont l’intérêt pratique est évident et, d’autre part,
celles dont les propriétés sont les plus attrayantes et les plus élégantes. Ces deux critères sont
souvent concordants ; de plus, les opérations non retenues comme primitives peuvent souvent
se dériver des opérations primitives . . . au moyen de la logique. On définit par exemple la
divisibilité (ne pas confondre avec la division) à partir de l’égalité et de la multiplication :
x|y =def ∃z (x.z = y) .
On se sert de cette nouvelle opération pour définir la primarité :
Pr(x) =def x > 1 ∧ ∀y [y|x ≡ (y = 1 ∨ y = x)] .
En logique propositionnelle aussi, nous aurons des connecteurs fondamentaux et des
connecteurs dérivés.
Notons aussi que certaines “opérations” arithmétiques ne sont pas considérées comme
telles par les mathématiciens, parce qu’elles dépendent non seulement des nombres eux-mêmes
mais aussi de points annexes, par exemple le formalisme utilisé pour les représenter. Ainsi, la
“longueur” d’un nombre n’est pas une véritable opération arithmétique, puisqu’elle n’est pas
“numérifonctionnelle” :
ℓ(13) = 2 ,
ℓ(6 + 7) = 3 ,
ℓ(78/6) = 4 ,
ℓ(II0I) = 4 ,
ℓ(treize) = 6 ,
ℓ(thirteen) = 8 ,
ℓ(XIII) = 4 .
En logique aussi, les connecteurs non “vérifonctionnels” seront éliminés.
Les connecteurs propositionnels sont nombreux dans la langue française ; nous en avons
rencontré deux exemples :
16
– Un plus deux égalent trois et la terre tourne autour du soleil.
– Un plus deux égalent trois parce que la terre tourne autour du soleil.
Le connecteur et est vérifonctionnel : la proposition “A et B” sera vraie si et seulement si
les propositions “A” et “B” sont toutes deux vraies. En revanche, il n’est pas évident d’établir
un éventuel lien de cause à effet entre deux faits, et connaı̂tre les valeurs de vérité de “A” et
de “B” ne permet généralement pas de connaı̂tre la valeur de vérité de “A parce que B”. Les
propositions composées suivantes, dont nous supposons les composantes vraies, montrent que
le connecteur “parce que” n’est pas vérifonctionnel :
– La voiture dérape parce que la route est mouillée.
– La route est mouillée parce que la voiture dérape.
Dans un contexte où une voiture a dérapé sur une route mouillée, la première proposition
composée semble vraie mais la seconde est quasi certainement fausse. Or, les deux propositions
simples contenues dans les propositions composées sont vraies ; cela montre que la valeur de
vérité d’une proposition composée avec “parce que” ne dépend pas uniquement des valeurs de
vérité des composantes.
Voici quelques exemples d’emploi des connecteurs vérifonctionnels les plus fréquemment
utilisés en français.
– J’irai au théâtre ou bien j’irai au cinéma.
– Il pleut ou il vente.
– S’il pleut, alors la route est mouillée.
– Le ciel est bleu et la neige est blanche.
– Il n’est pas bête.
– Si c’est pile alors je gagne sinon tu perds !
– Elle réussit si elle travaille.
– Elle réussit seulement si elle travaille.
– Elle réussit si et seulement si elle travaille.
– Elle travaille, donc elle réussit.
– [Ils n’ont] ni Dieu, ni maı̂tre !
Dans ces exemples, la valeur de vérité de la proposition composée se déduit aisément de
la valeur de vérité des composants ; les connecteurs sont donc bien vérifonctionnels. Dans ce
cadre, il est possible de rendre compte de la validité de certains raisonnements, tel le suivant :
1. Tous les hommes sont mortels.
2. Si tous les hommes sont mortels et si Socrate est un homme,
alors Socrate est mortel.
3. Socrate est un homme.
4. Donc, Socrate est mortel.
Ce raisonnement est une instance, c’est-à-dire un exemple, du schéma
A , (A ∧ B) ⇒ C , B
C
17
et nous verrons plus loin que toutes les instances de ce schéma (qui comporte trois prémisses
et une conclusion) sont valides. On observe cependant que, en bonne logique (informelle) la
prémisse
2. Si tous les hommes sont mortels et si Socrate est un homme,
alors Socrate est mortel.
semble redondante, car elle exprime une tautologie, c’est-à-dire une évidence. Comme nous
l’avons signalé plus haut, le problème est que la validité du raisonnement
1. Tous les hommes sont mortels.
3. Socrate est un homme.
4. Donc, Socrate est mortel.
ne peut pas être établie dans le cadre du calcul des propositions mais seulement dans celui,
plus puissant, du calcul des prédicats. Notons enfin que, ici aussi, des curiosités linguistiques
peuvent compliquer l’emploi de la logique en langage naturel. Voici un exemple classique de
raisonnement qui, formellement, pourrait sembler valide mais qui, clairement, ne l’est pas.
1. Jacques est un personnage intelligent.
2. Un personnage intelligent a découvert la relativité.
3. Donc, Jacques a découvert la relativité.
En voici un autre :
1. Tout ce qui est rare est cher.
2. Une Rolls-Royce bon marché est rare.
3. Donc, une Rolls-Royce bon marché est chère.
Le calcul des prédicats classique ne pourra pas rendre compte de ces problèmes, qui sont plus
du ressort de la linguistique que de la logique.
18
x ◦1 ◦2 ◦3 ◦4
V V V F F
F V F V F
F IG . 4 – Les quatre connecteurs unaires.
Les tables de vérité des connecteurs importants, les plus fréquemment utilisés, sont reprises
à la figure 7.
Remarque. Les symboles utilisés pour représenter les connecteurs peuvent différer d’un
ouvrage à l’autre. Nous avons adopté les notations les plus courantes ; on notera cependant
que “⊃” est souvent utilisé au lieu de “⇒” ; en Prolog, le symbole “:-” est employé à la place
de “⇐” et la virgule remplace la conjonction.
Disposer de nombreux connecteurs permet une expression facile et concise des propositions
composées, mais rend le formalisme plus complexe, et son étude plus fastidieuse. Avec la
négation et un connecteur binaire bien choisi, il est possible de tout exprimer. Supposons par
exemple, comme le font souvent les mathématiciens, que les connecteurs “primitifs” sont la
19
x y ∧ ∨ ≡ ⊕ ⇒
x ¬x V V V V V F V
V F V F F V F V F
F V F V F V F V V
F F F F V F V
F IG . 7 – Les connecteurs importants.
négation et l’implication. On peut alors introduire les autres connecteurs comme suit :
On montre facilement que {¬, ∨} et {¬, ∧} constituent aussi des “paires primitives”
acceptables, au contraire de {¬, ≡} et {¬, ⊕}. Curieusement, le connecteur binaire ↑ permet à
lui seul de définir tous les autres ; on a par exemple ¬a =def (a ↑ a) et (a ∧ b) =def ((a ↑
b) ↑ (a ↑ b)). L’opérateur ↓ est le seul autre connecteur binaire jouissant de cette propriété.
En français, l’un des rares connecteurs ternaires d’usage courant est “si-alors-sinon”. La
proposition “si A alors B sinon C” a la valeur de B si A est vrai, et celle de C si A est faux. Ce
connecteur permet lui aussi de dériver tous les autres, si on lui adjoint les constantes de base
true et false.7 Il peut lui-même s’exprimer en termes de connecteurs binaires et de la négation :
“si A alors B sinon C” a même valeur de vérité que ((A ∧ B) ∨ (¬A ∧ C)), ou encore que
((A ⇒ B) ∧ (¬A ⇒ C)).
On a aussi le résultat suivant.
Théorème. Tout opérateur n-aire (n > 2) peut se réduire à une combinaison d’opérateurs
binaires et de négations.
Remarque. En logique, les théorèmes affirmant l’existence d’un certain objet se démontrent
souvent de façon constructive ; la preuve du théorème est une méthode (un algorithme) de
construction de l’objet en question. En outre, la preuve se fait souvent par récurrence ; cela
revient à dire que l’algorithme de construction est récursif. Enfin, une fois que l’on sait cela,
il suffit de mémoriser une simple ligne pour reconstituer le détail de la preuve. Dans le cas
présent, cette ligne peut être
20
2.2 Syntaxe du calcul des propositions
2.2.1 Les règles de base
Soit Π = {p, q, r, . . .}, un lexique propositionnel, c’est-à-dire un ensemble de symboles
arbitraires appelés propositions atomiques ou atomes. La notation p ∈ Π signifie que p
appartient à Π, ou est un élément de Π. Signalons aussi que l’ensemble vide, celui qui ne
contient aucun élément, est noté ∅.
Définition. Une formule du calcul des propositions est une chaı̂ne de symboles générée par la
grammaire
formula ::= p , pour tout p ∈ Π
formula ::= true | false
formula ::= ¬formula
formula ::= (formula op formula)
op ::= ∨ | ∧ | ⇒ | ≡ | ⇐
Chaque ligne s’interprète simplement. Par exemple, si nous savons déjà que “∧” est un
opérateur (connecteur) et que “(p ⇒ q)” et “¬r” sont des formules, la quatrième ligne
nous permet de conclure que “(p ⇒ q) ∧ ¬r” est une formule. On appelle dérivation un
développement détaillé montrant qu’un assemblage de symboles est une formule.8 Voici deux
exemples de dérivations, montrant que (p ∧ q) et ((p ⇒ q) ≡ (¬q ⇒ ¬p)) sont des formules :
1. formula
2. (formula ≡ formula)
3. ((formula ⇒ formula) ≡ formula)
1. formula
4. ((p ⇒ formula) ≡ formula)
2. (formula op formula)
5. ((p ⇒ q) ≡ formula)
3. (formula ∧ formula)
6. ((p ⇒ q) ≡ (formula ⇒ formula))
4. (p ∧ formula)
7. ((p ⇒ q) ≡ (¬formula ⇒ formula))
5. (p ∧ q)
8. ((p ⇒ q) ≡ (¬q ⇒ formula))
9. ((p ⇒ q) ≡ (¬q ⇒ ¬formula))
10. ((p ⇒ q) ≡ (¬q ⇒ ¬p))
L’ordre des dérivations n’est pas total mais partiel ; il est donc naturel de représenter une
dérivation par un arbre. Les arbres de dérivation de la figure 8 montrent l’importance des
parenthèses. Deux formules peuvent ne différer que par les positions des parenthèses et avoir
des sens très différents.9
8
Formellement, cette grammaire comporte deux symboles non terminaux formula et op. Une formule est donc
un mot du langage engendré par la grammaire, dépourvu de symboles non terminaux. C’est le dernier terme d’une
dérivation dont le premier terme est le symbole non terminal distingué formula.
9
Le même phénomène se produit en arithmétique ; les expressions arithmétiques a ∗ (b + c) et (a ∗ b) + c ont
généralement des valeurs différentes.
21
⇒
ւ ց
≡ p ≡
ւ ց ւ ց
⇒ ⇒ q ¬
ւ ց ւ ց ↓
p q ¬ ¬ ⇒
↓ ↓ ւ ց
q p q ¬
↓
p
22
ses opérandes. La notation habituelle est dite infixée. Changer de notation revient à changer
l’ordre de parcours des nœuds dans l’arbre de dérivation. A titre d’exemple, les trois parcours
possibles pour les arbres de dérivation de la figure 8 sont représentés à la figure 9.
23
pair) et (A ∧ B), (A ∨ B), (A ⇒ B) et (A ≡ B) comportent α + β + 2 parenthèses (nombre
pair), d’où la conclusion.
Un propriété plus intéressante affirme que toute formule en notation infixée peut s’écrire
en notation préfixée et en notation postfixée. C’est évident pour les propositions élémentaires.
D’autre part, si les versions préfixées de A et B sont α et β, alors les versions préfixées de ¬A,
(A∧B), (A∨B), (A ⇒ B) et (A ≡ B) sont respectivement ¬α, ∧αβ, ∨αβ, ⇒αβ et ≡ αβ. Le
principe d’induction permet de conclure. On peut aussi démontrer que la traduction est unique.
24
A I(A1 ) I(A2 ) I(A)
A1 ∨ A2 F F F
A1 ∨ A2 sinon V
A1 ∧ A2 V V V
A1 ∧ A2 sinon F
A1 ⇒ A2 V F F
A1 ⇒ A2 sinon V
A1 ⇐ A2 F V F
A1 ⇐ A2 sinon V
A1 ≡ A2 I(A1 ) = I(A2 ) V
A1 ≡ A2 I(A1 ) 6= I(A2 ) F
25
uniquement des valeurs attribuées à ses composants directs. L’arbre syntaxique étant fini, on
termine en attribuant une valeur à la formule elle-même, correspondant à la racine de l’arbre.
Exemple. La fonction d’interprétation v = {(p, V), (q, F), (r, V), (s, V)} se prolonge en
une interprétation I unique sur l’ensemble de toutes les formules basées sur le lexique
Π = {p, q, r, s}. Le cas de (p ∨ s) ≡ (s ∧ q) est traité à la figure 11.
I(p) = V ,
I(s) = V ,
I(p ∨ s) = V ,
I(q) = F ,
I(s ∧ q) = F ,
I((p ∨ s) ≡ (s ∧ q)) = F
F IG . 11 – Interprétation d’une formule composée.
Remarque. Le fait que toute fonction d’interprétation v se prolonge en une et une seule
interprétation I nous autorise, en pratique, à confondre les deux notions.
Remarque. L’examen exhaustif des interprétations d’une formule composée se fait souvent au
moyen d’une table de vérité ; cette notion sera approfondie plus loin, mais nous en donnons
déjà un exemple à la figure 12. Cette table montre que la formule (p ⇒ q) ⇒ (¬q ⇒ ¬p) est
vraie pour chacune des quatre interprétations possibles.
p q p ⇒ q ¬q ⇒ ¬p (p ⇒ q) ⇒ (¬q ⇒ ¬p)
V V V V V
V F F F V
F V V V V
F F V V V
26
indiquant une nuance temporelle ou causale. Il en va de même des versions naturelles de la
négation, de la disjonction et de l’équivalence.
Le connecteur d’implication pose toutefois un problème. Des phrases telles que
– Si 2 + 2 = 4, alors la terre tourne autour du soleil.
– Si la terre tourne autour du soleil, alors 2 + 2 = 4.
– Si 2 + 2 = 5, alors 2 + 2 = 6
sont vraies selon les règles sémantiques de la logique propositionnelle,13 elles pourraient bien
être tenues pour fausses (ou “absurdes”) par le non-logicien. Il se fait que, la plupart du temps,
la notion d’implication n’est pas vérifonctionnelle.
Nous avons déjà noté dans le chapitre introductif que l’implication logique correspondait
exactement à l’implication mathématique. Il n’empêche que, dans les théorèmes “utiles”, le
lien entre l’hypothèse (ou la conjonction des hypothèses) et la thèse n’est pas seulement
vérifonctionnel ; il s’y ajoute un autre lien, l’existence d’une démonstration permettant de
“passer” de l’hypothèse à la thèse. Il n’en est pas moins vrai qu’un énoncé tel que “si 2 + 2 = 5
alors 2 + 2 = 6” est un théorème de l’arithmétique, aussi valide qu’inutile.
On peut aborder le problème autrement. Il n’existe que 16 connecteurs binaires, et donc 16
possibilités de définir une approximation vérifonctionnelle de l’implication. En outre, certains
choix sont d’office exclus. En particulier, on admet aisément que la valeur de vérité d’une
implication (p ⇒ q) ne peut dépendre du seul antécédent p, ou du seul conséquent q ; on admet
de même que les rôles de l’antécédent et du conséquent ne sont pas interchangeables. Si l’on
se réfère à la figure 5, les seuls candidats possibles sont ◦3 , ◦5 , ◦12 et ◦14 . Si on admet en outre
que, quand l’antécédent est vrai, l’implication a la valeur du conséquent, il ne reste que ◦5 ,
c’est-à-dire l’implication logique telle qu’elle a été définie plus haut.
Une comparaison plus poussée entre la logique et l’arithmétique fournira une autre
“justification” de la notion d’implication (Fig. 13).
27
– A : le soleil a été la cause de l’Alternance de lumière et d’obscurité
pendant les trois premiers jours ;
– D : le sens du mot “jour” dans la bible est Différent du sens habituel.
Le raisonnement se formalise en
E ⇒ ¬Q , ¬Q ⇒ ¬A , D ∨ A
¬E ∨ D
On peut vérifier que toute interprétation rendant vraies les trois prémisses rend vraie la
conclusion. En effet, si la conclusion est fausse pour l’interprétation v, on a nécessairement
v(E) = V et v(D) = F. Les valeurs de vérité des trois prémisses sont alors
1. v(E ⇒ ¬Q) = v(¬Q) ;
2. v(¬Q ⇒ ¬A) ;
3. v(D ∨ A) = v(A).
On vérifie immédiatement qu’aucune des quatre manières d’attribuer des valeurs de vérité à
Q et A ne permet de rendre simultanément vraies les formules ¬Q, (¬Q ⇒ ¬A) et A. En
anticipant sur la section suivante, on peut donc affirmer que le raisonnement est correct.
Remarque. Notre analyse ne permet évidemment pas de porter un jugement sur la véracité
des trois prémisses. Une simple lecture de la Genèse permet de vérifier la véracité de la
première. Pour admettre la seconde, il faut admettre notamment que la cause doit précéder
(temporellement) l’effet. L’analyse de chacune des prémisses et de la conclusion requiert
naturellement une bonne connaissance du français. En fait, il est difficile d’inventorier avec
précision les connaissances, élémentaires mais nombreuses, nécessaires à la validation de ce
raisonnement.
28
a≡b a=b
a⇒b a≤b
a∧b min(a, b) ou encore a ∗ b
a∨b max(a, b)
a⊕b a 6= b ou encore (a + b) mod 2
¬a 1−a
29
– Une interprétation de E est une fonction v de Π dans {V, F} ; elle admet un
prolongement unique permettant d’interpréter toutes les formules dont le lexique est
inclus dans Π et, en particulier, toutes les formules de E.
– Une interprétation v de E est un modèle de E si elle est un modèle de tous les éléments
de E, c’est-à-dire si v(A) = V pour toute formule A ∈ E.
– E est satisfaisable ou consistant si E a au moins un modèle.
– E est insatisfaisable ou inconsistant si E n’est pas satisfaisable, c’est-à-dire si, pour
toute interprétation v, on a v(A) = F, pour au moins une formule A ∈ E.
Voici trois conséquences immédiates de ces définitions.
– Toute interprétation est un modèle de l’ensemble vide ∅.
– Les modèles du singleton {A} sont les modèles de la formule A.
– Les modèles de l’ensemble fini {A1 , . . . , An } sont les modèles de la conjonction
A1 ∧ · · · ∧ An .
Remarques. On peut définir la validité d’un ensemble E comme le fait que toute interprétation
est un modèle de E. Cela n’est guère intéressant car un ensemble valide n’est qu’un ensemble
de formules valides. La situation est différente en ce qui concerne la consistance. Il est clair
que les éléments d’un ensemble consistant sont des formules consistantes, mais un ensemble
de formules consistantes peut être inconsistant ; c’est par exemple le cas de la paire {p, ¬p}.
Une interprétation v d’un ensemble fini E = {A1 , . . . , An } est un modèle de E si et seulement
si c’est un modèle de la formule A1 ∧ · · · ∧ An ; c’est pourquoi on parle parfois d’ensemble
“conjonctif” de formules. Notons enfin que les notions d’interprétation et de consistance
restent pertinentes dans le cas d’un ensemble infini de formules. En revanche, la notion de
“conjonction infinie” ou de “formule infinie” n’existe pas dans notre contexte, parce qu’elle
correspondrait à un arbre sémantique infini, objet (informatique) difficilement manipulable.
Théorème. Si E ′ ⊂ E, tout modèle de E est un modèle de E ′ .
Corollaire. Tout sous-ensemble d’un ensemble consistant est consistant.
Corollaire. Tout sur-ensemble d’un ensemble inconsistant est inconsistant.
Remarque. La notation E ′ ⊂ E représente l’énoncé “tout élément de E ′ est un élément de E”.
|= A
30
conséquence logique de tout ensemble. Dans le même ordre d’idée, la notation
E |= false
exprime que l’ensemble E est inconsistant. En effet, le seul moyen que tout modèle de E soit
un modèle de false est que l’ensemble E n’admette aucun modèle.
Nous introduisons maintenant un résultat, immédiat mais important, permettant de ramener
la question “A est-elle conséquence logique de E ?” à la question “E ∪ {¬A} est-il
inconsistant ?”.
Théorème de la déduction (cas fini). Soit A une formule et soit U = {A1 , . . . , An } un ensemble
fini de formules. Les trois conditions suivantes sont équivalentes :
– A est une conséquence logique de U ; U |= A ;
– l’ensemble U ∪ {¬A} est inconsistant ; U ∪ {¬A} |= false ;
– l’implication (A1 ∧ . . . ∧ An ) ⇒ A est valide ; |= (A1 ∧ . . . ∧ An ) ⇒ A.
Théorème de la déduction (cas général). Soit A une formule et soit E un ensemble de formules.
Les deux conditions suivantes sont équivalentes :
– A est une conséquence logique de E ; E |= A ;
– l’ensemble E ∪ {¬A} est inconsistant ; E ∪ {¬A} |= false.
La théorie d’un ensemble E de formules est l’ensemble des conséquences logiques de E, soit
T (E) = {A : E |= A} ; les éléments de E sont les axiomes ou les postulats et les éléments
de T (E) sont les théorèmes. Cette notion est surtout employée dans le cadre de la logique des
prédicats.
Théorème. Soit E un ensemble de formules et soit U un ensemble de conséquences logiques
de E. Les ensembles E et E ∪ U admettent exactement les mêmes modèles.
Corollaire. On préserve la consistance d’un ensemble de formules par suppression de formules
(quelconques) et aussi par adjonction de conséquences logiques ; on préserve l’inconsistance
d’un ensemble par adjonction de formules (quelconques) et aussi par suppression de
conséquences logiques (de ce qui n’est pas supprimé !).
p q v(p ∨ q) v(q ∨ p)
V V V V
V F V V
F V V V
F F F F
31
Remarque. Le mot “équivalence” est employé dans trois cas bien distincts, que nous allons
énumérer.
1. Ce mot désigne des objets du langage formel qu’est la logique propositionnelle. On peut
écrire
– Le symbole ≡ représente le connecteur d’équivalence.
– La formule (p ∨ q) ≡ (q ∨ p) est une équivalence valide ;
– La formule p ≡ q est une équivalence contingente ;
– La formule p ≡ ¬p est une équivalence inconsistante.
2. Ce mot intervient aussi dans le métalangage, c’est-à-dire le formalisme, comportant des
notations spécifiques, qui permet de parler des objets logiques. On peut écrire
– Le symbole ↔ représente la relation d’équivalence logique.
– L’expression (p∨q) ↔ (q∨p) n’est pas une formule, mais un énoncé du métalangage ;
cet énoncé est vrai et exprime que les formules (p ∨ q) et (q ∨ p) sont logiquement
équivalentes.
– L’énoncé p ↔ q appartient au métalangage ; il est faux parce que les formules p et q
ne sont pas logiquement équivalentes.
3. Enfin, le mot “équivalence” est employé en français, la langue qui nous permet d’écrire
ce texte, et d’évoquer les objets du langage et du métalangage. On peut écrire
– Les expressions |= (A ≡ B) et A ↔ B appartiennent toutes les deux au métalangage ;
ce sont des énoncés interchangeables, ou équivalents, parce qu’ils sont tous les deux
vrais, ou tous les deux faux, selon les formules que les variables (du métalangage) A
et B représentent.
– Les énoncés “tout sous-ensemble d’un ensemble consistant est consistant” et
“tout sur-ensemble d’un ensemble inconsistant est inconsistant” appartiennent à la
langue française (et non au métalangage) ; ils sont équivalents, parce qu’ils sont
interchangeables ; un raisonnement (informel et élémentaire) permet de déduire un
énoncé de l’autre.
– La phrase française “Les énoncés |= (A ≡ B) et A ↔ B sont équivalents”
n’appartient pas au métalangage, mais exprime un fait (vrai) relatif à deux énoncés
du métalangage.
L’usage d’un même mot pour désigner des concepts différents se justifie (ou au moins
s’explique) par les liens étroits existant entre ces concepts. Ces liens apparaissent par exemple
dans le théorème suivant, qui exprime l’équivalence (au sens 3) entre deux énoncés du
métalangage.
Pour toutes formules A1 et A2 , on a A1 ↔ A2 si et seulement si on a |= (A1 ≡ A2 ).
Ce théorème, dont la démonstration élémentaire est laissée au lecteur, exprime que deux
formules sont logiquement équivalentes (sens 2) si et seulement si l’équivalence (sens 1) dont
elles sont les deux termes est valide.14
Selon les formules représentées par A1 et A2 , les quatre énoncés
14
Pour “chicaner” un peu plus, signalons que la locution “si et seulement si” est utilisée, en français, pour
exprimer l’équivalence (au sens 3) entre deux énoncés du métalangage . . . et parfois aussi entre deux énoncés du
français, c’est-à-dire entre deux phrases énonciatives quelconques. (Rassurons le lecteur qui nous a suivi jusqu’ici :
c’est fini sur ce point !)
32
– A1 ↔ A2 .
– |= (A1 ≡ A2 ).
– |= (A1 ⇒ A2 ) et |= (A2 ⇒ A1 ).
– {A1 } |= A2 et {A2 } |= A1 .
sont, ou bien tous vrais, ou bien tous faux.
Remarques. On écrit souvent A |= B au lieu de {A} |= B, et E, A, B |= C au lieu de
E ∪ {A, B} |= C. De plus, certains auteurs écrivent v |= A au lieu de v(A) = V. Cela vient de
ce que l’on assimile parfois l’interprétation v à l’ensemble des formules dont v est un modèle.
Mieux vaut éviter cette surcharge de sens pour une notation importante.
α = 2βx + 3(γ +δ)2(y−1)β = 2βx + 3(β +δ)2 (y−1)γ = 2βx + 3(γ +δ)2(y−1)γ .
Un autre type de remplacement est souvent employé dans les équations. De l’égalité bien
connue
(x + y)2 = x2 + 2xy + y 2 ,
on tire par exemple
(ab + 3c)2 = (ab)2 + 2ab3c + (3c)2 .
Notons deux différences importantes entre les deux types de remplacements :
– Dans le premier cas on exige l’égalité du terme remplaçant et du terme remplacé, mais
pas dans le second.
– Dans le second cas on exige le remplacement uniforme, de toutes les occurrences du
terme remplacé, mais pas dans le premier.
Ces deux résultats paraissent évidents mais on doit se méfier, pour au moins trois raisons.
La première est que les mathématiques fourmillent de “résultats évidents” . . . mais faux. La
propriété d’associativité de l’addition, souvent résumée par la formule
a + (b + c) = (a + b) + c
33
étant égaux. Cette propriété est valable pour toute somme finie, mais pas pour toute somme
infinie (série), comme le montre l’exemple suivant :15
?
1 = 1 + [(−1)+1] + · · · + [(−1)+1] + · · · = [1+(−1)] + · · · + [1+(−1)] + · · · = 0 .
La deuxième raison est que les résultats susmentionnés, si évidents qu’ils paraissent,
deviennent faux dans certains contextes particuliers. Par exemple, on apprend en astronomie
que “l’étoile du berger” est en fait une planète, Vénus ; on apprend aussi que les planètes,
au contraire des étoiles dites “fixes”, tournent autour du soleil. Un imprudent remplacement
conduirait à confondre les phrases
Jacques sait que Vénus tourne autour du Soleil.
et
Jacques sait que l’étoile du berger tourne autour du Soleil.
alors que pour beaucoup de gens la première phase est vraie mais pas la seconde. Voici un autre
exemple :
L’expression (x + y)3 s’écrit en moins de 10 caractères,
donc l’expression x3 + 3x2 y + 3xy 2 + y 3 s’écrit en moins de 10 caractères.
La troisième raison pour laquelle il n’est pas inutile de démontrer des “résultats évidents”
est que les preuves sont parfois aussi instructives que les théorèmes correspondants. En
particulier, la validité du premier principe de remplacement évoqué plus haut tient à une
propriété essentielle des opérateurs mathématico-logiques ; laquelle ?
34
Remarque. Cette démonstration se résume très bien en un dessin, que nous suggérons au lecteur
de tracer. La démonstration qui suit, plus dans le style des mathématiciens, n’implique pas la
représentation, même mentale, d’un objet graphique ; on utilise au lieu de cela la notion de
profondeur d’une sous-formule dans une formule . . . ce qui, en fait, revient au même.
Seconde démonstration du lemme. On raisonne par induction sur la profondeur d de la sous-
formule A dans C, qui correspond à la profondeur de la racine du sous-arbre syntaxique A dans
l’arbre C.16 Soit v une interprétation telle que v(A) = v(B).
– d = 0 : A = C et B = D, donc v(C) = v(D).
– d > 0 : C est de la forme ¬C ′ ou (C ′ op C ′′ ). Dans le premier cas, A est de profondeur
d − 1 dans C ′ et, en nommant D ′ le résultat du remplacement de A par B dans C ′ , on
a (hypothèse inductive) v(C ′ ) = v(D ′) ; comme C = ¬C ′ et D = ¬D ′ , on a aussi
v(C) = v(D). Dans le second cas, si l’occurrence à remplacer se trouve dans C ′ , on a
aussi v(C ′ ) = v(D ′ ), d’où v(C) = v(C ′ op C ′′ ) = v(D ′ op C ′′ ) = v(D).17
35
Exemple. Soient les formules
A: p⇒q
B : ¬p ∨ q
C : ((p ⇒ q) ∧ r) ∨ ((p ⇒ q) ⇒ r)
D : ((¬p ∨ q) ∧ r) ∨ ((p ⇒ q) ⇒ r)
p q r p ⇒ q (p ⇒ q) ∧ r (p ⇒ q) ⇒ r C
V V V V V V V
V V F V F F F
V F V F F V V
V F F F F V V
F V V V V V V
F V F V F F F
F F V V V V V
F F F V F F F
p q r p ⇒ q ¬p ∨ q (p ⇒ q) ∧ r (p ⇒ q) ⇒ r C
V V V V V V V V
V V F V V F F F
V F V F F F V V
V F F F F F V V
F V V V V V V V
F V F V V F F F
F F V V V V V V
F F F V V F F F
On change les têtes de colonnes concernées par le remplacement (ici, deux), sans changer
les colonnes elles-mêmes :
p q r p ⇒ q ¬p ∨ q (¬p ∨ q) ∧ r (p ⇒ q) ⇒ r D
V V V V V V V V
V V F V V F F F
V F V F F F V V
V F F F F F V V
F V V V V V V V
F V F V V F F F
F F V V V V V V
F F F V V F F F
36
Enfin, on supprime les colonnes devenues inutiles (ici, aucune) ; le résultat est une table de
vérité pour D.
Corollaire. Avec les notations du théorème de l’échange, si A et B sont logiquement
équivalents, alors C et D sont logiquement équivalents.19
Exemple. On donne A =def p , B =def ¬¬p et C =def (p ⇒ q) ≡ (¬q ⇒ ¬p) . Trois
choix sont possibles pour D :
– D =def (¬¬p ⇒ q) ≡ (¬q ⇒ ¬p) ;
– D =def (p ⇒ q) ≡ (¬q ⇒ ¬¬¬p) ;
– D =def (¬¬p ⇒ q) ≡ (¬q ⇒ ¬¬¬p) .
Comme A et B sont logiquement équivalents, C et D le sont aussi.
(X ∧ X) ↔ X ↔ (X ∨ X)
(X ∧ Y ) ↔ (Y ∧ X)
(X ∨ Y ) ↔ (Y ∨ X)
((X ∧ Y ) ∧ Z) ↔ (X ∧ (Y ∧ Z))
((X ∨ Y ) ∨ Z) ↔ (X ∨ (Y ∨ Z))
(X ⇒ X) ↔ true
((X ⇒ Y ) ∧ (Y ⇒ X)) ↔ (X ≡ Y )
(((X ⇒ Y ) ∧ (Y ⇒ Z)) ⇒ (X ⇒ Z)) ↔ true
(X ⇒ Y ) ↔ ((X ∧ Y ) ≡ X)
(X ⇒ Y ) ↔ ((X ∨ Y ) ≡ Y )
(X ∧ (Y ∨ Z)) ↔ ((X ∧ Y ) ∨ (X ∧ Z))
(X ∨ (Y ∧ Z)) ↔ ((X ∨ Y ) ∧ (X ∨ Z))
(X ⇒ (Y ⇒ Z)) ↔ ((X ⇒ Y ) ⇒ (X ⇒ Z))
(X ∨ ¬X) ↔ true ; (X ∧ ¬X) ↔ false
(X ∨ true) ↔ true ; (X ∧ true) ↔ X
(X ∨ false) ↔ X ; (X ∧ false) ↔ false
¬¬X ↔ X
¬(X ∧ Y ) ↔ (¬X ∨ ¬Y )
¬(X ∨ Y ) ↔ (¬X ∧ ¬Y )
37
– Ces équivalences décrivent des propriétés des connecteurs, telles l’associativité,
la commutativité et l’idempotence de ∧, ∨, la transitivité de l’implication et de
l’équivalence, etc.
– D’un point de vue sémantique, des formules telles que p ⇒ q et ¬p ∨ q ne doivent
pas être distinguées. L’ensemble des formules construites sur un lexique donné et
dans lequel des formules logiquement équivalentes ne “comptent” que pour une seule
formule est intéressant à étudier. Cela suggère (aux mathématiciens . . .) l’étude de
l’ensemble-quotient ΦΠ / ↔, où ΦΠ désigne l’ensemble des formules basées sur le
lexique Π. Cet ensemble-quotient est une algèbre de Boole particulière (appelée algèbre
de Lindenbaum), dont les opérations sont naturellement les connecteurs. Si Π = {p},
l’algèbre correspondante comporte quatre éléments ; on a A1 = {false, p, ¬p, true}. Si
Π = {p, q}, l’algèbre correspondante comporte seize éléments ; on a A2 = { false, p ∧ q,
p ∧ ¬q, ¬p ∧ q, ¬p ∧ ¬q, p, ¬p, q, ¬q, p ⊕ q, p ≡ q, p ∨ q, p ∨ ¬q, ¬p ∨ q, ¬p ∨ ¬q,
true }. L’algèbre An est isomorphe à P(En ), où En est un ensemble à 2n éléments.
La négation, la conjonction, la disjonction, l’implication et l’équivalence correspondent
respectivement à la complémentation, l’intersection, la réunion, l’inclusion et l’égalité.
38
comportant toute proposition intervenant dans C ou dans l’un des Ai , et telle que v(pi ) = v(Ai )
(i = 1, . . . , n), alors on a v(C[p1 , . . . , pn / A1 , . . . , An ]) = v(C).
Exemple de substitution uniforme. Soit
On a alors
C[p1 , p2 / A1 , A2 ] =def (p2 ∧ (p1 ∨ r)) ∨ (q ⇒ (p1 ∨ q)) .
Si on choisit v =def {(p1 , F), (p2 , V), (q, V), (r, F)} , on a v(A1 ) = v(p1 ) = F et v(A2 ) =
v(p2 ) = V ; on a aussi v([p1 , p2 / A1 , A2 ]) = v(C) = V.
Démonstration du lemme. Dans le cas où la substitution est indépendante, si ri désigne le
nombre d’occurrences de pi dans C, il suffit d’appliquer r1 + · · · + rn fois le lemme de
remplacement (ou n fois le théorème de l’échange). On laisse au lecteur l’extension au cas
des substitutions non indépendantes.
Théorème de substitution uniforme. Soient C, A1 , . . . , An des formules et p1 , . . . , pn des
propositions deux à deux distinctes ; si C est une tautologie, alors C[p1 , . . . , pn /A1 , . . . , An ]
est une tautologie.
Démonstration. On suppose d’abord que la substitution est indépendante ; aucun pi n’apparaı̂t
donc dans {A1 , . . . , An }, pas plus que dans C ′ =def C[p1 , . . . , pn / A1 , . . . , An ]. Soit v, une
interprétation quelconque de C ′ , et w l’extension de v obtenue en posant w(pi) =def v(Ai ).
Le lemme de substitution uniforme implique w(C ′ ) = w(C). Par hypothèse on a w(C) = V
et par construction on a w(C ′ ) = v(C ′ ). On a donc v(C ′ ) = V.
Remarque. Si les pi intervenaient dans les Ak , la technique pourrait ne pas fonctionner. De
|= p ≡ ¬¬p, on ne déduit pas immédiatement que |= (p ∨ r) ≡ ¬¬(p ∨ r) car l’interprétation
v : v(p) = F, v(r) = V telle que v(A) = v(p ∨ r) = V n’admet pas d’extension w telle
que w(p) = V. Le remède est simple. De |= p ≡ ¬¬p on déduit |= q ≡ ¬¬q, d’où on déduit
|= (p ∨ r) ≡ ¬¬(p ∨ r).
Suite de la démonstration. Si en revanche les pi interviennent dans {A1 , . . . , An },
on se donne une famille de nouveaux atomes qi . Si C est une tautologie, alors
C ′′ =def C(p1 /q1 , . . . , pn /qn ) est une tautologie. D’autre part, C ′ peut s’écrire
C ′′ [q1 , . . . , qn / A1 , . . . , An ], où les qi n’interviennent pas dans les Ak ; C ′ est donc une
tautologie.
Remarque. Où l’exigence d’uniformité de la substitution est-elle utilisée dans cette
démonstration ?
[(p ⇒ q) ∨ r] ↔ [r ∨ (p ⇒ q)] .
39
Il est clair que chaque ligne v de la table complète est “représentée” dans la “pseudo-table”,
par la ligne qui attribue à A la valeur v(p ⇒ q) et à B la valeur r. En revanche, certaines lignes
de la pseudo-table peuvent ne correspondre à aucune ligne de la table complète. C’est le cas
par exemple si A est instancié par une formule valide : les lignes de la pseudo-table concernant
les cas où A est faux n’ont pas de correspondant dans la table complète. Cela a la conséquence
suivante.
– Si C est une formule valide, alors C(p1 /A1 , . . . , pn /An ) est une formule valide ;
– Si C est une formule inconsistante, alors C(p1 /A1 , . . . , pn /An ) est une formule
inconsistante ;
– Si C est une formule simplement consistante, on ne peut rien dire.
Donnons un contre-exemple très simple pour le dernier cas : soit C =def p. On voit que
C est simplement consistante, tandis que C[p/(q ∨ ¬q)] est valide et que C[p/(q ∧ ¬q)] est
inconsistante.
et la thèse devient
40
Théorème d’interpolation de Craig. En logique propositionnelle, l’interpolation doit
permettre notamment l’optimisation des circuits digitaux ; une formule comportant n variables
propositionnelles distinctes correspond à un circuit digital à n entrées et une sortie. Le plus
souvent, un circuit digital n’est pas complètement spécifié et le concepteur peut mettre à
profit les degrés de liberté tolérés par la spécification pour obtenir un circuit aussi simple que
possible. Dans le cas où la spécification prend la forme d’un intervalle logique, le théorème
d’interpolation donne lieu à une technique de simplification.
Théorème. Soient A et B deux formules propositionnelles. Si |= A ⇒ B, il existe une formule
C, ne contenant que des propositions communes à A et B, telle que |= A ⇒ C et |= C ⇒ B.
Démonstration. On raisonne par induction sur l’ensemble Π des propositions communes à A et
B. Cela signifie que l’on démontre d’abord le théorème dans le cas particulier où l’ensemble Π
est vide (cas de base). On suppose ensuite que le théorème est vrai dans le cas d’un ensemble,
quelconque mais fixé, ne contenant pas une proposition, elle aussi quelconque mais fixée (cette
supposition est l’hypothèse inductive), puis on démontre que le théorème reste vrai dans le cas
de cet ensemble augmenté de cette proposition.
Cas de base. Si Π = ∅, |= A ⇒ B implique que A est inconsistante (et on choisit
C =def false) ou que B est valide (et on choisit C =def true). Cela se démontre par l’absurde.
S’il existait des interprétations u et v (de domaines disjoints) telles que u(A) = V et v(B) = F,
l’interprétation w =def u ∪ v serait telle que w(A ⇒ B) = F.
Cas inductif. Si p ∈ Π, l’hypothèse inductive affirme l’existence d’interpolantes CT
et CF relatives à A(p/true), B(p/true) et à A(p/false), B(p/false), respectivement.
On vérifie immédiatement que la formule (p ∧ CT ) ∨ (¬p ∧ CF ) interpole A et B.
41
D’autre part, on a
|= B ⇒ [A(p/r) ⇒ r] , d’où
|= [B ∧ A(p/r)] ⇒ r , d’où
|= A(p/r) ⇒ (B ⇒ r) , et par substitution
|= A(p/q) ⇒ (B ⇒ q) .
On en déduit la thèse, sous la forme
|= A(p/q) ⇒ (q ≡ B) , ou sous la forme
|= A(p/r) ⇒ (r ≡ B) , ou encore
|= A ⇒ (p ≡ B) .
42
La condition est suffisante. L’ensemble E = {ϕ ∈ Φ : v(ϕ) = V} est (finiment) consistant,
puisqu’il admet le modèle (unique) v, et est maximal, parce que si ψ 6∈ E, l’ensemble E ∪ {ψ}
contient le sous-ensemble fini inconsistant {¬ψ, ψ}.
La condition est nécessaire. On se restreint au cas où le lexique Π est dénombrable, soit
Π = {p1 , p2 , . . .}. Soit E un sous-ensemble f.c. maximal de Φ.
– Pour tout i, E contient exactement un des éléments de la paire {pi , ¬pi }. D’une part, il
ne peut contenir les deux éléments, puisque {pi , ¬pi } est inconsistant. D’autre part, si
pi 6∈ E, l’ensemble E ∪ {pi } n’est pas finiment consistant et E admet un sous-ensemble
fini E ′ tel que E ′ ∪ {pi } est inconsistant ; on a alors E ′ |= {¬pi }. On en déduit que
E ∪ {¬pi } est finiment consistant [si E ′′ ⊂ E, tout modèle de E ′′ ∪ E ′ est un modèle de
E ′′ ∪ {¬pi }] d’où, vu la maximalité, ¬pi ∈ E.
– Pour tout i, soit ℓi l’unique élément de {pi , ¬pi } appartenant à E ; ces éléments
déterminent une interprétation unique, rendant vrais tous les ℓi . On note v cette
interprétation, dont on va montrer qu’elle est celle requise par l’énoncé.
– On commence par démontrer l’inclusion E ⊂ {ϕ ∈ Φ : v(ϕ) = V}. Soit ϕ ∈ E
et {pi1 , . . . , pin } les propositions intervenant dans ϕ. Comme E est finiment consistant,
son sous-ensemble {ℓi1 , . . . , ℓin , ϕ} est consistant, d’où v(ϕ) = V.
– On conclut en observant que, l’ensemble E étant finiment consistant maximal,
l’inclusion E ⊂ {ϕ ∈ Φ : v(ϕ) = V} doit être une égalité puisque {ϕ ∈ Φ : v(ϕ) = V}
est visiblement consistant, donc aussi finiment consistant.
Théorème. Tout ensemble finiment consistant est consistant.
Remarque. Il suffit de prouver que tout ensemble finiment consistant est inclus dans un
ensemble finiment consistant maximal.
Démonstration. Soit D un ensemble finiment consistant. On pose E0 = D et, si n > 0,
En = En−1 ∪ {pn } si cet ensemble est finiment consistant, En = En−1 ∪ {¬pn } sinon.
On démontre par récurrence que tous les En sont finiment consistants. C’est trivial pour n = 0.
Pour En , c’est trivial si En−1 ∪ {pn } est finiment consistant. Sinon, il existe un sous-ensemble
fini E ′ ⊂ En−1 tel que E ′ ∪ {pn } est inconsistant, et donc que E ′ |= ¬pn . Dans ce cas,
En = En−1 ∪ {¬pn } est finiment consistant, car pour tout sous-ensemble fini E ′′ ⊂ En−1 , tout
modèle de E ′′ ∪ E S ′
est aussi un modèle de E ′′ ∪ {¬pn }.
On pose E =def n En . L’intersection {pi , ¬pi } ∩ E contient un élément unique ℓi . Ces ℓi
déterminent une interprétation unique v telle que v(ϕ) = V pour tout ϕ ∈ E. L’ensemble D,
comme l’ensemble E, est donc inclus dans l’ensemble maximal {ϕ ∈ Φ : v(ϕ) = V}.
Remarque. Le théorème de compacité facilite l’emploi de l’outil logique, mais indique aussi
une certaine faiblesse de cet outil. Par exemple, en arithmétique (théorie des nombres entiers),
un ensemble infini de formules peut être inconsistant tout en étant finiment consistant. Si z0
est une constante sur le domaine Z, on pose Ez0 = {(z > z0 ) : z ∈ Z}. Cet ensemble
est inconsistant, puisque pour toute interprétation v, l’entier v(z0 ) admet des minorants.
Néanmoins, tout sous-ensemble fini de Ez0 est consistant. Un tel ensemble s’écrit {(z >
z0 ) : z ∈ A}, où A est un ensemble fini d’entiers. Un modèle v s’obtient en posant
v(z0 ) = (inf A) − 1. Cela montre simplement que le calcul des propositions ne permet pas
d’exprimer toute la théorie arithmétique.
Variante de la démonstration. On peut combiner la construction d’un sur-ensemble maximal et
la démonstration du théorème de compacité. Il suffit d’observer que si Π est dénombrable, alors
43
S
Φ l’est aussi ; en effet, on a Φ = n Φn , où Φn est l’ensemble (fini) des formules construites
avec le lexique {p1 , . . . , pn } et comportant au plus n connecteurs. On peut alors considérer une
énumération (ϕ1 , ϕ2 , . . .) de l’ensemble Φ et récrire la démonstration comme suit.
Soit D un ensemble finiment consistant. On pose E0 = D et, si n > 0, En = En−1 ∪ {ϕn }
si cet ensemble est finiment consistant, En = En−1 ∪ {¬ϕn } sinon.
On démontre par récurrence que tous les En sont finiment consistants. C’est trivial pour n = 0.
Pour En , c’est trivial si En−1 ∪ {ϕn } est finiment consistant. Sinon, il existe un sous-ensemble
fini E ′ ⊂ En−1 tel que E ′ ∪ {ϕn } est inconsistant, et donc tel que E ′ |= ¬ϕn . Dans ce cas,
′′
En = En−1 ∪ {¬ϕn } est finiment consistant, car pour tout sous-ensemble fini ES ⊂ En−1 ,
tout modèle de E ′′ ∪ E ′ est aussi un modèle de E ′′ ∪ {¬ϕn }. On pose E =def n En . Par
construction, pour tout i > 0, l’intersection {pi , ¬pi } ∩ E contient un élément unique ℓi . Ces
éléments déterminent une interprétation v, dont on montre qu’elle est un modèle de E. En effet,
soit ϕ ∈ E et {pi1 , . . . , pin } les propositions intervenant dans ϕ. Soit k le plus petit naturel
tel que l’ensemble Ek comporte tous les éléments de {ℓi1 , . . . , ℓin , ϕ} (k existe toujours).
Comme Ek est finiment consistant, son sous-ensemble {ℓi1 , . . . , ℓin , ϕ} est consistant et admet
un modèle. Ce modèle ne peut être que v (ou plus exactement la restriction de v au lexique
{pi1 , . . . , pin }), d’où v(ϕ) = V.
Remarquons qu’en arithmétique ce résultat est faux. L’ensemble
est inconsistant, car aucun nombre n’est plus grand que tous les autres, mais tous ses sous-
ensembles finis sont consistants.
Pourquoi ce théorème est-il important ? Pour plusieurs raisons, mais nous n’en citons que
deux. La première raison est technique. Supposons qu’une formule A soit conséquence logique
de l’ensemble infini E de formules. A priori, on pourrait craindre qu’une infinité de formules
de E soient des hypothèses nécessaires pour obtenir la conclusion A. Le théorème de compacité
montre que cette crainte n’est pas fondée. En effet, si A est conséquence logique de E, alors
E ∪ {¬A} est inconsistant et, par le théorème de compacité, il existe un sous-ensemble fini E ′
de E tel que E ′ ∪ {¬A} soit inconsistant, et donc tel que A soit conséquence logique de E ′ .
La seconde raison est plus philosophique. L’une des motivations de Frege, dans sa tentative
remarquablement réussie de formaliser la logique, était de “réduire” les mathématiques à la
logique. Ce “logicisme”, dans la lignée du projet leibnizien de “calculus ratiocinator”, ne
peut réussir que de manière très partielle. Le théorème de compacité (surtout dans le cadre
prédicatif, que nous aborderons plus loin) montre que l’arithmétique ne peut se réduire à la
logique. Les célèbres résultats d’incomplétude de Gödel montrent que cela a des conséquences
importantes.
44
3 Procédures de décision analytiques
Le théorème de la déduction permet de ramener le problème fondamental de la logique
à la détermination de la consistance d’un ensemble de formules, en réduisant la question
“la formule A est-elle conséquence logique de l’ensemble de formules E ?” à la question
“l’ensemble de formules E ∪{¬A} est-il inconsistant ?”. En pratique, on développe surtout des
algorithmes de détermination de la consistance d’une formule ou d’un ensemble de formules.
Un tel algorithme permet aussi de résoudre le problème de la validité : un ensemble de formules
est valide si et seulement si tous ses éléments sont valides23 et une formule est valide si
et seulement si sa négation est inconsistante. Une formule est simplement consistante, ou
contingente, si elle n’est ni valide ni inconsistante.
(p ⇒ q) ∨ (q ⇒ r) .
C’est une disjonction de deux implications. La première implication n’est fausse que si p est
vrai et q faux, mais dans ce cas la deuxième implication est vraie ; la formule est donc valide.
Nous n’approfondissons pas ici les raffinements que l’on peut apporter à la méthode des
tables de vérité, parce qu’il existe d’autres méthodes nettement plus efficaces.24
23
Rappelons ici qu’un ensemble de formules consistantes peut être inconsistant.
24
La méthode des tables de vérité (avec simplifications) reste intéressante pour résoudre certaines questions
théoriques et surtout pour analyser “à la main” des formules très courtes.
45
p q p ⇒ q ¬q ⇒ ¬p (p ⇒ q) ⇒ (¬q ⇒ ¬p)
V V V V V
V F F F V
F V V V V
F F V V V
p q p∧q
V V V
V F F
F V F
F F F
p q p ∨ q ¬p ¬q (p ∨ q) ∧ ¬p ∧ ¬q
V V V F F F
V F V F V F
F V V V F F
F F F V V F
46
structure arborescente particulière, appelée tableau sémantique.26
(p ⇒ q) ∧ ¬(p ⇒ r) (p ⇒ q) ∧ ¬(p ⇒ r)
↓ ↓
p ⇒ q , ¬(p ⇒ r) p ⇒ q , ¬(p ⇒ r)
↓ ւ ց
p ⇒ q , p , ¬r ¬p, ¬(p ⇒ r) q, ¬(p ⇒ r)
ւ ց ↓ ↓
¬p, p, ¬r q, p, ¬r ¬p, p, ¬r q, p, ¬r
Une formule peut donner lieu à plusieurs tableaux sémantiques différents suivant l’ordre
d’application des règles de construction, mais tous conduisent à la même conclusion (la
bonne !) concernant la consistance de la formule. La signification commune des deux tableaux
de la figure 16 est
26
Cette structure est bien un arbre, mais ne doit pas être confondue, d’une part, avec la notion d’arbre syntaxique
déjà introduite ni, d’autre part, avec la notion d’arbre sémantique qui sera introduite plus loin.
47
Une interprétation est un modèle de la formule (p ⇒ q) ∧ ¬(p ⇒ r)
si et seulement si c’est un modèle de l’un des ensembles {¬p, p, ¬r} , {q, p, ¬r}.
α α1 α2 β β1 β2
A1 ∧ A2 A1 A2 B1 ∨ B2 B1 B2
¬(A1 ∨ A2 ) ¬A1 ¬A2 ¬(B1 ∧ B2 ) ¬B1 ¬B2
¬(A1 ⇒ A2 ) A1 ¬A2 B1 ⇒ B2 ¬B1 B2
¬(A1 ⇐ A2 ) ¬A1 A2 B1 ⇐ B2 B1 ¬B2
Le processus général de construction d’un tableau sémantique pour une formule donnée ϕ
est décrit à la figure 18. Ce tableau est un arbre dont chaque nœud est étiqueté par un ensemble
de formules. Un nœud est terminal quand son étiquette ne comporte que des littéraux. Quand la
construction du tableau est achevée, toutes les feuilles sont des nœuds terminaux. On convient
de marquer un nœud terminal par si l’étiquette est consistante (feuille ouverte), et par × si
l’étiquette est inconsistante (feuille fermée).
On utilise parfois des assertions plutôt que des formules, une assertion étant l’attribution
d’une valeur de vérité à une formule. La figure 19 comporte un tableau classique, en notation
“formule”, et sa variante signée, en notation “assertion”.
27
On remplacera donc une équivalence X ≡ Y par une formule conjonctive (X ⇒ Y ) ∧ (Y ⇒ X), ou par une
formule disjonctive (X ∧ Y ) ∨ (¬X ∧ ¬Y ), au choix. On élimine de même les formules du type X ⊕ Y .
28
Ce point sera nuancé plus loin.
29
Dans la suite, on notera souvent α une formule conjonctive et β une formule disjonctive ; les composants
respectifs seront notés respectivement α1 et α2 , et β1 et β2 . Soulignons qu’en général il s’agit de composants
sémantiques et non de composants syntaxiques ; par exemple, ¬p n’est pas un composant syntaxique de la formule
disjonctive p ⇒ q.
48
– Initialisation. On crée une racine étiquetée {ϕ}.
– Itération. On sélectionne une feuille non marquée ℓ, d’étiquette U(ℓ).
– Si U(ℓ) est un ensemble de littéraux :
– si U(ℓ) contient une paire complémentaire,
alors marquer ℓ comme étant fermée ;
– sinon, marquer ℓ comme étant ouverte.
– Si U(ℓ) n’est pas un ensemble de littéraux,
sélectionner une formule dans U(ℓ) :
– si c’est une α-formule A,
créer un nouveau nœud ℓ′ , descendant de ℓ,
et étiqueter ℓ′ avec
U(ℓ′ ) = (U(ℓ) − {A}) ∪ {α1 , α2 };
– si c’est une β-formule B,
créer deux nouveaux nœuds ℓ′ et ℓ′′ , descendants de ℓ,
et étiqueter ℓ′ avec
U(ℓ′ ) = (U(ℓ) − {B}) ∪ {β1 }
et étiqueter ℓ′′ avec
U(ℓ′′ ) = (U(ℓ) − {B}) ∪ {β2 }.
– Terminaison. La construction est achevée
quand toutes les feuilles sont marquées ‘×’ ou ‘ ’.
p ∧ ¬(q ∧ p) p ∧ ¬(q ∧ p) = V
↓ ↓
p, ¬(q ∧ p) p = V, q ∧ p = F
ւ ց ւ ց
p, ¬q p, ¬p p = V, q = F p = V, p = F
× ×
Remarque. Si on adopte cette variante, les liens α-conjonction et β-disjonction ne sont plus
valable tels quels ; par exemple, l’assertion p ∧ q = V est de type α, l’assertion p ∧ q = F
est de type β. En revanche, les liens α-prolongation et β-ramification subsistent. C’est pour
éviter ces complications (à tout le moins, ces apparences de complication) que nous n’avons
pas directement introduit les tableaux signés, pourtant fréquemment utilisés.
49
qui étiquète déjà un ancêtre de n. Avec ces conventions, le tableau
(p ∨ q) ∧ (¬p ∧ ¬q)
↓
p ∨ q, ¬p ∧ ¬q
↓
p ∨ q, ¬p, ¬q
ւ ց
p, ¬p, ¬q q, ¬p, ¬q
× ×
(p ∨ q) ∧ (¬p ∧ ¬q),
p ∨ q, ¬p ∧ ¬q, ¬p, ¬q
ւ ց
p q
× ×
Une autre économie possible est de ne pas étiqueter les nœuds directement avec des sous-
formules, mais plutôt avec des pointeurs vers les sous-arbres correspondants dans l’arbre
syntaxique. Enfin, certaines branches d’un tableau sémantique sont très semblables. Il est
possible d’éviter aussi les redondances de ce type en utilisant non plus une structure d’arbre,
mais une structure de graphe sans cycle. Ces raffinements sortent du cadre de ces notes (voir
[L2] pour plus de détails).
50
3.2.3 Propriétés de la méthode des tableaux sémantiques
La méthode des tableaux sémantiques est le plus souvent utilisée pour montrer la validité
d’une formule (ou l’inconsistance de sa négation), ou encore pour montrer l’inconsistance d’un
ensemble fini de formules. On souhaite naturellement que la méthode donne uniquement des
résultats corrects ; elle ne peut conclure, par exemple, à l’inconsistance d’une formule, que
si la formule est effectivement inconsistante. Cette propriété est l’adéquation de la méthode.
D’autre part, on souhaite que, si une formule est inconsistante, la méthode mette ce fait en
évidence ; c’est la propriété de complétude. En résumé, une méthode est adéquate si elle est
correcte ; elle est complète si elle est assez puissante.
Dans le cas présent, prouver l’adéquation revient à prouver l’un des énoncés suivants :
– si T (A) est fermé, alors A est inconsistante ;
– si T (¬B) est fermé, alors B est valide ;
– si A est consistante, alors T (A) est ouvert ;
– si B n’est pas valide, alors T (¬B) est ouvert.
Prouver la complétude revient à prouver la réciproque, c’est-à-dire l’un des énoncés suivants :
– si A est inconsistante, alors T (A) est fermé ;
– si B est valide, alors T (¬B) est fermé ;
– si T (A) est ouvert, alors A est consistante ;
– si T (¬B) est ouvert, alors B n’est pas valide.
51
h(n′ ) < h(n) et h(n′′ ) < h(n) ; les ensembles U(n′ ) et U(n′′ ) sont tous deux
inconsistants. Pour toute interprétation v,
1. soit il y a une formule A′ ∈ U0 ⊆ U(n) : v(A′ ) = F
2. soit v(β1 ) = v(β2 ) = F, d’où v(β) = F (cf. règles β).
Dans les deux cas, il y a une formule dans U(n) que v rend fausse ; v étant quelconque,
on en déduit que U(n) est inconsistant.
52
2. Pour toute α-formule α ∈ U, l’arbre étant complet, la règle α correspondante a dû être
utilisée à un certain nœud n. Par construction, α1 , α2 ∈ U(n′ ) ⊆ U.
3. Pour toute β-formule β ∈ U, l’arbre étant complet, la règle β correspondante a dû être
utilisée à un certain nœud n. Par construction, β1 ∈ U(n′ ) et β2 ∈ U(n′′ ), et U(n′ ) ⊆ U
ou U(n′′ ) ⊆ U, d’où β1 ∈ U ou β2 ∈ U.
v(p) = V si ¬p 6∈ U
v(p) = F si ¬p ∈ U
L’interprétation v assigne une et une seule valeur de vérité à chaque atome de Π (car U est un
ensemble de Hintikka). Il faut démontrer que pour tout A ∈ U, on a v(A) = V. Cela se fait
par induction sur la structure de A :
– A est un littéral. Par définition de v on a :
– Si A = p, alors v(A) = v(p) = V.
– Si A = ¬p, alors v(p) = F, d’où v(A) = V.
– A est une α-formule α. On a α1 , α2 ∈ U, donc par hypothèse inductive, v(α1 ) = V et
v(α2 ) = V, d’où v(α) = V par définition des règles α.
– A est une β-formule β. On a β1 ∈ U ou β2 ∈ U, donc par hypothèse inductive,
v(β1 ) = V ou v(β2 ) = V, d’où v(β) = V par définition des règles β.
53
La garde exprime l’existence d’un nœud, “feuille provisoire”, dont l’étiquette comporte une
formule α ou β. Le corps de la boucle consiste en la génération du ou des successeur(s) direct(s)
d’une “feuille provisoire” du tableau.
Rien n’empêche donc l’application de la méthode des invariants. En fait, cette application
est simple et éclairante ; l’invariant de boucle est la propriété suivante :
Les modèles de la formule de départ sont exactement les interprétations
qui sont modèles d’au moins une étiquette de feuille provisoire.
Lorsque le tableau est achevé, le mot “provisoire” disparaı̂t et, clairement, la formule de
départ est consistante si et seulement si le tableau comporte au moins une feuille ouverte.
En ce qui concerne la terminaison, le raisonnement fait plus haut reste valable dans le cadre
de la méthode des invariants.
54
p ∧ (¬q ∨ ¬p)
↓
prolongation (type α) H A
règle conjonctive → ¬p, q → ¬p, p
p, ¬q ∨ ¬p ramification (type β)
règle conjonctive
ւ
ramification (type β)
ց règle disjonctive → ¬p, q ∧ p
prolongation (type α)
règle disjonctive
p, ¬q p, ¬p → ¬p ∨ (q ∧ p)
×
¬p ∨ (q ∧ p) = F
↓
prolongation (type α) H A
règle conjonctive → ¬p, q → ¬p, p
p = V, q ∧ p = F ramification (type β)
règle conjonctive
ւ ց
ramification (type β) → ¬p, q ∧ p
règle disjonctive prolongation (type α)
règle disjonctive
p = V, q = F p = V, p = F → ¬p ∨ (q ∧ p)
×
3.3.2 Interprétation
Fondamentalement, le contenu sémantique d’une dérivation de séquent est le même que
celui du tableau correspondant, mais la dualité permet de présenter ce contenu différemment.
– Chaque étiquette d’une dérivation de séquent s’interprète comme un ensemble disjonctif
de formules.
– Les feuilles correspondent à des clauses c’est-à-dire à des disjonctions de littéraux.
– Les feuilles valides sont étiquetées A ; ce symbole signifie “Axiome” : vérité universelle.
Les feuilles non valides sont étiquetées H ; ce symbole signifie “Hypothèse” : énoncé
contingent.
– La ligne horizontale s’interprète comme la relation d’équivalence logique : une
interprétation rend vraie(s) la (les) prémisse(s), au numérateur, si et seulement si elle
rend vraie la conclusion, au dénominateur.
On a aussi les définitions et règles suivantes.
– Une clause est un axiome si elle comporte une paire complémentaire de littéraux, et une
hypothèse sinon.
– Les règles d’inférence sont de deux types
– règles α (prolongation) :
→ U ∪ {α1 , α2 }
→ U ∪ {α}
– règles β (ramification) :
55
→ U ∪ {β1 } → U ∪ {β2 }
→ U ∪ {β}
α α1 α2 β β1 β2
A1 ∨ A2 A1 A2 B1 ∧ B2 B1 B2
¬(A1 ∧ A2 ) ¬A1 ¬A2 ¬(B1 ∨ B2 ) ¬B1 ¬B2
A1 ⇒ A2 ¬A1 A2 ¬(B1 ⇒ B2 ) B1 ¬B2
A1 ⇐ A2 A1 ¬A2 ¬(B1 ⇐ B2 ) ¬B1 B2
Rappelons que les doubles négations sont systématiquement simplifiées et que les
connecteurs d’équivalence et de disjonction exclusive sont interdits. On observe (figure 23) que
les formules conjonctives donnent lieu à une ramification (type β) et les formules disjonctives
à une prolongation (type α). C’était le contraire pour les tableaux sémantiques.
Si on lit la dérivation de haut en bas, les règles de décomposition deviennent des règles de
composition, ou règles d’inférence.
56
les anciennes règles
→ V, ¬A, B → V, A → V, ¬B
→ V, (A ⇒ B) → V, ¬(A ⇒ B)
U → V, ¬A, B U → V, A U → V, ¬B
U → V, (A ⇒ B) U → V, ¬(A ⇒ B)
U, A → V, B U → V, A U, B → V
U → V, (A ⇒ B) U, (A ⇒ B) → V
U → V, A U, B → V
U, (A ⇒ B) → V
est réversible : la barre horizontale peut s’interpréter comme l’équivalence logique. Dans une
règle non réversible,
V la conclusionWest conséquence logique des prémisses, mais non l’inverse.
Si on pose Uc = U et Vd = V , la règle ci-dessus exprime que les modèles communs
des formules Uc ⇒ (Vd ∨ A) et (Uc ∧ B) ⇒ Vd sont exactement les modèles de la formule
(Uc ∧ (A ⇒ B)) ⇒ Vd .
Cette règle est aussi analytique : toute formule apparaissant en haut apparaı̂t aussi en bas
(comme formule ou sous-formule). Les dérivations de séquents peuvent se lire de bas en haut
(analyse d’une formule) ou de haut en bas (déduction d’une formule au départ d’axiomes et/ou
d’hypothèses).
Il existe aussi des méthodes synthétiques de déduction, ne se prêtant pas directement à
l’analyse des formules. La méthode synthétique est le plus souvent la seule utilisable en
mathématique. On utilise des règles où la barre s’interprète comme la relation (non symétrique)
de conséquence logique. L’exemple le plus connu de règle synthétique (donc non analytique)
et non réversible est sans doute le Modus ponens :
U → A U → (A ⇒ B)
U → B
57
La formule A et ses sous-formules peuvent ne pas apparaı̂tre dans les conclusions. Il est donc
difficile de “deviner” des prémisses adéquates au départ des conclusions.30
A, B, C → D, E, F
noté parfois
A, B, C ⊢ D, E, F
est “L’implication (A ∧ B ∧ C) ⇒ (D ∨ E ∨ F ) est valide”.
¬p ∨ (q ∧ p) = F H A
↓ p → q p → p
p = V, q ∧ p = F
ւ ց p → q∧p
p = V, q = F p = V, p = F
× → ¬p ∨ (q ∧ p)
30
Les deux règles synthétiques de Modus ponens et de coupure formalisent deux modes de raisonnement
omniprésents en mathématique et dans la vie quotidienne. Le Modus ponens traduit la notion même de théorème
ou de résultat général : “appliquer” (A ⇒ B), c’est déduire B dans le cas où A est connu. La règle de coupure
formalise le raisonnement par cas : si on infère V de U quand A est vrai, et aussi quand A est faux, on infère V
de U en toute généralité.
58
3.4 Le raisonnement automatique
3.4.1 Introduction
La logique formelle permet, comme on vient de le voir tout au long de ce chapitre, de
transformer le raisonnement en un objet mathématique, susceptible d’être traité, et même
construit, par un ordinateur. Nous avons vu, au paragraphe 2.3.3, qu’un texte court mais
relativement dense, présentant un raisonnement, pouvait être transformé en formules et ainsi
devenir accessible à une analyse fiable et automatique.31 Un célèbre ouvrage de science-
fiction32 évoque ainsi l’analyse formelle d’un très compliqué et volumineux document
diplomatique . . . aboutissant à la conclusion que ce document était sémantiquement vide
et que ses auteurs méritaient, étymologiquement du moins, leur statut de diplomate. Plus
concrètement, un livre d’analyse mathématique a été entièrement vérifié par ordinateur dans
le cadre d’un projet d’intelligence artificielle. Peut-on réellement espérer ramener ainsi le
raisonnement au calcul, dans le but de l’automatiser ?
59
Si nous utilisons les tables de vérité, et si l’ensemble en question comporte des occurrences
de n propositions élémentaires distinctes, il suffit de construire une table de vérité . . . qui
comportera 2n lignes. Si n vaut 30, la table comportera plus d’un milliard de lignes ; si n
vaut 100, ce qui n’a rien d’irréaliste, le problème est, sauf cas particulier, définitivement
hors d’atteinte de tout ordinateur présent ou à venir. Observons au passage que multiplier
par 1 000 les performances d’un ordinateur ne permet que d’ajouter 10 nouvelles variables
propositionnelles à notre lexique.
Il existe a priori deux moyens de contourner cet écueil. D’une part, il est possible de
développer des procédures de décision plus rapides que la méthode des tables de vérité et,
d’autre part, on peut essayer d’isoler certains types de formules et d’ensembles de formules
pour lesquels le problème de la consistance pourrait se résoudre plus rapidement. Nous avons
déjà adopté la première approche : la méthode des tableaux sémantiques est souvent — mais
pas toujours — nettement plus efficace que celle des tables de vérité. Une analyse plus fine
montrerait quand même que cette méthode et, à des degrés divers, toutes les méthodes connues
actuellement, restent fondamentalement trop lentes. Plus précisément, dans beaucoup de cas,
les performances se dégradent très vite dès que la dimension du problème augmente. Une
théorie récemment développée34 laisse peu de chances de progrès significatifs dans cette voie.
La seconde approche est plus prometteuse ; nous la développons dans la suite de ce chapitre.
p q r X(p, q, r)
V V V V
V V F F
V F V V
V F F F
F V V V
F V F V
F F V F
F F F F
60
Cette formule peut s’écrire différemment, et notamment
(p ∧ r) ∨ (¬p ∧ q) ,
ou encore
(p ⇒ r) ∧ (¬p ⇒ q) .
Le point important est que toute formule, puisqu’elle admet une table de vérité, est équivalente
à une disjonction de cubes, ce que l’on appelle aussi une forme disjonctive normale.
Observons aussi que la négation d’une disjonction de cubes est une conjonction de clauses,
ce que l’on appelle aussi une forme conjonctive normale. On obtient aisément la forme
conjonctive normale d’une formule à partir de la forme disjonctive normale de la négation de
cette formule ; on peut aussi l’obtenir directement à partir de la table de vérité, en considérant
les lignes pour lesquelles la formule est fausse. Par exemple, la formule X(p, q, r) est fausse
dans quatre cas ; elle peut donc s’écrire
ou encore
(¬p ∨ ¬q ∨ r) ∧ (¬p ∨ q ∨ r) ∧ (p ∨ q ∨ ¬r) ∧ (p ∨ q ∨ r) ,
ce qui est une forme conjonctive normale, c’est-à-dire une conjonction de clauses ; la formule
peut se simplifier en
(¬p ∨ r) ∧ (p ∨ q) ,
qui est encore une forme conjonctive normale, appelée aussi forme clausale.
Le principe de la déduction affirme que la formule A est conséquence logique de
l’ensemble E si et seulement si l’ensemble E ∪ {¬A} est inconsistant. Chaque formule de ce
dernier ensemble est logiquement équivalente à une conjonction de clauses ; si C est l’ensemble
de toutes ces clauses, on peut dire que A est conséquence logique de E si et seulement si C est
inconsistant. Le problème fondamental de la logique se résume donc à celui de déterminer si
un ensemble de clauses est inconsistant ou non.
Remarque. Construire la table de vérité d’une formule donnée n’est généralement pas le moyen
le plus rapide d’obtenir une forme normale disjonctive ou conjonctive logiquement équivalente
à cette formule.
61
Les pi et q sont des propositions élémentaires.35 La formule exprime simplement que toute
interprétation rendant vraies les propositions p1 , . . . , pn rend vraie aussi la conclusion q.36
On voit immédiatement que cette formule est une clause, que l’on peut récrire en
¬p1 ∨ · · · ∨ ¬pn ∨ q .
{S := S0 }
Tant que ✷ 6∈ S faire
choisir p et c tels que
p est une clause unitaire positive de S,
c est une clause de S contenant ¬p ;
r := c \ {¬p} ;
S := (S \ {c}) ∪ {r} .
F IG . 26 – Résolution unitaire
Le principe de cet algorithme est très simple. Il consiste à supprimer, dans les clauses d’un
ensemble S de clauses de Horn, tous les littéraux négatifs dont la proposition sous-jacente
apparaı̂t comme clause unitaire, jusqu’à ce qu’une clause soit devenue vide, ou que plus aucune
suppression ne soit possible. Dans le premier cas, on conclut à l’inconsistance, dans le second,
à la consistance. La notation “:=” signifie “devient” ; exécuter l’instruction x := x + y signifie
que la nouvelle valeur de x est l’ancienne valeur de x + y. Si c est une clause contenant ¬p,
c \ {¬p} est la clause obtenue en supprimant ¬p. La clause vide, qui ne contient aucun littéral,
est représentée par le symbole ✷. Une clause est vraie si au moins un de ses littéraux est vrai ;
la clause vide est donc logiquement équivalente à false. Si c est une clause de l’ensemble S,
35
On peut considérer que cette formule représente un théorème mathématique, dont les pi sont les hypothèses
et q la thèse.
36
On observera que cette formule, même si elle représente un théorème de mathématique, n’est pas valide. La
raison en est que dans le cadre de la logique propositionnelle, les propositions élémentaires ne sont pas analysées.
62
S \ {c} est l’ensemble obtenu en enlevant c de S. Si r est une clause, S ∪ {r} est l’ensemble
obtenu en ajoutant r à S.
La figure 27 donne un exemple d’exécution de l’algorithme, permettant de montrer que
l’ensemble
S = {p ∨ ¬r ∨ ¬t , q , r , t ∨ ¬p ∨ ¬r , t ∨ ¬q , ¬p ∨ ¬q ∨ ¬r}
est inconsistant.
1. p ∨ ¬r ∨ ¬t q r t ∨ ¬p ∨ ¬r t ∨ ¬q ¬p ∨ ¬q ∨ ¬r
2. p ∨ ¬r ∨ ¬t q r t ∨ ¬p ∨ ¬r t ¬p ∨ ¬q ∨ ¬r
3. p ∨ ¬t q r t ∨ ¬p ∨ ¬r t ¬p ∨ ¬q ∨ ¬r
4. p ∨ ¬t q r t ∨ ¬p ∨ ¬r t ¬p ∨ ¬r
5. p ∨ ¬t q r t ∨ ¬p ∨ ¬r t ¬p
6. p q r t ∨ ¬p ∨ ¬r t ¬p
7. p q r t ∨ ¬p ∨ ¬r t ✷
S = {p ∨ ¬r ∨ ¬t , q , s , t ∨ ¬p ∨ ¬r , t ∨ ¬q ∨ ¬s , ¬p ∨ ¬q ∨ ¬r}
est consistant.
1. p ∨ ¬r ∨ ¬t q s t ∨ ¬p ∨ ¬r t ∨ ¬q ∨ ¬s ¬p ∨ ¬q ∨ ¬r
2. p ∨ ¬r ∨ ¬t q s t ∨ ¬p ∨ ¬r t ∨ ¬s ¬p ∨ ¬q ∨ ¬r
3. p ∨ ¬r ∨ ¬t q s t ∨ ¬p ∨ ¬r t ¬p ∨ ¬q ∨ ¬r
4. p ∨ ¬r ∨ ¬t q s t ∨ ¬p ∨ ¬r t ¬p ∨ ¬r
5. p ∨ ¬r q s t ∨ ¬p ∨ ¬r t ¬p ∨ ¬r
63
que S0 (l’ensemble de départ, celui qui nous intéresse) est consistant si et seulement si Sf est
consistant. Il se fait que déterminer si Sf est consistant est immédiat. En effet, il n’y a que deux
possibilités :
– L’ensemble Sf contient la clause vide, qui est inconsistante, donc Sf est inconsistant.
– L’ensemble Sf ne contient pas la clause vide. Soit I l’interprétation qui rend vraies
toutes les clauses unitaires (positives) de Sf et fausses toutes les autres propositions.
Cette interprétation rend vraies toutes les clauses unitaires, et aussi toutes les clauses
non unitaires, puisque ces dernières contiennent au moins un littéral négatif dont la
proposition sous-jacente est fausse par définition de I (car cette proposition n’est pas
une clause unitaire, sinon elle donnerait lieu à une étape supplémentaire).
On appelle base de connaissance un ensemble de clauses de Horn positives ; on appelle
question une conjonction de propositions. L’algorithme de résolution unitaire permet de
déterminer si une question A est conséquence logique d’une base de connaissance H ; ce sera
le cas si l’ensemble H ∪ {¬A} est reconnu inconsistant.
Remarque. On peut aussi tester l’ensemble H seul ; il est nécessairement consistant puisqu’il
ne comporte que des clauses de Horn positives.37 La détermination de Hf permet d’obtenir
l’ensemble de toutes les propositions qui sont conséquences logiques de H ; ce sont les
propositions qui apparaissent comme clauses unitaires dans Hf . L’interprétation qui rend vraies
ces propositions et seulement celles-là est le modèle canonique, ou modèle minimal de H. Le
modèle minimal de l’ensemble traité à la figure 28 est donc l’interprétation qui rend vraies les
propositions q, s et t et seulement celles-là.
Remarque. On représente souvent les exécutions de l’algorithme de résolution unitaire sous
forme arborescente ; la représentation correspondant à l’exécution de la figure 27 se trouve à
la figure 29. L’arborescence s’appelle arbre de dérivation, ou arbre de réfutation dans le cas
particulier où on dérive la clause vide.
t ∨ ¬p ∨ ¬r p ∨ ¬r ∨ ¬t r t ∨ ¬q q ¬p ∨ ¬q ∨ ¬r
❅ ❏ ❅ ❅
❅ ❏ ❅ ❅
❅ ❏ ❅ ❅
p ∨ ¬t ❏ t ¬p ∨ ¬r
❏ ✦✦ ✦✦
❅
❅ ✦✦❏ ✦✦
❅✦✦ ❏✦✦
p ¬p
❅
❅
❅
✷
37
L’interprétation qui rend vraies toutes les propositions est donc un modèle de H.
64
3.4.7 La programmation logique propositionnelle
Le problème de la programmation logique propositionnelle consiste à déterminer si une
proposition est ou n’est pas conséquence logique d’un ensemble de clauses de Horn définies,
appelé base de connaissance ou programme logique. Nous venons de voir que l’algorithme
de résolution unitaire est une solution générale et raisonnablement efficace pour ce problème.
Elle n’est cependant pas optimale en pratique. La raison en est que, dans la plupart des cas, la
base de connaissance est énorme, voire infinie, et que la plupart des clauses qu’elle contient
n’ont rien à voir avec la question particulière à traiter. L’algorithme de résolution unitaire
n’accorde aucun rôle particulier à la question traitée, dont la négation est simplement ajoutée à
la base de connaissance. L’algorithme de résolution d’entrée est une variante de l’algorithme
de résolution unitaire, dans laquelle la négation de la question joue un rôle privilégié. Cette
variante est représentée à la figure 30, où L désigne un programme logique.
{G = G0 }
Tant que G 6= ✷ faire
choisir p et c tels que
¬p ∈ G,
c ∈ L et
p ∈ c;
G := (G \ {¬p}) ∨ (c \ {p}).
F IG . 30 – Résolution d’entrée
Cet algorithme utilise une variable G, appelée le but, dont la valeur est toujours une clause
de Horn négative ; initialement, le but est la négation de la question. A chaque étape, le but est
transformé selon la règle suivante : un littéral ¬p du but est remplacé par (c \ {p}), où c est
une clause de la base de connaissance, dont le littéral positif est p. On pourrait démontrer que
l’algorithme de résolution d’entrée est équivalent à l’algorithme de résolution unitaire. A titre
d’exemple, nous montrons à la figure 31 que la proposition p est bien conséquence logique du
programme logique
L = { t ∨ ¬p ∨ ¬r , p ∨ ¬r ∨ ¬t , r , t ∨ ¬q , q } .
On voit que, dans un arbre de réfutation d’entrée, il existe une branche principale unissant
le but initial (ici, ¬p) à la clause vide. Les branches auxiliaires sont de longueur 1 et unissent
une clause d’entrée (d’où le nom de l’algorithme) à un but intermédiaire.
65
t ∨ ¬p ∨ ¬r ¬p p ∨ ¬r ∨ ¬t r t ∨ ¬q q
❅
❅ ✡✡ ✡✡ ✡
✡
❅ ✡ ✡ ✡
¬r ∨ ¬t ✡ ✡ ✡
✡ ✡ ✡
❅
❅ ✡ ✡ ✡
❅✡ ✡ ✡
¬t ✡ ✡
✡ ✡
❅
❅ ✡ ✡
❅✡ ✡
¬q ✡
✡
❅
❅ ✡
❅✡
✷
dans une clause est mal choisi. A titre d’exemple, voici la version Prolog du programme
logique L donné plus haut :
t :- p,r.
p :- r,t.
r.
t :- q.
q.
On voit que la virgule a valeur conjonctive et que le symbole “:-” représente le connecteur ⇐
(inverse de l’implication). L’ordre n’est pas adéquat ici car la clause inutile “t :- p,r.”
court-circuite la clause utile “t :- q.”. Si on omet la clause inutile, le système Prolog
détecte que la proposition p est conséquence logique du programme logique L. Nous
reviendrons sur le système Prolog dans le cadre prédicatif, qui permet des applications plus
intéressantes.
66
La méthode des tables de vérité est peu intéressante ici car le lexique utilisé comporte quatre
propositions ; la table de vérité aurait donc seize lignes. La méthode des tableaux sémantiques
peut s’appliquer ; si nous croyons que l’argument est correct, la racine de notre tableau sera la
négation de l’implication associée à cet argument. La figure 32 représente ce tableau.
Ce tableau est fermé, donc l’argument est correct. On notera cependant que cette
construction n’est que marginalement moins fastidieuse que celle d’une table de vérité à seize
lignes. Il serait souhaitable de disposer de techniques plus expéditives, non seulement pour
gagner du temps, mais aussi pour limiter le risque d’erreur.38 En relisant attentivement la
justification de la méthode des tableaux sémantiques, on peut observer que l’étiquette d’un
nœud peut être remplacée par une autre, pour peu que les deux étiquettes admettent exactement
les mêmes modèles.39
La figure 33 donne un tableau sémantique exploitant ce principe. Les simplifications
successives se basent sur les faits suivants :
– Les ensembles {E ⇒ ¬Q , E} et {¬Q , E} sont logiquement équivalents ;
– Les ensembles {D ∨ A , ¬D} et {A , ¬D} sont logiquement équivalents ;
– Les ensembles {¬Q ⇒ ¬A , A} et {Q , A} sont logiquement équivalents.
Chacune de ces simplifications a permis l’économie d’un branchement.40
38
On dit parfois que le taux d’erreur d’un développement formel (non vérifié par ordinateur) est proportionnel
au carré de la taille de ce développement. . .
39
De plus, pour éviter le risque de non-terminaison, la nouvelle étiquette ne pourra être plus complexe que
l’ancienne.
40
Une autre manière de justifier ces simplifications est d’observer que chaque couple simplifiable comporte
une formule disjonctive et un littéral, et que la décomposition de la formule disjonctive donne lieu à une branche
comportant le littéral opposé et à une branche comportant le couple simplifié. Le “raccourci” proposé consiste à
faire l’économie de la première branche, inutile puisque fermable immédiatement.
67
¬([(E ⇒ ¬Q) ∧ (¬Q ⇒ ¬A) ∧ (D ∨ A)] ⇒ (¬E ∨ D))
↓
[(E ⇒ ¬Q) ∧ (¬Q ⇒ ¬A) ∧ (D ∨ A)] , ¬(¬E ∨ D)
↓
(E ⇒ ¬Q) , (¬Q ⇒ ¬A) , (D ∨ A) , ¬(¬E ∨ D)
↓
(E ⇒ ¬Q) , (¬Q ⇒ ¬A) , (D ∨ A) , E , ¬D
↓
¬Q , (¬Q ⇒ ¬A) , (D ∨ A) , E , ¬D
↓
¬Q , (¬Q ⇒ ¬A) , A , E , ¬D
↓
¬Q , Q , A , E , ¬D
×
{E ⇒ ¬Q , ¬Q ⇒ ¬A , D ∨ A , ¬(¬E ∨ D)} ,
qui se récrit en
{ ¬E ∨ ¬Q , Q ∨ ¬A , D ∨ A , E , ¬D } .
L’une des clauses de cet ensemble comporte deux littéraux positifs, ce qui est incompatible
avec l’utilisation de la théorie de Horn. Dans le cas présent, on remédie à ce problème par
obversion.41 On introduit donc la proposition D̃, définie comme logiquement équivalente à la
formule ¬D. L’ensemble devient
{ ¬E ∨ ¬Q , Q ∨ ¬A , ¬D̃ ∨ A , E , D̃ } .
Cet ensemble de Horn est bien inconsistant, comme le montre le développement de la figure 34.
Croire aux fantômes ? C’est ce que nous suggère le raisonnement ci-dessous, qu’il est
prudent d’analyser . . .
Si on considère que les gens qui étudient les perceptions extra-sensorielles sont honnêtes,
alors il faut admettre l’existence de telles perceptions. De plus, si l’on met à l’épreuve
l’existence des perceptions extra-sensorielles, on se doit de considérer sérieusement la
doctrine de la clairvoyance. Admettre l’existence des perceptions extra-sensorielles doit
nous pousser à mettre celles-ci à l’épreuve et à les expliquer.
41
L’obversion consiste à introduire ou à supprimer une négation dans une phrase sans en changer le sens. Par
exemple, la phrase “Tout ensemble contenant une paire complémentaire de littéraux est inconsistant” devient par
obversion “Aucun ensemble contenant une paire complémentaire de littéraux n’est consistant”.
68
1. ¬E ∨ ¬Q Q ∨ ¬A ¬D̃ ∨ A E D̃
2. ¬Q Q ∨ ¬A ¬D̃ ∨ A E D̃
3. ¬Q Q ∨ ¬A A E D̃
3. ¬Q Q A E D̃
4. ✷ Q A E D̃
hon ⇒ fan .
Les procédés utilisés pour résoudre le problème du récit biblique s’appliquent également
à ce problème ; nous considérons ici seulement la résolution unitaire. La prémisse adm ⇒
(epr ∧ exp) n’est pas une clause, mais est logiquement équivalente à la conjonction des deux
69
clauses adm ⇒ epr et adm ⇒ exp ; de même, la négation de la conclusion hon ⇒ fan
n’est pas une clause, mais est logiquement équivalente à la conjonction des deux clauses hon
et ¬fan. On obtient ainsi le développement de la figure 35, dans laquelle les clauses (de Horn)
ont gardé leur forme implicative.
On voit immédiatement que l’obtention de la nouvelle clause unitaire cla ne permet pas de
progresser, car l’unique autre occurrence de cla est positive, dans la prémisse cla ⇐ occ .
Cependant, si la prémisse
La doctrine de la clairvoyance doit être considérée sérieusement si on est prêt à considérer
sérieusement les phénomènes occultes.
était remplacée par la prémisse
La doctrine de la clairvoyance doit être considérée sérieusement seulement si on est prêt
à considérer sérieusement les phénomènes occultes.
ou encore, ce qui revient au même, par la prémisse
Si la doctrine de la clairvoyance est considérée sérieusement, alors on doit aussi considérer
sérieusement les phénomènes occultes.
la clause cla ⇐ occ serait remplacée par la clause cla ⇒ occ ; cela rendrait l’argument
correct, comme le montre le développement de la figure 36. On voit toute l’importance qu’un
seul mot peut avoir dans un texte . . .
70
1. hon ⇒ adm , epr ⇒ cla , adm ⇒ epr , adm ⇒ exp
cla ⇒ occ , occ ⇒ med , med ⇒ com , com ⇒ fan , hon , ¬fan
2. adm , epr ⇒ cla , adm ⇒ epr , adm ⇒ exp
cla ⇒ occ , occ ⇒ med , med ⇒ com , com ⇒ fan , hon , ¬fan
3. adm , epr ⇒ cla , epr , exp
cla ⇒ occ , occ ⇒ med , med ⇒ com , com ⇒ fan , hon , ¬fan
4. adm , cla , epr , exp
cla ⇒ occ , occ ⇒ med , med ⇒ com , com ⇒ fan , hon , ¬fan
5. adm , cla , epr , exp
occ , occ ⇒ med , med ⇒ com , com ⇒ fan , hon , ¬fan
6. adm , cla , epr , exp
occ , med , med ⇒ com , com ⇒ fan , hon , ¬fan
7. adm , cla , epr , exp
occ , med , com , com ⇒ fan , hon , ¬fan
8. adm , cla , epr , exp , occ , med , com , fan , hon , ¬fan
9. adm , cla , epr , exp , occ , med , com , fan , hon , ✷
71
A B X Y C 1 D1 C 2 D2 C 3 D3 C 4 D4
V V V V V V V V V V V V
V V V F F F V V F F F F
V V F V V V V V V V F F
V V F F V V V V V V V V
F V V V V V V V V V V V
F V V F V F F V V F F F
F V F V V V V V V V F F
F V F F V V V V F V V V
F F V V V V V V V V V V
F F V F V V F F V V F F
F F F V V V V V V V F F
F F F F V V V V F F V V
3.5.3 Problèmes
Le coffre partagé. Cinq personnes (A, B, C, D, E) ont des économies en commun dans un
coffre. N’ayant pas confiance l’une en l’autre, elles décident que le coffre ne pourra s’ouvrir
qu’en présence de A et B, ou de A et C, ou de B, D et E. Combien de serrures le coffre doit-il
avoir ? Combien faut-il de clés et à qui les donne-t-on ?
72
(A ⇒ B) ∧ ¬([(X ⇒ B) ∨ Y ] ⇒ [(X ⇒ A) ∨ Y ])
(A ⇒ B) , ¬([(X ⇒ B) ∨ Y ] ⇒ [(X ⇒ A) ∨ Y ])
(A ⇒ B) , [(X ⇒ B) ∨ Y ] , ¬[(X ⇒ A) ∨ Y ]
(A ⇒ B) , [(X ⇒ B) ∨ Y ] , ¬(X ⇒ A) , ¬Y
(A ⇒ B) , [(X ⇒ B) ∨ Y ] , X , ¬A , ¬Y
✟❍
✟✟ ❍❍
✟✟ ❍❍
✟✟ ❍❍
✟✟ ❍❍
✟✟ ❍❍
¬A , [(X ⇒ B) ∨ Y ] B , [(X ⇒ B) ∨ Y ]
X , ¬A , ¬Y X , ¬A , ¬Y
✟✟❍
❍ ✟✟❍
❍
✟✟ ❍❍ ✟✟ ❍❍
✟✟ ❍❍ ✟✟ ❍❍
¬A , (X ⇒ B) ¬A , Y B , (X ⇒ B) B, Y
X , ¬A , ¬Y X , ¬A , ¬Y X , ¬A , ¬Y X , ¬A , ¬Y
✟❍ ✟❍
✟✟ ❍❍ × ✟✟ ❍❍ ×
✟ ❍ ✟ ❍
¬A , ¬X ¬A , B B , ¬X B, B
X , ¬A , ¬Y X , ¬A , ¬Y X , ¬A , ¬Y X , ¬A , ¬Y
× ×
73
(A ⇒ B) ∧ ¬([(X ⇒ B) ∨ Y ] ⇒ [(X ⇒ A) ∨ Y ])
(A ⇒ B) , ¬([(X ⇒ B) ∨ Y ] ⇒ [(X ⇒ A) ∨ Y ])
(A ⇒ B) , [(X ⇒ B) ∨ Y ] , ¬[(X ⇒ A) ∨ Y ]
(A ⇒ B) , [(X ⇒ B) ∨ Y ] , ¬(X ⇒ A) , ¬Y
(A ⇒ B) , (X ⇒ B) , ¬(X ⇒ A) , ¬Y
(A ⇒ B) , (X ⇒ B) , X , ¬A , ¬Y
(X ⇒ B) , X , ¬A , ¬Y
B , X , ¬A , ¬Y
Ceci montre qu’une solution à quatre serrures (1, 2, 3, 4) convient, avec la distribution de clés
suivante :
A : 1, 2, 3 ; B : 1, 4 ; C : 4 ; D : 2 ; E : 3 .
Penser ou payer ! Vous entrez dans un pub écossais et le barman vous dit : “Vous voyez ces
trois hommes ? L’un d’eux est Monsieur X, qui dit toujours la vérité, un autre est Monsieur Y,
qui ment toujours, et le troisième est Monsieur Z, qui répond au hasard sans écouter les
questions. Vous pouvez poser trois questions (appelant une réponse par oui ou non), en
indiquant chaque fois lequel des trois doit répondre. Si après cela vous pouvez identifier
correctement ces messieurs, ils vous offrent un whisky !”. Comment vous y prenez-vous ?
Il est clair que les réponses de Monsieur Z sont sans intérêt, aussi une bonne tactique consistera
à repérer d’abord quelqu’un qui n’est pas Monsieur Z ; cela peut se faire au moyen d’une
question bien choisie. C’est à ce quelqu’un que l’on posera les deux dernières questions.
On pose à l’un des hommes (I) la question
Votre voisin de gauche (G) est-il plus menteur que votre voisin de droite (D) ?
Examinons, pour les six dispositions possibles, la réponse fournie, étant entendu que Y est plus
menteur que Z, lui-même plus menteur que X :
Réponse Réponse
I G D
exacte fournie
X Y Z oui oui
X Z Y non non
Y X Z non oui
Y Z X oui non
Z X Y non oui/non
Z Y X oui oui/non
74
On observe que si la réponse fournie est oui, le voisin de gauche n’est jamais Z ; c’est donc à
lui que l’on s’adressera pour les deux questions suivantes. de même, si la réponse fournie est
non, c’est au voisin de droite, qui n’est jamais Z, que l’on s’adressera.
Dans les deux cas, on posera ensuite une question dont on connaı̂t la réponse, par exemple
“Etes-vous Monsieur Z ?”, qui identifiera ce nouvel interlocuteur (X si “non”, Y si “oui”). La
troisième question, “Votre voisin de gauche est-il Monsieur Z ?”, permettra de compléter les
identifications.
L’enquête policière. Cinq suspects (A, B, C, D et E) sont interrogés à propos d’un crime.
Voici leurs déclarations :
A: C et D mentent.
B: A et E mentent.
C: B et D mentent.
D: C et E mentent.
E: A et B mentent.
A: a ≡ (¬c ∧ ¬d)
B: b ≡ (¬a ∧ ¬e)
C: c ≡ (¬b ∧ ¬d)
D: d ≡ (¬c ∧ ¬e)
E: e ≡ (¬a ∧ ¬b)
A: ¬c, ¬d
B: ¬b
C: c ≡ ¬d
D: d ≡ ¬c
E: ¬e
On obtient une contradiction, ce qui montre que A a menti. La situation est donc
A: ¬a, c ∨ d
B: b ≡ ¬e
C: c ≡ (¬b ∧ ¬d)
D: d ≡ (¬c ∧ ¬e)
E: e ≡ ¬b
75
Si B dit la vérité, on obtient ¬a, c ∨ d, b, ¬e, ¬c, d.
Si B a menti, on obtient ¬a, c ∨ d, ¬b, e, c, ¬d
En conclusion, A est certainement menteur mais, pour les quatre autres suspects, il y a deux
possibilités : B et D disent la vérité et C et E mentent, ou B et D mentent et C et E disent la
vérité.
Forme normale disjonctive. La figure 40 montre qu’une formule est toujours équivalente à
une disjonction de conjonctions de littéraux.
On appelle forme normale disjonctive (FND) toute disjonction de conjonctions de littéraux.
Toute formule est donc équivalente à une FND.
Remarque. Il s’agit de disjonctions et de conjonctions généralisées, c’est-à-dire à nombre
quelconque (mais fini) de termes.42
V une formule (ℓ
Un cube est une conjonction de littéraux, c’est-à-dire V1 ∧ ℓ2 ∧ · · · ∧ ℓn ) ,
(n ∈ N) , où les ℓi sont des littéraux. On écrit parfois {ℓ1 , . . . , ℓn }, ou i ℓi , ou simplement
{ℓ1 , . . . , ℓn }.
42
W V W V W V
NB : ∅ ↔ false , ∅ ↔ true , {A} ↔ A ↔ {A} , {A, B} ↔ A ∨ B , {A, B} ↔ A ∧ B.
76
p q r p⇒q (p ⇒ q) ⇒ r
V V V V V
V V F V F ( p∧ q ∧ r)
V F V F V ∨ ( p ∧ ¬q ∧ r)
V F F F V ∨ ( p ∧ ¬q ∧ ¬r)
F V V V V ∨ (¬p ∧ q ∧ r)
F V F V F ∨ (¬p ∧ ¬q ∧ r)
F F V V V
F F F V F
Remarque. Dans ce contexte, les connecteurs “0-aires” true et false ne sont pas utilisés.
On observe immédiatement qu’un cube est inconsistant si et seulement s’il contient une
paire complémentaire de littéraux ; de plus, le cube vide est le seul cube valide.
Une forme normale disjonctive est inconsistante si et seulement si tous ses cubes sont
inconsistants. En particulier, la forme normale disjonctive vide est inconsistante.
Intérêt des formes normales. Une forme normale doit être, idéalement
– assez générale pour que chaque formule soit réductible à une forme normale équivalente,
43
Il faut se méfier de cette dernière notation : une clause est un ensemble disjonctif de littéraux.
77
– aussi restrictive que possible, pour que les algorithmes qui traitent les formes normales
soient plus simples que les algorithmes généraux.
Des formes normales conjonctives ou disjonctives distinctes peuvent être équivalentes.
Exemple. La forme normale disjonctive
(p ∧ q ∧ r) ∨ (p ∧ ¬q ∧ r) ∨ (p ∧ ¬q ∧ ¬r) ∨ (¬p ∧ q ∧ r) ∨ (¬p ∧ ¬q ∧ ¬r)
se simplifie en
(p ∧ r) ∨ (¬q ∧ ¬r) ∨ (q ∧ r)
A ∨ (B ∧ C) ↔ (A ∨ B) ∧ (A ∨ C)
(A ∧ B) ∨ C ↔ (A ∨ C) ∧ (B ∨ C)
(¬p ⇒ ¬q) ⇒ (p ⇒ q)
¬(¬¬p ∨ ¬q) ∨ (¬p ∨ q) (élimination ⇒)
(¬¬¬p ∧ ¬¬q) ∨ (¬p ∨ q) (propagation ¬)
(¬p ∧ q) ∨ (¬p ∨ q) (double négation)
(¬p ∨ ¬p ∨ q) ∧ (q ∨ ¬p ∨ q) (distributivité)
78
Algorithme de normalisation (variante). Une variante intéressante de l’algorithme de
normalisation est représentée à la figure 41. La donnée manipulée est un ensemble conjonctif L
de disjonctions généralisées. Initialement, l’unique élément de L est la formule donnée A (vue
comme une disjonction généralisée à un terme). La valeur finale de L est une FNC équivalente
à A. On appelle non-clause toute disjonction (généralisée) dont au moins un terme n’est pas
un littéral. La preuve de terminaison est analogue à celle pour la construction des tableaux
sémantiques. La valeur finale de L est l’ensemble de clauses cherché.
Remarque. Cet algorithme n’est qu’une reformulation de l’algorithme précédent. L’intérêt est
lié à la méthode de résolution vue plus loin.
L := {A} ;
Tant queVL comporte une non-clause faire
{ L ↔ A est invariant }
choisir une non-clause D ∈ L ;
choisir un non-littéral t ∈ D ;
∗ si t = ¬¬t′ faire
D ′ := (D − t) + t′ ;
{ D ↔ D′ }
L := (L\{D}) ∪ {D ′ }
∗ si t = α faire
t1 := α1 ; t2 := α2 ;
D1 := (D − t) + t1 ; D2 := (D − t) + t2 ;
{ D ↔ D1 ∧ D2 }
L := (L\{D}) ∪ {D1 , D2 }
∗ si t = β faire
t1 := β1 ; t2 := β2 ;
D ′ := ((D − t) + t1 ) + t2 ;
{ D ↔ D′ }
L := (L\{D}) ∪ {D ′ }
F IG . 41 – Algorithme de normalisation.
79
1. On peut supprimer les répétitions de littéraux au sein d’une même clause.
Exemple : (¬p ∨ q ∨ ¬p) ∧ (r ∨ ¬p) ↔ (¬p ∨ q) ∧ (r ∨ ¬p).
2. Les clauses valides (elles contiennent une paire complémentaire de littéraux) peuvent
être supprimées.
Exemple : (¬p ∨ q ∨ p) ∧ (r ∨ ¬p) ↔ (r ∨ ¬p).
3. Une clause contenant une autre clause peut être supprimée.
Exercice : justifier la règle.
Exemple : (r ∨ q ∨ ¬p) ∧ (¬p ∨ r) ↔ (¬p ∨ r).
Ces simplifications élémentaires sont faciles à mettre en œuvre mais ne conduisent pas à une
forme normale unique. Par exemple, elles ne permettent pas de réduire (p ∨ ¬q) ∧ q en p ∧ q.
A ∨ X , B ∨ ¬X
A∨B
Fermeture par résolution. On définit par induction la relation ⊢R (que nous noterons
simplement ⊢) entre un ensemble de clauses et une clause ; c’est la plus petite relation vérifiant
les deux conditions suivantes :
1. Si C ∈ S, alors S ⊢ C.
2. Soient C1 = (C1′ ∨ p) et C2 = (C2′ ∨ ¬p) ;
si S ⊢ C1 et S ⊢ C2 , alors S ⊢ C1′ ∨ C2′ .
Les deux clauses C1 et C2 sont dites résolvables (par rapport à p) ; leur résolvante est la clause
res(C1 , C2 ) =def C1′ ∨ C2′ .
Si S est un ensemble de clauses, S R dénote la fermeture de S par résolution, c’est-à-dire le
plus petit sur-ensemble de S contenant les résolvantes de ses éléments. On a S R = {C : S ⊢
C} = {C : S R ⊢ C}.
80
2. Soient C1 = (C1′ ∨ p) et C2 = (C2′ ∨ ¬p) ;
si S |= C1 et S |= C2 , alors S |= C1′ ∨ C2′ .
La première condition est évidente, la seconde est une conséquence de l’énoncé {(A ∨
X), (B ∨ ¬X)} |= (A ∨ B) , valable quelles que soient les formules A, B et X.
Remarque. On déduit de ceci que les ensembles S et S R sont logiquement équivalents, pour
tout ensemble S de clauses.
{p, ¬p} |= q ,
Preuve de complétude dans le cas fini. Soit S inconsistant et fini ; on doit prouver S ⊢
✷. Comme d’habitude, on souhaite une preuve constructive, c’est-à-dire un moyen effectif
d’obtenir ✷ au départ de S, par applications répétées de la règle de résolution.
81
p p
q q q q
r r r r r r r r
Soit A un arbre sémantique pour S. Chaque chemin dans cet arbre allant de la racine à un
nœud n définit un ensemble de propositions Π(n) et une interprétation vn pour cet ensemble ;
vn rend vrais les littéraux étiquetant le chemin.
S est inconsistant, donc S est falsifié par toutes les interprétations définies par les feuilles
de A. Par conséquent, à chaque feuille f de l’arbre correspond au moins une clause Cf ∈ S
telle que
ΠCf ⊆ Π(f ) = ΠS et vf (Cf ) = F .
(ΠCf est l’ensemble des propositions intervenant dans Cf .) La feuille f est étiquetée Cf .
Soit S R = S ∪ {C : S ⊢ C}. On va montrer qu’il est possible d’étiqueter chaque nœud
intérieur n de l’arbre au moyen d’une clause Cn ∈ S R telle que
On suppose
Cn1 ∈ S R et ΠCn1 ⊆ Π(n1 ) et vn1 (Cn1 ) = F
Cn2 ∈ S R et ΠCn2 ⊆ Π(n2 ) et vn2 (Cn2 ) = F
L’étiquette Cn de n sera Cn1 ou Cn2 ou res(Cn1 , Cn2 ) et ne contiendra ni p ni ¬p ; cela suggère
la politique de choix suivante :
– Si p 6∈ ΠCni pour i = 1 ou 2, alors Cn = Cni .
82
– Si p ∈ ΠCn1 et p ∈ ΠCn2 :
vn1 (Cn1 ) = F implique Cn1 = Cn′ 1 ∨ ¬p et vn2 (Cn2 ) = F implique Cn2 = Cn′ 2 ∨ p.
On pose Cn = Cn′ 1 ∨ Cn′ 2 = res p (Cn1 , Cn2 ).
Dans les deux cas, on a Cn ∈ S R et ΠCn ⊆ Π(n) et vn (Cn ) = F.
Ceci achève la démonstration du cas fini.
Un exemple d’étiquetage complet de l’arbre sémantique est donné à la figure 43.
¬p p p p
q q q q p∨q
¬p ¬p p ∨ ¬q
r r r r r r r r
Complétude dans le cas infini, preuve indirecte. On a jusqu’ici supposé que S était fini
mais, vu le théorème de compacité, le résultat
reste valable si S est infini. En effet, si S est inconsistant, il admet un sous-ensemble fini Sf
inconsistant ; on en déduit ✷ ∈ SfR , d’où a fortiori ✷ ∈ S R .
Complétude dans le cas infini, preuve directe. Prouver directement ce résultat revient à
donner une autre preuve, moins abstraite, du théorème de compacité. On se limite au cas
habituel où le lexique Π est un ensemble dénombrable. L’arbre sémantique correspondant
A comporte une infinité de branches, elles-mêmes infinies. A chaque nœud n on associe vn
comme précédemment ; le nœud n est un nœud-échec s’il existe Cn ∈ S telle que vn (Cn ) = F.
On obtient l’arbre B en élaguant A, de telle sorte que les feuilles de B soient des nœuds-
échecs et que les nœuds intérieurs ne le soient pas. (Les feuilles de B ne sont pas nécessairement
toutes au même niveau.)
L’ensemble S étant inconsistant, toutes les branches de B sont finies. Un arbre binaire dont
toutes les branches sont finies est nécessairement fini (c’est un cas particulier du classique
lemme de König, dont nous (re)verrons la démonstration au paragraphe suivant). On applique
à B la technique d’étiquetage introduite pour le cas fini. L’ensemble S0 ⊂ S des clauses
associées aux feuilles de B est donc tel que ✷ ∈ S0R , et S0 est un sous-ensemble fini
83
inconsistant de S. On a donc prouvé que tout ensemble inconsistant de clauses construit au
moyen d’un lexique dénombrable admet un sous-ensemble fini inconsistant. Toute formule
étant logiquement équivalente à un ensemble (conjonctif) de clauses, on a en fait démontré que
tout ensemble inconsistant de formules construit au moyen d’un lexique dénombrable admet
un sous-ensemble fini inconsistant.
Lemme de König. Définition. Un arbre fini est un arbre comportant un nombre fini de nœuds.
Un arbre est finitaire si chaque nœud a un nombre fini de fils.
Lemme. Tout arbre infini finitaire a au moins une branche infinie.
Démonstration. Considérons un arbre infini finitaire. Soit n0 sa racine. L’arbre est infini, donc
n0 a un nombre infini de descendants. L’arbre est finitaire, donc n0 a un descendant direct,
soit n1 , qui a un nombre infini de descendants. De même, n1 doit avoir un descendant direct,
soit n2 , qui a un nombre infini de descendants. On peut itérer indéfiniment ; on obtient ainsi la
branche infinie n0 , n1 , n2 , . . .
F IG . 44 – Procédure de résolution.
Remarque sur l’invariant de boucle. Ajouter à S des conséquences logiques de ses éléments ne
change pas l’ensemble MS des modèles de S.
Remarque sur la procédure de choix. On admet qu’aucune paire de clauses résolvables ne peut
être choisie plus d’une fois ; cela garantit la terminaison puisqu’un lexique de n propositions
donne lieu à 3n clauses distinctes non valides. Le programme peut se terminer normalement
(garde falsifiée) ou anormalement (plus de choix possible).
Terminaison normale. Si la garde devient fausse, la valeur finale Sf vérifie MSf = MS0 et
✷ ∈ Sf , ce qui implique l’inconsistance de Sf et de S0 .
Terminaison anormale. Si toutes les résolvantes ont été calculées sans produire ✷, on a
MSf = MS0 et ✷ 6∈ Sf . Cela implique la consistance de Sf et de S0 .
Remarque. Une dérivation de ✷ (false) à partir de S est appelée une réfutation de S.
84
Exemples de réfutations. Soit S l’ensemble des quatre clauses suivantes :
1. p∨q
2. p∨r
3. ¬q ∨ ¬r
4. ¬p
Cet ensemble est inconsistant ; il admet au moins une réfutation. Comme souvent, il en existe
plusieurs, telles que
5. q (1, 4) 5. p ∨ ¬r (1, 3)
6. r (2, 4) 6. q (1, 4)
7. ¬q (3, 6) 7. p ∨ ¬q (2, 3)
8. ✷ (5, 7) 8. r (2, 4)
9. p (2, 5)
10. ¬r (3, 6)
11. ¬q (3, 8)
12. ¬r (4, 5)
13. ¬q (4, 7)
14. ✷ (4, 9)
85
3.7 Exercice de récapitulation
Soit A la formule [(p ∧ q) ∨ (r ⇒ s)] ⇒ [(p ∨ (r ⇒ s)) ∧ (q ∨ (r ⇒ s))] .
On utilise diverses méthodes pour prouver la validité de A.
p=V:
[(T ∧ q) ∨ (r ⇒ s)] ⇒ [(T ∨ (r ⇒ s)) ∧ (q ∨ (r ⇒ s))],
[q ∨ (r ⇒ s)] ⇒ [T ∧ (q ∨ (r ⇒ s))],
[q ∨ (r ⇒ s)] ⇒ [q ∨ (r ⇒ s)],
V;
p=F:
[(F ∧ q) ∨ (r ⇒ s)] ⇒ [(F ∨ (r ⇒ s)) ∧ (q ∨ (r ⇒ s))],
[F ∨ (r ⇒ s)] ⇒ [(r ⇒ s) ∧ (q ∨ (r ⇒ s))],
(r ⇒ s) ⇒ [(r ⇒ s) ∧ (q ∨ (r ⇒ s))] ;
q = V : (r ⇒ s) ⇒ [(r ⇒ s) ∧ (T ∨ (r ⇒ s))],
(r ⇒ s) ⇒ [(r ⇒ s) ∧ T ],
(r ⇒ s) ⇒ (r ⇒ s),
V;
q = F : (r ⇒ s) ⇒ [(r ⇒ s) ∧ (F ∨ (r ⇒ s))],
(r ⇒ s) ⇒ [(r ⇒ s) ∧ (r ⇒ s)],
(r ⇒ s) ⇒ (r ⇒ s),
V.
Diverses variantes existent selon le nombre de règles simplificatrices admises (assez réduit
ici) et le niveau auquel on les applique (ici, tous).
86
3.7.3 Tableau sémantique (notation réduite)
¬A, (p ∧ q) ∨ (r ⇒ s),
¬[(p ∨ (r ⇒ s)) ∧ (q ∨ (r ⇒ s))]
ւ ց
¬(p ∨ (r ⇒ s)), ¬(q ∨ (r ⇒ s)),
¬p, ¬(r ⇒ s) ¬q, ¬(r ⇒ s)
ւ ց ւ ց
p ∧ q, p, q r⇒s p ∧ q, p, q r⇒s
× × × ×
On observe une certaine redondance dans les calculs ; c’est le prix à payer pour une méthode
facilement mécanisable.
Une conjonction est valide si et seulement si tous ses termes sont valides. On prouve donc
séparément la validité des deux formules
A1 =def (¬p ∧ r ∧ ¬s) ∨ (¬q ∧ r ∧ ¬s) ∨ p ∨ ¬r ∨ s
et
A2 =def (¬p ∧ r ∧ ¬s) ∨ (¬q ∧ r ∧ ¬s) ∨ q ∨ ¬r ∨ s.
Chacune de ces formules se réduit à une conjonction de 9 clauses ; on considère seulement
la formule A1 . Les clauses sont
¬p ∨ ¬q ∨ p ∨ ¬r ∨ s
¬p ∨ r ∨ p ∨ ¬r ∨ s
¬p ∨ ¬s ∨ p ∨ ¬r ∨ s
r ∨ ¬q ∨ p ∨ ¬r ∨ s
r ∨ r ∨ p ∨ ¬r ∨ s
r ∨ ¬s ∨ p ∨ ¬r ∨ s
¬s ∨ ¬q ∨ p ∨ ¬r ∨ s
¬s ∨ r ∨ p ∨ ¬r ∨ s
¬s ∨ ¬s ∨ p ∨ ¬r ∨ s
Chaque clause comporte une paire complémentaire de littéraux et est donc valide.
87
3.7.5 Résolution
On commence par réduire ¬A en forme clausale.
88
1. ¬A
2. (p ∧ q) ∨ ¬r ∨ s 1, α1
3. ¬[(p ∨ ¬r ∨ s) ∧ (q ∨ ¬r ∨ s)] 1, α2
4. ¬(p ∨ ¬r ∨ s) ∨ ¬(q ∨ ¬r ∨ s) 3, β
5. p ∨ ¬r ∨ s 2, α1
6. q ∨ ¬r ∨ s 2, α2
7. ¬(q ∨ ¬r ∨ s) 4, 5, R
8. ✷ 6, 7, R
est de la forme
(A ∨ B) ⇒ (C ∧ D) ,
et qu’une telle formule est valide si et seulement si les formules A ⇒ C, A ⇒ D, B ⇒ C,
B ⇒ D sont valides. On doit donc prouver
|= (p ∧ q) ⇒ (p ∨ (r ⇒ s)) ,
|= (p ∧ q) ⇒ (q ∨ (r ⇒ s)) ,
|= (r ⇒ s) ⇒ (p ∨ (r ⇒ s)) ,
|= (r ⇒ s) ⇒ (q ∨ (r ⇒ s)) ,
ce qui est évident dans chaque cas.
89
4 Méthodes déductives : le système de Hilbert
4.1 Introduction
Nous avons vu qu’une théorie est l’ensemble des conséquences logiques d’un ensemble
donné de formules, appelées axiomes ou postulats. Ces conséquences logiques sont appelées
théorèmes. Développer une théorie consiste donc à repérer les théorèmes parmi les formules
construites au moyen du lexique (du langage) utilisé pour introduire les postulats. Deux grandes
techniques existent pour cela, la méthode analytique et la méthode synthétique.
Jusqu’ici, nous avons utilisé la méthode analytique, sous la forme d’une procédure de
décision. Pour analyser une formule propositionnelle, il suffit de construire un ou deux
tableau(x) sémantique(s). Cette approche est excellente . . . quand elle est possible. En logique
prédicative, qui est la logique des mathématiciens, on ne dispose pas en général d’une
procédure de décision ; même quand elle existe, elle peut être difficile à mettre en œuvre.
De plus, une procédure de décision pour la validité ne donne guère d’information sur le
lien sémantique entre axiomes et théorèmes. Enfin, les procédures de décision sont souvent
inefficaces parce qu’elles ne réutilisent pas les résultats. On ne peut pas, en général, accélérer
la validation d’un théorème sur base d’autres théorèmes antérieurement démontrés.
Les mathématiciens utilisent le plus souvent la méthode synthétique. Des théorèmes
simples sont obtenus à partir des postulats au moyen de quelques mécanismes de raisonnement.
Ces mêmes mécanismes, appliqués aux théorèmes simples, permettent de démontrer des
théorèmes plus difficiles, et ainsi de suite. L’approche synthétique est également utilisée dans
les autres sciences exactes, et notamment en physique ; dans une certaine mesure, on utilise
également l’approche synthétique en médecine, en psychologie, en sociologie, etc. Un aspect
typique de cette approche est l’exploitation de résultats antérieurs pour produire des résultats
nouveaux. Le principal avantage de cette approche est sa généralité. La méthode synthétique
s’accommode d’un ensemble infini de postulats (chaque preuve n’en utilise qu’un nombre
fini) ; elle permet d’isoler les postulats nécessaires à la production d’un théorème donné,
ce qui permet notamment de déterminer si un théorème subsiste ou non quand l’ensemble
des postulats est modifié. La théorie est développée de manière modulaire, chaque théorème
pouvant être assimilé à un postulat supplémentaire, disponible pour l’obtention de nouveaux
théorèmes.
Ces avantages ont un prix. L’obtention de théorèmes par l’approche synthétique est
un processus foncièrement non déterministe, pouvant requérir créativité, inventivité . . . et
tâtonnement, au contraire de l’approche analytique dans laquelle le non-déterminisme est
inexistant (tables de vérité) ou peu important (tableaux sémantiques). Des choix inadéquats
conduisent à des théorèmes corrects mais inintéressants ; on voit qu’une certaine forme de
créativité est nécessaire ici. On peut même dire que le talent du mathématicien consiste
essentiellement à opérer les bons choix, ceux qui conduisent à valider (ou à infirmer) les
conjectures les plus remarquables.44
La logique propositionnelle est suffisamment élémentaire pour être correctement
44
Une autre facette du talent du mathématicien est l’aptitude à créer de nouveaux ensembles de postulats
conduisant à des théories intéressantes.
90
appréhendée au moyen des seules méthodes analytiques. Nous introduisons néanmoins
l’approche synthétique pour préparer le lecteur à son utilisation dans le cadre plus complexe
de la logique prédicative.
A, B et C sont des formules quelconques, n’utilisant que les connecteurs “¬” et “⇒”.45
Un axiome proprement dit s’obtient en instanciant l’un des trois schémas, c’est-à-dire en
remplaçant A, B, C par des formules. Par exemple, la formule (p ⇒ q) ⇒ (p ⇒ (p ⇒ q))
est un axiome, obtenu en appliquant la substitution [A/(p ⇒ q), B/p] au premier schéma. La
notation “⊢ ϕ” se lit “ϕ est un théorème”. Rappelons ici que tout axiome est un théorème. Le
système de Hilbert comporte la seule règle d’inférence “Modus ponens”. Cette règle permet
d’obtenir le théorème B au départ des théorèmes A et A ⇒ B.
4.3 Preuves
Une preuve dans H est une séquence de formules, chaque formule étant
– l’instance d’un axiome, ou
– inférée de deux formules la précédant dans la séquence, au moyen de la règle d’inférence
Modus ponens.
Par définition, tout élément d’une preuve, et en particulier le dernier, est un théorème ; si A est
le dernier élément de la séquence, celle-ci est une preuve de A. A titre d’exemple, une preuve
de l’implication p ⇒ p est donnée à la figure 45.
Remarques. Par facilité, chaque élément d’une preuve est précédé d’un numéro d’ordre et suivi
d’une brève justification ; “Axiome 1” veut dire “instance du schéma d’axiome 1” et “4, 3, MP”
veut dire “obtenu à partir des formules de numéros 4 et 3 (prémisses) par la règle du Modus
ponens”. La preuve donnée ici établit que la formule (p ⇒ p) est un théorème, ou encore que
l’assertion ⊢ (p ⇒ p) (lire : “(p ⇒ p) est un théorème”) est un métathéorème (c’est-à-dire un
théorème au sens mathématique courant ; le préfixe “méta” est souvent omis).46 L’expression
45
Il existe des variantes permettant l’emploi de tous les connecteurs habituels, mais la version présentée ici est
plus simple, sans être réellement restrictive ; on considère p ∨ q comme une abréviation de ¬p ⇒ q, et p ∧ q
comme une abréviation de ¬(p ⇒ ¬q).
46
Signalons que (p ⇒ p) est une formule, donc un objet du langage, tandis que ⊢ (p ⇒ p) est une assertion,
donc un objet du métalangage.
91
1. ⊢ p ⇒ ((p ⇒ p) ⇒ p) (Axiome 1)
2. ⊢ (p ⇒ ((p ⇒ p) ⇒ p)) ⇒ ((p ⇒ (p ⇒ p)) ⇒ (p ⇒ p)) (Axiome 2)
3. ⊢ (p ⇒ (p ⇒ p)) ⇒ (p ⇒ p) (1, 2, MP)
4. ⊢ p ⇒ (p ⇒ p) (Axiome 1)
5. ⊢ p ⇒ p (4, 3, MP)
(A ⇒ A) est un schéma de théorème ; toute instance d’un schéma de théorème est un théorème.
On transforme facilement la preuve de (p ⇒ p) en une preuve de (p ⇒ q) ⇒ (p ⇒ q), par
exemple.
La preuve donnée plus haut peut se représenter de manière arborescente (figure 46). Cette
représentation est plus naturelle que la représentation séquentielle introduite plus haut, mais
n’est guère utilisée à cause de son encombrement.
⊢ (p ⇒ (p ⇒ p)) ⇒ (p ⇒ p) ⊢ p ⇒ (p ⇒ p)
⊢p⇒p
On peut aussi (figure 47) ne mentionner dans l’arborescence que les numéros des formules
impliquées, ce qui réduit l’encombrement.
1 2
3 4
5
Il existe une nette analogie entre une preuve de Hilbert (représentée de manière
arborescente) et une dérivation de séquent, mais il y a aussi quelques différences :
– Le symbole “⊢” remplace le symbole “→”.
– Les antécédents sont vides (pour l’instant).
– Les succédents comportent un seul élément.
– Le sens de “axiome” a changé.
– L’unique règle est le Modus ponens, qui n’est pas analytique, ni réversible.
92
En dépit de ces différences, on peut dire que le système de Hilbert est un calcul de séquent
(synthétique).
Remarque. Le mot “axiome” a en fait plusieurs sens relativement voisins, mais qu’il convient
de distinguer. Dans le cadre de la méthode (analytique) des séquents, un axiome est un séquent
d’un type particulier, dont la validité est immédiate. Dans le cadre du système de Hilbert, un
axiome est une tautologie d’un certain type, obtenue par instantiation d’un schéma particulier.
Dans les deux cas, l’idée de validité est importante. En revanche, dans le langage courant,
dans le langage mathématique général et dans le cadre plus technique des théories logiques
(surtout prédicatives), les axiomes ne sont pas des tautologies mais des énoncés consistants
dont on souhaite étudier l’ensemble des conséquences logiques. Dans le cadre de cette étude
seulement, les axiomes sont considérés comme toujours vrais ; il s’agit donc d’une validité
“locale”, limitée à un certain contexte. En pratique, ce contexte peut paraı̂tre universel. C’est le
cas de l’énoncé “l’addition est commutative”, traduit par la formule ∀x ∀y (x+y = y+x). Cette
formule n’est pourtant valide que si on interprète de manière adéquate le symbole fonctionnel
“+” et le symbole prédicatif “=”.
Notons aussi que le mot “postulat” est synonyme du mot “axiome” mais que ce dernier
insiste plus sur l’aspect “vérité universelle” tandis que “postulat” met plus l’accent sur l’aspect
relatif de la validité. Le célèbre énoncé d’Euclide “Par tout point extérieur à une droite passe
une et une seule parallèle à cette droite” est un axiome de la géométrie classique47 et un
postulat — auquel il est parfois profitable de renoncer — de la géométrie moderne. De même,
la commutativité de l’addition est un axiome (ou un théorème) en arithmétique et un postulat
en théorie des groupes.
4.4 Dérivations
Un ensemble U de formules quelconques étant donné, une dérivation ou preuve avec
hypothèses dans H est une séquence de formules, chaque formule étant
– une hypothèse (élément de U), ou
– une instance d’un axiome, ou
– inférée de deux formules précédentes, au moyen du Modus ponens.
Le métathéorème relatif à une preuve avec hypothèses s’écrit U ⊢H A ou U ⊢ A . Un exemple
de dérivation est donné à la figure 48. Comme pour les preuves, les lignes sont numérotées et
accompagnées d’une courte justification. En outre, l’ensemble des hypothèses est rappelé à
chaque ligne. On verra plus loin pourquoi.
Remarque. En général, le dernier élément A d’une dérivation n’est pas un théorème. On verra
plus loin que U ⊢ A a lieu si et seulement si on a U |= A ; en particulier, ⊢ A a lieu si et
seulement si A est une tautologie.
Remarques. Il est souvent plus facile d’établir A, B, C ⊢ D que ⊢ A ⇒ (B ⇒ (C ⇒ D)),
mais on montrera qu’une dérivation du premier énoncé se convertit automatiquement en une
preuve du second ; la dérivation ci-dessus établit donc indirectement
⊢ (p ⇒ (q ⇒ r)) ⇒ (q ⇒ (p ⇒ r)) .
47
Après en avoir longtemps été une conjecture, dont les mathématiciens ont finalement déterminé qu’elle ne
pouvait être déduite des autres axiomes.
93
1. p ⇒ (q ⇒ r), q, p ⊢ p ⇒ (q ⇒ r) (Hypothèse)
2. p ⇒ (q ⇒ r), q, p ⊢ p (Hypothèse)
4. p ⇒ (q ⇒ r), q, p ⊢ q (Hypothèse)
La représentation arborescente, style séquent, reste possible. Les hypothèses deviennent les
éléments des antécédents. (Le sens du mot “hypothèse” a donc changé.)
94
aurons montré que U ⊢ A est assimilable à U |= A , on pourra prouver facilement qu’une
règle est correcte. Par exemple, la règle
U , ¬X ⊢ X
U ⊢ X
est correcte, parce que si X est conséquence logique de U ∪{¬X}, alors X est est conséquence
logique de U. Nous devrons cependant établir directement certaines règles, nécessaires pour
démontrer que les relations ⊢ et |= sont coextensives.
Remarque. Dans ce contexte, “U, A” abrège “U ∪ {A}”.
On notera que les principes de composition et de substitution uniforme peuvent se traduire
par des règles dérivées, de même que le principe de monotonie, selon lequel une hypothèse
supplémentaire n’altère pas les dérivations faites sans elle. On a
U ⊢A U, A ⊢ B
U ⊢B
U ⊢A
U[p/B] ⊢ A[p/B]
U ⊢A
U, B ⊢ A
95
n′ . U ⊢ A ⇒ X.
On distingue quatre cas :
1. X est un axiome ;
2. X est une hypothèse de l’ensemble U ;
3. X est la nouvelle hypothèse A ;
4. X est inféré par Modus ponens.
– Dans les cas 1 et 2, l’étape
n. U, A ⊢ X (Ai ou H)
est remplacée par les trois étapes suivantes :
n′ −2. U ⊢ X (Ai ou H)
′
n −1. U ⊢ X ⇒ (A ⇒ X) (A1)
′ ′ ′
n. U ⊢ A⇒X (n −2, n −1, MP)
– Dans le cas 3, l’étape U, A ⊢ A est remplacée par cinq étapes calquées sur la
démonstration de ⊢ (p ⇒ p) donnée plus haut ; la dernière de ces cinq nouvelles étapes
est naturellement U ⊢ (A ⇒ A).
– Dans le cas 4, la preuve Π1 comporte les étapes
i. U, A ⊢ Y (. . .)
j. U, A ⊢ Y ⇒ X (. . .)
n. U, A ⊢ X (i, j, MP)
Le préfixe déjà construit de Π2 comportera
i′ . U ⊢ A ⇒ Y (. . .)
′
j . U ⊢ A ⇒ (Y ⇒ X) (. . .)
Le fragment de Π2 relatif à la nième étape de Π1 sera :
n′ −2. U ⊢ (A ⇒ (Y ⇒ X)) ⇒ ((A ⇒ Y ) ⇒ (A ⇒ X)) (A2)
′ ′ ′
n −1. U ⊢ (A ⇒ Y ) ⇒ (A ⇒ X) (j , n −2, MP)
′
n. U ⊢ (A ⇒ X) (i′ , n′ −1, MP)
Ceci achève la démonstration.
96
1. ⊢ (A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C))
2. ⊢ (A ⇒ (B ⇒ C)) ⇒ (B ⇒ (A ⇒ C))
3. ⊢ ¬A ⇒ (A ⇒ B)
4. ⊢ A ⇒ (¬A ⇒ B)
5. ⊢ ¬¬A ⇒ A
6. ⊢ A ⇒ ¬¬A
7. ⊢ (A ⇒ B) ⇒ (¬B ⇒ ¬A)
8. ⊢ B ⇒ (¬C ⇒ ¬(B ⇒ C))
9. ⊢ (B ⇒ A) ⇒ ((¬B ⇒ A) ⇒ A)
Il s’agit en fait de schémas de théorèmes ; chacune des lettres A, B et C désigne ici n’importe
quelle formule.
Dans la suite, on évitera la construction des preuves ; on préférera démontrer simplement
l’existence d’une preuve. Les notions de dérivation et de règle dérivée ont pour but de faciliter
ces démonstrations d’existence.
A titre d’exemple, une dérivation du théorème 6 est donnée à la figure 49, les théorèmes 1
à 5 étant supposés déjà démontrés. On voit ici l’utilité capitale du principe de composition ; la
règle de déduction facilite le travail de justification . . . qui n’est quand même pas évident.
F IG . 49 – Justification de ⊢ A ⇒ ¬¬A .
Remarque. Une règle dérivée évidente, le plus souvent utilisée implicitement, est la règle
d’augmentation ; elle s’écrit
U ⊢A
U, B ⊢ A
et exprime qu’une hypothèse disponible ne doit pas nécessairement être utilisée.
97
4.7.2 Quelques autres règles dérivées
Notons d’emblée un puissant moyen de construire des règles dérivées.
U ⊢A
Métarègle. Si ⊢ A ⇒ B, alors est une règle dérivée correcte.
U ⊢B
Cela formalise une démarche intuitive :
1. Ayant démontré A en supposant U, soit U ⊢ A,
2. on utilise le théorème ⊢ A ⇒ B
3. et on applique la règle du Modus ponens à (1) et (2) pour obtenir U ⊢ B.
On obtient ainsi diverses règles dérivées utiles, dont voici quatre exemples :
U ⊢ ¬B ⇒ ¬A
Contraposée
U ⊢A⇒B
U ⊢ A⇒B U ⊢ B ⇒C
Transitivité
U ⊢A⇒C
U ⊢ ¬¬A
Double négation
U ⊢A
U ⊢ A ⇒ (B ⇒ C)
Echange d’antécédents
U ⊢ B ⇒ (A ⇒ C)
U, B ⊢ A U, ¬B ⊢ A
U ⊢A
98
U, B ⊢ A Prémisse
U ⊢B⇒A Déduction
⊢ (B ⇒ A) ⇒ ((¬B ⇒ A) ⇒ A) Théorème 9, § 4.7.1
U ⊢ (¬B ⇒ A) ⇒ A MP
U, ¬B ⊢ A Prémisse
U ⊢ ¬B ⇒ A Déduction
U ⊢A MP
U |= A
99
Le système le plus simple de vérification de tautologie est sans doute la méthode des tables
de vérité.49 Le lemme de Kalmar spécifie qu’à chaque ligne d’une table de vérité correspond
une dérivation dans le système de Hilbert.
Lemme. Soit A une formule construite à partir des propositions p1 , . . . , pn et des
connecteurs “¬” et “⇒”. Soit v une interprétation. Si on définit p′k comme pk ou ¬pk selon
que v(pk ) est V ou F, et si on définit A′ comme A ou ¬A selon que v(A) est V ou F, on a
{p′1 , . . . , p′n } ⊢ A′
p q r s (p ⇒ q) ⇒ ¬(¬r ⇒ s)
F F V V F
Remarque. Le lemme de Kalmar permet de “coder” une ligne de table de vérité dans le système
de Hilbert ; il contribue donc à établir que U |= A implique U ⊢ A.
100
Premier sous-cas. Deuxième sous-cas.
v(B) = F et v(A) = V. v(B) = V et v(A) = F.
{p′1 , . . . , p′n } ′
⊢B , {p′1 , . . . , p′n } ⊢ B ′
{p′1 , . . . , p′n } ⊢ ¬B , {p′1 , . . . , p′n } ⊢ B ,
{p′1 , . . . , p′n } ⊢ A , B ⊢ ¬¬B ,
{p′1 , . . . , p′n } ⊢ A′ . {p′1 , . . . , p′n } ⊢ ¬¬B ,
{p′1 , . . . , p′n } ⊢ ¬A ,
{p′1 , . . . , p′n } ⊢ A′ .
Remarque. On a raisonné par cas pour établir {p′1 , . . . , p′n } ⊢ A′ , sans pour autant utiliser la
règle dérivée de disjonction des cas.50 En fait, cette règle dérivée est, comme les autres, une
version particulière et formelle d’une technique de raisonnement (informel).
{p′1 , . . . , p′n } ⊢ A ,
{p′1 , . . . , p′n−1 } ⊢ A ,
50
En revanche, cette règle sera utilisée explicitement au paragraphe suivant.
101
et, plus généralement, les 2k théorèmes suivants, pour tout k ∈ {0, 1, . . . , n} :
{p′1 , . . . , p′k } ⊢ A ,
⊢ A,
102
En mathématique, on définit une relation R d’arité n sur les ensembles D1 , D2 , . . . , Dn
comme un sous-ensemble du produit cartésien D1 × D2 × · · · × Dn . Voici à titre d’exemple la
description de quelques relations importantes de l’arithmétique :
PPQ(x, y) = {(x, y) ∈ (N × N) : x < y}
= {(0, 1), (0, 2), (0, 3), . . . , (1, 2), (1, 3), . . . , (2, 3), . . .}
CARRE (x, y) = {(x, y) ∈ (N × N) : y = x2 } = {(0, 0), (1, 1), (2, 4), (3, 9), . . .}
PR(x) = {x ∈ N : x est un nombre premier} = {2, 3, 5, 7, 11, 13, . . .}
Définitions. Soit D un ensemble. R est une relation d’arité n sur le domaine D si R est une
relation sur D n . Le prédicat R associé à R est défini par
On aura donc
PR(3) = V , PR(8) = F . . .
On voit qu’un prédicat est une proposition paramétrique, vraie pour certains éléments d’un
domaine et fausse pour les autres.
Il faut souligner d’emblée que le principal apport du calcul des prédicats ne sera pas
l’étude des formules paramétriques pour elles-mêmes, mais plutôt l’étude de formules non
paramétriques dont certaines composantes sont paramétriques. Pour prendre un exemple
célèbre, la question de Fermat n’est pas de savoir si la formule
xn + y n = z n ∧ x, y, z 6= 0 ∧ n > 2 (1)
est vraie pour des entiers x, y, z, n donnés, mais bien de savoir si, oui ou non, il existe un
quadruplet d’entiers tel que la formule soit vraie. La première question, du ressort du calcul
élémentaire, est clairement paramétrique ; le fait que 23 + 33 = 35 6= 64 = 43 établit clairement
que la formule est fausse pour le quadruplet (2, 3, 4, 3) mais ne détermine pas la valeur de vérité
pour le quadruplet (12, 13, 14, 15) par exemple. En revanche, le fait que la formule
soit fausse (ce fait a été — avec beaucoup de difficulté — démontré récemment) établit bien
que la formule paramétrique précédente est fausse pour tous les quadruplets, et notamment
pour (12, 13, 14, 15).
Remarque. Insistons sur le fait que la formule 1 est paramétrique (et sans grand intérêt) alors
que la formule 2 ne l’est pas ; il s’agit d’une “honnête” proposition, qui ne peut être que vraie ou
103
fausse, indépendamment de tout contexte.51 Cela n’a pas empêché les mathématiciens d’étudier
cette formule pendant plus de trois siècles.
Notre introduction à la logique des prédicats se limitera à l’essentiel. On verra d’abord
que l’interprétation d’une formule prédicative, quantifiée ou non, implique un domaine de
référence D et l’association, à chaque prédicat, d’une relation sur ce domaine. Les constantes
individuelles et les variables libres s’interprètent en des éléments de D. On peut aussi introduire
des constantes fonctionnelles, dont l’interprétation sera naturellement une fonction qui, à tout
n-uplet d’éléments de D, associe un élément de D.
On étudiera ensuite comment les procédures de décision introduites pour la logique
propositionnelle s’adaptent à la logique prédicative ; nous verrons que ces techniques (tableaux
sémantiques de Beth et Hintikka, séquents de Gentzen, systèmes axiomatiques de Hilbert et
résolution de Davis, Putnam et Robinson) donnent lieu à des “semi-procédures” de décision.
104
que les connecteurs binaires. Notons aussi que, dans le cas d’une formule dont l’opérateur
principal est un connecteur binaire, il est d’usage d’omettre les parenthèses extérieures.52
program Principal ;
var x : integer ;
procedure p ;
var x : integer ;
begin x := 1 ; writeln(x + x) end ;
procedure q ;
var y : integer ;
begin y := 1 ; writeln(x + y) end ;
begin x := 5 ; p; q end.
On remarque que les portées de x local et de y sont disjointes et incluses dans la portée de
x global. Dans la procédure q, on se réfère au x global. De même, dans
les première et dernière occurrences de x sont libres, de même que la variable y, tandis que
les deuxième et troisième occurrences de x sont liées. (On pourrait dire, plus justement, que la
deuxième occurrence est “liante” et que la troisième est liée.)
Ces notions apparaissent également en mathématique, et notamment en algèbre et en
analyse. Dans l’expression
Xn
Cij = Aik Bkj ,
k=1
52
Selon la syntaxe adoptée ici, les formules quantifiées et les négations ne comportent pas de paire de
parenthèses extérieures.
53
Les parenthèses extérieures d’une formule dont le connecteur principal est binaire peuvent être omises, mais
il n’en découle pas, pour A =def p(x) ∨ q(x), que la portée de ∀x dans ∀x p(x) ∨ q(x) soit p(x) ∨ q(x) ; cette
portée est p(x). La formule ∀x A doit s’écrire ∀x (p(x) ∨ q(x)).
105
les variables i et j sont libres, la variable k est liée.54 Dans l’expression
Z x
y(x) = y(x0 ) + f (t, y(t)) dt ,
x0
S = πR2 ,
il est “naturel” de considérer π comme la constante bien connue 3.14 . . ., parce que l’égalité
évoque la relation existant entre la surface d’un cercle et son rayon. En revanche, l’égalité
V = hb2
évoque la relation entre le volume d’un parallélipipède à base carrée et ses dimensions b et h ;
il sera alors tout aussi naturel de considérer h comme une variable libre. La confusion provient
des libertés de notation que se permettent les mathématiciens. Les deux formules ci-dessus
peuvent se récrire
∀C ∈ C [S(C) = π(R(C))2 ] ,
et
∀P ∈ P [V (P ) = h(P )(b(P ))2 ] ,
ce qui évite toute ambiguı̈té. Notons cependant que, parfois, le mathématicien est moins laxiste
que le logicien. En analyse, on évitera d’écrire
Z x
y(x) = y(x0 ) + f (x, y(x)) dx ,
x0
P (x) ∧ ∀x Q(x) ,
106
2. ϕ2 =def ∃x∀xA .
Ici aussi, deux quantifications sur x sont imbriquées. La sémantique de ϕ2 est celle
de ∃y∀xA, pour n’importe quelle variable y sans occurrence (libre) dans A ; la
quantification sur y étant inutile, la formule équivaut à ∀xA.
3. ϕ3 =def ∀x p(x, a) ⇒ ∃x q(x) .
Deux variables liées ont le même nom, mais les portées sont disjointes ; il n’y a donc pas
de problème.
4. ϕ4 =def ∀x p(x, a) ⇒ q(x) .
Une variable libre et une variable liée ont le même nom x. C’est acceptable, mais il est
préférable de renommer la variable liée et d’écrire, par exemple, ∀y p(y, a) ⇒ q(x).
107
une valeur de vérité à toute formule A et associe un élément de D à tout terme t. En ce qui
concerne les termes, on a
– Si x est une variable libre, I[x] = Iv [x].
– Si a est une constante, I[a] = Ic [a].
En ce qui concerne les formules, on a
– Si p est un symbole prédicatif d’arité n et si t1 , . . . , tn sont des termes, alors
I[p(t1 , . . . , tn )] = (Ic [p])(I[t1 ], . . . , I[tn ]).
– I[true] = V et I[false] = F.
– Si A est une formule, alors ¬A s’interprète comme dans le calcul des propositions, c’est-
à-dire I[¬A] = V si I[A] = F et I[¬A] = F si I[A] = V.
– Si A1 et A2 sont des formules, alors (A1 ∨ A2 ), (A1 ∧ A2 ), (A1 ⇒ A2 ), (A1 ≡ A2 )
s’interprètent comme dans le calcul des propositions.
I[(A1 ∧ A2 )] vaut V si I[A1 ] = V et I[A2 ] = V, et vaut F sinon.
I[(A1 ∨ A2 )] vaut V si I[A1 ] = V ou I[A2 ] = V, et vaut F sinon.
I[(A1 ⇒ A2 )] vaut V si I[A1 ] = F ou I[A2 ] = V, et vaut F sinon.
I[(A1 ≡ A2 )] vaut V si I[A1 ] = I[A2 ], et vaut F sinon.
Notation. Si I = (DI , Ic , Iv ) est une interprétation, si x est une variable et si d est un élément
de DI , alors Ix/d désigne l’interprétation J = (DJ , Jc , Jv ) telle que DJ = DI , Jc = Ic ,
Jv [x] = d et Jv [y] = Iv [y] pour toute variable y distincte de x.
– Si A est une formule et x une variable, I[∀xA] vaut V si Ix/d [A] = V pour tout élément
d de D, et vaut F sinon.
– Si A est une formule et x une variable, I[∃xA] vaut V si Ix/d [A] = V pour au moins
un élément d de D, et vaut F sinon.
108
5.3.4 Satisfaction, modèle
Une formule A est vraie pour une interprétation I ou A est satisfaite par une
interprétation I ou I est un modèle de A si I[A] = V. Cela se note |=I A.
Remarque. On rencontre parfois l’écriture I |= A, mais nous ne l’emploierons pas dans ce
cours, pour éviter tout risque de confusion avec l’écriture U |= A, introduite au paragraphe
suivant.
Exemples. Soit A la formule ∀x p(a, x). Les quatre interprétations introduites plus haut
attribuent à A une valeur de vérité :
– DI1 = N, I1c [p] = ≤, I1c [a] = 0 ; on a |=I1 A .
– DI2 = N, I2c [p] = ≤, I2c [a] = 1 ; on a 6|=I2 A .
– DI3 = Z, I3c [p] = ≤, I3c [a] = 0 ; on a 6|=I3 A .
– DI4 = S, I4c [p] = ⊑, I4c [a] = λ ; on a |=I4 A .
Définitions. Soit A une formule du calcul des prédicats.
– A est satisfaisable ou consistante si A a au moins un modèle.
– A est valide (cela se note |= A) si I[A] = V pour toute interprétation I.
– A est insatisfaisable ou inconsistant si A n’est pas satisfaisable, donc si I[A] = F pour
toute interprétation I.
– A est simplement consistante ou contingente si A est consistante mais non valide.
Théorème (dualité validité – consistance). La formule A est valide si et seulement si ¬A est
inconsistante.
Exemples.
– ∀x p(a, x) est consistante mais non valide.
DI1 = N, I1c [p] =≤, I1c [a] = 0 : |=I1 A .
DI3 = Z, I3c [p] =≤, I3c [a] = 0 : 6|=I3 A .
– ∀x p(x) ⇒ p(a) est valide.
– ∃x p(x) ⇒ p(a) est simplement consistante.
Remarque. Tout schéma propositionnel valide est aussi un schéma prédicatif valide. Par
exemple, du schéma propositionnel valide ¬¬A ≡ A , on peut déduire ¬¬(p ∧ q) ≡ (p ∧ q),
mais aussi ¬¬∀xp(x) ≡ ∀xp(x).
109
– ∃x∃yA ≡ ∃y∃xA
– ∃x∀yA ⇒ ∀y∃xA
On observera que le remplacement d’une implication par une équivalence produit, dans chaque
cas, une formule non valide. Considérons par exemple le cas de la formule ∃x(A ∧ B) ⇒
(∃xA ∧ ∃xB) . Il est évident, vu la règle sémantique se rapportant à l’existentielle, que,
si C ⇒ D est valide, alors ∃xC ⇒ ∃xD est valide. En conséquence, les deux formules
∃x(A ∧ B) ⇒ ∃xA et ∃x(A ∧ B) ⇒ ∃xB sont valides. D’autre part, si C ⇒ D et
C ⇒ E sont vraies ou valides, alors C ⇒ (D ∧ E) est vraie ou valide. Il en découle que
∃x(A ∧ B) ⇒ (∃xA ∧ ∃xB) est valide.
Pour montrer que l’implication inverse (ou réciproque, ou converse) n’est pas valide, il
suffit d’en donner un antimodèle. On prend pour domaine l’ensemble N ; A(x) est interprété en
“x est pair” et B(x) en “x est impair”. La formule ∃xA∧∃xB est vraie : elle signifie qu’il existe
au moins un entier naturel pair, et au moins un entier naturel impair. La formule ∃x(A ∧ B) est
fausse : elle signifie qu’il existerait au moins un entier naturel à la fois pair et impair.
Notons enfin que le passage des quantifications informelles aux quantifications formelles
(et réciproquement) est un exercice important, souvent facile, mais parfois délicat. Considérons
un exemple :
Toutes les licornes sont dangereuses, donc il existe une licorne dangereuse.
Une modélisation hâtive telle que
∀xLD (x) ⇒ ∃xLD (x)
pourrait laisser croire à la validité du raisonnement informel, ce qui serait incorrect. En
effet, les licornes n’existent pas ; on peut donc les qualifier sans erreur de dangereuses (ou
d’inoffensives), mais on ne peut pas affirmer qu’il existe une licorne, dangereuse ou non. Le
paradoxe apparent disparaı̂t si l’on utilise un modèle formel correct, à savoir
∀x[L(x) ⇒ D(x)] ⇒ ∃x[L(x) ∧ D(x)]
Cette dernière formule est consistante mais n’est pas valide.
110
sont en général pas logiquement équivalentes, mais ∀x A(x) et ∀y A(y) le sont. On évite
des complications sans perdre d’expressivité en considérant les problèmes de validité, de
consistance et de conséquence logique seulement pour les formules fermées. Lors de la
fermeture d’une formule, l’ordre des quantifications n’a pas d’importance (c’est pourquoi on
parle de “la” fermeture universelle ou existentielle d’une formule).
Théorème de l’échange. Soit A une sous-formule d’une formule B et soit A′ une formule telle
que A ↔ A′ . Soit B ′ la formule résultant du remplacement de A par A′ dans B. On a B ↔ B ′ .
Démonstration. Comme dans le cas propositionnel, on procède par induction structurelle. Les
seuls cas inductifs nouveaux sont liés à la quantification. Pour la quantification universelle, on
doit seulement montrer que si B(x) ↔ B ′ (x), on a aussi ∀x B(x) ↔ ∀x B ′ (x), ce qui est
évident.
111
6 Analyse des formules prédicatives
6.1 Méthode simple pour formules simples
En logique propositionnelle, l’application directe des règles sémantiques permet toujours
d’analyser une formule, c’est-à-dire de déterminer si elle est valide, contingente ou
inconsistante. La méthode des tables de vérité concrétise cette approche fondamentalement
simple. En logique prédicative, la situation est moins favorable parce qu’une formule
consistante admet souvent une infinité de modèles très différents. Néanmoins, si on accepte
certaines restrictions sur l’emploi des quantificateurs, l’approche sémantique directe reste
possible.
La formule Φ comporte quatre atomes syntaxiquement distincts qui, par ordre d’occurrence,
sont P (a, a), P (a, x), Q(a, b) et Q(a, a). La version propositionnelle de Φ s’obtient en
substituant uniformément à ces quatre atomes les propositions élémentaires distinctes, par
exemple p1 , p2 , p3 et p4 , respectivement, ce qui donne
p1 ∧ ¬p2 ∧ p3 ∧ (p4 ⇒ p2 )
112
La condition est suffisante. Soit J un modèle de la version propositionnelle de Φ. On construit
un modèle I de Φ comme suit. Le domaine d’interprétation se compose des constantes et des
variables de Φ. La fonction d’interprétation I applique chaque terme sur lui-même. Il reste
à définir I(P ), pour tout prédicat P intervenant dans Φ. Si P est, par exemple, d’arité 2, il
faut définir, vu le choix que nous avons fait pour D, I(P (d1, d2 )) pour tous d1 , d2 ∈ D. On
distingue deux cas : si P (d1 , d2 ) est le kième atome de Φ, on pose I(P (d1, d2 )) = J(pk ), sinon
on choisit (arbitrairement) I(P (d1, d2 )) = V.
113
¬ (∀x (p(x) ⇒ q(x)) ⇒ (∀x p(x) ⇒ ∀x q(x)))
↓
∀x (p(x) ⇒ q(x)) , ¬ (∀x p(x) ⇒ ∀x q(x))
↓
∀x (p(x) ⇒ q(x)) , ∀x p(x), ¬∀x q(x)
↓
∀x (p(x) ⇒ q(x)) , ∀x p(x), ¬q(a)
↓
∀x (p(x) ⇒ q(x)) , p(a), ¬q(a)
↓
p(a) ⇒ q(a), p(a), ¬q(a)
ւ ց
¬p(a), p(a), ¬q(a) q(a), p(a), ¬q(a)
× ×
Exemple 3. Test de ∀x∃y p(x, y) ∧ ∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z)) .
Le tableau sémantique de la figure 53 est infini. Son unique branche doit être considérée comme
ouverte car elle définit un modèle (nécessairement infini) de la formule testée.
Exemple 4. Test de validité pour la formule
∀x∃y p(x, y) ∧ ∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z)) ∧ ∀x (q(x) ∧ ¬q(x)) .
Si, dans le tableau 54, on instanciait indéfiniment ∀x∃y p(x, y) , en négligeant à tort les autres
formules, la branche ne se fermerait pas et serait infinie.
Les exemples 1 et 2 suggèrent que l’instantiation des existentielles, ou exemplification,
114
¬ (∀x (p(x) ∨ q(x)) ⇒ (∀x p(x) ∨ ∀x q(x)))
↓
∀x (p(x) ∨ q(x)) , ¬ (∀x p(x) ∨ ∀x q(x))
↓
∀x (p(x) ∨ q(x)) , ¬∀x p(x), ¬∀x q(x)
↓
∀x (p(x) ∨ q(x)) , ¬∀x p(x), ¬q(a)
↓
∀x (p(x) ∨ q(x)) , ¬p(b), ¬q(a)
↓
∀x (p(x) ∨ q(x)) , p(a) ∨ q(a), ¬p(b), ¬q(a)
↓
∀x (p(x) ∨ q(x)) , p(b) ∨ q(b), p(a) ∨ q(a), ¬p(b), ¬q(a)
ւ ց
∀x (p(x) ∨ q(x)) , p(b), ∀x (p(x) ∨ q(x)) , q(b)
p(a) ∨ q(a), ¬p(b), p(a) ∨ q(a), ¬p(b), ¬q(a)
¬q(a) ւ ց
× ∀x (p(x) ∨ q(x)) , ∀x (p(x) ∨ q(x)) ,
q(b), p(a), q(b), q(a),
¬p(b), ¬q(a) ¬p(b), ¬q(a)
×
se fasse au moyen de constantes inédites, appelées aussi paramètres. Cela n’exclut pas les
formules à “petits” modèles : en l’absence du prédicat spécial d’égalité, si {a, b} par exemple
est le domaine d’un modèle de A, {a, a1 , . . . , b, b1 , . . .} donnera aussi lieu à un modèle, si les
ai et bj sont des “clones” de a et b, c’est-à-dire tels que ϕ, ϕ[a/ai ] et ϕ[b/bj ] aient même valeur
de vérité, pour toute formule ϕ.
L’exemple 3 montre que la construction d’un tableau sémantique peut ne pas se terminer, en
particulier si la formule étudiée est consistante mais n’admet que des modèles infinis. On espère
néanmoins que la méthode permettra toujours de reconnaı̂tre les formules inconsistantes,
négations de formules valides.
L’exemple 4 indique enfin que cette inconsistance pourrait n’être pas reconnue si les règles
de décomposition n’étaient pas appliquées de manière “équitable” ; il faut notamment se méfier
de la règle générative d’instantiation des universelles, qui peut s’appliquer indéfiniment. On
doit l’appliquer à toute constante introduite par la règle d’exemplification (sauf si la branche
se ferme).
115
∀x∃y p(x, y) ∧ ∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), ∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), ∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), ∃y p(a1 , y),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), p(a1, a2 ),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), ∃y p(a2 , y), p(a1, a2 ),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), p(a2, a3 ), p(a1 , a2 ),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
∀x∃y p(x, y), p(a2, a3 ), p(a1 , a2 ),
∀x¬p(x, x), ¬p(a1 , a1 ), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
↓
..
.
α α1 α2 β β1 β2
A1 ∧ A2 A1 A2 B1 ∨ B2 B1 B2
¬(A1 ∨ A2 ) ¬A1 ¬A2 ¬(B1 ∧ B2 ) ¬B1 ¬B2
¬(A1 ⇒ A2 ) A1 ¬A2 B1 ⇒ B2 ¬B1 B2
¬(A1 ⇐ A2 ) ¬A1 A2 B1 ⇐ B2 B1 ¬B2
– Règles génératives (type γ) et exemplatives (type δ)
γ γ(c) δ δ(a)
(constante c quelconque)
∀x A(x) A(c) ∃x A(x) A(a)
(constante a inédite)
¬∃x A(x) ¬A(c) ¬∀x A(x) ¬A(a)
Rappelons aussi la règle d’élimination des doubles négations.
116
∀x∃y p(x, y)
∧ ∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
∧ ∀x (q(x) ∧ ¬q(x))
↓
∀x∃y p(x, y),
∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
∧ ∀x (q(x) ∧ ¬q(x))
↓
∀x∃y p(x, y),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z))
∧ ∀x (q(x) ∧ ¬q(x))
↓
∀x∃y p(x, y),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z)) ,
∀x (q(x) ∧ ¬q(x))
↓
∀x∃y p(x, y),
∀x¬p(x, x), ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z)) ,
∀x (q(x) ∧ ¬q(x)) , q(a) ∧ ¬q(a)
↓
∀x∃y p(x, y),
∀x¬p(x, x) ∧ ∀x∀y∀z (p(x, y) ∧ p(y, z) ⇒ p(x, z)) ,
∀x (q(x) ∧ ¬q(x)) , q(a), ¬q(a)
×
F IG . 54 – Exemple 4.
117
U(ℓ).56
Terminaison : survient quand toutes les feuilles sont marquées.
Règles additionnelles de construction.
Le non-déterminisme de l’algorithme de construction intervient
1. lors du choix du nœud à développer ;
2. lors du choix de la formule à décomposer dans ce nœud ;
3. lors du choix du terme c lors d’une γ-réduction.57
Il faut adopter une stratégie qui garantisse les deux conditions suivantes.
– Toute formule qui apparaı̂t sur une branche ouverte de l’arbre se voit appliquer une règle
de décomposition quelque part sur cette branche.
Autrement dit, toute formule décomposable est décomposée, à moins que la branche se
ferme.
– Pour toute γ-formule A et toute constante a qui apparaissent sur une branche ouverte,
une règle d’instantiation est appliquée à la formule A avec la constante a quelque part
sur cette branche.
Toute constante apparaissant sur une branche est utilisée à un moment donné pour
instancier les γ-formules sur cette branche, à moins qu’elle se ferme.
Un moyen simple et classique d’assurer le respect des conditions d’équité est d’étiqueter
les nœuds par des listes de formules. Le(s) nœud(s) successeurs de n est (sont) obtenus par
“décomposition” de la première formule de la liste U(n) non réduite à un littéral ; la liste U(n′ )
(et U(n′′ ), s’il y a lieu) est obtenue en supprimant de U(n) la formule traitée, et en ajoutant
en fin de liste le(s) “composant(s)” adéquats. Dans le cas d’une formule générative, la formule
supprimée en tête de liste est réinsérée en queue de liste.
Une autre méthode appropriée est la suivante. Lorsqu’une règle générative est activée, on
construit immédiatement les instances correspondant à toutes les constantes introduites jusque
là dans la branche. De même, quand une exemplification est faite, ce qui provoque l’adjonction
dans la branche d’une constante inédite, on “réactive” les γ-réductions déjà accomplies, pour
insérer les instances correspondant à cette nouvelle constante. Ceci nécessite une gestion
organisée de l’ensemble des constantes et des activations de règles génératives.
La stratégie n’est pas nécessaire pour obtenir l’adéquation, mais elle l’est pour obtenir
la complétude. En effet, la stratégie ne vise qu’à éviter le report définitif de réductions
susceptibles de fermer une branche. Le point est d’ailleurs délicat, puisque la construction
d’un tableau sémantique peut ne pas se terminer.
56
On voit que cette constante n’apparaı̂t pas non plus dans l’étiquette d’un ancêtre de ℓ ; cette contrainte devrait
être introduite explicitement si on convenait de ne pas récrire les littéraux étiquetant un nœud dans l’étiquette
de ses successeurs (convention que l’on adopte parfois pour alléger la construction). Dans ce cas, il convient de
préciser que la recherche de paires complémentaires se fait dans toute la branche, et non seulement dans son
dernier nœud.
57
Lors d’une δ-réduction, la constante choisie doit être inédite ; on a vu que le non-respect de cette condition
rendait la méthode inadéquate (exemple 1). En revanche, le choix du nom de cette constante inédite est
clairement sans importance ; les δ-réductions, au contraire des γ-réductions, n’introduisent donc pas de vrai non-
déterminisme.
118
Rappelons enfin que certaines règles de priorité permettent souvent d’accélérer la
construction du tableau. En particulier, on effectuera les α-réductions avant les β-réductions,
pour limiter le nombre de branchements. On évitera d’instancier une γ-formule par une
constante inédite (c’est inutile) sauf naturellement dans le cas où aucune δ-réduction n’a pu
être effectuée. L’exemple 5 (fig. 55) illustre certaines de ces règles. Il illustre aussi un point
délicat. La formule ∀x∃y r(x, y) ⇒ ∃y∀x r(x, y), où r est un prédicat binaire, est non valide ;
on en déduit naturellement que, si R(x, y) est une formule quelconque admettant x et y comme
variables libres, la formule ∀x∃y R(x, y) ⇒ ∃y∀x R(x, y) est généralement non valide. Pour
certains choix de R, la formule peut cependant être valide ; c’est le cas notamment si R(x, y)
est p(x) ⇒ q(y).
¬ ∀x∃y (p(x) ⇒ q(y)) ⇒ ∃y∀x (p(x) ⇒ q(y))
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∃y∀x (p(x) ⇒ q(y))
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∀x (p(x) ⇒ q(c)) , ¬∃y∀x (p(x) ⇒ q(y))
↓
∀x∃y (p(x) ⇒ q(y)) , ¬(p(a) ⇒ q(c)) , ¬∃y∀x (p(x) ⇒ q(y))
↓
∀x∃y (p(x) ⇒ q(y)) , p(a) , ¬q(c) , ¬∃y∀x (p(x) ⇒ q(y))
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∃y∀x (p(x) ⇒ q(y))
∃y (p(a) ⇒ q(y)) , p(a) , ¬q(c)
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∃y∀x (p(x) ⇒ q(y))
p(a) ⇒ q(b) , p(a) , ¬q(c)
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∀x (p(x) ⇒ q(b)) , ¬∃y∀x (p(x) ⇒ q(y))
p(a) ⇒ q(b) , p(a) , ¬q(c)
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∃y∀x (p(x) ⇒ q(y))
¬(p(d) ⇒ q(b)) , p(a) ⇒ q(b) , p(a) , ¬q(c)
↓
∀x∃y (p(x) ⇒ q(y)) , ¬∃y∀x (p(x) ⇒ q(y))
p(d) , ¬q(b) , p(a) ⇒ q(b) , p(a) , ¬q(c)
ւ ց
∀x∃y (. . .) , ¬∃y∀x (. . .) ∀x∃y (. . .) , ¬∃y∀x (. . .)
p(d), ¬q(b), ¬p(a), p(a), ¬q(c) p(d), ¬q(b), q(b), p(a), ¬q(c)
↓ ↓
× ×
F IG . 55 – Exemple 5.
119
¬ ∀x∃y (p(x) ∧ q(y)) ⇒ ∃y∀x (p(x) ∧ q(y))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
↓
∀x∃y (p(x) ∧ q(y)) , ∃y (p(c) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
↓
∀x∃y (p(x) ∧ q(y)) , (p(c) ∧ q(a)) , ¬∃y∀x (p(x) ∧ q(y))
↓
∀x∃y (p(x) ∧ q(y)) , p(c) , q(a)) , ¬∃y∀x (p(x) ∧ q(y))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
p(c) , q(a)) , ¬∀x (p(x) ∧ q(a))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
p(c) , q(a)) , ¬(p(b) ∧ q(a))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
∃y (p(b) ∧ q(y)) , p(c) , q(a)) , ¬(p(b) ∧ q(a))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
(p(b) ∧ q(d)) , p(c) , q(a)) , ¬(p(b) ∧ q(a))
↓
∀x∃y (p(x) ∧ q(y)) , ¬∃y∀x (p(x) ∧ q(y))
p(b) , q(d) , p(c) , q(a) , ¬(p(b) ∧ q(a))
ւ ց
∀x∃y (. . .) , ¬∃y∀x (. . .) ∀x∃y (. . .) , ¬∃y∀x (. . .)
p(b) , q(d) , p(c) , q(a) , ¬p(b) p(b) , q(d) , p(c) , q(a) , ¬q(a)
↓ ↓
× ×
F IG . 56 – Exemple 6.
120
– Cas de base, h = 0 : le nœud n est une feuille, nécessairement fermée, donc U(n)
contient une paire complémentaire et est inconsistant.
– Cas inductif, h > 0 : une règle α, β, γ ou δ a été utilisée pour créer le(s) descendant(s)
du nœud n. Les cas α et β sont les mêmes que dans la démonstration de la version
propositionnelle du théorème. On considère successivement les cas γ et δ.
– Règle γ : n : {∀x A(x)} ∪ U0
↓
n′ : {∀x A(x), A(c)} ∪ U0
U(n′ ) est inconsistant par hypothèse inductive, donc U(n) est inconsistant ; en effet,
tout modèle de U(n) serait aussi un modèle de U(n′ ), ou s’étendrait immédiatement
en un tel modèle, au cas où la constante c n’interviendrait pas dans U0 .
– Règle δ : n : {∃x A(x)} ∪ U0
↓
′
n : {A(a)} ∪ U0
où a est une constante qui n’apparaı̂t pas dans U(n). Si U(n) était consistant, il
existerait une interprétation I = (D, Ic , Iv ) telle que I[∃x A(x)] = V, donc il
existerait d ∈ D tel que Ix/d [A(x)] = V.
Définissons J = (D, Jc , Iv ) avec Jc obtenu en étendant59 Ic de sorte que Jc [a] = d.
Alors, J [A(a)] = V et J [U0 ] = I[U0 ] = V, donc J satisfait U(n′ ), une
contradiction.
121
Remarque. La branche b peut être infinie ; dans ce cas, elle est nécessairement ouverte et elle
définit un modèle infini.
Lemme de Hintikka. Tout ensemble de Hintikka est consistant.
Démonstration. Soit U un ensemble de Hintikka. Le modèle canonique IU = (D, Ic , Iv )
associé à U est défini comme suit :
– D = {a, b, . . . , } est l’ensemble des constantes apparaissant dans les formules de U ;
– On construit la fonction d’interprétation Ic comme suit :
– Pour toute constante d ∈ D, on pose Ic [d] = d.
– Pour tout symbole prédicatif p (arité m) apparaissant dans U, on pose
Ic [p](Ic [a1 ], . . . , Ic [am ]) = V, si p(a1 , . . . , am ) ∈ U,
Ic [p](Ic [a1 ], . . . , Ic [am ]) = F, si ¬p(a1 , . . . , am ) ∈ U.
Ic [p](Ic [a1 ], . . . , Ic [am ]) est arbitraire si {p(a1 , ..., am ), ¬p(a1 , ..., am )} ∩ U = ∅.
– Iv est quelconque, puisqu’il n’y a pas de variables libres.
Il reste à montrer que pour toute formule (fermée) A ∈ U, on a I[A] = V. Cela se fait par
induction sur la structure de A. (Exercice.)
est démontrée par la méthode des tableaux (figure 57) puis par celle des séquents sans
antécédent (figure 58). D’une figure à l’autre, l’arbre est retourné et chaque formule est
remplacée par son complément. Les feuilles fermées deviennent des séquents valides ou
axiomes ; les feuilles ouvertes deviennent des séquents non valides ou hypothèses. Dans les
tableaux sémantiques, les ensembles de formules sont conjonctifs et la virgule a donc valeur
122
conjonctive. Dans les séquents, la virgule a valeur disjonctive quand elle se trouve à droite de
la flèche, dans le succédent. Un séquent peut aussi avoir un antécédent, dans lequel la virgule a
valeur conjonctive. On ne change pas la sémantique d’un séquent en faisant passer l’une de ses
formules du succédent vers l’antécédent ou réciproquement, à condition de changer sa polarité.
Par exemple, les quatre séquents ci-dessous sont équivalents :
→ A, ¬B B → A ¬A → ¬B ¬A, B →
F IG . 57 – Un tableau sémantique . . .
A A
→ ¬∀x p(x), ¬p(a), p(a), q(a) → ¬∀x q(x), ¬q(a), p(a), q(a)
123
A A
∀x p(x), p(a) → p(a), q(a) ∀x q(x), q(a) → p(a), q(a)
sont les mêmes que dans le cadre propositionnel. Nous rappelons seulement celles relatives à
l’implication.
– règle α :
U, A → V, B
U → V, (A ⇒ B)
– règle β :
U → V, A U, B → V
U, (A ⇒ B) → V
On ajoute des règles génératives (règles γ) et les règles d’exemplification (règles δ), pour
traiter les formules quantifiées :
– règles γ :
U → V, ∃x A(x), A(c)
∃:
U → V, ∃x A(x)
U, ∀x A(x), A(c) → V
∀:
U, ∀x A(x) → V
– règles δ :
U → V, A(a)
∀: si a n’apparaı̂t pas dans la conclusion.
U → V, ∀x A(x)
U, A(a) → V
∃: si a n’apparaı̂t pas dans la conclusion.
U, ∃x A(x) → V
La dérivation de la figure 58 (séquents sans antécédent) est reprise dans le cadre général à
la figure 59. La figure 60 montre la dérivation relative à une formule importante. On voit à la
figure 61 comment l’analyse d’une formule non valide peut conduire à une séquence infinie.
La figure 62 illustre le danger du non-respect de la restriction attachée à la règle δ. C’est cette
restriction qui empêcherait ici la fermeture (incorrecte). La dérivation de la figure 62 montre
que la formule est vraie dans un domaine réduit à un élément, sans mettre en évidence le fait
124
— essentiel — que la même formule est le plus souvent fausse dans un domaine comportant
plusieurs éléments.
A
∀y p(a, y), p(a, b), p(a, a) → ∃x p(x, b), p(a, b)
(règle γ, ∀)
∀y p(a, y), p(a, a) → ∃x p(x, b), p(a, b)
(règle γ, ∀)
∀y p(a, y) → ∃x p(x, b), p(a, b)
(règle γ, ∃)
∀y p(a, y) → ∃x p(x, b)
(règle δ, ∀)
∀y p(a, y) → ∀y∃x p(x, y)
(règle δ, ∃)
∃x∀y p(x, y) → ∀y∃x p(x, y)
(règle α, ⇒)
→ ∃x∀y p(x, y) ⇒ ∀y∃x p(x, y)
H?
∀∃ , p(d, b) , p(e, c) , p(c, a) → ∃∀, p(b, f ), p(c, g), p(a, b)
δ
∀∃ , ∃x p(x, b) , ∃x p(x, c) , p(c, a) → ∃∀, ∀y p(b, y), ∀y p(c, y), p(a, b)
γ
∀y∃x p(x, y) , p(c, a) → ∃x∀y p(x, y), p(a, b)
δ
∀y∃x p(x, y) , ∃x p(x, a) → ∃x∀y p(x, y), ∀y p(a, y)
γ
∀y∃x p(x, y) → ∃x∀y p(x, y)
α⇒
→ ∀y∃x p(x, y) ⇒ ∃x∀y p(x, y)
125
A
!! ∀y∃x p(x, y) , p(a, a) → ∃x∀y p(x, y), p(a, a) !!
!! δ !!
∀y∃x p(x, y) , ∃x p(x, a) → ∃x∀y p(x, y), ∀y p(a, y)
γ
∀y∃x p(x, y) → ∃x∀y p(x, y)
α⇒
→ ∀y∃x p(x, y) ⇒ ∃x∀y p(x, y)
Terminaison. L’obtention d’une dérivation adéquate exige le respect d’une stratégie équitable,
comme pour les tableaux sémantiques. Malgré cela, l’analyse d’une formule non valide peut
donner lieu à une dérivation infinie.
Analyticité. Une règle est analytique si tous les composants (formules et sous-formules) des
prémisses apparaissent dans la conclusion. Les règles α et β sont analytiques. L’idée sous-
jacente est que la découverte de prémisse(s) appropriée(s) au départ de la conclusion doit être
triviale. En ce sens, on peut considérer que les règles δ sont analytiques. Pour les règles γ, le
choix de la constante c devient critique s’il peut être effectué d’une infinité de manières. Ce
sera le cas pour le calcul des prédicats avec symboles fonctionnels (pour l’instant, c ne peut
être qu’une constante individuelle).
Réversibilité. Tout modèle des prémisses d’une règle (correcte) est aussi un modèle de sa
conclusion. Une règle est réversible si la réciproque est également vraie. Les règles α, β et γ
sont réversibles. Les règles δ sont “quasi réversibles” : tout modèle de la conclusion peut être
étendu en un modèle de la prémisse. Dans tous les cas, la validité de la conclusion implique
celle de la ou des prémisse(s).
Remarque. La correction des règles δ n’est pas évidente ; elle dépend crucialement de la
condition imposée à la constante a.
126
– la règle d’inférence Modus Ponens :
⊢A ⊢A⇒B
⊢B
– la règle de Généralisation :
⊢ A(x)
⊢ ∀x A(x)
Remarque. La restriction relative à la capture est naturellement essentielle ; l’instance
∀x ∃y p(x, y) ⇒ ∃y p(y, y) ne peut pas être un axiome, parce que ce n’est pas une formule
valide. De même, l’instance ∀x (p(x) ⇒ p(x)) ⇒ (p(x) ⇒ ∀x p(x)) du schéma 5 ne peut pas
être un axiome.
Remarques. L’expression
A ⇒ (B ⇒ A)
est un schéma d’axiome ; cela implique, notamment, que la formule
(p ⇒ q) ⇒ ((¬p ⇒ r) ⇒ (p ⇒ q))
127
la technique donnée dans le cas propositionnel. Le seul point délicat est la conversion des
fragments du type
U, A ⊢ C(x) ,
U, A ⊢ ∀x C(x) .
La conversion est
U ⊢ A ⇒ C(x) ,
U ⊢ ∀x (A ⇒ C(x)) ,
U ⊢ ∀x (A ⇒ C(x)) ⇒ (A ⇒ ∀x C(x)) ,
U ⊢ A ⇒ ∀x C(x) .
La troisième ligne n’est correcte que si x n’intervient pas dans A, d’où la restriction concernant
l’emploi de la règle de généralisation dans les dérivations.
128
6.4.4 Quelques dérivations
Théorème. ⊢ p(a) ⇒ ∃x p(x)
Démonstration.
1. ⊢ ∀x¬p(x) ⇒ ¬p(a) (Axiome 4)
2. ⊢ p(a) ⇒ ¬∀x¬p(x) (PC, 1)
3. ⊢ p(a) ⇒ ∃x p(x) (Définition ∃)
Théorème. ⊢ (A ⇒ ∀x C(x)) ⇒ ∀x (A ⇒ C(x)) , si x n’a pas d’occurrence libre dans A.
Démonstration.
1. A, A ⇒ ∀x C(x) ⊢ ∀x C(x) (Hypothèse, MP)
2. A, A ⇒ ∀x C(x) ⊢ C(x) (Axiome 4, 1)
3. A ⇒ ∀x C(x) ⊢ (A ⇒ C(x)) (Déduction, 2)
4. A ⇒ ∀x C(x) ⊢ ∀x (A ⇒ C(x)) (Généralisation, 3)
5. ⊢ (A ⇒ ∀x C(x)) ⇒ ∀x (A ⇒ C(x)) (Déduction, 4)
Remarque. Quelle(s) étape(s) de la démonstration serai(en)t illicite(s) si la restriction n’était
pas respectée ?
Théorème. ⊢ ∀x (p(x) ⇒ q) ≡ (∃x p(x) ⇒ q) , si x n’a pas d’occurrence libre dans q.
Démonstration.
1. ∀x (p(x) ⇒ q) ⊢ ∀x (p(x) ⇒ q) (Hypothèse)
2. ∀x (p(x) ⇒ q) ⊢ ∀x (¬q ⇒ ¬p(x)) (PC, échange, 1)
3. ∀x (p(x) ⇒ q) ⊢ ¬q ⇒ ∀x ¬p(x)) (Axiome 5, 2)
4. ∀x (p(x) ⇒ q) ⊢ ∃x p(x) ⇒ q (PC, ∃, 3)
5. ∃x p(x) ⇒ q ⊢ ∃x p(x) ⇒ q (Hypothèse)
6. ∃x p(x) ⇒ q ⊢ ¬q ⇒ ∀x ¬p(x) (PC, ∃, 5)
7. ∃x p(x) ⇒ q ⊢ ∀x (¬q ⇒ ¬p(x)) (Théorème, 6)
8. ∃x p(x) ⇒ q ⊢ ∀x (p(x) ⇒ q) (PC, 7)
9. ⊢ ∀x (p(x) ⇒ q) ≡ (∃x p(x) ⇒ q) (Déduction, 4, 8)
Remarque. Quelle(s) étape(s) de la démonstration serai(en)t illicite(s) si la restriction n’était
pas respectée ?
Il est permis d’utiliser une existentielle ∃x p(x) en posant “soit x tel que p(x)”, ou “soit a
tel que p(a)”. La règle des constantes formalise ce mode de raisonnement.
Théorème. (Règle C). Si U ⊢ ∃x p(x), si x n’a pas d’occurrence libre dans A et si on peut
établir U, p(x) ⊢ A sans généralisation sur x, alors U ⊢ A.
Démonstration.
1. U, p(x) ⊢ A (Hypothèse)
2. U ⊢ p(x) ⇒ A (Déduction, 1)
3. U ⊢ ∀x(p(x) ⇒ A) (Généralisation, 2)
4. U ⊢ ∃x p(x) ⇒ A (Théorème)
5. U ⊢ ∃x p(x) (Hypothèse)
6. U ⊢ A (PC, 4, 5)
Remarque. L’usage de la règle C est soumis à deux restrictions importantes, dont le non-respect
conduit naturellement à des erreurs.
129
1. Le “blocage” de la généralisation sur x est nécessaire ; il permet l’application de la règle
de déduction (ligne 2 de la démonstration). Négliger ce blocage permettrait de prouver
par exemple ∃x p(x) ⊢ ∀x p(x) . En posant U = {∃x p(x)} et A = ∀x p(x), on aurait
1. ∃x p(x) ⊢ ∃x p(x) (Hypothèse)
2. ∃x p(x) , p(x) ⊢ p(x) (Hypothèse)
3. ∃x p(x) , p(x) ⊢ ∀x p(x) (Généralisation)
4. ∃x p(x) ⊢ ∀x p(x) (Règle C [usage incorrect])
2. L’absence d’occurrence libre de x dans A permet d’utiliser le (méta)théorème
∀x(p(x) ⇒ A) ⊢ (∃x p(x) ⇒ A) à la ligne 4 de la démonstration. Négliger cette
exigence permettrait aussi de prouver ∃x p(x) ⊢ ∀x p(x) . En posant cette fois U =
{∃x p(x)} et A = p(x), on aurait
1. ∃x p(x) ⊢ ∃x p(x) (hypothèse)
2. ∃x p(x) , p(x) ⊢ p(x) (hypothèse)
3. ∃x p(x) ⊢ p(x) (Règle C [usage incorrect])
4. ∃x p(x) ⊢ ∀x p(x) (Généralisation)
Remarque. Nous avons signalé qu’un moyen simple et radical d’éviter les risques de
généralisation abusive était de proscrire toute variable libre à gauche du symbole ⊢. L’emploi
de la règle C est une entorse temporaire à cette pratique. En particulier, même si ce n’est
pas formellement requis, l’ensemble U des hypothèses devrait ne contenir que des formules
fermées.
La règle C n’est pas indispensable mais elle a le mérite de rendre plus intuitives certaines
preuves, et de formaliser une démarche fréquente en mathématique. Observons par exemple
qu’une dérivation directe de
ou encore de prouver
p(a, y) ⇒ ∃x p(x, y)
ce qui est évident.
Remarque. Certains auteurs utilisent la règle “naturelle”
U ⊢ ∃x p(x)
(a inédit)
U ⊢ p(a)
Cette règle a un sens intuitif clair : on donne un nom (inédit) à un objet dont l’existence est
prouvée. Si on accepte cette règle (ce que nous ne faisons pas), on doit nuancer le fait que,
en l’absence de variables libres, U ⊢ A équivaut à U |= A. Dans le même ordre d’idée, on
pourrait refuser (ce que nous ne faisons pas non plus) toute généralisation de variable libre
présente dans une hypothèse, et en fait se restreindre aux hypothèses sans variable libre. Cela
130
bloquerait une déduction du type p(x) ⊢ ∀x p(x). En fait, plusieurs variantes existent pour le
système de Hilbert, chacune ayant ses avantages et ses inconvénients.
Remarque. Une théorie du premier ordre est définie par une collection d’axiomes utilisant un
lexique spécial, pouvant comporter des constantes individuelles. Par exemple, ∀x [x ∗ i(x) = e]
est un axiome de la théorie des groupes, où e dénote l’élément neutre. La constante e ne sera
jamais “inédite” au sens où ce mot est utilisé ici, même si elle n’a qu’une seule occurrence
dans les hypothèses d’une dérivation. En particulier, la “dérivation”
1. U ⊢ ∀x [x ∗ i(x) = e] (hypothèse)
2. U ⊢ ∀y ∀x [x ∗ i(x) = y] (Généralisation 1)
est naturellement incorrecte ; elle illustre les dangers de la règle “naturelle” que nous venons
d’évoquer.
⊢ W ∨ ¬A ∨ B
⊢ W ∨ (A ⇒ B)
131
Lemme β. La règle de Gentzen
→ V, A → V, ¬B
→ V, ¬(A ⇒ B)
⊢W ∨A ⊢ W ∨ ¬B
⊢ W ∨ ¬(A ⇒ B)
⊢ W ∨ ∃x A(x) ∨ A(c)
⊢ W ∨ ∃x A(x)
Démonstration.
1. ⊢ ∀x ¬A(x) ⇒ ¬A(c) (Axiome 4)
2. ⊢ ¬∀x ¬A(x) ∨ ¬A(c) (PC 1)
3. ⊢ V ∨ ¬∀x ¬A(x) ∨ ¬A(c) (PC 2)
4. ⊢ V ∨ ∃x A(x) ∨ ¬A(c) (∃)
5. ⊢ V ∨ ∃x A(x) ∨ A(c) (Hypothèse)
6. ⊢ V ∨ ∃x A(x) (PC 4, 5)
Lemme δ. La règle de Gentzen
→ V, A(a)
→ V, ∀xA(x)
est simulée dans le système de Hilbert par la règle
⊢ W ∨ A(x)
⊢ W ∨ ∀xA(x)
Démonstration.
1. ⊢ V ∨ A(x) (Hypothèse)
2. ⊢ ¬V ⇒ A(x) (PC 1)
3. ⊢ ∀x(¬V ⇒ A(x)) (Généralisation 2)
4. ⊢ ¬V ⇒ ∀x A(x) (Axiome 5, PC 4)
5. ⊢ V ∨ ∀x A(x) (PC 4)
Corollaire. Le système de Hilbert est complet.
Corollaire. Si U et A sont sans variables libres on a U ⊢ A si et seulement si U |= A.
132
6.4.6 Preuve indirecte du théorème de compacité
On doit prouver que tout ensemble inconsistant admet un sous-ensemble fini inconsistant ;
on peut se limiter aux ensembles de formules fermées. Soit U un ensemble inconsistant
de formules fermées, donc tel que U |= A pour toute formule A, et en particulier pour
A = ¬(p ⇒ p). Vu la complétude du système de Hilbert, on a U ⊢ A, donc il existe une
dérivation dont la dernière ligne est U ⊢ A. Cette dérivation est nécessairement finie (par
définition) et ne peut donc évoquer qu’un nombre fini d’hypothèses. Ces hypothèses forment
un sous-ensemble fini V de U, tel que V ⊢ A. Le système de Hilbert étant adéquat, on a
nécessairement V |= A, ce qui montre que V est inconsistant.
x > y ⇒ (x + 1) > (y + 1) ,
Il est naturel et utile de compléter le langage des prédicats par des symboles fonctionnels qui
représenteront des fonctions sur le domaine d’interprétation.
On introduit donc
– F = {f, g, h, . . .} : un ensemble de symboles arbitraires appelés symboles fonctionnels
(chacun ayant une arité),
en plus des symboles prédicatifs, des constantes et des variables.
133
Exemples de formules atomiques :
134
7.3.1 Lois de passage
Si on envisage de modifier la portée d’une quantification sans altérer la sémantique de la
formule concernée, il faut connaı̂tre les relations existant entre les quantifications et les atomes,
entre les quantifications et les connecteurs et entre les quantifications entre elles.
Si Φ est un atome ne comportant pas la variable x ou, plus généralement, une formule
ne comportant pas d’occurrence libre de x, alors les trois formules Φ, ∀x Φ et ∃x Φ sont
logiquement équivalentes. Concrètement, cela signifie que toute quantification portant sur une
formule ne comportant pas d’occurrence libre de la variable quantifiée est superflue et donc,
en pratique, supprimée. Une formule telle que ∀x ∀y ∃x P (x, y) peut donc se simplifier en
∀y ∃x P (x, y) ; la formule ∀z A(x, y) se simplifie en A(x, y) mais ∀x A(x, y) ne se simplifie
pas.
Les formules valides introduites au paragraphe 5.3.5 constituent un bon point de départ
pour déterminer les relations entre quantificateurs et connecteurs. Un raisonnement sémantique
direct permet de vérifier les équivalences logiques suivantes, concernant les connecteurs de
négation, de conjonction et de disjonction :
∀x ¬Φ ↔ ¬∃x Φ ∃x ¬Φ ↔ ¬∀x Φ
∀x (Φ ∧ Ψ) ↔ ∀x Φ ∧ ∀x Ψ ∃x (Φ ∨ Ψ) ↔ ∃x Φ ∨ ∃x Ψ
∀x (Φ ∨ Ξ) ↔ ∀x Φ ∨ Ξ ∃x (Φ ∧ Ξ) ↔ ∃x Φ ∧ Ξ
Dans ce tableau,
Φ et Ψ désignent des formules quelconques,
Ξ désigne une formule sans occurrence libre de x
135
7.3.3 Forme prénexe
Une formule est en forme prénexe si elle est de la forme
Q1 x1 · · · Qn xn M
| {z } |{z}
préfixe matrice
où chaque Qi désigne soit ∀, soit ∃, pour i = 1, . . . , n et où la matrice M est une formule sans
quantification. La portée du préfixe doit être la matrice tout entière.
Remarque. On peut supposer (sans restriction) que seules les variables apparaissant (libres)
dans la matrice sont quantifiées dans le préfixe.
Théorème. Pour toute formule du calcul des prédicats, il existe (au moins) une formule en
forme prénexe qui lui est équivalente.
¬∀xA → ∃x¬A ,
¬∃xA → ∀x¬A ,
¬¬C → C
Renommer si nécessaire :
∃x p(x) ∧ ∀x q(x) → ∃x p(x) ∧ ∀y q(y) → ∃x ∀y (p(x) ∧ q(y)) .
Ex. : ∀x∀y∃u (p(x) ∧ (q(u, y) ∨ r(a, u, y))).
136
7.3.5 Forme de Skolem
Certaines définitions du cadre propositionnel restent valables dans le cadre prédicatif.
– Un littéral est un atome ou la négation d’un atome.
– Une clause (un cube) est une disjonction (une conjonction) de littéraux.
– Une forme conjonctive (disjonctive) normale est une conjonction (disjonction) de clauses
(de cubes).
– Une forme prénexe est conjonctive (disjonctive) si sa matrice est en forme conjonctive
(disjonctive) normale.
Une forme de Skolem est une forme prénexe sans quantifications existentielles. A toute
forme prénexe, on associe une forme de Skolem au moyen de l’algorithme suivant.
Pour chaque quantification existentielle ∃x se trouvant dans la portée de k ≥ 0 quantifications
universelles (∀x1 · · · ∀xk ),
1. remplacer chaque occurrence de x dans la matrice par f (x1 , . . . , xk ) où f est un
nouveau symbole fonctionnel d’arité k (k = 0 n’est pas exclu).
2. supprimer la quantification ∃x.
Exemples :
– ∀x∀y∃u (q(u, y) ⇒ r(a, u, y, z))
se transforme en
∀x∀y (q(f (x, y), y) ⇒ r(a, f (x, y), y, z)).
– ∀x∃u∀v∃w∀x∀y∃z M(u, v, w, x, y, z)
se simplifie en
∃u∀v∃w∀x∀y∃z M(u, v, w, x, y, z)
qui se transforme en
∀v∀x∀y M(a, v, f (v), x, y, g(v, x, y)).
La formule A =def ∀x∀y∃u [q(u, y) ⇒ r(a, u, y, x)] affirme l’existence d’un certain u,
dépendant de x et y, tel que la formule q(u, y) ⇒ r(a, u, y, x) soit vraie. Le passage à la
forme de Skolem associée SA consiste simplement à nommer ce u ; le nom f (x, y) rappelle la
dépendance. Le symbole f représente une fonction de choix.
Remarque. Il n’est pas indispensable de passer par la forme prénexe pour obtenir une forme de
Skolem. Il suffit de reconnaı̂tre les quantifications sémantiquement existentielles et de nommer
l’objet dont l’existence est assertée. Par exemple,
∃z ∀x (p(x) ⇒ ¬∀y [q(x, y) ⇒ p(z)])
devient ∀x (p(x) ⇒ ¬[q(x, f (x)) ⇒ p(a)])
Motivation. Pour déterminer la consistance d’une formule quelconque ϕ, il suffira d’étudier la
consistance de la forme de Skolem associée à une forme prénexe logiquement équivalente à ϕ.
On rappelle aussi qu’une formule est consistante si et seulement si sa fermeture existentielle
est consistante.
Théorème de Skolem. La forme de Skolem SA associée à la forme prénexe A est consistante si
et seulement si A est consistante.
La démonstration n’est pas difficile mais les notations sont lourdes. Un exemple simple suffira
à illustrer les points essentiels : tout modèle de SA est un modèle de A, et tout modèle de A
s’étend en un modèle de SA si on donne une interprétation adéquate aux symboles de Skolem.
137
Exemple. Soit A : ∀x∃y p(x, y) et SA : ∀x p(x, f (x)).
On se donne d’abord un modèle de A, soit I = ({1, 2}, Ic, Iv ), où Ic [p] est vrai pour (1, 1),
(1, 2) et (2, 1), et faux pour (2, 2).
On obtient un modèle J = ({1, 2}, Jc , Jv ) de SA en étendant Ic en Jc ; Jc [f ] appliquera
naturellement 1 sur 1 ou 2 (au choix) et 2 sur 1 (obligatoirement).
La sémantique de ∃ garantit la possibilité de construire la fonction Jc [f ] (totale sur D).
Réciproquement, on peut obtenir I à partir de J en “oubliant” Jc [f ]. La totalité de Jc [f ]
garantit le respect de la sémantique de ∃.
On a |=I A, |=J A et |=J SA , mais pas |=I SA (I n’est pas une interprétation pour SA ).
Remarque. Peut-on dire qu’une forme prénexe A est valide si et seulement si la forme de
Skolem associée SA est valide ? Peut-on dire que A et SA sont logiquement équivalentes ?
138
7.4.1 Domaines de Herbrand
Soit S une forme de Skolem dont les constantes et les symboles fonctionnels forment les
ensembles A et F . Le domaine de Herbrand HS (ou univers de Herbrand) de S est défini
récursivement de la manière suivante.
– Si a ∈ A, alors a ∈ HS . (Si A = ∅, créer une constante arbitraire a ∈ Hs ; un domaine
ne peut être vide.)
– Si f ∈ F (f d’arité m) et t1 , . . . , tm ∈ HS , alors f (t1 , . . . , tm ) ∈ HS .
Les éléments du domaine de Herbrand sont des objets syntaxiques, sans signification
particulière : ce sont tous les termes clos que l’on peut construire à l’aide de A et F .
139
7.4.3 Simplification de Herbrand
Soit ϕ =def ∀x [p(x) ⇒ p(f (x))] . Soit I l’interprétation de domaine N, telle que
Ic [f ](n) = 4 ∗ n et Ic [p](n) = V si n est un carré. On voit immédiatement que I[ϕ] = V.
Informellement, on le justifie en notant que l’on a I[p(n) ⇒ p(f (n))] = V, ou p(n) ⇒ p(4∗n),
pour tout n ∈ N. Cette écriture est abusive, parce qu’elle mêle des objets syntaxiques (p, f, x)
et des objets sémantiques (0, 4, n, ∗). L’écriture correcte est Ix/n [p(x) ⇒ p(f (x))] = V.
Plus généralement, Ix/d [A(x)] ou Ix/d [B] est correct (si d est un élément du domaine
d’interprétation), tandis que I[A(d)] ou I[B(x/d)] est abusif.
Soit alors H une interprétation de Herbrand. Le domaine est H = {a, f (a), f (f (a)), . . .}. On a
H[ϕ] = V si et seulement si Hx/h [p(x) ⇒ p(f (x))] = V pour tout h ∈ H. On observe qu’ici,
la notation simplifiée n’est plus abusive : on a
Hx/h [p(x) ⇒ p(f (x))] = H[p(h) ⇒ p(f (h))]
puisque l’objet h a le double statut syntaxique et sémantique.
140
1. On commence par donner une fonction w qui à tout élément h ∈ H du domaine de
Herbrand H associe un élément w(h) ∈ D.
(a) Si au moins une constante apparaı̂t dans S, toutes ces constantes sont interprétées
par I et on pose w(ci) = I[ci ] = Ic [ci ] ∈ D ; sinon, la constante arbitraire a est
interprétée en un élément d = w(a) ∈ D quelconque.
(b) Pour tout terme composé h = f (h1 , . . . , hm ) ∈ H, on pose
w(h) = Ic [f ](w(h1 ), . . . , w(hn )) ∈ D . (Cette expression est simplement I[h], sauf
si on a ajouté une constante arbitraire.)
2. Pour donner une interprétation de Herbrand H, il faut spécifier l’ensemble des atomes
fondamentaux qui seront vrais dans H.
Soient h1 , . . . , hn ∈ H et p un symbole prédicatif d’arité n. Pour interpréter l’atome
fondamental p(h1 , . . . , hn ), on pose H[p(h1 , . . . , hn )] = Ic [p](w(h1 ), . . . , w(hn ))
(Ic [p] est une fonction de D n dans {V, F}).
On a donc
Hx1 /h1 ,...,xn /hn [p(x1 , . . . , xn )] = Ix1 /w(h1 ),...,xn /w(hn ) [p(x1 , . . . , xn )]
3. Soit ϕ(x1 , . . . , xn ) une matrice ne contenant aucune variable libre autre que x1 , . . . , xn .
On a Hx1 /h1 ,...,xn /hn [ϕ(x1 , . . . , xn )] = Ix1 /w(h1 ),...,xn/w(hn ) [ϕ(x1 , . . . , xn )]
4. Toute formule de la forme ∀x1 · · · ∀xn ϕ(x1 , . . . , xn ) satisfaite par I est aussi satisfaite
par H. On a successivement
I[∀x1 · · · ∀xn ϕ(x1 , . . . , xn )] = V (hypothèse) ,
Ix1 /d1 ,...,xn /dn [ϕ(x1 , . . . , xn )] = V , pour tous les d1 , . . . , dn ∈ D,
Ix1 /w(h1 ),...,xn /w(hn ) [ϕ(x1 , . . . , xn )] = V , pour tous les h1 , . . . , hn ∈ H.
Hx1 /h1 ,...,xn /hn [ϕ(x1 , . . . , xn )] = V , pour tous les h1 , . . . , hn ∈ H.
H[∀x1 · · · ∀xn ϕ(x1 , . . . , xn )] = V .
Remarque. La théorie de Herbrand s’applique seulement aux formes de Skolem. Par exemple,
la formule
p(a) ∧ ∃x¬p(x)
est consistante, mais n’a pas de modèle de Herbrand : l’univers de Herbrand (si on le considère
comme défini) serait le singleton {a}, et la formule n’admet que des modèles à deux éléments
au moins. En revanche, la forme de Skolem correspondante
p(a) ∧ ¬p(b)
141
Second théorème de Herbrand. Une formule S en forme de Skolem est inconsistante si
et seulement s’il existe une conjonction finie inconsistante d’instances fondamentales de sa
matrice M.
Démonstration.
– La formule S est consistante si et seulement si elle admet un modèle de Herbrand.
– L’interprétation de Herbrand H est un modèle de S si et seulement si H′ [M] = V pour
toute variante H′ de H attribuant aux variables de M des valeurs quelconques prise dans
l’univers de Herbrand.
– On a H′ [M] = H[M ′ ], où M ′ est l’instance fondamentale de M obtenue en remplaçant
dans M les variables par les valeurs qui leur sont attribuées par H′ .
En conclusion, S est (in)consistant si et seulement si l’ensemble de ses instances fondamentales
est (in)consistant. Vu le théorème de compacité (logique des propositions), S est inconsistant
si et seulement s’il existe un ensemble fini inconsistant d’instances fondamentales de M.
Corollaire. Une formule en forme clausale S est inconsistante si et seulement s’il existe une
conjonction finie inconsistante de clauses fondamentales.
Remarque. Soit ∀x ∀y ∀z [C1 (x, y) ∧ C2 (y, z)] une forme clausale et H son domaine de
Herbrand. L’ensemble des instances fondamentales de la matrice est
lui-même équivalent à
{C1 (h, h′ ), C2 (h, h′ ) : h, h′ ∈ H} ,
qui est l’ensemble des clauses fondamentales.
142
C1 =def p(f (f (a)), a) ∨ p(f (f (a)), g(a)) ,
C2 =def ¬p(f (f (a)), a) ,
C3 =def ¬p(f (f (a)), g(a)).
{C1 , C2 , C3 } est inconsistant, donc S est inconsistant.
Rappel. Attention aux quantifications implicites. Les deux formules éléments de S sont en fait
∀x ∀y [p(f (x), a) ∨ p(y, g(a))] et ∀z ¬p(f (f (a)), z).
Semi-procédure de décision. Le théorème de Herbrand suggère une semi-procédure de décision
pour la validité des formules du calcul des prédicats :
1. Considérer la négation de la formule donnée.
2. La mettre en forme clausale.
3. Générer un ensemble fini de clauses fondamentales.
4. Vérifier si cet ensemble de clauses fondamentales est inconsistant.
Les points 1 et 2 sont triviaux, même si la mise en forme normale est une procédure parfois
longue et fastidieuse. Le point 4 se fait dans le cadre propositionnel ; les atomes fondamentaux
se traitent en effet comme des atomes de logique des propositions. Seul le point 3 pose un
réel problème ; produire des instances fondamentales est facile, produire “les bonnes” est plus
délicat.
143
Ces clauses forment un ensemble inconsistant, donc la formule A est inconsistante et la règle
est correcte.
Remarque. La règle reste correcte si p(x), q(x) et r(x) sont des formules quelconques dont x
est l’unique variable libre.
Deuxième exemple.
Soient
H1 : p(a) ,
H2 : ∀x (p(x) ⇒ p(f (x))) ,
C : ∀x p(x) .
On voudrait montrer que
H1 , H2
C
est une règle correcte, c’est-à-dire que
A =def H1 ∧ H2 ∧ ¬C
est une formule inconsistante.
Transformons A en forme clausale :
p(a) ∧ ∀x (p(x) ⇒ p(f (x))) ∧ ¬∀x p(x) ,
p(a) ∧ ∀x (¬p(x) ∨ p(f (x))) ∧ ∃x ¬p(x) ,
p(a) ∧ ∀x (¬p(x) ∨ p(f (x))) ∧ ¬p(b) .
Le domaine de Herbrand est H = {a, b, f (a), f (b), . . .} = {f n (a), f n (b) : n ∈ N} .
La base de Herbrand est B = {p(f n (a)), p(f n (b)) : n ∈ N} .
Une interprétation de Herbrand intéressante est H = {p(f n (a)) : n ∈ N} .
Cette interprétation rend vraies les clauses p(a) et ¬p(b), ainsi que toutes les instances
fondamentales de ¬p(x) ∨ p(f (x)). C’est donc un modèle de l’ensemble des clauses
fondamentales ; cela montre que A est une formule consistante, et aussi que la règle est
incorrecte.
144
Tant que ✷ 6∈ S, répéter :
choisir C1 = (C1′ ∨ ℓ), C2 = (C2′ ∨ ¬ℓ) ∈ S
redéfinir S := S ∪ {res(C1 , C2 )}
145
8 Logiques prédicatives décidables
Le calcul des prédicats est indécidable, mais admet des fragments intéressants décidables.
Nous en considérons ici deux exemples, la logique des prédicats monadiques et la logique de
Bernays et Schönfinkel.
La formule de base et ses variantes Etant donnés deux prédicats unaires62 P et Q (dans cet
ordre), on appelle formule de base la formule ∀x (P (x) ⇒ Q(x)). Les variantes s’obtiennent
en introduisant des négations, portant sur le conséquent de l’implication ou sur toute la formule.
On a donc quatre possibilités, souvent identifiées par les quatre lettres A, E, I et O :63
Ces quatre formules sont dites “de type PQ”. Une formule dont le type est PQ ou QP est une
{P, Q}-formule ; il y a donc huit {P, Q}-formules.
146
termes P (x), Q(x) et R(x) sont dits respectivement mineur, moyen et majeur.64 Le syllogisme
catégorique est la règle d’inférence
majeure mineure
conclusion
Etant donnés les trois prédicats P , Q et R, il existe donc 256 syllogismes catégoriques.
Le problème est de déterminer lesquels sont valides, c’est-à-dire tels que la conclusion soit
conséquence logique des prémisses. Une grande partie des raisonnements courants (y compris
beaucoup de raisonnements incorrects) se formalisent naturellement en des enchaı̂nements de
syllogismes, ce qui justifie l’intérêt particulier que cette notion a suscité dans le passé. Le point
de vue moderne accorde peu d’importance à la théorie du syllogisme, simple fragment de la
logique monadique ; la raison essentielle en est que, le nombre de syllogismes étant fini, leur
étude est triviale : il suffit de les passer en revue un à un et de tester, pour chacun d’eux, sa
validité. Cela se fait aisément, par exemple en utilisant la méthode des tableaux sémantiques
ou celles de Herbrand.65
Le mode d’un syllogisme est déterminé par la nature des prémisses et de la conclusion. Par
exemple, le mode AEI désigne le cas où la majeure est universelle affirmative (A), la mineure
est universelle négative (E) et la conclusion est particulière affirmative (I). Il y a donc 43 = 64
modes possibles, chacun pouvant exister dans les quatre figures. Cependant, on peut vérifier
que 12 modes seulement peuvent donner lieu à des syllogismes valides. Ce sont
AAA , AAI , AEE , AEO , AII , AOO , EAE , EAO , EIO , IAI , IEO , OAO .
147
4. Si une prémisse est négative, la conclusion doit être négative.
5. Si les deux prémisses sont affirmatives, la conclusion doit être affirmative.
Ces règles, dont l’exactitude avait été reconnue empiriquement, permettent de rejeter les 52
modes “stériles”. Par exemple, la première des règles permet d’éliminer des modes tels que EEE
et OEO ; la deuxième permet d’éliminer III (entre autres) ; la troisième provoque notamment le
rejet de AIA ; des modes tels que AOI et AIO contreviennent respectivement aux quatrième et
cinquième règles.
Il ne reste donc que 12 × 4 = 48 syllogismes potentiellement valides ; parmi ceux-ci, nous
allons voir que 15 syllogismes seulement sont valides.
Les diagrammes de Venn. C’est par une démarche informelle qu’Aristote et les Scolastiques
ont déterminé quels syllogismes étaient valides et lesquels ne l’étaient pas. Les syllogismes
valides ont reçu des noms conventionnels, dont les voyelles rappellent le mode. Par exemple,
le raisonnement classique “Tous les humains sont mortels, tous les Grecs sont des humains,
donc tous les Grecs sont mortels” est un syllogisme dont on détecte aisément la structure :66
(M) Tous les humains sont mortels.
(m) Tous les Grecs sont des humains.
(C) Tous les Grecs sont mortels.
Ce syllogisme appartient à la première figure et au mode AAA ; cette combinaison se note
AAA -1 ou, de manière plus classique (et plus poétique), BARBARA . Les trois “A ” rappellent
que les prémisses et la conclusion sont toutes trois des universelles affirmatives. De même, le
syllogisme
(M) Tous les étudiants sont intelligents.
(m) Certains humains ne sont pas intelligents.
(C) Certains humains ne sont pas des étudiants.
appartient à la deuxième figure ; c’est un exemple de AOO -2 ou BAROCO, la majeure étant
universelle affirmative, la mineure et la conclusion étant particulières négatives.
Un moyen simple et concret d’appréhender la validité d’un syllogisme consiste à utiliser
un diagramme de Venn à trois composants (figure 64). Le cercle de gauche représente le
mineur P (x), celui de droite le majeur R(x), le cercle du haut correspondant au moyen Q(x).
Ces cercles déterminent huit zones numérotées de 0 à 7. Tout objet appartient à l’une de ces
zones, selon la valeur de vérité qu’il attribue au mineur, au majeur et au moyen. Par exemple,
la zone 4 est intérieure aux cercles mineur et moyen, mais extérieure au cercle majeur ; elle
regroupe donc les objets rendant vrais le mineur et le moyen, mais faux le majeur.
Les prémisses et conclusions des syllogismes correspondent à des assertions de vacuité ou
de non-vacuité de certaines zones ; un syllogisme sera valide si son “interprétation graphique”
est correcte. Nous illustrons cette technique de vérification par quelques exemples et contre-
exemples.
Le syllogisme AAA -1 que nous venons d’évoquer s’analyse aisément. La prémisse majeure
∀x (Q(x) ⇒ R(x)) signifie que tout objet vérifiant le moyen vérifie aussi le majeur, donc que
les zones 1 et 4 sont vides, ce que nous notons 1 ∪ 4 = ∅ ; de même, la prémisse mineure
66
Nous convenons d’énoncer systématiquement la majeure avant la mineure, quoique l’ordre des prémisses soit
sans influence sur la validité d’un raisonnement.
148
Q
0
1
4 5
7
2 3
6
P R
F IG . 64 – Diagramme de Venn
149
PQ-formule particulière (ou existentielle) correspondante.67 Le mécanisme de subalternation
consiste à déduire la subalterne de la formule universelle correspondante.
Ce mécanisme n’est pas valide stricto sensu, puisque la subalterne n’est pas conséquence
logique de l’universelle ; on a
Cependant, on peut, au moyen d’une prémisse additionnelle, obtenir une version correcte de la
subalternation :
Dans le langage naturel, on peut parfois considérer que la prémisse manquante est implicite.
Nous qualifierons de quasi-valide un syllogisme dont la validité dépend de l’emploi de la
subalternation, et donc de l’existence d’une prémisse implicite. Cette prémisse sera toujours
de la même nature : elle affirme l’existence d’un objet au moins vérifiant le majeur, le moyen
ou le mineur. Dans le cadre des diagrammes de Venn, cette prémisse prend donc l’une des trois
formes suivantes :
(Moyen) 1 ∪ 4 ∪ 5 ∪ 7 6= ∅ ;
(Mineur) 2 ∪ 4 ∪ 6 ∪ 7 6= ∅ ;
(Majeur) 3 ∪ 5 ∪ 6 ∪ 7 6= ∅.
Le tableau récapitulatif des syllogismes valides ou quasi-valides est représenté à la figure 65.68
Les quinze syllogismes valides sont AAA -1, EAE -1, AII -1 et EIO -1 pour la première figure,
AEE -2, EAE -2, AOO -2 et EIO -2 pour la deuxième figure, AII -3, IAI -3, EIO -3 et OAO -3 pour la
troisième figure, et AEE -4, IAI -4 et EIO -4, pour la quatrième figure. Dans le tableau, les noms
anciens ont été utilisés ; on obtient la nomenclature moderne en ne retenant que les voyelles.69
Cinq syllogismes valides ont une conclusion universelle ; en remplaçant celle-ci par sa
subalterne, on obtient cinq syllogismes quasi-valides. Les dix autres syllogismes valides, dont
la conclusion est particulière, ont également une prémisse particulière ;70 en remplaçant celle-
ci par sa superalterne, on obtient aussi des syllogismes quasi-valides, dont quatre distincts des
précédents. On a donc en tout neuf syllogismes quasi-valides.
150
Première figure Deuxième figure
on imagine aisément qu’elle reste applicable pour une classe infinie de formules.71 Pour
déterminer une telle classe, aussi grande que possible, nous reconsidérons des syllogismes
et essayons de les généraliser.
71
Il est plus commode de parler de formules que de raisonnement ; rappelons que le raisonnement dont les
prémisses sont P1 , . . . , Pn et dont la conclusion est C est valide (ou correct) si et seulement si la formule
(P1 ∧ · · · ∧ Pn ) ⇒ C est valide.
151
Concrètement, valider le syllogisme BARBARA revient à valider la disjonction
Il semble clair que la méthode des diagrammes de Venn restera applicable si les disjonctions
comportent plus de trois éléments et si matrices des formules impliquées sont des fonctions
booléennes quelconques des formes P (x), Q(x) et R(x). De même, rien ne devrait empêcher
l’introduction d’une quatrième forme S(x) : on pourrait alors maintenir la forme graphique
élégante de la méthode de Venn en passant dans l’espace à trois dimensions, les formes étant
représentées par quatre sphères, délimitant en tout 24 = 16 zones. On pourrait aussi renoncer à
l’aspect graphique de la méthode et autoriser n prédicats distincts.72
Dans la suite de ce chapitre, on précise ces extensions et leur traitement, ce qui conduit à
une procédure de décision pour le calcul des prédicats monadiques.
Schémas monadiques booléens sur une variable. Un schéma monadique booléen (SMB)
sur la variable x est une combinaison booléenne (finie) de formes telles que P (x), Q(x), . . .
résultant de l’application à la variable x d’un prédicat monadique.
Dans la méthode de Venn, on se préoccupe seulement de savoir si une zone est vide ou
non, sans distinguer les cas où une zone contient un ou plusieurs élément(s) ; c’est justifié par
le théorème suivant :
Théorème. Si un SMB Φ(x) admet un modèle, alors il admet un modèle à un seul élément.
Démonstration. Soit I une interprétation de Φ(x) de domaine D et soit a ∈ D tel que I[x] = a.
L’interprétation J de domaine {a} telle que J[x] = a et, pour tout prédicat (monadique) P ,
telle que J[P ] est la restriction à {a} de I[P ] est telle que J(Φ) = I(Φ).
Définition. Une interprétation fondamentale d’un SMB Φ(x) est une interprétation de Φ(x)
dont le domaine comporte un seul élément.
Remarque. Les interprétations dont le domaine est un singleton ont une propriété intéressante
dépassant le cadre monadique. Une telle interprétation attribue toujours la même valeur de
vérité à une formule (quelconque), à sa fermeture universelle et à sa fermeture existentielle.
Remarque. Etant donné le lexique Π = {P1 , . . . , Pn }, un SMB Φ(x) admet 2n interprétations
fondamentales distinctes.
Corollaire. Un SMB est valide s’il est vrai pour toutes les interprétations fondamentales ; il est
consistant s’il est vrai pour une interprétation fondamentale au moins.
Remarque. Les schémas monadiques booléens peuvent être assimilés aux formules
propositionnelles ; ils ne sont donc pas intéressants en soi.
152
Remarque. La matrice d’un SMQ ne contient pas d’autre variable que la variable quantifiée
(unique) ; un SMQ est donc une formule fermée.
Théorème. Un schéma monadique quantifié est valide (resp. consistant, contingent) si et
seulement si sa matrice est valide (resp. consistante, contingente).
Démonstration. Il suffit de démontrer que, pour tout schéma monadique booléen Φ(x),
la validité de ∃x Φ(x) entraı̂ne celle de Φ(x). On procède par l’absurde. Si Φ(x) admet
un antimodèle, il existe un antimodèle à un seul élément ; celui-ci est nécessairement un
antimodèle de ∃x Φ(x).
Corollaire. Si Φ(x) est un SMB, les trois formules Φ(x), ∀x Φ(x) et ∃x Φ(x) sont
simultanéments valides, contingentes ou inconsistantes.73
Remarque. Ce corollaire montre que les schémas monadiques quantifiés, pris isolément, ne sont
pas non plus très intéressants. En revanche, les combinaisons booléennes de tels schémas le
sont, comme nous le voyons au paragraphe suivant. La formule correspondant à un syllogisme
peut toujours s’écrire comme une disjonction de trois SMQ.
153
singleton {ak }. On définit une interprétation I dont le domaine est {a1 , . . . , an } ; pour tout
prédicat P et pour tout k ∈ {1, . . . , n}, on pose I[P ](ak ) = Ik [P ](ak ) si P intervient dans Ek
et I[P ](ak ) = V (par exemple) sinon. L’interprétation I est un modèle commun à tous les Ek
et donc un modèle de la conjonction car, par construction, Ix/ak (Mk ) = V donc I(Ek ) = V.
Remarque. On ne peut pas déduire de ce qui précède qu’en logique monadique, la formule
∃x [Φ(x) ∧ Ψ(x)] serait logiquement équivalente à la formule ∃x Φ(x) ∧ ∃x Ψ(x). En outre, le
résultat selon lequel un schéma existentiel consistant admet un modèle fondamental ne s’étend
pas à une conjonction de tels schémas. Un contre-exemple commun évident est fourni par les
deux schémas ∃x P (x) et ∃x ¬P (x).
Théorème. Un schéma existentiel ∃x Ψ(x) est conséquence logique d’un schéma existentiel
∃x Φ(x) si et seulement si la matrice Ψ(x) est conséquence logique de la matrice Φ(x).
Démonstration. La condition est visiblement suffisante. Soit I un modèle fondamental de
∃x Φ(x) ; c’est aussi un modèle (fondamental) de Φ(x), de Ψ(x) et de ∃x Ψ(x). La condition est
aussi nécessaire. Si Ψ(x) n’est pas conséquence logique de Φ(x), alors le SMB Φ(x) ∧ ¬Ψ(x)
admet un modèle fondamental, qui est aussi un modèle de ∃x Φ(x), mais un antimodèle
fondamental de Ψ(x) et donc de ∃x Ψ(x).
Corollaire. La conjonction (∃x Φ(x) ∧ ∀x Ψ(x)) est (in)consistante si et seulement si le SMB
Φ(x) ∧ ¬Ψ(x) est (in)consistant.
Corollaire. Si ∃x Ψ(x) n’est pas conséquence logique de ∃x Φ(x), la conjonction ∃x Φ(x) ∧
∀x ¬Ψ(x) admet un modèle fondamental.
Il reste à étudier le cas où la conjonction de SMQ comporte aussi un schéma universel ou
plusieurs ; on peut se limiter à un seul, puisque la conjonction de schémas universels est un
schéma universel.76
On note d’abord que la conjonction d’un schéma existentiel E et d’un schéma universel U
est consistante si et seulement si le schéma existentiel ¬U n’est pas conséquence logique du
schéma existentiel E, ce que l’on peut tester par le théorème précédent.
On a enfin le théorème suivant.
Théorème. La conjonction E1 ∧ · · · ∧ En ∧ U est consistante si et seulement si chacune des
conjonctions Ek ∧ U est consistante.
Démonstration. La condition est visiblement nécessaire. Elle est aussi suffisante. Vu
le corollaire précédent, si les conjonctions Ek ∧ U sont consistantes, elles admettent
respectivement les modèles fondamentaux Ik , de domaine {ak }. On définit alors
l’interprétation I de domaine est {a1 , . . . , an } ; pour tout prédicat P et pour tout k ∈
{1, . . . , n}, on pose I[P ](ak ) = Ik [P ](ak ) si P intervient dans Ek ou dans U et I[P ](ak ) = V
(par exemple) sinon. L’interprétation I est un modèle commun à U et à tous les Ek et donc
un modèle de la conjonction car, par construction, on a Ix/ak (Mk ) = Ix/ak (M)V donc
I(Ek ∧ U) = V, où Mk et M sont les matrices de Ek et U.
Corollaire. La disjonction U1 ∨ · · · ∨ Un ∨ E est valide si et seulement si au moins une des
disjonctions Uk ∨ E est valide.
Remarque. On teste la validité d’une combinaison booléenne de SMQ en la transformant en
une conjonction de disjonctions de SMQ, et en traitant séparément chaque disjonction. Le test
d’une disjonction de n SMQ se ramène à au plus n tests de conséquence logique entre deux
76
V V
Quelles que soient les formules Ai et la variable x, les formules ∀x i Ai et i ∀x Ai sont logiquement
équivalentes.
154
SMQ existentiels ou, plus simplement, entre deux SMB sur une même variable x et donc, plus
simplement encore, au test de validité de n SMB sur x. Enfin, un SMB est valide si et seulement
si le schéma propositionnel correspondant (obtenu en remplaçant chaque occurrence de Pi (x)
par l’atome pi ) est valide.
Remarque. La technique vue ici s’étend immédiatement aux combinaisons booléennes
comportant non seulement des SMQ mais aussi des propositions élémentaires.
Exemples. Nous reconsidérons d’abord les cas des syllogismes BARBARA et FERIO évoqués
au paragraphe 8.1.2. La disjonction
elle est valide si son premier élément est conséquence logique de son second, ou encore si
c’est-à-dire si
¬[p ⇒ r] |= [q ∧ ¬r] ∨ [p ∧ ¬q] ,
ce qui est visiblement le cas. De même, la disjonction
elle est valide si son premier élément est conséquence logique de son second, ou encore si
c’est-à-dire si
¬[p ⇒ ¬q] |= [q ∧ r] ∨ [p ∧ ¬r] ,
ce qui est visiblement le cas.
On étudie ensuite DARAPTI. Sans le présupposé d’existence, la disjonction correspondante
est
∃x [Q(x) ∧ ¬R(x)] ∨ ∃x [Q(x) ∧ ¬P (x)] ∨ ∃x [P (x) ∧ R(x)] ,
qui se récrit en
[q ∧ ¬r] ∨ [q ∧ ¬p] ∨ [p ∧ r] ,
155
ce qui n’est pas le cas. En revanche, avec le présupposé d’existence, la disjonction
correspondante devient
qui se récrit en
Cette disjonction est valide si son second élément est conséquence logique de la négation de
son premier, ou encore si la formule
{q , q ⇒ r , q ⇒ p} |= p ∧ r ,
ou encore à l’énoncé
On note que la méthode de Venn n’est autre qu’une version graphique de la méthode introduite
et justifiée dans les paragraphes précédents ; elle est donc correcte.
Remarque. Le traitement de DARAPTI par la méthode de Herbrand revient à déterminer
l’inconsistance de l’ensemble
la méthode de Venn est donc dans ce cas une version graphique de la méthode de Herbrand.
156
Théorème. Une formule est simple si et seulement si elle est une combinaison booléenne de
SMQ et d’atomes.
Démonstration. La condition est visiblement suffisante. On établit qu’elle est nécessaire par
induction sur la structure syntaxique des formules.
Corollaire. Une formule est simple et fermée si et seulement si elle est une combinaison
booléenne de SMQ et d’atomes sans variable.77
Lois de passage. Les lois de passage sont des schémas d’équivalence logique entre formules.
Associées au théorème de l’échange,78 elles permettent de réduire les formules à la forme
simple. On a :
– ∀x A ↔ A et ∃x A ↔ A, si A ne comporte pas d’occurrence libre de x.
– ∀x ¬A ↔ ¬∃x A ; ∃x ¬A ↔ ¬∀x A.
– ∀x (A ∧ B) ↔ (∀x A ∧ ∀x B) ; ∃x (A ∨ B) ↔ (∃x A ∨ ∃x B).
– ∀x (A ∨ B) ↔ (∀x A ∨ B) ; ∃x (A ∧ B) ↔ (∃x A ∧ B), si B ne comporte pas
d’occurrence libre de x.
Rappelons que ces règles sont valables en logique prédicative générale.
Il est clair que la première formule est conséquence logique de la seconde, mais la réciproque
est fausse. Pour le voir, on réduit d’abord la première formule à la forme simple. Dans la liste
ci-dessous, toutes les formules sont logiquement équivalentes.
77
Les atomes sans variable sont true, false et les propositions élémentaires. Bien que ces dernières soient
assimilées à des prédicats à 0 argument, il est commode de les admettre en logique monadique. D’ailleurs, on
pourrait éliminer les atomes sans variable en les remplaçant par des SMQ particuliers.
78
Le théorème de l’échange permet de remplacer une sous-formule par une sous-formule logiquement
équivalente, sans changer la sémantique de départ.
157
∀x ∃y [(P x ∨ Qy) ∧ (Rx ∨ Sy)] ,
∀x ∃y [(P x ∧ Rx) ∨ (P x ∧ Sy) ∨ (Qy ∧ Rx) ∨ (Qy ∧ Sy)] ,
∀x [(P x ∧ Rx) ∨ (P x ∧ ∃y Sy) ∨ (∃y Qy ∧ Rx) ∨ ∃y (Qy ∧ Sy)] ,
∀x [(P x ∧ Rx) ∨ (P x ∧ ∃y Sy) ∨ (∃y Qy ∧ Rx)] ∨ ∃y (Qy ∧ Sy) ,
∀x [(P x ∨ ∃y Qy) ∧ (P x ∨ Rx) ∧ (Rx ∨ ∃y Sy)] ∨ ∃y (Qy ∧ Sy) ,
[(∀x P x ∨ ∃y Qy) ∧ ∀x (P x ∨ Rx) ∧ (∀x Rx ∨ ∃y Sy)] ∨ ∃y (Qy ∧ Sy) .
En comparant les deux formes normales, on observe que la première comporte les mêmes cubes
que la seconde, plus un cube supplémentaire. Il est donc possible de rendre la première formule
vraie tout en falsifiant la seconde, au moyen d’une interprétation rendant faux les quatre cubes
ci-dessus et vrai le cube supplémentaire
Une telle interprétation sur le domaine {a, b} est par exemple celle qui rend vrais les atomes
P a, Qa, Rb, Sb et faux les atomes P b, Qb, Ra, Sa.
On peut aussi appliquer la technique vue au paragraphe 8.1.3. Il faut montrer la consistance
d’une conjonction de cinq formules, dont les quatre premières sont les négations des cubes
communs aux deux formules étudiées et dont la cinquième est le cube supplémentaire. Les
cinq membres de la conjonction sont donc
1. ¬(∀x P x ∧ ∀x Rx), soit ∃x (¬P x ∨ ¬Rx) ;
2. ¬(∀x P x ∧ ∃y Sy), soit ∃x ¬P x ∨ ∀y ¬Sy ;
3. ¬(∃y Qy ∧ ∀x Rx), soit ∀y ¬Qy ∨ ∃x ¬Rx ;
4. ¬∃y (Qy ∧ Sy), soit ∀y (¬Qy ∨ ¬Sy) ;
5. ∃y Qy ∧ ∀x (P x ∨ Rx) ∧ ∃y Sy .
158
Tout modèle éventuel devra satisfaire ∃y Qy et ∃y Sy (formule 5), ce qui permet de simplifier
d’emblée les formules 2 et 3 en ∃x ¬P x et ∃x ¬Rx, respectivement. Cette simplification
montre que la formule 1 est inutile et peut donc être omise. Il reste donc à trouver un modèle
pour la conjonction
∃x ¬P x ∧ ∃x ¬Rx ∧ ∀y (¬Qy ∨ ¬Sy) ∧ ∃y Qy ∧ ∀x (P x ∨ Rx) ∧ ∃y Sy .
En regroupant les deux schémas universels et par renommage de y en x, cette formule se récrit
en
∃x ¬P x ∧ ∃x ¬Rx ∧ ∃x Qx ∧ ∃x Sx ∧ ∀x [(¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx)] .
D’après les résultats du paragraphe 8.1.3, il suffit de vérifier séparément la consistance des
formules
∃x ¬P x ∧ ∀x [(¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx)] ,
∃x ¬Rx ∧ ∀x [(¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx)] ,
∃x Qx ∧ ∀x [(¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx)] ,
∃x Sx ∧ ∀x [(¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx)] ,
ou encore (§ 8.1.3) des formules
¬P x ∧ (¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx) ,
¬Rx ∧ (¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx) ,
Qx ∧ (¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx) ,
Sx ∧ (¬Qx ∨ ¬Sx) ∧ (P x ∨ Rx) ,
ce qui est évident dans chaque cas.
Remarque. Rappelons que, dans la recherche de modèles pour ces formules, on peut se limiter
aux modèles fondamentaux. On peut aussi, à partir des quatre modèles obtenus, créer un
modèle commun, mais ce modèle ne sera généralement pas fondamental. Dans notre exemple,
il comportera au minimum deux éléments ; le modèle à deux éléments donné plus haut rend
vraies les quatre formules, en considérant l’instance x = a pour les deuxième et troisième
formules, et l’instance x = b pour les deux autres formules.
159
8.2.2 Logique prédicative sans quantification
Si on s’interdit de quantifier les variables, celles-ci deviennent, sur le plan sémantique,
indistinguables des constantes. En effet, interpréter une constante ou une variable est
simplement lui associer un élément du domaine d’interprétation. On peut donc admettre qu’en
l’absence de quantification, les seuls termes sont les constantes.
Une formule de la logique sans quantification est une combinaison linéaire d’atomes
sans variables. Si une telle formule comporte n atomes distincts, elle admettra 2n
interprétations, exactement comme en logique propositionnelle. On notera que deux atomes
sont (complètement) indépendants dès qu’ils sont syntaxiquement distincts ; il n’y a pas
plus de liens sémantiques entre, par exemple, P (a, a, b) et P (a, b, b) qu’entre P (a, a, b) et
Q(c, d). L’étude des formules predicatives sans quantification se ramène à l’étude des formules
booléennes correspondantes.
160
8.2.4 Logique prédicative avec une alternance de quantification
La technique du paragraphe précédent permet d’analyser toutes les formules monadiques
et de nombreuses autres formules utiles, notamment celles dont la forme prénexe comporte une
seule alternance de quantificateurs.
Exemple. La formule
∃x ∀y P (x, y) ⇒ ∀y ∃x P (x, y)
est logiquement équivalente à la forme prénexe
donc ces trois formules sont valides si et seulement si la dernière est valide, ce qui est le cas
puisque la disjonction
[P (x, x) ⇒ P (x, y)] ∨ [P (x, x) ⇒ P (y, y)] ∨ [P (x, y) ⇒ P (x, y)] ∨ [P (x, y) ⇒ P (y, y)]
est valide.
161
Remarque. On voit immédiatement l’intérêt de ce théorème qui permet, lors de la recherche de
modèles, de se limiter aux interprétations de Herbrand, donc à un domaine générique, unique
et simple.
Démonstration. La condition est visiblement suffisante. On montre qu’elle est nécessaire
en donnant une technique de transformation d’un modèle quelconque I (de domaine D
quelconque) en un modèle de Herbrand H (de domaine H = HS ).
1. On commence par donner une fonction w qui à tout élément h ∈ H du domaine de
Herbrand H associe un élément w(h) ∈ D. Si au moins une constante apparaı̂t dans S,
toutes ces constantes sont interprétées par I et on pose w(ci ) = I[ci ] = Ic [ci ] ∈ D ;
sinon, la constante arbitraire c est interprétée en un élément d = w(a) ∈ D quelconque.
2. Pour donner une interprétation de Herbrand H, il faut spécifier l’ensemble des atomes
fondamentaux qui seront vrais dans H.
Soient h1 , . . . , hn ∈ H et p un symbole prédicatif d’arité n. Pour interpréter l’atome
fondamental p(h1 , . . . , hn ), on pose H[p(h1 , . . . , hn )] = Ic [p](w(h1 ), . . . , w(hn ))
(Ic [p] est une fonction de D n dans {V, F}).
On a donc
Hx1 /h1 ,...,xn /hn [p(x1 , . . . , xn )] = Ix1 /w(h1 ),...,xn /w(hn ) [p(x1 , . . . , xn )]
3. Soit ϕ(x1 , . . . , xn ) une matrice ne contenant aucune variable libre autre que x1 , . . . , xn .
On a Hx1 /h1 ,...,xn /hn [ϕ(x1 , . . . , xn )] = Ix1 /w(h1 ),...,xn/w(hn ) [ϕ(x1 , . . . , xn )]
4. Toute formule de la forme ∀x1 · · · ∀xn ϕ(x1 , . . . , xn ) satisfaite par I est aussi satisfaite
par H. On a successivement
I[∀x1 · · · ∀xn ϕ(x1 , . . . , xn )] = V (hypothèse) ,
Ix1 /d1 ,...,xn /dn [ϕ(x1 , . . . , xn )] = V , pour tous les d1 , . . . , dn ∈ D,
Ix1 /w(h1 ),...,xn /w(hn ) [ϕ(x1 , . . . , xn )] = V , pour tous les h1 , . . . , hn ∈ H.
Hx1 /h1 ,...,xn /hn [ϕ(x1 , . . . , xn )] = V , pour tous les h1 , . . . , hn ∈ H.
H[∀x1 · · · ∀xn ϕ(x1 , . . . , xn )] = V .
Procédures de décision Une conséquence immédiate du petit théorème de Herbrand est que,
pour tester la consistance d’une forme universelle
Remarque. La théorie de Herbrand a une portée très générale ; elle n’est pas restreinte au cas
particulier des formes universelles pures. que ce qui vient d’être s’applique seulement aux
formes de Skolem. Par exemple, la formule
p(a) ∧ ∃x¬p(x)
est consistante, mais n’a pas de modèle de Herbrand : l’univers de Herbrand (si on le considère
comme défini) serait le singleton {a}, et la formule n’admet que des modèles à deux éléments
au moins. En revanche, la forme de Skolem correspondante
p(a) ∧ ¬p(b)
162