344 pages
Français

Logique pour l'informatique

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Cet ouvrage débute par une introduction à la logique des prédicats du premier ordre : syntaxe, sémantique et preuves formelles. Il guide ensuite le lecteur vers quelques uns de ses aspects plus avancés : théorème de complétude, théorème d'indécidabilité. Se tournant ensuite vers les rapports de la logique et de l'informatique, il présente les méthodes algorithmiques de démonstration automatique comme la résolution et l'unification ainsi que des applications plus directes des concepts logiques au domaine informatique (problème SAT, bases de données relationnelles, vérification de modèle, etc.)

Sa lecture ne demande aucun prérequis en la matière et peut s'adresser à tout étudiant débutant en logique (licence ou master d'informatique, élève ingénieur). L'exposé des notions de base de logique sont accompagnées de nombreux exercices corrigés.

Sujets

Informations

Publié par
Date de parution 10 novembre 2020
Nombre de lectures 2
EAN13 9782340044920
Langue Français
Poids de l'ouvrage 4 Mo

Informations légales : prix de location à la page 0,1350€. Cette information est donnée uniquement à titre indicatif conformément à la législation en vigueur.

Mathieu Jaume
Matthieu Journault
Marie-Jeanne Lesot
Pascal Manoury
Isabelle Mounier
LicenceLicence
Master Master
Logique pour
l’informatique
M. Jaume, M. Journault,
M.-J. Lesot, P. Manoury,
Logique pour l’informatique
I. MounierRéférences sciences
Logique
pour l’informatique
Mathieu Jaume
Matthieu Journault
Marie-Jeanne Lesot
Pascal Manoury
Isabelle MounierCollection Références sciences
dirigée par Paul de Laboulaye
paul.delaboulaye@editions-ellipses.fr
Préface
Retrouvez tous les livres de la collection et des extraits sur www.editions-ellipses.fr
La logique consiste à préciser ce qu’est un énoncé et plus précisément comment
on assemble des briques de base du langage pour former des énoncés complexes.
Dès l’antiquité, avec Aristote, on a compris que cet assemblage ne dépendait pas du
domaine du discours et ne nécessitait que quelques connecteurs logiques et quelques
quantificateurs. Dans son syllogisme le plus connu : «tous les hommes sont mortels,
Socrate est un homme donc Socrate est mortel», on a déjà la conjonction (la virgule),
l’implication(«donc»)etlaquantificationuniverselle(«tous»).Etmêmesilaquestion
ne se posait sans doute pas à cette époque, on sait aujourd’hui qu’il suffit de rajouter
la négation pour avoir un jeu complet permettant de construire tous les énoncés.
La logique consiste aussi à préciser comment on établit la vérité d’un énoncé à
partir des axiomes d’un domaine. Là encore, cela ne dépend pas du domaine et peut
s’étendre dans une certaine mesure à la physique, la philosophie ou même la politique,
etdèsl’époqued’Aristote,uncertainnombrederègles de démonstration étaitconnues,
par exemple pour établir la vérité du syllogisme sus-cité.
Depuisledébutdu20esiècle,avecHilbert,Frege,Gentzen,Gödel,etbiend’autres,
on connaît la logique du premier ordre qui permet d’exprimer tous les énoncés. On
connaît aussi plusieurs notions de démonstration, toutes équivalentes, bien que très
différentes (systèmes à la Hilbert, méthode des tableaux, déduction naturelle, etc.).
On sait même que pour tout domaine contenant l’arithmétique, il y aura toujours
des énoncés vrais dont on ne peut établir la vérité, c-à-d des énoncés vrais mais
indémontrables (c’est le premier théorème d’incomplétude de Gödel).
La logique du premier ordre, présentée dans cet ouvrage, définit formellement
l’ensemble des énoncés comme des arbres, la vérité dans un modèle et la prouvabilité par
l’existence d’un enchaînement de règles permettant de passer des axiomes à l’énoncé
visé.ISBN 9782340-042612
Quant à l’informatique, elle est aussi née dès l’antiquité, avec les premiers algo-© Ellipses Édition Marketing S.A., 2020
32, rue Bargue 75740 Paris cedex 15 rithmes tel que l’algorithme d’Euclide pour le calcul du pgcd (plus grand commun
diviseur) de deux entiers. Les premiers langages de programmation comme leλ-calcul

de Church, le système T de Gödel ou les machines de Turing sont apparus dans les

années 1930, avant les premiers ordinateurs. La «thèse de Church» affirme que tous
ces langages sont équivalents.
À cette époque, il s’agissait de comprendre la différence entre recherche de preuves
etcalculmécanique.Hilbert,danssonfameuxprogramme,sedemandaitsiiln’existait
pas un moyen mécanique d’établir la vérité des énoncés. Et c’est justement le résultatPréface
La logique consiste à préciser ce qu’est un énoncé et plus précisément comment
on assemble des briques de base du langage pour former des énoncés complexes.
Dès l’antiquité, avec Aristote, on a compris que cet assemblage ne dépendait pas du
domaine du discours et ne nécessitait que quelques connecteurs logiques et quelques
quantificateurs. Dans son syllogisme le plus connu : «tous les hommes sont mortels,
Socrate est un homme donc Socrate est mortel», on a déjà la conjonction (la virgule),
l’implication(«donc»)etlaquantificationuniverselle(«tous»).Etmêmesilaquestion
ne se posait sans doute pas à cette époque, on sait aujourd’hui qu’il suffit de rajouter
la négation pour avoir un jeu complet permettant de construire tous les énoncés.
La logique consiste aussi à préciser comment on établit la vérité d’un énoncé à
partir des axiomes d’un domaine. Là encore, cela ne dépend pas du domaine et peut
s’étendre dans une certaine mesure à la physique, la philosophie ou même la politique,
etdèsl’époqued’Aristote,uncertainnombrederègles de démonstration étaitconnues,
par exemple pour établir la vérité du syllogisme sus-cité.
Depuisledébutdu20esiècle,avecHilbert,Frege,Gentzen,Gödel,etbiend’autres,
on connaît la logique du premier ordre qui permet d’exprimer tous les énoncés. On
connaît aussi plusieurs notions de démonstration, toutes équivalentes, bien que très
différentes (systèmes à la Hilbert, méthode des tableaux, déduction naturelle, etc.).
On sait même que pour tout domaine contenant l’arithmétique, il y aura toujours
des énoncés vrais dont on ne peut établir la vérité, c-à-d des énoncés vrais mais
indémontrables (c’est le premier théorème d’incomplétude de Gödel).
La logique du premier ordre, présentée dans cet ouvrage, définit formellement
l’ensemble des énoncés comme des arbres, la vérité dans un modèle et la prouvabilité par
l’existence d’un enchaînement de règles permettant de passer des axiomes à l’énoncé
visé.
Quant à l’informatique, elle est aussi née dès l’antiquité, avec les premiers
algorithmes tel que l’algorithme d’Euclide pour le calcul du pgcd (plus grand commun
diviseur) de deux entiers. Les premiers langages de programmation comme leλ-calcul
de Church, le système T de Gödel ou les machines de Turing sont apparus dans les
années 1930, avant les premiers ordinateurs. La «thèse de Church» affirme que tous
ces langages sont équivalents.
À cette époque, il s’agissait de comprendre la différence entre recherche de preuves
etcalculmécanique.Hilbert,danssonfameuxprogramme,sedemandaitsiiln’existait
pas un moyen mécanique d’établir la vérité des énoncés. Et c’est justement le résultatii Préface
de Gödel et la thèse de Church qui ont établi une distinction définitive entre énoncés
prouvables et énoncés calculables.
Avec ce point de vue la logique et l’informatique sont intimement liées. En effet,
la première définit les énoncés prouvables, c-à-d les énoncés pour lesquels on peut
produire une démonstration. Tandis que la seconde définit les énoncés calculables,
cà-d les énoncés pour lesquels on peut définir un programme qui distingue les énoncés
vrais des faux. Ce lien profond justifie à lui seul que la logique soit un des
Table des matièrespiliers de base d’un cursus d’informatique.
Par ailleurs, avec l’augmentation de la puissance des ordinateurs et la découverte
denouveauxalgorithmes,lapreuveautomatiqueafaitd’immensesprogrèsetsetrouve
de plus en plus présente en particulier pour vérifier des circuits logiques et des
programmes informatiques. On voit ici un double lien entre l’informatique et la logique :
l’utilisation de l’informatique pour écrire des algorithmes recherchant des preuves
d’énoncés et l’utilisation de ces mêmes algorithmes pour démontrer la correction de
Introduction 1
matériels ou logiciels informatiques. Cet ouvrage donne les bases pour appréhender
ces deux aspects dans les derniers chapitres en abordant la résolution, une méthode
1 Langages logiques 5
classique de recherche de preuves, et en évoquant le model checking pour exprimer et
1.1 Constantes, fonctions, prédicats et connecteurs . . . . . . . . . . . . . 6
vérifier des propriétés de logiciels.
1.1.1 Principes ......................... ..... 7De plus, il existe un lien profond entre preuves et programmes! En effet, on peut
1.1.2 Langage de termes .................... ..... 8voir une preuve d’une implicationA⇒B comme un programme calculant une preuve
1.1.3 Formules atomiques, connecteurs, formules logiques . . . . . . . 13deB à partir d’une preuve deA. Cette correspondance dite de Curry-Howard n’est
1.2 Variables et quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . 15pas juste une curiosité théorique. Elle est présente et mise en œuvre dans tous les
1.2.1 Principe et motivations . . . . . . . . . . . . . . . . . . . . . . 15langages fonctionnels typés de la famille ML comme OCaml ou Haskell. Utiliser au
1.2.2 Termes, formules atomiques, formules logiques . . . . . . . . . 17maximum cette correspondance est l’une des voies prometteuses que l’on explore pour
1.3 Substitution .... ............................. 20produire des logiciels prouvés soit en enrichissant les langages de la famille ML, soit
en extrayant directement des programmes à partir de preuves avec des logiciels d’aide 1.3.1 Portée d’un quantificateur, variables libres, variables liées . . . 20
à la construction de preuves comme CoQ. 1.3.2 Formules closes, clôture universelle . . . . . . . . . . . . . . . . 23
Enfin, les logiciels que l’on met en œuvre pour ou avec la logique sont relativement 1.3.3 Substitution dans une formule logique . . . . . . . . . . . . . . 23
différents des informatiques plus classiques sur les graphes ou les tableaux. 1.4 Exercices ....................... ........... 27
Ceci et les liens profonds entre logique et informatique que nous avons évoqués plus
haut rendent cet ouvrage indispensable pour compléter une culture générale en in- 2 Preuves formelles 33
formatique. Le livre «Logique pour l’informatique» que vous vous apprêtez à lire est 2.1 De la démonstration à la preuve . . . . . . . . . . . . . . . . . . . . . 33
donc bien un incontournable du domaine. 2.2 Emboîtements et règles de la déduction naturelle . . . . . . . . . . . . 37
2.2.1 Emboîtements de règles ...................... 37
Christophe RAFFALLI 2.2.2 Règles de la déduction naturelle de la logique intuitionniste . . 38
Ancien Maître de Conférences 2.3 Preuves et formules prouvables . . . . . . . . . . . . . . . . . . . . . . 44
Capitaine d’Ou La La
2.3.1 Définitions ............................. 44
2.3.2 Exemple d’élaboration d’une preuve . . . . . . . . . . . . . . . 46
2.3.3 Une autre présentation des preuves . . . . . . . . . . . . . . . . 47
2.4 Logique classique ................ .............. 50
2.5 Règles dérivées, passage au contexte . . . . . . . . . . . . . . . . . . . 52
2.5.1 Introduction de nouvelles règles de raisonnement . . . . . . . . 53
2.5.2 Quelques règles dérivées de la logique intuitionniste . . . . . . 55
2.5.3 Quelques règles dérivées de la logique classique . . . . . . . . . 60
2.5.4 Passage au contexte .................. ...... 63
2.6 Exercices ....................... ........... 64Table des matières
Introduction 1
1 Langages logiques 5
1.1 Constantes, fonctions, prédicats et connecteurs . . . . . . . . . . . . . 6
1.1.1 Principes ......................... ..... 7
1.1.2 Langage de termes .................... 8
1.1.3 Formules atomiques, connecteurs, formules logiques . . . . . . . 13
1.2 Variables et quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.1 Principe et motivations . . . . . . . . . . . . . . . . . . . . . . 15
1.2.2 Termes, formules atomiques, formules logiques . . . . . . . . . 17
1.3 Substitution .... ............................. 20
1.3.1 Portée d’un quantificateur, variables libres, variables liées . . . 20
1.3.2 Formules closes, clôture universelle . . . . . . . . . . . . . . . . 23
1.3.3 Substitution dans une formule logique . . . . . . . . . . . . . . 23
1.4 Exercices ....................... ........... 27
2 Preuves formelles 33
2.1 De la démonstration à la preuve . . . . . . . . . . . . . . . . . . . . . 33
2.2 Emboîtements et règles de la déduction naturelle . . . . . . . . . . . . 37
2.2.1 Emboîtements de règles ...................... 37
2.2.2 Règles de la déduction naturelle de la logique intuitionniste . . 38
2.3 Preuves et formules prouvables . . . . . . . . . . . . . . . . . . . . . . 44
2.3.1 Définitions ............................. 44
2.3.2 Exemple d’élaboration d’une preuve . . . . . . . . . . . . . . . 46
2.3.3 Une autre présentation des preuves . . . . . . . . . . . . . . . . 47
2.4 Logique classique ................ .............. 50
2.5 Règles dérivées, passage au contexte . . . . . . . . . . . . . . . . . . . 52
2.5.1 Introduction de nouvelles règles de raisonnement . . . . . . . . 53
2.5.2 Quelques règles dérivées de la logique intuitionniste . . . . . . 55
2.5.3 règles dérivées de la classique . . . . . . . . . 60
2.5.4 Passage au contexte .................. ...... 63
2.6 Exercices ....................... ........... 64iv Table des matières Table des matières v
3 Interprétation : fonctions, prédicats et connecteurs 69 7 Le fragment propositionnel 143
3.1 Structures .................. ................ 70 7.1 Restriction du langage .... ....................... 145
7.1.1 Syntaxe .............. ................. 1453.1.1 Principe ............... 70
7.1.2 Sémantique .................. ........... 1463.1.2 Définition formelle ......... 71
7.1.3 Interprétation et fonctions booléennes . . . . . . . . . . . . . . 1473.2 Interprétation des formules logiques . . . . . . . . . . . . . . . . . . . 71
7.2 Représentation des fonctions booléennes . . . . . . . . . . . . . . . . . 1493.2.1 Interprétation des termes . . . . . . . . . . . . . . . . . . . . . 72
7.2.1 Tables de vérité ......................... .. 1493.2.2 Inter des formules atomiques . . . . . . . . . . . . . . 72
7.2.2 Diagrammes de décision . . . . . . . . . . . . . . . . . . . . . . 1523.2.3 Interprétation des formules par des expressions booléennes . . . 73
7.3 Satisfiabilité, décidabilité, complexité . . . . . . . . . . . . . . . . . . . 1583.2.4 Évaluation des expressions booléennes . . . . . . . . . . . . . . 74
7.3.1 Des formules aux tables ...................... 1583.2.5 Formules équivalentes ....... ................ 78
7.3.2 Décidabilité, complexité . . . . . . . . . . . . . . . . . . . . . . 1593.3 Formules satisfiables, formules valides . . . . . . . . . . . . . . . . . . 79
7.4 Formes normales conjonctives et disjonctives . . . . . . . . . . . . . . 1613.3.1 Modèles, satisfiabilité, validité. . . . . . . . . . . . . . . . . . . 79
7.4.1 Littéraux, clauses et formes normales. . . . . . . . . . . . . . . 1613.3.2 Conséquence sémantique . . . . . . . . . . . . . . . . . . . . . . 80
7.4.2 Construction de formes normales par réécriture . . . . . . . . . 1623.4 Exercices ...................... ............ 82
7.4.3 Satisfiabilité d’une forme normale disjonctive . . . . . . . . . . 164
7.5 Clauses de Horn ...................... ........ 1654 Variables et quantificateurs 89
7.5.1 Modèle minimal d’un ensemble de clauses de Horn . . . . . . . 1654.1 Règles de déduction .... ........................ 89
7.5.2 Construction du modèle minimal par point fixe . . . . . . . . . 1674.1.1 Règle d’introduction du quantificateur universel : I ...... 89∀
7.5.3 Algorithme de décision pour les clauses de Horn . . . . . . . . 1704.1.2 Règle d’élimination du quantificateur universel : E 90∀
4.1.3 Règle d’introduction du quantificateur existentiel : I ..... 91∃
8 Résolution, unification 173
4.1.4 Règle d’élimination du quantificateurtiel : E ...... 91∃
8.1 Résolution ........... ....................... 173
4.1.5 Présentation arborescente des règles . . . . . . . . . . . . . . . 93
8.1.1 Résolution propositionnelle . . . . . . . . . . . . . . . . . . . . 174
4.2 Interprétation : variables et quantificateurs . . . . . . . . . . . . . . . 94
8.1.2 Résolution en logique des prédicats . . . . . . . . . . . . . . . . 180
4.2.1 Valuations, termes et formules atomiques . . . . . . . . . . . . 94
8.2 Programmation logique .......................... 183
4.2.2 Interprétation des formules logiques . . . . . . . . . . . . . . . 96
8.2.1 Résolution et programmation logique . . . . . . . . . . . . . . . 183
4.2.3 Formules satisfiables, formules valides . . . . . . . . . . . . . . 101
8.2.2 Langage de programmation Prolog . . . . . . . . . . . . . . . . 187
4.3 Exercices ...................... ............ 105
8.3 Unification .... ............................. 190
5 Correction et complétude 113 9 La correspondance preuves-programmes 199
5.1 Correction ....... ........................... 114 9.1 Logique minimale ............ .................. 200
5.2 Complétude ...... 117 9.1.1 Types et programmes ..... .................. 200
5.2.1 Principe de la démonstration . . . . . . . . . . . . . . . . . . . 117 9.1.2 Typage et preuve ........ .................. 204
5.2.2 Ensembles cohérents, ensembles complets . . . . . . . . . . . . 118 9.2 Conjonctions et disjonctions . . . . . . . . . . . . . . . . . . . . . . . . 207
5.2.3 Témoins de Henkin ......................... 120 9.2.1 Type produit et conjonction . . . . . . . . . . . . . . . . . . . . 207
5.2.4 Démonstration du théorème de complétude . . . . . . . . . . . 124 9.2.2 Type somme et disjonction . . . . . . . . . . . . . . . . . . . . 209
9.3 Élimination des coupures ........ ................. 213
6 Calculabilité et décidabilité 129
9.3.1 Exécution des programmes . . . . . . . . . . . . . . . . . . . . 213
6.1 Modèles de calculabilité .......................... 129 9.3.2 Élimination des coupures et exécution des programmes . . . . . 214
6.2 Indécidabilité de l’arrêt des machines à registres . . . . . . . . . . . . 133
6.2.1 Formulation du problème . . . . . . . . . . . . . . . . . . . . . 133 10 Bases de données 219
6.2.2 Démonstration ........................... 136 10.1 Les bases de données relationnelles . . . . . . . . . . . . . . . . . . . . 219
6.3 Indécidabilité de la logique des prédicats . . . . . . . . . . . . . . . . . 137 10.2 Syntaxe et sémantique associées . . . . . . . . . . . . . . . . . . . . . . 222
6.3.1 Principe de la réduction . . . . . . . . . . . . . . . . . . . . . . 137 10.2.1 Syntaxe ............. .................. 222
6.3.2 Construction de la formule F .............. ..... 138 10.2.2 Sémantique ................. ............ 224p
6.3.3 Adéquation de F ................ ......... 139 10.3 Interprétation logique des opérateurs relationels et des requêtes . . . . 225p
6.3.4 Démonstration de l’indécidabilité de la logique des prédicats . . 141 10.3.1 Principe ................ ............... 225Table des matières v
7 Le fragment propositionnel 143
7.1 Restriction du langage .... ....................... 145
7.1.1 Syntaxe .............. ................. 145
7.1.2 Sémantique .................. ........... 146
7.1.3 Interprétation et fonctions booléennes . . . . . . . . . . . . . . 147
7.2 Représentation des fonctions booléennes . . . . . . . . . . . . . . . . . 149
7.2.1 Tables de vérité ......................... .. 149
7.2.2 Diagrammes de décision . . . . . . . . . . . . . . . . . . . . . . 152
7.3 Satisfiabilité, décidabilité, complexité . . . . . . . . . . . . . . . . . . . 158
7.3.1 Des formules aux tables ...................... 158
7.3.2 Décidabilité, complexité . . . . . . . . . . . . . . . . . . . . . . 159
7.4 Formes normales conjonctives et disjonctives . . . . . . . . . . . . . . 161
7.4.1 Littéraux, clauses et formes normales. . . . . . . . . . . . . . . 161
7.4.2 Construction de formes normales par réécriture . . . . . . . . . 162
7.4.3 Satisfiabilité d’une forme normale disjonctive . . . . . . . . . . 164
7.5 Clauses de Horn ...................... ........ 165
7.5.1 Modèle minimal d’un ensemble de clauses de Horn . . . . . . . 165
7.5.2 Construction du modèle minimal par point fixe . . . . . . . . . 167
7.5.3 Algorithme de décision pour les clauses de Horn . . . . . . . . 170
8 Résolution, unification 173
8.1 Résolution ........... ....................... 173
8.1.1 Résolution propositionnelle . . . . . . . . . . . . . . . . . . . . 174
8.1.2 en logique des prédicats . . . . . . . . . . . . . . . . 180
8.2 Programmation logique .......................... 183
8.2.1 Résolution et programmation logique . . . . . . . . . . . . . . . 183
8.2.2 Langage de Prolog . . . . . . . . . . . . . . . . 187
8.3 Unification .... ............................. 190
9 La correspondance preuves-programmes 199
9.1 Logique minimale ............ .................. 200
9.1.1 Types et programmes ..... 200
9.1.2 Typage et preuve ........ 204
9.2 Conjonctions et disjonctions . . . . . . . . . . . . . . . . . . . . . . . . 207
9.2.1 Type produit et conjonction . . . . . . . . . . . . . . . . . . . . 207
9.2.2 Type somme et disjonction . . . . . . . . . . . . . . . . . . . . 209
9.3 Élimination des coupures ........ ................. 213
9.3.1 Exécution des programmes . . . . . . . . . . . . . . . . . . . . 213
9.3.2 Élimination des coupures et exécution des programmes . . . . . 214
10 Bases de données 219
10.1 Les bases de données relationnelles . . . . . . . . . . . . . . . . . . . . 219
10.2 Syntaxe et sémantique associées . . . . . . . . . . . . . . . . . . . . . . 222
10.2.1 Syntaxe ............. .................. 222
10.2.2 Sémantique ................. ............ 224
10.3 Interprétation logique des opérateurs relationels et des requêtes . . . . 225
10.3.1 Principe ................ ............... 225vi Table des matières
10.3.2 Identité (requête atomique) . . . . . . . . . . . . . . . . . . . . 226
10.3.3 Sélection ..... ......................... 227
10.3.4 Projection 229
10.3.5 Produit et jointure 231
10.3.6 Opérateurs ensemblistes . . . . . . . . . . . . . . . . . . . . . . 234
10.3.7 Opérateur de division ............. .......... 235
11 Model checking et logiques temporelles 239 Introduction
11.1 Model checking .............. ................. 240
11.1.1 Modèle d’un système ........ ................ 240
11.1.2 Model checking et logique des prédicats du premier ordre . . . 242
11.2 Logiques temporelles ............ 245
11.2.1 Computational Tree Logic (CTL) ............. .... 246
11.2.2 Linear Temporal Logic (LTL) .... ............... 248 Depuis son antique origine chez Aristote, la logique cherche à déterminer les lois
11.2.3 CTL et LTL : pouvoir d’expression incomparable . . . . . . . . 249 générales du raisonnement. Pour mener à bien cette entreprise, elle considère deux
Pour conclure .. .............................. ... 249
aspects du langage par quoi le raisonnement est exprimé :
— quels sont les énoncés dont on peut dire qu’ils sont «vrais» ou qu’ils sont
A Solution des exercices 253
«faux»?A.1 Langages logiques ................. ............. 253
— quels sont les enchaînements de tels énoncés dont on peut affirmer que la véritéA.2 Règles de déduction : connecteurs . . . . . . . . . . . . . . . . . . . . . 261
des uns a pour conséquence la vérité des autres?A.3 Interprétation : fonctions, prédicats et connecteurs . . . . . . . . . . . 276
Au fur et à mesure de son développement, la logique s’est rapprochée des méthodesA.4 Variables et quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . 291
des mathématiques. Dans cette intention, le philosophe et mathématicien G. W.
LeibeBibliographie 325 niz a tenté, au XVII siècle, de définir une langue formelle (la lingua caracteristica)
dans laquelle on énonce les problèmes à trancher et de lui adjoindre une procédure
Index 329
de calcul (le calculus ratiocinator) permettant de trancher effectivement la question.
eAu XIX siècle, G. Boole [Boo92] donna une tournure mathématique à ce projet de
calcul logique en exhibant comment l’on pouvait réduire certains de ses aspects à
un simple calcul sur un domaine à deux valeurs ({«vrai», «faux»}; {0, 1}) que l’on
appelle depuis valeurs booléennes. Poursuivant cet effort de «mathématisation» de la
e elogique, G. Frege [Fre99] donna, au tournant des XIX et XX siècles, une nouvelle
analyse des énoncés élémentaires que considère la logique basée sur les notions de
«variable» et de «fonction» tels que l’usage s’en était développé en mathématique.
Il développa une langue logique purement formelle : l’idéographie (Begriffsschrift).
Avec G. Frege, les énoncés sont devenus des formules. Reste une dernière étape à
franchir, un formalisme purement symbolique pour l’écriture des démonstrations. Les
premières tentatives en ce sens s’inspiraient de la méthode axiomatique (un ensemble
fini de schémas de formules admises comme «vraies») complétée par des règles de
déduction. G. Gentzen [Gen55] paracheva en quelque sorte l’entreprise en élaborant
un système de preuve où tout est règle de déduction. La langue logique étant devenue
parfaitement abstraite, ses formules n’y ont aucun sens par elles-mêmes. Leur
sémantique doit être apportée par un élément externe : un domaine d’interprétation pour
les symboles de variable et les relations que peuvent entretenir entre eux les éléments
de ce domaine. Les formules, une fois interprétées, ont une valeur de vérité. Cette
notion fut assez longtemps utilisée intuitivement jusqu’à ce que A. Tarski [Tar72] la
précise plus formellement.
La «logique» que nous présentons et étudions dans ce livre est l’héritière de ces
travaux. C’est la logique des prédicats du premier ordre.Introduction
Depuis son antique origine chez Aristote, la logique cherche à déterminer les lois
générales du raisonnement. Pour mener à bien cette entreprise, elle considère deux
aspects du langage par quoi le raisonnement est exprimé :
— quels sont les énoncés dont on peut dire qu’ils sont «vrais» ou qu’ils sont
«faux»?
— quels sont les enchaînements de tels énoncés dont on peut affirmer que la vérité
des uns a pour conséquence la vérité des autres?
Au fur et à mesure de son développement, la logique s’est rapprochée des méthodes
des mathématiques. Dans cette intention, le philosophe et mathématicien G. W.
Leibeniz a tenté, au XVII siècle, de définir une langue formelle (la lingua caracteristica)
dans laquelle on énonce les problèmes à trancher et de lui adjoindre une procédure
de calcul (le calculus ratiocinator) permettant de trancher effectivement la question.
eAu XIX siècle, G. Boole [Boo92] donna une tournure mathématique à ce projet de
calcul logique en exhibant comment l’on pouvait réduire certains de ses aspects à
un simple calcul sur un domaine à deux valeurs ({«vrai», «faux»}; {0, 1}) que l’on
appelle depuis valeurs booléennes. Poursuivant cet effort de «mathématisation» de la
e elogique, G. Frege [Fre99] donna, au tournant des XIX et XX siècles, une nouvelle
analyse des énoncés élémentaires que considère la logique basée sur les notions de
«variable» et de «fonction» tels que l’usage s’en était développé en mathématique.
Il développa une langue logique purement formelle : l’idéographie (Begriffsschrift).
Avec G. Frege, les énoncés sont devenus des formules. Reste une dernière étape à
franchir, un formalisme purement symbolique pour l’écriture des démonstrations. Les
premières tentatives en ce sens s’inspiraient de la méthode axiomatique (un ensemble
fini de schémas de formules admises comme «vraies») complétée par des règles de
déduction. G. Gentzen [Gen55] paracheva en quelque sorte l’entreprise en élaborant
un système de preuve où tout est règle de déduction. La langue logique étant devenue
parfaitement abstraite, ses formules n’y ont aucun sens par elles-mêmes. Leur
sémantique doit être apportée par un élément externe : un domaine d’interprétation pour
les symboles de variable et les relations que peuvent entretenir entre eux les éléments
de ce domaine. Les formules, une fois interprétées, ont une valeur de vérité. Cette
notion fut assez longtemps utilisée intuitivement jusqu’à ce que A. Tarski [Tar72] la
précise plus formellement.
La «logique» que nous présentons et étudions dans ce livre est l’héritière de ces
travaux. C’est la logique des prédicats du premier ordre.2 Introduction Introduction 3
Les quatre premiers chapitres de ce livre donnent la définition de cette logique sous Le chapitre 5 se conclut en situant ces résultats dans les enjeux de l’histoire de la
ses trois aspects : le langage des formules, le système de preuve et l’interprétation logique.
des formules. La matière de ces chapitres est issue d’un cours de logique dispensé Le chapitre 6 présente un autre résultat concernant la logique des prédicats du
à des étudiants de licence d’informatique. Chacun d’eux se termine par un ensemble premier ordre : son indécidabilité. Pour énoncer et démontrer ce résultat, nous
introd’exercices dont les solutions sont données en annexe à la fin de cet ouvrage. Le niveau duisons en première partie de ce chapitre une notion formelle de calculabilité qui est
d’exposition de ces quatre premiers chapitres mais aussi des suivants reste adapté à nécessaire pour énoncer ce qu’est un problème de décidabilité. Dans cette première
ce public et ne réclame aucun prérequis. partie, nous démontrons qu’un problème propre à la théorie de la calculabilté est
indécidable : le problème dit «de l’arrêt». Dans une seconde partie de ce chapitre, nous enLe premier chapitre est consacré à la présentation du langage de la logique des
déduisons l’indécidabilité de la logique des prédicats. Les démonstrations contenuesprédicats du premier ordre. C’est essentiellement celui défini par G. Frege.
Techniquedans ce chapitre sont bien moins «fouillées» que celles du chapitre précédent,
essenment, l’ensemble des formules, c-à-d l’ensemble des suites de caractères considérées
tiellement parce que leur développement aurait nécessité beaucoup trop de place dans
comme des formules, y est défini par un ensemble de règles d’assemblage syntaxique
ce livre. Nous espérons toutefois avoir pu y être suffisamment simples et convaincants.
de symboles : symboles de variable, constante et fonction, symboles de prédicat,
symboles des connecteurs et quantificateurs logiques. Nous terminons ce chapitre par la
La formalisation de la logique ouvre la possibilité de sa mise en œuvre par desdéfinition d’une opération de transformation purement syntaxique des formules : la
moyens informatiques. Les cinq derniers chapitres se tournent vers quelques uns desubstitution.
ces aspects.
Le deuxième chapitre est consacré au système de preuve de la déduction naturelle
restreint aux formules sans variable de la logique des prédicats (le «fragment proposi- Le chapitre 7 s’attache à la question de la recherche des conditions de vérité
tionnel» du langage). Nous faisons dans ce chapitre un sort particulier au «raisonne- d’une formule du fragment propositionnel de la logique. Cette question est connue
ment par l’absurde» dont l’usage ou non distingue une logique dite «classique» d’une sous le nom de problème de la satisfiabilité des formules propositionnelles. Nous y
logique dite «intuitionniste». donnons une définition plus précise de ce «fragment», sa syntaxe et sa sémantique.
Le troisième chapitre est consacré, toujours sur le fragment propositionnel, à la dé- Nous étudions comment sa sémantique entretient un rapport étroit avec les fonctions
finitiondel’interprétationsémantique(la«signification»)descomposantssyntaxiques booléennes. Enfin, nous isolons quelques formes particulières de formules
propositiondes formules : les symboles de constante et de fonction sont projetés sur des objets nelles qui jouent un rôle important tant du point de vue théorique que pratique : les
d’une «structure»; les symboles de prédicat sur les propriétés de ces objets ou leurs formes normales disjonctives et conjonctives, ainsi que les clauses de Horn.
relations; les symboles logiques sur des fonctions booléennes. Sur cette base, on sait Le chapitre 8 est consacré à une méthode de preuve alternative à la déduction
donner un sens à l’expression «formule vraie» ou à une déduction correcte appelée naturelle qui a donné lieu à d’importantes applications en informatique. Il s’agit de
conséquence sémantique. la méthode de preuve par résolution. Parmi ces importantes applications figure celle
Le quatrième chapitre ajoute aux deux précédents l’usage des symboles de va- de programmation logique. Les réalisations concrètes de la méthode de résolution
reriable et des symboles de quantification au système de la déduction naturelle et à la posentsurunalgorithmeimportant: l’unification.Nousdonnonsuneversionabstraite
sémantique des formules. de cet algorithme dans la dernière section de ce chapitre.
Le chapitre 9 présente une très brève et intuitive introduction à un développement
remarquable de la théorie des preuves en déduction naturelle : la correspondance entreÀ l’issue de ces quatre premiers chapitres, la logique est devenue un objet
parfaitepreuves et programmes (plus formellement, entre preuves et fonctions calculables).mentcernédontonpeutétudierlespropriétés.Lesdeuxchapitressuivantss’attachent
Le chapitre 10 illustre comment, dans le domaine concret des bases de données, laà deux d’entre elles.
logique des prédicats du premier ordre, sa syntaxe et sa sémantique sont au fondementLe chapitre 5 contient les démonstrations de deux résultats mettant en relation
delaconceptiondeslangagesderequêtespermettantd’exploiterlesdonnéesrecueilliespreuves en déduction naturelle et conséquence sémantique. Il s’agit :
dans une base.— du théorème de correction qui établit que les déductions prouvables en
déducEnfin le chapitre 11 présente une réalisation des méthodes formelles de vérificationtion naturelle sont sémantiquement fondées;
de systèmes informatiques basée sur les concepts élaborés en logique formelle : la— du théorème de complétude, réciproque de la correction, qui établit que toutes
vérification de modèle (model checking).les déductions sémantiquement fondées sont prouvables en déduction naturelle.
Nous avons tenté de rendre les preuves de ces théorèmes aussi abordables que possible
pour un lecteur qui n’aurait de connaissance du domaine que le contenu des quatre
premiers chapitres de ce livre. La démonstration du théorème de correction, quoiqu’un
peu fastidieuse, ne requiert rien d’autre que ce qui a été dit dans cet ouvrage. La
démonstration du théorème de complétude, plus sophistiquée, fait appel à quelques
notions externes à la logique que nous présentons aussi succinctement que possible.Introduction 3
Le chapitre 5 se conclut en situant ces résultats dans les enjeux de l’histoire de la
logique.
Le chapitre 6 présente un autre résultat concernant la logique des prédicats du
premier ordre : son indécidabilité. Pour énoncer et démontrer ce résultat, nous
introduisons en première partie de ce chapitre une notion formelle de calculabilité qui est
nécessaire pour énoncer ce qu’est un problème de décidabilité. Dans cette première
partie, nous démontrons qu’un problème propre à la théorie de la calculabilté est
indécidable : le problème dit «de l’arrêt». Dans une seconde partie de ce chapitre, nous en
déduisons l’indécidabilité de la logique des prédicats. Les démonstrations contenues
dans ce chapitre sont bien moins «fouillées» que celles du chapitre précédent,
essentiellement parce que leur développement aurait nécessité beaucoup trop de place dans
ce livre. Nous espérons toutefois avoir pu y être suffisamment simples et convaincants.
La formalisation de la logique ouvre la possibilité de sa mise en œuvre par des
moyens informatiques. Les cinq derniers chapitres se tournent vers quelques uns de
ces aspects.
Le chapitre 7 s’attache à la question de la recherche des conditions de vérité
d’une formule du fragment propositionnel de la logique. Cette question est connue
sous le nom de problème de la satisfiabilité des formules propositionnelles. Nous y
donnons une définition plus précise de ce «fragment», sa syntaxe et sa sémantique.
Nous étudions comment sa sémantique entretient un rapport étroit avec les fonctions
booléennes. Enfin, nous isolons quelques formes particulières de formules
propositionnelles qui jouent un rôle important tant du point de vue théorique que pratique : les
formes normales disjonctives et conjonctives, ainsi que les clauses de Horn.
Le chapitre 8 est consacré à une méthode de preuve alternative à la déduction
naturelle qui a donné lieu à d’importantes applications en informatique. Il s’agit de
la méthode de preuve par résolution. Parmi ces importantes applications figure celle
de programmation logique. Les réalisations concrètes de la méthode de résolution
reposentsurunalgorithmeimportant: l’unification.Nousdonnonsuneversionabstraite
de cet algorithme dans la dernière section de ce chapitre.
Le chapitre 9 présente une très brève et intuitive introduction à un développement
remarquable de la théorie des preuves en déduction naturelle : la correspondance entre
preuves et programmes (plus formellement, entre preuves et fonctions calculables).
Le chapitre 10 illustre comment, dans le domaine concret des bases de données, la
logique des prédicats du premier ordre, sa syntaxe et sa sémantique sont au fondement
delaconceptiondeslangagesderequêtespermettantd’exploiterlesdonnéesrecueillies
dans une base.
Enfin le chapitre 11 présente une réalisation des méthodes formelles de vérification
de systèmes informatiques basée sur les concepts élaborés en logique formelle : la
vérification de modèle (model checking).CHAPITRE1
Langages logiques
La logique fournit un langage permettant d’écrire des assertions qui peuvent être
« vraies » ou « fausses ». Les « phrases » de ce langage sont les formules logiques.
Elles expriment des propriétés sur des objets d’un certain «univers du discours». Par
exemple, les trois énoncés :
« Socrate suit en cours de logique » (1.1)
« Socrate lit ses messages sur son smartphone » (1.2)
« Socrate comprend la logique » (1.3)
portent sur l’objet Socrate (les individus sont ici des objets) et spécifient trois
propriétés qui peuvent être satisfaites, ou non, par Socrate. Ces propriétés sont a priori
indépendantes : par exemple Socrate peut très bien suivre un cours de logique sans
lire ses messages sur son smartphone, tout comme il peut comprendre la logique en
lisant ses messages sur son smartphone. Toutes les situations sont ici envisageables.
Dans la mesure où la valeur de vérité de chacun de ces trois énoncés est indépendante
des lois de la logique, on pose qu’ils constituent des formules atomiques du langage.
Pour éliminer certaines situations, et donc pour introduire une certaine
dépendance entre les valeurs de vérité de formules logiques, on les combine avec des
connecteurs logiques. Les combinaisons logiques sont basées sur les conjonctions de
coordination « et », « ou », de subordination « si alors » ou simplement la négation. Par
exemple, la phrase :
« Si Socrate ne lit pas ses messages sur son smartphone
et qu’il suit un cours de logique, (1.4)
alors il comprend la logique. »
est une combinaison des trois formules atomiques (1.1), (1.2) et (1.3). C’est à son tour
une formule et elle n’est pas atomique : sa valeur de vérité dépend non seulement de
celle des formules atomiques qui la composent mais aussi du sens que l’on donne aux
connecteurs qui relient ces formules. Par exemple, s’il s’avère que Socrate ne lit pas
ses messages sur son smartphone et qu’il suit un de cours de logique mais qu’il ne
comprend pas la logique, la formule (1.4) a la valeur de vérité « faux ». Toutefois si
Socrate ne lit pas ses messages sur son smartphone, ne suit pas de cours de logique
et comprend tout de même la logique, la formule (1.4) a la valeur de vérité « vrai ».
Certains énoncés ne portent pas sur un individu particulier (que l’on a désigné ici
par son nom : Socrate), mais sur un ou des individu(s) indéterminé(s).CHAPITRE1
Langages logiques
La logique fournit un langage permettant d’écrire des assertions qui peuvent être
« vraies » ou « fausses ». Les « phrases » de ce langage sont les formules logiques.
Elles expriment des propriétés sur des objets d’un certain «univers du discours». Par
exemple, les trois énoncés :
« Socrate suit en cours de logique » (1.1)
« Socrate lit ses messages sur son smartphone » (1.2)
« Socrate comprend la logique » (1.3)
portent sur l’objet Socrate (les individus sont ici des objets) et spécifient trois
propriétés qui peuvent être satisfaites, ou non, par Socrate. Ces propriétés sont a priori
indépendantes : par exemple Socrate peut très bien suivre un cours de logique sans
lire ses messages sur son smartphone, tout comme il peut comprendre la logique en
lisant ses sur son smartphone. Toutes les situations sont ici envisageables.
Dans la mesure où la valeur de vérité de chacun de ces trois énoncés est indépendante
des lois de la logique, on pose qu’ils constituent des formules atomiques du langage.
Pour éliminer certaines situations, et donc pour introduire une certaine
dépendance entre les valeurs de vérité de formules logiques, on les combine avec des
connecteurs logiques. Les combinaisons logiques sont basées sur les conjonctions de
coordination « et », « ou », de subordination « si alors » ou simplement la négation. Par
exemple, la phrase :
« Si Socrate ne lit pas ses messages sur son smartphone
et qu’il suit un cours de logique, (1.4)
alors il comprend la logique. »
est une combinaison des trois formules atomiques (1.1), (1.2) et (1.3). C’est à son tour
une formule et elle n’est pas atomique : sa valeur de vérité dépend non seulement de
celle des formules atomiques qui la composent mais aussi du sens que l’on donne aux
connecteurs qui relient ces formules. Par exemple, s’il s’avère que Socrate ne lit pas
ses messages sur son smartphone et qu’il suit un de cours de logique mais qu’il ne
comprend pas la logique, la formule (1.4) a la valeur de vérité « faux ». Toutefois si
Socrate ne lit pas ses messages sur son smartphone, ne suit pas de cours de logique
et comprend tout de même la logique, la formule (1.4) a la valeur de vérité « vrai ».
Certains énoncés ne portent pas sur un individu particulier (que l’on a désigné ici
par son nom : Socrate), mais sur un ou des individu(s) indéterminé(s).6 Chapitre 1. Langages logiques 1.1. Constantes, fonctions, prédicats et connecteurs 7
Par exemple, en français, on dirait : 1.1.1 Principes
« Si on ne lit pas ses messages sur son smartphone On distingue traditionnellement deux niveaux du langage logique sans variable :
et que l’on suit un cours de logique, (1.5) la logique des propositions et la logique des prédicats.
alors on comprend la logique. »
Logique des propositions La logique des propositions fournit un langage très rudi-L’indétermination est marquée ici par l’emploi du pronom indéfini «on». En logique,
comme en algèbre, on a recours à l’emploi d’un ensemble de symboles particuliers pour mentaire dans lequel chaque énoncé atomique est représenté par un symbole
apparmarquer l’indétermination : les symboles de variable. Par exemple, le symbole x : tenant à un ensemble notéP .0
Par exemple, en choisissant les symboles p , p et p pour représenter les énoncés1 2 3« Si x ne lit pas ses messages sur son smartphone
(1.1), (1.2) et (1.3), l’énoncé négatif « Socrate ne lit pas ses messages sur son
smartet x suit un cours de logique, (1.6)
phone » s’écrit comme la négation de p , c-à-d «non p ». On transcrit alors la phrase2 2alors x comprend la logique. »
(1.4) par la formule :
Enfin,onpeutquantifiercetteindéterminationenconstruisantdesénoncésquiportent « si p et non p alors p »1 2 3
sur tout ou partie (c-à-d au moins un) des objets de l’univers du discours :
Quoique que d’aspect assez pauvre, ce langage n’est pas sans contenir quelques
« Pour tout x, propriétés logiques fondamentales. Par exemple, on sait y déterminer que la formule
si x ne lit pas ses messages sur son smartphone « p et non p»est«fausse»quellequesoitlavaleurdevéritédelaformuleatomique p.(1.7)
et x suit un cours de logique, Ce langage sera étudié plus en détail dans le chapitre 7. En revanche, le langage de la
alors x comprend la logique. » logique des propositions interdit toute finesse pour les formules atomiques qui y sont
réduites à un seul symbole. Ainsi, la transcription de la phrase (1.4) par la formule «si
« Il existe x tel que
p et non p alors p » masque que c’est le même Socrate qui suit et comprend le cours1 2 3si x ne lit pas ses messages sur son smartphone
(1.8) de logique. Pour dégager cette dépendance, il faut décomposer l’énoncé «Socrate suit
et x suit un cours de logique,
un cours de logique » en un sujet (Socrate) et un prédicat (suit un cours de logique).
alors x comprend la logique. »
Le langage de la logique des prédicats utilisé dans toute la suite ajoute cette
Les locutions « pour tout » et « il existe » correspondent aux constructions logiques possibilité de structuration plus riche des énoncés atomiques.
appelées quantificateurs.
Il existe plusieurs langages logiques offrant un pouvoir d’expression plus ou moins Logique des prédicats Le langage de la logique des prédicats ajoute aux symboles
grand selon les constructions qu’ils permettent. Dans cet ouvrage, nous étudions le utilisés pour désigner les objets du discours (comme Socrate) des symboles utilisés
langage des formules logiques obtenues à partir de formules atomiques que l’on peut pour désigner ce que l’on en dit, les propriétés qu’on leur attribue. Ce que l’on désigne
combiner à l’aide de connecteurs propositionnels et moduler par les quantificateurs sous le terme générique de prédicat. Par exemple on dit de Socrate qu’il «suit un cours
« pour tout » et « il existe » portant sur des variables désignant des objets de l’uni- de logique».Pourcomposerobjets etprédicats,on«applique»un symbole de prédicat
vers du discours. Ce langage est celui de logique des prédicats du premier ordre. Dans au symbole de l’objet (comme on « applique » une fonction à son argument) :
notre présentation, nous distinguons le fragment de langage sans variable, qui
constisuit_un_cours_de_logique(Socrate)tue le fragment propositionnel du langage et le langage complet avec variables et
quantificateurs.
Dans le langage de la logique des prédicats, le terme de « prédicat » s’étend auxCe chapitre présente formellement les aspects syntaxiques de ces deux parties
«relations» qui relient entre eux des objets. Par exemple, si l’univers du discours estdu langage, successivement dans les sections 1.1 et 1.2, avant de décrire, dans la
celui des nombres, on pourra énoncer qu’un nombre est plus petit qu’un autre. Onsection 1.3, des outils de manipulation des variables utiles pour la suite. Dans les
choisit un symbole, disons le (pour less or equal), pour désigner la relation d’ordrechapitres suivants les deux principales approches permettant d’établir qu’une formule
sur les nombres, et on écrit que « 6 est inférieur à 3 » (indépendamment du souci deest « vraie » ou « fausse » sont introduites.
savoir si c’est « vrai » ou « faux ») comme l’application du symbole de prédicat aux
désignations symboliques des objets : le(6,3).
Ainsi,certainssymbolesdeprédicats’appliquentàunobjet,d’autresàdeuxobjets,1.1 Constantes, fonctions, prédicats et connecteurs
d’autres à trois, etc. Le nombre d’objets auxquels s’applique un symbole est appelé
Cette section présente le langage logique des prédicats du premier ordre sans son arité. On parle de prédicat unaire (arité 1), binaire (arité 2), etc.
variable:aprèsuneillustrationdesprincipesdanslasection1.1.1,ildécritleséléments Plus encore, le langage de la logique des prédicats permet de décomposer les objets
du langage, appelés termes, dans la section 1.1.2, puis les formules logiques qu’ils eux-mêmes. En effet, pour rester dans le domaine numérique, un nombre peut être le
permettent de construire dans la section 1.1.3. résultat d’une fonction appliquée à un, deux, etc. autres nombres. Par exemple, en1.1. Constantes, fonctions, prédicats et connecteurs 7
1.1.1 Principes
On distingue traditionnellement deux niveaux du langage logique sans variable :
la logique des propositions et la logique des prédicats.
Logique des propositions La logique des propositions fournit un langage très
rudimentaire dans lequel chaque énoncé atomique est représenté par un symbole
appartenant à un ensemble notéP .0
Par exemple, en choisissant les symboles p , p et p pour représenter les énoncés1 2 3
(1.1), (1.2) et (1.3), l’énoncé négatif « Socrate ne lit pas ses messages sur son
smartphone » s’écrit comme la négation de p , c-à-d «non p ». On transcrit alors la phrase2 2
(1.4) par la formule :
« si p et non p alors p »1 2 3
Quoique que d’aspect assez pauvre, ce langage n’est pas sans contenir quelques
propriétés logiques fondamentales. Par exemple, on sait y déterminer que la formule
« p et non p»est«fausse»quellequesoitlavaleurdevéritédelaformuleatomique p.
Ce langage sera étudié plus en détail dans le chapitre 7. En revanche, le langage de la
logique des propositions interdit toute finesse pour les formules atomiques qui y sont
réduites à un seul symbole. Ainsi, la transcription de la phrase (1.4) par la formule «si
p et non p alors p » masque que c’est le même Socrate qui suit et comprend le cours1 2 3
de logique. Pour dégager cette dépendance, il faut décomposer l’énoncé «Socrate suit
un cours de logique » en un sujet (Socrate) et un prédicat (suit un cours de logique).
Le langage de la logique des prédicats utilisé dans toute la suite ajoute cette
possibilité de structuration plus riche des énoncés atomiques.
Logique des prédicats Le langage de la logique des prédicats ajoute aux symboles
utilisés pour désigner les objets du discours (comme Socrate) des symboles utilisés
pour désigner ce que l’on en dit, les propriétés qu’on leur attribue. Ce que l’on désigne
sous le terme générique de prédicat. Par exemple on dit de Socrate qu’il «suit un cours
de logique».Pourcomposerobjets etprédicats,on«applique»un symbole de prédicat
au symbole de l’objet (comme on « applique » une fonction à son argument) :
suit_un_cours_de_logique(Socrate)
Dans le langage de la logique des prédicats, le terme de « prédicat » s’étend aux
«relations» qui relient entre eux des objets. Par exemple, si l’univers du discours est
celui des nombres, on pourra énoncer qu’un nombre est plus petit qu’un autre. On
choisit un symbole, disons le (pour less or equal), pour désigner la relation d’ordre
sur les nombres, et on écrit que « 6 est inférieur à 3 » (indépendamment du souci de
savoir si c’est « vrai » ou « faux ») comme l’application du symbole de prédicat aux
désignations symboliques des objets : le(6,3).
Ainsi,certainssymbolesdeprédicats’appliquentàunobjet,d’autresàdeuxobjets,
d’autres à trois, etc. Le nombre d’objets auxquels s’applique un symbole est appelé
son arité. On parle de prédicat unaire (arité 1), binaire (arité 2), etc.
Plus encore, le langage de la logique des prédicats permet de décomposer les objets
eux-mêmes. En effet, pour rester dans le domaine numérique, un nombre peut être le
résultat d’une fonction appliquée à un, deux, etc. autres nombres. Par exemple, en8 Chapitre 1. Langages logiques 1.1. Constantes, fonctions, prédicats et connecteurs 9
choisissant le symbole add pour désigner l’addition, l’application add(4,2) désigne le 2. Si f ∈F est un symbole de fonction d’arité n, et si t ,··· ,t sont des termes,n 1 n
nombre obtenu par somme de 4 et 2. On exprime la relation entre ce nombre et la alors f(t ,··· ,t ) est un terme.1 n
constante3aveclaformuleatomique le(add(4,2),3).Commelessymbolesdeprédicat,
Notez que pour former des termes, outre les symboles d’une signature, on utilise les
les symboles de fonction ont une arité.
deux parenthèses, ouvrante et fermante, ainsi que la virgule.
Les formules atomiques ainsi obtenues sont composables à l’aide des connecteurs
Exemple 1.1 Pour prendre un exemple simple de langage de termes, considérons lespropositionnels. Pour prendre un exemple issu de l’informatique, on considère le
taensembles F = {a,b}, F = {f} et F = {h} et posons F = F ∪F ∪F . Parmi lesbleau suivant : 0 1 2 0 1 2
2 5 6 9 termesde cet ensemble T (F) particulier ontrouve a, f(b), h(b,a), f(f(a)), f(h(a,b)),0
h(f(a),a), h(f(b),h(a,b)), etc.
On énonce que les éléments de ce tableau sont rangés par ordre croissant par la
formule : Si l’on veut pouvoir utiliser correctement les symboles d’une signature pour définir
le(2,5) et le(5,6) et le(6,9) un langage de termes, il faut faire deux hypothèses sur les ensembles F , F , etc.0 1
— La première est que F n’est pas vide : il existe au moins un symbole de0
Mais ici manque encore l’information que 2, 5, 6 et 9 sont les valeurs d’un certain
constante. Elle est d’une importance cruciale car elle garantit que l’ensemble
tableau.Pourprécisercelaonchoisitunsymboledefonctionbinaire posetl’ondésigne
de termes T (F) ainsi défini n’est pas vide, puisqu’il contient au moins les01le i-èmeélémentd’untableau tpar pos(t,i) .Sil’onappelle tabletableauquicontient
symboles de constante.
la suite 2,5,6,9, on énonce que ses éléments y sont rangés par ordre croissant avec la
— La seconde est que les ensembles F sont deux à deux disjoints : un mêmei
formule :
symbole ne peut pas avoir deux arités différentes. Cette hypothèse a pour but
d’éviter toute incertitude lors de l’analyse syntaxique des termes. En effet,
le(pos(tab,0),pos(tab,1)) et le(pos(tab,1),pos(tab,2)) et le(pos(tab,2),pos(tab,3))
comment dire que le terme a(a) est «bien formé» ou non, si a est à la fois un
symbole de constante et un symbole de fonction?Dans le paragraphe suivant nous présentons un schéma général de définition du
fragment du langage de la logique des prédicats destiné à désigner les objets de
l’universdudiscoursappelélangage des termes.Nousprésentonsensuiteunschémagénéral
de définition des formules atomiques et de leur combinaison à l’aide des connecteurs
Lesrèglesdeformationdestermespeuventêtreluescommedesrèglesdeconstrucpropositionnels. Le langage des formules défini dans ces deux paragraphes est un tion d’arbres dont les étiquettes sont les symboles deF. Selon l’arité des symboles, un
langage sans symbole de variable. L’usage des variables est l’objet du paragraphe 1.2. nœud de l’arbre a un, deux, etc. sous-arbres. Les feuilles de l’arbre sont les symboles
de constantes : d’arité 0, on ne leur attache pas de sous-arbre.
Par exemple, avec la signature de l’exemple 1.1 donné ci-dessus, le terme :1.1.2 Langage de termes
h(h(f(f(a)),f(f(f(b)))),f(a))Signature Les termes sont les expressions syntaxiques qui désignent les objets du
discours. Pour définir l’ensemble des termes on se donne un ensemble F de symboles peut être vu comme l’arbre :
de constante et de fonction, appelé une signature. Ainsi, dans les exemples précédents,
hon a utilisé les constantes Socrate, tab, 2, 3 et les fonctions add et pos.
fhL’ensembleF estconstruitcommel’uniondessymbolesdeconstante,dessymboles
de fonction d’arité 1, de fonction d’arité 2, etc. que l’on veut utiliser dans les formules. f f
aOn note F l’ensemble des symboles de constante (on considère les constantes comme0
f fdes fonctions d’arité 0) et, plus généralement,F l’ensemble des symboles de fonctionn
d’arité n. On pose :
a f
F =F ∪F ∪F ∪··· = F0 1 2 n
n≥0
b
Définition 1.1 (Ensemble T (F) de termes sans variable)0
La définition 1.1 donne les règles d’assemblage de symboles d’une signature, des
Étant donnée une signature F, l’ensemble T (F) des termes est défini inductivement0
parenthèses et de la virgule pour construire un ensemble de termes. Ces symboles
comme suit.
constituent le lexique du langage des termes. On peut lire la définition 1.1 comme une
1. Si k ∈F est un symbole de constante, alors k est un terme.0 grammaire définissant les écritures acceptables des termes. Dans ce cas, la
représentation arborescente d’un terme correspond à son arbre de syntaxe abstraite.1. Nous adoptons la convention usuelle en informatique selon laquelle la première position dans
un tableau est désignée par 0.1.1. Constantes, fonctions, prédicats et connecteurs 9
2. Si f ∈F est un symbole de fonction d’arité n, et si t ,··· ,t sont des termes,n 1 n
alors f(t ,··· ,t ) est un terme.1 n
Notez que pour former des termes, outre les symboles d’une signature, on utilise les
deux parenthèses, ouvrante et fermante, ainsi que la virgule.
Exemple 1.1 Pour prendre un exemple simple de langage de termes, considérons les
ensembles F = {a,b}, F = {f} et F = {h} et posons F = F ∪F ∪F . Parmi les0 1 2 0 1 2
termesde cet ensemble T (F) particulier ontrouve a, f(b), h(b,a), f(f(a)), f(h(a,b)),0
h(f(a),a), h(f(b),h(a,b)), etc.
Si l’on veut pouvoir utiliser correctement les symboles d’une signature pour définir
un langage de termes, il faut faire deux hypothèses sur les ensembles F , F , etc.0 1
— La première est que F n’est pas vide : il existe au moins un symbole de0
constante. Elle est d’une importance cruciale car elle garantit que l’ensemble
de termes T (F) ainsi défini n’est pas vide, puisqu’il contient au moins les0
symboles de constante.
— La seconde est que les ensembles F sont deux à deux disjoints : un mêmei
symbole ne peut pas avoir deux arités différentes. Cette hypothèse a pour but
d’éviter toute incertitude lors de l’analyse syntaxique des termes. En effet,
comment dire que le terme a(a) est «bien formé» ou non, si a est à la fois un
symbole de constante et un symbole de
fonction?

Lesrèglesdeformationdestermespeuventêtreluescommedesrèglesdeconstruction d’arbres dont les étiquettes sont les symboles deF. Selon l’arité des symboles, un
nœud de l’arbre a un, deux, etc. sous-arbres. Les feuilles de l’arbre sont les symboles
de constantes : d’arité 0, on ne leur attache pas de sous-arbre.
Par exemple, avec la signature de l’exemple 1.1 donné ci-dessus, le terme :
h(h(f(f(a)),f(f(f(b)))),f(a))
peut être vu comme l’arbre :
h
fh
f f
a
f f
a f
b
La définition 1.1 donne les règles d’assemblage de symboles d’une signature, des
parenthèses et de la virgule pour construire un ensemble de termes. Ces symboles
constituent le lexique du langage des termes. On peut lire la définition 1.1 comme une
grammaire définissant les écritures acceptables des termes. Dans ce cas, la
représentation arborescente d’un terme correspond à son arbre de syntaxe abstraite.10 Chapitre 1. Langages logiques 1.1. Constantes, fonctions, prédicats et connecteurs 11
Définition inductive, induction structurelle La définition 1.1 qui donne les règles En fait, les ensembles IN et T (F) sont ici isomorphes : à chaque entier n on peut0
de construction des termes indique que tout assemblage de symboles qui n’obéit pas associer un terme et réciproquement. Intuitivement, le passage de IN versT (F) s’ef-0
aux règles (symbole de fonction inconnu, arité non respectée, parenthèse mal fermée, fectue de la façon suivante : (i) à 0 on associe Z; (ii) si à n on associe t, alors, à
etc.) n’est pas un élément de cet ensemble. Il faut souligner que l’expression « défini n+1 on associe S(t). Réciproquement, le passage de T (F) vers IN est défini de la0
inductivement »indiqueaussiquetous les termes deT (F)sontobtenusenappliquant façon suivante : à Z on associe 0;à S(t), on associe n +1 où n est l’entier associé0
un nombre de fois fini les règles de construction données. à t. Formellement, on définit deux fonctions i2t : IN→T (F) et t2i :T (F)→ IN, la0 0
Ainsi, on peut parler de tous les termes en considérant simplement les cas où un première par récurrence sur les entiers et la seconde par induction sur la construction
terme est un symbole de constante k et les cas où il est obtenu par application d’un des termes :
symbole de fonction à d’autres termes f(t ,...,t ). Cette possibilité ouvre celle de1 n
i2t(0) = Z t2i(Z) =0poser sur l’ensemble des termes un schéma de raisonnement par induction
structui2t(n+1) = S(i2t(n)) t2i(S(t)) = t2i(t)+1relle qui permet de démontrer que tous les termes d’un ensemble T (F) vérifient une0
certaine propriété. Si P est une propriété portant sur les éléments de T (F),on a:0
Ces deux fonctions sont des bijections entre IN etT (F) et elles sont réciproques l’une0
si tout k ∈F vérifie P0 de l’autre : i2t(t2i(t)) = t et t2i(i2t(n)) = n.
et pour tout t ,··· ,t ∈T (F) et tout f ∈F ,1 n 0 n
supposer que t ,··· ,t vérifient P entraîne que f(t ,...,t ) vérifie P1 n 1 n Exemple 1.3 (Expressions arithmétiques sans variable)
alors tout t ∈T (F) vérifie P0 Pour définir sa théorie de l’arithmétique, Peano va un peu plus loin en ajoutant deux
(1.9) symboles de fonction d’arité 2 : l’un pour l’addition, l’autre pour la multiplication.
La notion d’induction structurelle est d’une importance primordiale dans le domaine Posons F = {add,mul} et F = F ∪F ∪F . L’ensemble T (F) des expressions2 0 1 2 0
de la logique mais également de l’informatique. Nous nous y réfèrerons et l’utiliserons désignant des entiers est maintenant défini par :
à de multiples reprises dans cet ouvrage.
— Z ∈T (F) (puisque Z ∈F )0 0
— si t∈T (F) alors S(t)∈T (F) (puisque S ∈F )0 0 1Exemple 1.2 (Entiers de Peano)
— si t ∈T (F) et t ∈T (F) alors add(t ,t ) ∈T (F) et mul(t ,t ) ∈T (F)1 0 2 0 1 2 0 1 2 0Le langage de la logique des prédicats a été mis au point entre la fin du XIXe et le
e (puisque add∈F et mul∈F ).2 2débutduXX siècledanslecadrederecherchessurlesfondementsdesmathématiques.
Ces expressions sont également représentables comme des structures d’arbre dont lesEn particulier G. Peano (1858-1932) s’intéressa auxts de l’arithmétique et
nœudsont2,1ouaucunfils.Parexemplel’expressionarithmétiqueusuelle2×3+1estposa la définition d’un langage de termes permettant de désigner tous les nombres
transcrite par le terme add(mul(S(S(Z)),S(S(S(Z)))),S(Z)) qui peut se représenterentiers positifs, que l’on appelle depuis les entiers de Peano.
par l’arbre :Pour cela, il se donna le symbole Z de constante pour désigner 0 et un symbole
de fonction unaire S pour désigner le successeur d’un entier (la fonction qui associe
n +1 à n). En posant F = F ∪F avec F = {Z} et F = {S}, l’ensemble des add0 1 0 1
entiers de Peano est défini comme une « particularisation » de la définition 1.1 de mul S
l’ensemble T (F) :0 S S
— Z ∈T (F) (puisque Z ∈F ) Z0 0
— si t ∈T (F) alors S(t) ∈T (F) (puisque S ∈F )0 0 1 S S
On s’est ainsi donné un moyen pour écrire les entiers 0, 1, 2, 3, etc. sous la forme Z,
S(Z), S(S(Z)), S(S(S(Z))), etc. Si cette écriture n’est pas utile en pratique, elle est Z S
suffisante en théorie.
Z
Induction structurelle et récurrence sur les entiers Avec la définition des entiers
2de Peano, le principe usuel de récurrence sur les entiers s’exprime comme le principe
Termes et calculs Dans le langage de termes de Peano, add(S(S(Z)),S(S(Z)))d’induction structurelle sur les termes de T (F). En effet, pour toute propriété P,0
est un terme qui désigne un entier, mais lequel? Si l’on sait que add représente la
si P(Z), fonction d’addition et que S(S(Z)) représente l’entier 2 alors on peut deviner que
et si pour tout t ∈T (F), P(t) entraîne P(S(t))0 add(S(S(Z)),S(S(Z))) représente l’entier 4 car on sait calculer 2 +2. Mais sait-on
alors, pour tout t ∈T (F), P(t)0 réellement calculer 2+2 ou avons nous simplement appris par cœur que « 2 et 2
égalent 4 »? Avec son langage de termes, G. Peano fournit un moyen de calculer2. En considérant une propriété P, la récurrence usuelle sur les entiers s’exprime de la façon
suivante : siP(0) et si pour tout entierm,P(m) entraîneP(m+1), alors pour tout entiern,P(n). effectivement la somme de deux entiers. Pour cela, il pose les égalités élémentaires1.1. Constantes, fonctions, prédicats et connecteurs 11
En fait, les ensembles IN et T (F) sont ici isomorphes : à chaque entier n on peut0
associer un terme et réciproquement. Intuitivement, le passage de IN versT (F) s’ef-0
fectue de la façon suivante : (i) à 0 on associe Z; (ii) si à n on associe t, alors, à
n+1 on associe S(t). Réciproquement, le passage de T (F) vers IN est défini de la0
façon suivante : à Z on associe 0;à S(t), on associe n +1 où n est l’entier associé
à t. Formellement, on définit deux fonctions i2t : IN→T (F) et t2i :T (F)→ IN, la0 0
première par récurrence sur les entiers et la seconde par induction sur la construction
des termes :

i2t(0) = Z t2i(Z) =0
i2t(n+1) = S(i2t(n)) t2i(S(t)) = t2i(t)+1
Ces deux fonctions sont des bijections entre IN etT (F) et elles sont réciproques l’une0
de l’autre : i2t(t2i(t)) = t et t2i(i2t(n)) = n.
Exemple 1.3 (Expressions arithmétiques sans variable)
Pour définir sa théorie de l’arithmétique, Peano va un peu plus loin en ajoutant deux
symboles de fonction d’arité 2 : l’un pour l’addition, l’autre pour la multiplication.
Posons F = {add,mul} et F = F ∪F ∪F . L’ensemble T (F) des expressions2 0 1 2 0
désignant des entiers est maintenant défini par :
— Z ∈T (F) (puisque Z ∈F )0 0
— si t∈T (F) alors S(t)∈T (F) (puisque S∈F )0 0 1
— si t ∈T (F) et t ∈T (F) alors add(t ,t ) ∈T (F) et mul(t ,t ) ∈T (F)1 0 2 0 1 2 0 1 2 0
(puisque add∈F et mul∈F ).2 2
Ces expressions sont également représentables comme des structures d’arbre dont les
nœudsont2,1ouaucunfils.Parexemplel’expressionarithmétiqueusuelle2×3+1est
transcrite par le terme add(mul(S(S(Z)),S(S(S(Z)))),S(Z)) qui peut se représenter
par l’arbre :
add
mul S
S S
Z
S S
Z S
Z
Termes et calculs Dans le langage de termes de Peano, add(S(S(Z)),S(S(Z)))
est un terme qui désigne un entier, mais lequel? Si l’on sait que add représente la
fonction d’addition et que S(S(Z)) représente l’entier 2 alors on peut deviner que
add(S(S(Z)),S(S(Z))) représente l’entier 4 car on sait calculer 2 +2. Mais sait-on
réellement calculer 2+2 ou avons nous simplement appris par cœur que « 2 et 2
égalent 4 »? Avec son langage de termes, G. Peano fournit un moyen de calculer
effectivement la somme de deux entiers. Pour cela, il pose les égalités élémentaires12 Chapitre 1. Langages logiques 1.1. Constantes, fonctions, prédicats et connecteurs 13
suivantes pour tous termes t et t : Pour définir l’ensemble T (F) de tous les termes, on définit les ensembles de termes1 2 0
s de chaque sorte et on les réunit. On note T (F) l’ensemble des termes de sorte s.0add(Z,t )= t2 2
Pour notre exemple, cela donne :
add(S(t ),t )= S(add(t ,t ))1 2 1 2 nat list— Z ∈T (F) et nil∈T (F)0 0
nat natAvec la donnée de ces équations on peut par exemple calculer : — si t∈T (F) alors S(t)∈T (F)0 0
nat nat nat— si t ,t ∈T (F) alors add(t ,t )∈T (F) et mul(t ,t )∈T (F)1 2 0 1 2 0 1 2 0add(S(S(Z)),S(S(Z))) = S(add(S(Z),S(S(Z))))
nat list list— si t ∈T (F) et t ∈T (F) alors cons(t ,t )∈T (F)1 0 2 0 1 2 0= S(S(add(Z,S(S(Z)))))
list list— si t ,t ∈T (F) alors append(t ,t )∈T (F)1 2 0 1 2 0= S(S(S(S(Z))))
nat listet, pour l’ensemble des termes, T (F)=T (F) ∪T (F)0 0 0
De manière générale, on se donne un ensemble Σ de symboles de sorte de base.
Pour aller plus loin : langage de termes avec sortes Originellement consacré à la
∗ nOn note Σ la réunion des n-uplets Σ . Par abus, on appelle également sorten∈INformalisation des mathématiques, le langage de la logique des prédicats n’avait qu’un
∗les éléments de Σ . Les ensembles de symboles ne sont maintenant plus indicés par
seul univers du discours : les nombres pour l’arithmétique ou les ensembles pour
∗des entiers désignant leur arité mais par des sortes (dans Σ ): F .(s ,...,s )1 kla théorie des ensembles. Mais, et en particulier avec l’apparition de l’informatique,
sOn définit ainsi les ensembles T (F) pour chaque sorte de base s∈Σ :0s’est fait sentir le besoin de langages désignant des valeurs de natures différentes.
s— pour toute sorte de base s∈Σ, si k ∈F alors k ∈T (F)s 0Par exemple, des nombres et des listes de nombres. Le principe de définition 1.1 des
∗— pour toute sorte (s ,...,s ,s )∈Σ ,1 n n+1ensembles de termes n’est pas adaptée à ce besoin.
s s1 nsi f ∈F , si t ∈T (F) , ..., t ∈T (F)(s ,...,s ) 1 0 n 01 n+1Reprenons les éléments de signature donnés dans les deux exemples précédents
sn+1alors f(t ,...,t )∈T (F) .1 n 0pour formaliser l’arithmétique : Z, S, add et mul. Ajoutons-y les symboles suivants sOn pose : T (F)= T (F) .3 0 0s∈Σpour représenter les listes :
— nil pour désigner la liste vide;
— cons pour l’opération binaire d’ajout d’une valeur en tête de liste;
— append pour désigner l’opération binaire de concaténation de deux listes. Le programmeur aura reconnu dans l’association des sortes aux symboles,
l’assiEn nous basant sur le seul principe de définition 1.1, nous aurions : gnation de type des langages de programmation. Les contraintes portant sur les sortes
dans la définition des termes ne sont rien d’autre que les règles de typage.F ={Z,nil}, F ={S} et F ={add,mul,cons,append}0 1 2
Les termes S(nil), add(nil,Z), cons(S(Z),Z), append(Z,nil) seraient alors des
éléments de notre langage. Or, nous ne souhaitons pas avoir à donner une valeur par
1.1.3 Formules atomiques, connecteurs, formules logiquesexemple à l’addition de 0 et de la liste vide ou à l’ajout de 1 en tête de la liste 0, etc.
Notez que la notion d’arité permet déjà d’exclure du langage des termes des
comFormules atomiques Nous avons illustré comment les énoncés atomiques sont
débinaisons non pertinentes; par exemple, add(Z)∈T (F) puisque add est un symbole0 composés en un symbole de prédicat appliqué à un ou plusieurs termes. Ces «
apd’arité 2. Pour exclure les constructions non pertinentes d’un langage où cohabitent
plications » forment l’ensemble des formules atomiques du langage de la logique de
plusieurs sortes d’objet, on étend la notion d’arité en une notion de sortes. Dans notre
prédicats.
exemple, nous avons deux sortes de base, disons : nat pour les entiers et list pour les
Nous avons vu comment se définit un ensemble de termes à partir d’un ensembleF
listes d’entiers. À chaque symbole, on associe, selon son arité n, un (n+1)-uplet de
de symboles de constante et de fonction. Pour définir l’ensemble des formules
atosortes indiquant, si besoin, la sorte des arguments et la sorte du terme obtenu. Dans
miques, suivant le modèle adopté pour les symboles de fonction, nous nous munissons
notre exemple, nous aurions la correspondance résumée dans le tableau suivant :
d’un ensemble, noté P, de symboles de prédicat :
symbole n-uplet de sortes
P =P ∪P ∪P ∪···= P0 1 2 nZ → (nat)
n≥0S → (nat,nat)
add → (nat,nat,nat)
où P est un ensemble de symboles d’arité n. Les symboles d’arité 0 représentent lesnmul → (nat,nat,nat)
énoncés que l’on ne décompose pas en sujet/prédicat, comme « il pleut ». Ils jouent,
nil → (list)
au niveau des formules, le rôle que jouent les constantes pour les termes.
cons → (nat,list,list)
append → (list,list,list) Définition 1.2 (Ensemble L (F,P) de formules atomiques sans variable)0
Étant donnés une signature F et un ensemble P de symboles de prédicat, l’ensemble3. Nous reprenons ici les noms de fonctions utilisés par le langage de programmation LISP et ses
successeurs. L (F,P) des formules atomiques est défini comme suit.01.1. Constantes, fonctions, prédicats et connecteurs 13
Pour définir l’ensemble T (F) de tous les termes, on définit les ensembles de termes0
sde chaque sorte et on les réunit. On note T (F) l’ensemble des termes de sorte s.0
Pour notre exemple, cela donne :
nat list— Z ∈T (F) et nil∈T (F)0 0
nat nat— si t∈T (F) alors S(t)∈T (F)0 0
nat nat nat— si t ,t ∈T (F) alors add(t ,t )∈T (F) et mul(t ,t )∈T (F)1 2 0 1 2 0 1 2 0
nat list list— si t ∈T (F) et t ∈T (F) alors cons(t ,t )∈T (F)1 0 2 0 1 2 0
list list— si t ,t ∈T (F) alors append(t ,t )∈T (F)1 2 0 1 2 0
nat listet, pour l’ensemble des termes, T (F)=T (F) ∪T (F)0 0 0
De manière générale, on se donne un ensemble Σ de symboles de sorte de base.

∗ nOn note Σ la réunion des n-uplets Σ . Par abus, on appelle également sorten∈IN
∗les éléments de Σ . Les ensembles de symboles ne sont maintenant plus indicés par
∗des entiers désignant leur arité mais par des sortes (dans Σ ): F .(s ,...,s )1 k
sOn définit ainsi les ensembles T (F) pour chaque sorte de base s∈Σ :0
s— pour toute sorte de base s∈Σ, si k ∈F alors k ∈T (F)s 0
∗— pour toute sorte (s ,...,s ,s )∈Σ ,1 n n+1
s s1 nsi f ∈F , si t ∈T (F) , ..., t ∈T (F)(s ,...,s ) 1 0 n 01 n+1
sn+1alors f(t ,...,t )∈T (F) .1 n 0 sOn pose : T (F)= T (F) .0 0s∈Σ

Le programmeur aura reconnu dans l’association des sortes aux symboles,
l’assignation de type des langages de programmation. Les contraintes portant sur les sortes
dans la définition des termes ne sont rien d’autre que les règles de typage.
1.1.3 Formules atomiques, connecteurs, formules logiques
Formules atomiques Nous avons illustré comment les énoncés atomiques sont
décomposés en un symbole de prédicat appliqué à un ou plusieurs termes. Ces «
applications » forment l’ensemble des formules atomiques du langage de la logique de
prédicats.
Nous avons vu comment se définit un ensemble de termes à partir d’un ensembleF
de symboles de constante et de fonction. Pour définir l’ensemble des formules
atomiques, suivant le modèle adopté pour les symboles de fonction, nous nous munissons
d’un ensemble, noté P, de symboles de prédicat :

P =P ∪P ∪P ∪···= P0 1 2 n
n≥0
où P est un ensemble de symboles d’arité n. Les symboles d’arité 0 représentent lesn
énoncés que l’on ne décompose pas en sujet/prédicat, comme « il pleut ». Ils jouent,
au niveau des formules, le rôle que jouent les constantes pour les termes.
Définition 1.2 (Ensemble L (F,P) de formules atomiques sans variable)0
Étant donnés une signature F et un ensemble P de symboles de prédicat, l’ensemble
L (F,P) des formules atomiques est défini comme suit.014 Chapitre 1. Langages logiques 1.2. Variables et quantificateurs 15
1. Si p∈P est un symbole de prédicat d’arité 0, alors p est une formule atomique. Donnons-nous les formules atomiques suivantes :0
2. Si p∈P est un symbole de prédicat d’arité n et si t ,··· ,t sont des termesn 1 n F : il_pleut1
de T (F), alors p(t ,··· ,t ) est une formule atomique.0 1 n F : suit_un_cours_de_logique(Socrate)2
F : lit_ses_messages_sur_son_smartphone(Socrate)3
Comme pour les termes, nous avons ici un «schéma général» de définition que l’on F : comprend_la_logique(Socrate)4
«particularisera» pour définir, par exemple, les formules atomiques de l’arithmétique
L’énoncé « s’il ne pleut pas et que Socrate suit un cours de logique, alors Socrateen choisissant le contenu des ensembles F et P.
comprend la logique ou Socrate lit ses messages sur son smartphone » correspond à
la formule logique :Connecteurs logiques Les connecteurs logiques sont des opérateurs de composition
(¬F ∧F )⇒ (F ∨F )1 2 4 3des formules. Ils viennent des conjonctions de coordination de la langue naturelle : et,
ou, non ainsi que si-alors. On désigne chacun d’eux par un symbole. Remarquez que dans la formule ci-dessus, nous n’avons pas complètement respecté la
règle 4. en omettant les parenthèses externes. Nous ferons souvent cet abus. On peut
Connecteur Symbole représenter cette formule sous forme d’un arbre de syntaxe abstraite :
et ∧

ou ∨
∧ ∨non ¬
¬ F F Fsi-alors ⇒ 2 4 3
À l’exception du «non», tous les connecteurs sont des symboles binaires pour lesquels F1
onutiliseralanotation infixe quiconsisteàécrireleconnecteurentrelesdeuxformules
auxquelles il s’applique.
Connecteur pour l’équivalence On utilise souvent le symbole ⇔ pour exprimer
l’équivalence entre formules. Nous ne l’ajoutons toutefois pas à notre ensemble dePar convenance, nous utiliserons également deux « constantes » de formules que
symboles logiques de base : on verra la formule F ⇔ F comme un simple «raccourcinous écrirons true et false. 1 2
syntaxique » de la formule (F ⇒ F )∧(F ⇒ F ).1 2 2 1
Formules logiques Étant donnés une signatureF et un ensembleP de symboles de
prédicat, on a défini un ensembleL (F,P) de formules atomiques. Sur cette base, on0 1.2 Variables et quantificateurs
définit à présent l’ensemble IF (F,P) des formules logiques.0
Nous complétons le langage de la logique des prédicats avec les symboles de
vaDéfinition 1.3 (Ensemble IF (F,P) des formules logiques sans variable)0 riable et les opérateurs logiques de quantification. Pour cela, il nous faut étendre le
Étant donnés une signature F et un ensemble P de symboles de prédicat, l’ensemble
langagedestermespouryinclurelesvariablesetlelangagedesformulesendéfinissant
IF (F,P) des formules logiques est défini comme suit.0 comment utiliser les quantificateurs pour combiner variables et formules.
Après en avoir discuté le principe et les motivations, cette section présente for-1. true et false sont des formules logiques.
mellement le langage logique avec variables en complétant les définitions de termes,2. Si F est une formule atomique, alors F est une formule logique.
formules atomiques et formules logiques décrites dans la section précédente.
3. Si F est une formule logique, alors ¬F est une formule logique.
4. Si F et F sont des formules logiques, alors (F ∧F ), (F ∨F ) et (F ⇒ F )1 2 1 2 1 2 1 2 1.2.1 Principe et motivations
sont aussi des formules logiques.
Considérons à nouveau l’exemple du tableau contenant la suite d’entiers 2, 5, 6, 9
(introduit page 8). Appelons-le tab. La formule qui exprime que ses éléments y sontIl s’agit ici encore d’une définition inductive : toutes les formules logiques sont
obterangés en ordre croissant est :nues en appliquant un nombre fini de fois ces règles de construction.
le(pos(tab,0),pos(tab,1))∧le(pos(tab,1),pos(tab,2))∧le(pos(tab,2),pos(tab,3))
Exemple 1.4 Considérons F =F avec F ={Socrate} et P =P ∪P avec :0 0 0 1
  Considérons maintenant un tableau tab contenant 99 éléments. Pour exprimer la2
 suit_un_cours_de_logique,  propriété d’ordre sur ce tableau, on pourrait écrire :
P ={il_pleut}P = lit_ses_messages_sur_son_smartphone,0 1
  le(pos(tab ,0),pos(tab ,1))∧···∧le(pos(tab ,97),pos(tab ,98))comprend_la_logique 2 2 2 21.2. Variables et quantificateurs 15
Donnons-nous les formules atomiques suivantes :
F : il_pleut1
F : suit_un_cours_de_logique(Socrate)2
F : lit_ses_messages_sur_son_smartphone(Socrate)3
F : comprend_la_logique(Socrate)4
L’énoncé « s’il ne pleut pas et que Socrate suit un cours de logique, alors Socrate
comprend la logique ou Socrate lit ses messages sur son smartphone » correspond à
la formule logique :
(¬F ∧F )⇒ (F ∨F )1 2 4 3
Remarquez que dans la formule ci-dessus, nous n’avons pas complètement respecté la
règle 4. en omettant les parenthèses externes. Nous ferons souvent cet abus. On peut
représenter cette formule sous forme d’un arbre de syntaxe abstraite :

∧ ∨
¬ F F F2 4 3
F1
Connecteur pour l’équivalence On utilise souvent le symbole ⇔ pour exprimer
l’équivalence entre formules. Nous ne l’ajoutons toutefois pas à notre ensemble de
symboles logiques de base : on verra la formule F ⇔ F comme un simple «raccourci1 2
syntaxique » de la formule (F ⇒ F )∧(F ⇒ F ).1 2 2 1
1.2 Variables et quantificateurs
Nous complétons le langage de la logique des prédicats avec les symboles de
variable et les opérateurs logiques de quantification. Pour cela, il nous faut étendre le
langagedestermespouryinclurelesvariablesetlelangagedesformulesendéfinissant
comment utiliser les quantificateurs pour combiner variables et formules.
Après en avoir discuté le principe et les motivations, cette section présente
formellement le langage logique avec variables en complétant les définitions de termes,
formules atomiques et formules logiques décrites dans la section précédente.
1.2.1 Principe et motivations
Considérons à nouveau l’exemple du tableau contenant la suite d’entiers 2, 5, 6, 9
(introduit page 8). Appelons-le tab. La formule qui exprime que ses éléments y sont
rangés en ordre croissant est :
le(pos(tab,0),pos(tab,1))∧le(pos(tab,1),pos(tab,2))∧le(pos(tab,2),pos(tab,3))
Considérons maintenant un tableau tab contenant 99 éléments. Pour exprimer la2
propriété d’ordre sur ce tableau, on pourrait écrire :
le(pos(tab ,0),pos(tab ,1))∧···∧le(pos(tab ,97),pos(tab ,98))2 2 2 216 Chapitre 1. Langages logiques 1.2. Variables et quantificateurs 17
Ici, l’utilisation de points de suspension dispense d’écrire les 98 formules atomiques Langage logique vs langage mathématique Le langage mathématique courant
utique le lecteur est censé être capable de retrouver mais ce n’est pas réellement une lise des abréviations pour exprimer des propriétés faisant intervenir des
quantificaformule du langage des formules que nous avons défini. teurs. C’est le cas par exemple pour exprimer que tous les éléments d’un ensemble
Si l’on examine les couples de position – (0,1)(1,2)...(97,98) – utilisés dans cha- vérifient une certaine propriété :∀x∈ Ep(x). Cette expression n’est pas une formule
cune des formules atomiques, on remarque qu’ils sont tous de la forme (i,i+1) pour i logique mais correspond à une abréviation de la formule logique∀x (x∈ E ⇒ p(x)).
allant de 0 à 97. La notation mathématique suivante permet d’éviter le recours à ces La propriété p(x) est en effet vérifiée par tous les éléments de E et cette formule
expoints de suspension : prime qu’il suffit qu’un élément x appartienne à l’ensemble E pour qu’il vérifie p(x).
Ici le symbole ∈ est un symbole de prédicat d’arité 2, utilisé en notation infixe. De
97 même, l’expression ∀x > 5 p(x) correspond à une abréviation de la formule logique
le(pos(tab ,i),pos(tab ,i+1))2 2 ∀x (x > 5⇒ p(x)). On utilise également souvent des abréviations avec le
quantificai=0
teur existentiel∃. Par exemple, pour exprimer qu’il existe au moins un élément dans
On voit apparaître dans cette formulation le symbole i dont la valeur parcourt l’in- un ensemble qui vérifie une certaine propriété, on écrit∃x∈ Ep(x). Il s’agit ici d’une
tervalle des entiers compris entre 0 et 97. Cette catégorie de symbole est celle des abréviation de la formule logique ∃x (x ∈ E∧ p(x)). La propriété p(x) est en effet
symboles de variable. vérifiée par au moins un élément de E et cette formule exprime qu’il existe un élément
La «formule» ci-dessus exprime que pour tout entier i, si le(0,i) et le(i,97), alors appartenant à E et que cet élément est tel que p(x) est vérifié. De même, l’expression
le(pos(tab ,i),pos(tab ,i+1)) ce que l’on écrit comme une formule de la logique des ∃x > 5 p(x) correspond à une abréviation de la formule logique∃x (x > 5∧p(x)).2 2
prédicats en reprenant le symbole de fonction add pour l’addition et en introduisant Enfin, on utilise parfois une abréviation pour exprimer l’existence et l’unicité d’un
le symbole ∀ pour la quantification universelle : élément x satisfaisant une certaine propriété :∃!x p(x). Le langage logique que nous
considérons ne contient pas de symbole permettant d’exprimer directement l’unicité
∀i (le(0,i)∧ le(i,97))⇒ le(pos(tab ,i),pos(tab ,add(i,1))) (1.10)2 2 mais en utilisant le prédicat binaire d’égalité eq, on peut écrire la formule logique
∃x (p(x)∧∀y (p(y) ⇒ eq(x,y))). Cette formule exprime l’existence d’un élément xOn peut encore généraliser cet énoncé en ajoutant le symbole de fonction unaire
tel que p(x) et tel que tout autre élément y satisfaisant p(y) est nécessairement égallen∈F dont l’application à un tableau donne son nombre d’éléments (sa longueur).1
à x, ce qui revient à exprimer l’unicité de l’élément x.La formule de la logique des prédicats exprimant qu’un tableau quelconque tab est
4 Nous n’utiliserons pas ces raccourcis dans cet ouvrage.trié s’écrit :

∀i (le(0,i)∧ le(add(i,2),len(tab)))⇒ le(pos(tab,i),pos(tab,add(i,1)))
Spécification de programmes La formule ∀x (p(x) ⇒∃yq(x,y)) exprime queL’autre type de quantification que nous avons évoqué dans notre introduction est la
pour tout élément x qui vérifie p(x), il existe au moins un élément y tel que q(x,y).quantification existentielle. Par exemple, nous voulons dire que le tableau tab contient
Cette formule exprime seulement l’existence d’un élément y (sans indiquer comment(au moins une fois) la valeur 42. Notons eq le prédicat d’égalité. Pour exprimer qu’au
l’obtenir) et lorsque l’on sait construire cet élément à partir de x avec une fonction f,moins une valeur du tableau tab est égale à 42, on peut écrire :
on peut alors écrire la formule ∀x p(x) ⇒ q(x,f(x)). Il s’agit de la spécification de
eq(pos(tab,0),42)∨···∨ eq(pos(tab,98),42) la fonction f. Lorsque f désigne un programme, sa spécification exprime alors que f
prend un argument x qui vérifie la précondition p(x) et calcule un résultat y (qui
En utilisant une variable et la notation mathématique de la disjonction généralisée,
dépend de l’argument x) tel que q(x,y).
on évite les points de suspension en écrivant :
98
eq(pos(tab,i),42) 1.2.2 Termes, formules atomiques, formules logiques
i=0
Termes Comme nous l’avons illustré avec l’utilisation du symbole de variable i dans
La « formule » ci-dessus exprime que pour au moins une valeur de i entre 0 et 98,
la section précédente, le langage des termes de la logique des prédicats est construit à
pos(tab,i) est égal à la valeur 42. En d’autres termes : il existe un indice i, entre 0
partir d’une signatureF et d’un ensemble X de symboles de variable. L’ensemble X
et 98 tel que pos(tab,i) est égal à la valeur 42. Le langage de la logique des prédicats
doit bien sûr être disjoint de F et de P. De plus, comme nous aurons à le voir plus
utilise le symbole ∃ pour noter la quantification existentielle :
tard (en particulier, au paragraphe 1.3.3), nous supposons que X contient une infinité
5de symboles . On étend donc la définition 1.1 p. 8 en ajoutant le cas des variables.∃i (le(0,i)∧ le(add(i,1),len(tab))∧ eq(pos(tab,i),42))
4. Pour s’assurer que i est supérieur ou égal à 0 et que i+1 est inférieur ou égal à len(tab)−1, 5. Plus précisément cet ensemble est supposé dénombrable, c-à-d que ses éléments peuvent être
on écrit que 0 est inférieur ou égal à i et que i+2 est inférieur ou égal à len(tab). numérotés. Nous reviendrons sur cette notion dans le chapitre 5.1.2. Variables et quantificateurs 17
Langage logique vs langage mathématique Le langage mathématique courant
utilise des abréviations pour exprimer des propriétés faisant intervenir des
quantificateurs. C’est le cas par exemple pour exprimer que tous les éléments d’un ensemble
vérifient une certaine propriété :∀x∈ Ep(x). Cette expression n’est pas une formule
logique mais correspond à une abréviation de la formule logique∀x (x∈ E ⇒ p(x)).
La propriété p(x) est en effet vérifiée par tous les éléments de E et cette formule
exprime qu’il suffit qu’un élément x appartienne à l’ensemble E pour qu’il vérifie p(x).
Ici le symbole ∈ est un symbole de prédicat d’arité 2, utilisé en notation infixe. De
même, l’expression ∀x > 5 p(x) correspond à une abréviation de la formule logique
∀x (x > 5⇒ p(x)). On utilise également souvent des abréviations avec le
quantificateur existentiel∃. Par exemple, pour exprimer qu’il existe au moins un élément dans
un ensemble qui vérifie une certaine propriété, on écrit∃x∈ Ep(x). Il s’agit ici d’une
abréviation de la formule logique ∃x (x ∈ E∧ p(x)). La propriété p(x) est en effet
vérifiée par au moins un élément de E et cette formule exprime qu’il existe un élément
appartenant à E et que cet élément est tel que p(x) est vérifié. De même, l’expression
∃x > 5 p(x) correspond à une abréviation de la formule logique∃x (x > 5∧p(x)).
Enfin, on utilise parfois une pour exprimer l’existence et l’unicité d’un
élément x satisfaisant une certaine propriété :∃!x p(x). Le langage logique que nous
considérons ne contient pas de symbole permettant d’exprimer directement l’unicité
mais en utilisant le prédicat binaire d’égalité eq, on peut écrire la formule logique
∃x (p(x)∧∀y (p(y) ⇒ eq(x,y))). Cette formule exprime l’existence d’un élément x
tel que p(x) et tel que tout autre élément y satisfaisant p(y) est nécessairement égal
à x, ce qui revient à exprimer l’unicité de l’élément x.
Nous n’utiliserons pas ces raccourcis dans cet ouvrage.

Spécification de programmes La formule ∀x (p(x) ⇒∃yq(x,y)) exprime que
pour tout élément x qui vérifie p(x), il existe au moins un élément y tel que q(x,y).
Cette formule exprime seulement l’existence d’un élément y (sans indiquer comment
l’obtenir) et lorsque l’on sait construire cet élément à partir de x avec une fonction f,
on peut alors écrire la formule ∀x p(x) ⇒ q(x,f(x)). Il s’agit de la spécification de
la fonction f. Lorsque f désigne un programme, sa spécification exprime alors que f
prend un argument x qui vérifie la précondition p(x) et calcule un résultat y (qui
dépend de l’argument x) tel que q(x,y).
1.2.2 Termes, formules atomiques, formules logiques
Termes Comme nous l’avons illustré avec l’utilisation du symbole de variable i dans
la section précédente, le langage des termes de la logique des prédicats est construit à
partir d’une signatureF et d’un ensemble X de symboles de variable. L’ensemble X
doit bien sûr être disjoint de F et de P. De plus, comme nous aurons à le voir plus
tard (en particulier, au paragraphe 1.3.3), nous supposons que X contient une infinité
5de symboles . On étend donc la définition 1.1 p. 8 en ajoutant le cas des variables.
5. Plus précisément cet ensemble est supposé dénombrable, c-à-d que ses éléments peuvent être
numérotés. Nous reviendrons sur cette notion dans le chapitre 5.18 Chapitre 1. Langages logiques 1.3. Substitution 19
Définition 1.4 (Ensemble T(X,F) de termes avec variables) Formules logiques Pour étendre la définition 1.2 p. 13 des formules atomiques, il
Étant donnés une signature F et un ensemble infini dénombrable X de symboles de suffit de considérer des formules atomiques construites à partir de termes deT (X,F),
variable, l’ensemble T(X,F) des termes est défini par : au lieu de T (F).0
1. Si x∈X est un symbole de variable, alors x est un terme.
Définition 1.5 (Ensemble L(X,F,P) de formules atomiques avec variables)
2. Si k ∈F est un symbole de constante, alors k est un terme.0 Étant donnés une signature F, un ensemble infini dénombrable X de symboles de
variable et un ensembleP de symboles de prédicat, l’ensembleL(X,F,P) des formules3. Si f ∈F est un symbole de fonction d’arité n, et si t ,··· ,t sont des termes,n 1 n
atomiques est défini comme suit.alors f(t ,··· ,t ) est un terme.1 n
1. Sip∈P est un symbole de prédicat d’arité 0, alorsp est une formule atomique.0
Exemple 1.5 Transcrivons,dansnotrelangagedel’arithmétiquebasésurlessymboles
2. Si p∈P est un symbole de prédicat d’arité n et si t ,··· ,t sont des termesn 1 n2 2Z,addetmul,l’expressionmathématiquex +2xy+y ,oùxety sontdessymboles de
de T (X,F), alors p(t ,··· ,t ) est une formule atomique.1 n2variable. L’élévation au carré x est transcrite avec la multiplication mul(x,x).
L’expressioncomplèteesttranscriteparadd(mul(x,x),add(mul(2,mul(x,y)),mul(y,y))).
Pour construire l’ensemble IF(X,F,P) des formules logiques, il suffit d’étendre la
La structure d’arbre correspondant à cette formule est :
définition 1.3 p. 14, en considérant maintenant des formules atomiques deL(X,F,P),
au lieu deL (F,P), et d’ajouter deux constructions correspondant aux deux quanti-0
add
ficateurs ∀ et ∃.
mul add
Définition 1.6 (Ensemble IF(X,F,P) des formules logiques avec variables)
x x mul mul
Étant donnés une signature F, un ensemble infini dénombrable X de symboles de
variable et un ensembleP de symboles de prédicat, l’ensemble IF(X,F,P) des formulesy y2 mul
logiques est défini inductivement comme suit.
yx
1. true et false sont des formules logiques.
2. Si F est une formule atomique, alors F est une formule logique.
Induction La définition 1.4 est, ici encore, une définition inductive : chaque terme 3. Si F est une formule logique, alors ¬F est une formule logique.
t∈T(X,F)estobtenuenappliquantunnombredefoisfinicesrèglesdeconstruction.
4. Si F et F sont des formules logiques, alors (F ∧F ), (F ∨F ) et (F ⇒F )1 2 1 2 1 2 1 2Aussi, pour définir une fonction sur T(X,F), il est possible de procéder de manière
sont aussi des formules logiques.
inductive en indiquant le résultat de l’application de la fonction au terme t pour
5. Si F est une formule logique et x est un symbole de variable, alors ∀xF etchacune des règles de construction de t.
∃xF sont aussi des formules logiques.Par exemple, la fonction ϑ : T(X,F) → ℘(X) permettant de calculer l’ensemble
des variables (℘(X) désigne l’ensemble des parties de l’ensembleX) apparaissant dans
Le langage logique obtenu est appelé langage de la logique du premier ordre. Il s’agitun terme est définie par :
d’unlangagedupremierordrecarlesquantificationsnepeuvents’effectuerquesurdes
symbolesdevariabledésignantdesobjetssurlesquelsportel’énoncé.Laformule(1.10)ϑ(x)= {x} si x∈X
introduite page 16 est un exemple de formule du langage de la logique des prédicats (leϑ(k)= ∅ si k ∈F0
lecteur pourra construire la structure d’arbre de cette formule pour s’en convaincre).ϑ(f(t ,··· ,t )) = ϑ(t )∪···∪ϑ(t ) si f ∈F et t ∈T(X,F)1 n 1 n n i
Les deux premières lignes traitent respectivement les deux cas de base, des variables Pour aller plus loin Lorsque l’on peut quantifier sur des symboles de prédicat (qui
et des constantes, la troisième ligne donne l’expression inductive. sont alors des variables de prédicat) on parle d’un langage du second ordre. Un langage
S’agissant d’une définition inductive, l’ensembleT(X,F) est également muni d’un du second ordre permet d’exprimer par une formule les schémas de raisonnement
schéma de raisonnement par induction permettant d’établir une propriétéP pour tous par induction. Par exemple, pour le schéma 1.9 d’induction sur les entiers introduit
les termes : il suffit d’ajouter au schéma (1.9), donné page 10, la démonstration de la page 10, on a :
propriété P pour tout symbole de variable (l’exercice 1.11 illustre l’utilisation de ce
schéma de raisonnement). ∀P((P(Z)∧∀m(P(m)⇒P(S(m))))⇒∀nP(n))
Enfin, un terme t ∈T(X,F) peut aussi être vu comme un arbre étiqueté par
des éléments de F∪X : les feuilles sont étiquetées par des constantes de F ou des Une autre possibilité est de quantifier sur des symboles de fonction. Mais nous n’abor-0
variables de X et chaque nœud étiqueté par un élément de F a exactement n fils. dons pas ce type de langages logiques dans cet ouvrage.n1.3. Substitution 19
Formules logiques Pour étendre la définition 1.2 p. 13 des formules atomiques, il
suffit de considérer des formules atomiques construites à partir de termes deT (X,F),
au lieu de T (F).0
Définition 1.5 (Ensemble L(X,F,P) de formules atomiques avec variables)
Étant donnés une signature F, un ensemble infini dénombrable X de symboles de
variable et un ensembleP de symboles de prédicat, l’ensembleL(X,F,P) des formules
atomiques est défini comme suit.
1. Sip∈P est un symbole de prédicat d’arité 0, alorsp est une formule atomique.0
2. Si p∈P est un symbole de prédicat d’arité n et si t ,··· ,t sont des termesn 1 n
de T (X,F), alors p(t ,··· ,t ) est une formule atomique.1 n
Pour construire l’ensemble IF(X,F,P) des formules logiques, il suffit d’étendre la
définition 1.3 p. 14, en considérant maintenant des formules atomiques deL(X,F,P),
au lieu deL (F,P), et d’ajouter deux constructions correspondant aux deux quanti-0
ficateurs ∀ et ∃.
Définition 1.6 (Ensemble IF(X,F,P) des formules logiques avec variables)
Étant donnés une signature F, un ensemble infini dénombrable X de symboles de
variable et un ensembleP de symboles de prédicat, l’ensemble IF(X,F,P) des formules
logiques est défini inductivement comme suit.
1. true et false sont des formules logiques.
2. Si F est une formule atomique, alors F est une formule logique.
3. Si F est une formule logique, alors ¬F est une formule logique.
4. Si F et F sont des formules logiques, alors (F ∧F ), (F ∨F ) et (F ⇒F )1 2 1 2 1 2 1 2
sont aussi des formules logiques.
5. Si F est une formule logique et x est un symbole de variable, alors ∀xF et
∃xF sont aussi des formules logiques.
Le langage logique obtenu est appelé langage de la logique du premier ordre. Il s’agit
d’undupremierordrecarlesquantificationsnepeuvents’effectuerquesurdes
symbolesdevariabledésignantdesobjetssurlesquelsportel’énoncé.Laformule(1.10)
introduite page 16 est un exemple de formule du langage de la logique des prédicats (le
lecteur pourra construire la structure d’arbre de cette formule pour s’en convaincre).
Pour aller plus loin Lorsque l’on peut quantifier sur des symboles de prédicat (qui
sont alors des variables de prédicat) on parle d’un langage du second ordre. Un langage
du second ordre permet d’exprimer par une formule les schémas de raisonnement
par induction. Par exemple, pour le schéma 1.9 d’induction sur les entiers introduit
page 10, on a :
∀P((P(Z)∧∀m(P(m)⇒P(S(m))))⇒∀nP(n))
Une autre possibilité est de quantifier sur des symboles de fonction. Mais nous
n’abordons pas ce type de langages logiques dans cet ouvrage.20 Chapitre 1. Langages logiques 1.3. Substitution 21
∀x1.3 Substitution

Très souvent lorsque l’on a un énoncé universel, on l’utilise sur un cas particulier.
p(x,y) ∃y
C’est par exemple le cas dans le célèbre syllogisme « Tous les hommes sont mortels,
or Socrate est un homme donc Socrate est mortel ». Dans le langage de la logique des ∧
prédicats du premier ordre, les énoncés universels sont des formules qui commencent
q(y) r(x,y,z)
par un quantificateur universel (par exemple : ∀x(Homme(x) ⇒ Mortel(x))).
Utiliser une telle formule revient concrètement à remplacer dans la formule privée de
Cette formule contient deux quantificateurs : un quantificateur universel associé au
son quantificateur la variable anciennement quantifiée par ce qui désigne le cas
parsymbole de variable x (∀x) et un quantificateur existentiel associé au symbole de
vaticulier, à savoir, un terme (par exemple, on peut remplacer x par Socrate dans
riable y (∃y). Le premier, qui est à la racine de l’arbre de la formule, a une portée qui
Homme(x)⇒ Mortel(x) pour obtenir Homme(Socrate)⇒ Mortel(Socrate)). Pour
s’étend sur toute la formule; le second a une portée qui ne s’étend que sur la formule
utiliser un cas particulier d’une formule universelle, il y a donc deux opérations :
supvenant après le connecteur ⇒ (à droite dans l’arbre). Les symboles de variable qui se
primer la quantification puis substituer un terme à une variable. C’est à cette seconde
trouvent dans la portée d’un quantificateur et qui sont identiques au symbole associé
opération que l’on s’intéresse dans cette section.
au quantifcateur sont dits liés par ce quantificateur. Ainsi, les symboles de variable x
L’opération de «remplacement» est une opération syntaxique sur la structure des apparaissant dans les formules atomiques p(x,y) et r(x,y,z) sont liés par la
quantififormules dont la définition demande quelques précisions. En effet, il faut éviter deux cation∀x. Mais attention, la situation est un peu plus complexe avec la quantification
situations critiques. ∃y : seules les occurrences de y qui apparaissent dans les formules atomiques q(y) et
Lapremièreestquel’onn’autorisepasl’opérationderemplacementdesymbolesde r(x,y,z) sont liées par la quantification; l’occurrence de y dans p(x,y) ne l’est pas
variable quantifiés. Si l’on souhaite remplacer un symbole de variable x par un terme puisquecetteformuleatomiquen’estpasdanslaportéeduquantificateur∃.Lorsqu’un
f(a), il ne faut pas opérer ce remplacement sur une formule de la forme∀x∀yp(x,y) symbole de variable n’est dans la portée d’aucun quantifcateur, il est dit libre.
car cela n’a guère de sens :∀f(a)∀yp(f(a),y) n’est pas une formule. En revanche, on Dans le schéma ci-dessous nous avons décoré l’arbre syntaxique de la formule
pourra remplacer x par f(a) dans∀yp(x,y). Cela donnera∀yp(f(a),y). L’opération ∀x(p(x,y) ⇒∃y(q(y)∧ r(x,y,z))) avec des flèches en pointillé indiquant la portée
deremplacementestlégitimeicicarelleopèresuruneoccurrenceditelibre dusymbole des quantificateurs. On y voit que le symbole y apparaissant dans p(x,y) n’est pas
de variable x dans la formule∀yp(x,y). A contrario, le symbole de variable y est dit dans la portée de ∃y.
lié dans∀yp(x,y). La définition 1.7 introduit formellement ces notions.
∀x
La seconde situation à éviter est ce que l’on appelle la capture de variable.
Imaginons que l’on veuille remplacer le symbole de variable x par le terme y (réduit ici au ⇒
symbole de variable y) dans la formule∀yp(x,y). Ici, x est bien libre et l’on peut
aup(x,y) ∃y
toriser le remplacement. Mais si l’on y procédait, on obtiendrait la formule∀yp(y,y)
dans laquelle la quantification universelle ∀y force le premier terme en argument du ∧
prédicat p à devoir varier en même temps que le second, alors que ce n’était pas le q(y) r(x,y,z)
cas dans la formule originale où le second argument de p pouvait varier sans que
cela affectât le premier. Nous verrons comment contourner la capture de variable en Pour définir l’ensemble des symboles de variable liés et l’ensemble des symboles
« renommant » les symboles de variable liés lorsque nécessaire. de variable libres d’une formule, nous utilisons la fonction ϑ définie dans la section
Cette section définit d’abord les notions de variables libres et liées, puis de for- 1.2.2, page 18, qui calcule l’ensemble des symboles de variable ayant une occurrence
mules closes et clôture universelle, qui sont nécessaires pour définir l’opération de dans un terme. On note Free(F) l’ensemble des symboles de variable ayant au moins
substitution dans la section 1.3.3. occurrence libre dans la formule F et Bound(F) l’ensemble des symboles de variable
y ayant au moins une occurrence liée.
Définition 1.7 (Variables libres/liées)
1.3.1 Portée d’un quantificateur, variables libres, variables liées
Soit F une formule, les ensembles Free(F) et Bound(F) sont définis inductivement
comme suit.La structure syntaxique des formules assigne aux symboles de quantification∀ et∃
1. Si F est la formule true ou false alorsune portée. La portée d’un quantificateur est la portion de la formule sur laquelle il
Free(F)=∅ et Bound(F)=∅.agit; ce qui se lit très bien sur la représentation arborescente des formules.
Considéronsparexemplelaformule∀x(p(x,y)⇒∃y (q(y)∧r(x,y,z)))dontl’arbre 2. Si F est la fomule atomique p(t ,··· ,t ) alors1 nn
syntaxique est : Free(F)= ϑ(t ) et Bound(F)=∅.ii=11.3. Substitution 21
∀x

p(x,y) ∃y

q(y) r(x,y,z)
Cette formule contient deux quantificateurs : un quantificateur universel associé au
symbole de variable x (∀x) et un quantificateur existentiel associé au symbole de
variable y (∃y). Le premier, qui est à la racine de l’arbre de la formule, a une portée qui
s’étend sur toute la formule; le second a une portée qui ne s’étend que sur la formule
venant après le connecteur ⇒ (à droite dans l’arbre). Les symboles de variable qui se
trouvent dans la portée d’un quantificateur et qui sont identiques au symbole associé
au quantifcateur sont dits liés par ce quantificateur. Ainsi, les symboles de variable x
apparaissant dans les formules atomiques p(x,y) et r(x,y,z) sont liés par la
quantification∀x. Mais attention, la situation est un peu plus complexe avec la quantification
∃y : seules les occurrences de y qui apparaissent dans les formules atomiques q(y) et
r(x,y,z) sont liées par la quantification; l’occurrence de y dans p(x,y) ne l’est pas
puisquecetteformuleatomiquen’estpasdanslaportéeduquantificateur∃.Lorsqu’un
symbole de variable n’est dans la portée d’aucun quantifcateur, il est dit libre.
Dans le schéma ci-dessous nous avons décoré l’arbre syntaxique de la formule
∀x(p(x,y) ⇒∃y(q(y)∧ r(x,y,z))) avec des flèches en pointillé indiquant la portée
des quantificateurs. On y voit que le symbole y apparaissant dans p(x,y) n’est pas
dans la portée de ∃y.
∀x

p(x,y) ∃y

q(y) r(x,y,z)
Pour définir l’ensemble des symboles de variable liés et l’ensemble des symboles
de variable libres d’une formule, nous utilisons la fonction ϑ définie dans la section
1.2.2, page 18, qui calcule l’ensemble des symboles de variable ayant une occurrence
dans un terme. On note Free(F) l’ensemble des symboles de variable ayant au moins
occurrence libre dans la formule F et Bound(F) l’ensemble des symboles de variable
y ayant au moins une occurrence liée.
Définition 1.7 (Variables libres/liées)
Soit F une formule, les ensembles Free(F) et Bound(F) sont définis inductivement
comme suit.
1. Si F est la formule true ou false alors
Free(F)=∅ et Bound(F)=∅.
2. Si F est la fomule atomique p(t ,··· ,t ) alors1 nn
Free(F)= ϑ(t ) et Bound(F)=∅.ii=1
22 Chapitre 1. Langages logiques 1.3. Substitution 23
3. Si F est la formule ¬F alors 1.3.2 Formules closes, clôture universelle0
Free(F) = Free(F ) et Bound(F) = Bound(F ).0 0
Une formule close est une formule F telle que Free(F)= ∅. À partir d’une for-4. Si F est la formule F ∧F ou F ∨F ou F ⇒ F alors1 2 1 2 1 2
mule F quelconque telle que Free(F)={x ,··· ,x }, il est possible de construire une1 nFree(F) = Free(F )∪Free(F ) et Bound(F) = Bound(F )∪Bound(F ).1 2 1 2 −→
formule close∀x ··· ∀x F, notée ∀F, en quantifiant chacune de ses variables libres1 n5. Si F est la formule ∀xF ou ∃xF alors0 0
avec le quantificateur∀. Cette formule est appelée clôture universelle de F. Bien sûr,Free(F) = Free(F )\{x} et Bound(F) = Bound(F )∪{x}.0 0
la clôture universelle d’une formule F déjà close est cette même formule F.
Par exemple, on a : Pour reprendre l’exemple du paragraphe précédent, une clôture universelle de la
formule ∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z))) est :Free(∀x(p(x,y)⇒∃y(q(y)∧r(x,y,z)))) ={y,z}
Bound(∀x(p(x,y)⇒∃y(q(y)∧r(x,y,z)))) ={x,y}
∀y∀z∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z)))
L’ensemble de tous les symboles ayant une occurrence dans une formule est l’union des
occurrences libres et des occurrences liées de symboles des variable de cette formule : Elle en admet toutefois une autre qui est :
ϑ(F) = Free(F)∪Bound(F) ∀z∀y∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z)))
Dans le schéma ci-dessous, nous avons encadré les occurrences libres de symboles de
De manière générale, une formule F contenant n symboles de variable admettant
variable; toutes les autres sont liées :
au moins une occurrence libre admet n! clôtures universelles différentes puisque l’on
∀x peut effectuer les quantifications universelles sur les variables de Free(F) dans un
ordrequelconque.Nousexpliqueronsauchapitre4pourquoil’ordredesquantificateurs
⇒ n’a ici pas d’incidence sur la signification des formules et que toutes les clôtures
p x, y ∃y universelles sont équivalentes.

1.3.3 Substitution dans une formule logiqueq(y) r x,y, z
Comme nous l’avons mentionné en introduction de cette section, on ne s’intéresse
Comme l’illustre notre exemple, il peut exister au sein d’une même formule des
qu’au remplacement des occurrences libres de variables dans une formule.
Traditionsymboles de variable dont certaines occurrences sont liées tandis que d’autres sont
nellement, on parle de substitution plutôt que de «remplacement». On note F[x := t]
libres. C’est le cas ici pour le symbole y. On peut toujours éviter cette situation et ne
la formule obtenue après substitution du terme t aux occurrences libres de x dans F.
considérer que des formules F telles que Bound(F)∩Free(F)=∅. En effet, d’un point
En fait, il peut exister plusieurs formules correspondant à F[x := t] puisque
cerdevuelogique,lenomdesvariablesliéespeutêtremodifiésanschangerlasignification
taines variables liées de F peuvent être renommées afin d’éviter les captures des6ni la valeur de vérité d’une formule . Il est clair que, si x et h sont des symboles de
vavariables du terme t, comme indiqué en introduction de cette section. Il y a donc
riable,lesdeuxformules∀x(homme(x)⇒ mortel(x))et∀h(homme(h)⇒ mortel(h))
possiblement plusieurs formules pouvant correspondre à F[x := t] selon les choix de
expriment exactement le même énoncé (ce point sera plus formellement établi au
chasymboles que l’on fait pour le renommage.
pitre 4). On peut donc toujours « renommer » les variables liées d’une formule par
Enfin, dans une formule, les symboles de variable apparaissent au sein des termes.
de nouveaux noms de variable sans affecter sa signification. Pour notre exemple, on
Pour définir l’opération de substitution dans une formule, il faut donc définir
l’opépourra considérer la formule équivalente ∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z))). Notez
ration de substitution d’un terme à un symbole de variable dans un terme. On note
que l’ensemble des variables libres de cette nouvelle formule ne change pas : c’est
t[x := u] le terme obtenu après substitution du terme u au symbole de variable x dans
toujours {y,z}.
le terme t.
Enfin, on peut effectivement toujours procéder au renommage des variables liées
car lorsque nous avons défini le langage des formules (définitions 1.4, 1.5 et 1.6),
Définition 1.8 (Substitution dans un terme)
nous avons pris la précaution de supposer que nous disposions d’un ensemble infini
Le terme t[x := u] est défini par induction (sur t) comme suit.
de symboles de variable. En effet, une formule étant une suite finie de symboles, elle
contient en particulier un nombre fini de symboles de variable et il reste donc encore
x[x := u]= u (avec x∈ X)
une infinité de symboles de variable n’ayant pas d’occurrence dans la formule et dans
y[x := u]= y (avec y∈ X et x = y)
laquelle on peut choisir des noms nouveaux pour les variables liées.
k[x := u]= k (avec k∈F )0
6. C’est pourquoi, dans certains textes, les variables liées sont aussi appelées « muettes ». f(t ,··· ,t )[x := u]= f(t [x := u],··· ,t [x := u]) (avec f ∈F )1 n 1 n n
1.3. Substitution 23
1.3.2 Formules closes, clôture universelle
Une formule close est une formule F telle que Free(F)= ∅. À partir d’une
formule F quelconque telle que Free(F)={x ,··· ,x }, il est possible de construire une1 n
−→
formule close∀x ··· ∀x F, notée ∀F, en quantifiant chacune de ses variables libres1 n
avec le quantificateur∀. Cette formule est appelée clôture universelle de F. Bien sûr,
la clôture universelle d’une formule F déjà close est cette même formule F.
Pour reprendre l’exemple du paragraphe précédent, une clôture universelle de la
formule ∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z))) est :
∀y∀z∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z)))
Elle en admet toutefois une autre qui est :
∀z∀y∀x(p(x,y)⇒∃w(q(w)∧r(x,w,z)))
De manière générale, une formule F contenant n symboles de variable admettant
au moins une occurrence libre admet n! clôtures universelles différentes puisque l’on
peut effectuer les quantifications universelles sur les variables de Free(F) dans un
ordrequelconque.Nousexpliqueronsauchapitre4pourquoil’ordredesquantificateurs
n’a ici pas d’incidence sur la signification des formules et que toutes les clôtures
universelles sont équivalentes.
1.3.3 Substitution dans une formule logique
Comme nous l’avons mentionné en introduction de cette section, on ne s’intéresse
qu’au remplacement des occurrences libres de variables dans une formule.
Traditionnellement, on parle de substitution plutôt que de «remplacement». On note F[x := t]
la formule obtenue après du terme t aux occurrences libres de x dans F.
En fait, il peut exister plusieurs formules correspondant à F[x := t] puisque
certaines variables liées de F peuvent être renommées afin d’éviter les captures des
variables du terme t, comme indiqué en introduction de cette section. Il y a donc
possiblement plusieurs formules pouvant correspondre à F[x := t] selon les choix de
symboles que l’on fait pour le renommage.
Enfin, dans une formule, les symboles de variable apparaissent au sein des termes.
Pour définir l’opération de substitution dans une formule, il faut donc définir
l’opération de substitution d’un terme à un symbole de variable dans un terme. On note
t[x := u] le terme obtenu après substitution du terme u au symbole de variable x dans
le terme t.
Définition 1.8 (Substitution dans un terme)
Le terme t[x := u] est défini par induction (sur t) comme suit.
x[x := u]= u (avec x∈ X)
y[x := u]= y (avec y∈ X et x = y)
k[x := u]= k (avec k∈F )0
f(t ,··· ,t )[x := u]= f(t [x := u],··· ,t [x := u]) (avec f ∈F )1 n 1 n n





24 Chapitre 1. Langages logiques 1.3. Substitution 25
Par exemple : dans laquelle on remplace les occurrences libres de x par le terme f(k,y,z) ce qui
donne :
f(x,g(y))[y := h(z)] = f(x[y := h(z)],g(y)[y := h(z)]) = f(x,g(y[y := h(z)])) (∃wp(g(w,f(k,y,z))))∨ (∀x p(h(x,z)))
= f(x,g(h(z)))
On peut, en quelque sorte «internaliser» l’opération de renommage puisque
cellePour prendre un exemple plus complet, on a : ci se résume à la substitution d’un terme (un nouveau symbole de variable) à une
variable. Voici une définition alternative de F[x := t] qui adopte cette approche :
f(g(x,b,a),g(f(a,y),b,x))[x := f(b,w)] = f(g(f(b,w),b,a),g(f(a,y),b,f(b,w)))
true[x := t]= true
Nous laissons au lecteur le soin de détailler les étapes du calcul de la substitution. false[x := t]= false
Nous illustrons ci-dessous cette opération sur l’arbre syntaxique des termes : p(t ,··· ,t )[x := t]= p(t [x := t],··· ,t [x := t]) (p∈P )1 n 1 n n
(¬F )[x := t]= ¬(F [x := t])0 0
f f (F ∧F )[x := t]= F [x := t]∧F [x := t]1 2 1 2
g g g g (F ∨F )[x := t]= F [x := t]∨F [x := t]1 2 1 2
[x := f(b,w)]
(F ⇒ F )[x := t]= F [x := t]⇒ F [x := t]1 2 1 2
x a x af f f fb b b b (∀x F )[x := t]= ∀x F0 0
(∀yF )[x := t]= ∀y (F [x := t]) (avec x = y et y∈ ϑ(t))0 0y ya w a wb b
(∀yF )[x := t]= ∀z (F [y := z][x := t]) (avec x = y,y ∈ ϑ(t)0 0
et z ∈ ϑ(t)∪ϑ(F ))0
De ce point de vue, la substitution consiste à remplacer des feuilles de l’arbre de (∃x F )[x := t]= ∃x F0 0
syntaxe d’un terme par des sous-arbres. (∃yF )[x := t]= ∃y (F [x := t]) (avec x = y et y∈ ϑ(t))0 0
(∃yF )[x := t]= ∃z (F [y := z][x := t]) (avec x = y,y ∈ ϑ(t)0 0
Définition 1.9 (Substitution dans une formule)
et z ∈ ϑ(t)∪ϑ(F ))0
Étant donnés une formule F et un terme t tel que Bound(F)∩ϑ(t)= ∅, on définit
inductivement sur F la formule F[x := t] comme suit. Remarquez que la substitution F [y := z] est bien définie car si y est liée dans ∀yF ,0 0
elle est libre dans F . Notez également comment on détermine le choix du symbole0
true[x := t]= true
de remplacement pour y lorsque y ∈ ϑ(t) en choisissant z ∈ ϑ(t) ∪ ϑ(F ), c-à-d,0
false[x := t]= false
z ∈ X \ ϑ(t)∪ ϑ(F ). De plus, comme nous l’avions souligné au paragraphe 1.3.1,0
p(t ,··· ,t )[x := t]= p(t [x := t],··· ,t [x := t]) (p∈P )1 n 1 n n puisque X est infini alors que ϑ(t)∪ϑ(F ) est fini, l’ensemble X\ϑ(t)∪ϑ(F ) laisse0 0
(¬F )[x := t]= ¬(F [x := t])0 0 une infinité de choix possibles pour le symbole de renommage z.
(F ∧F )[x := t]= F [x := t]∧F [x := t]1 2 1 2
(F ∨F )[x := t]= F [x := t]∨F [x := t]1 2 1 2
Propriétés de la substitution Dans des circonstances bien particulières, l’ordre des(F ⇒ F )[x := t]= F [x := t]⇒ F [x := t]1 2 1 2
substitutions peut être inversé. C’est ce que montrent les lemmes 1.1 et 1.2 ci-dessous.(∀x F )[x := t]= ∀x F0 0
Cette possibilité d’inverser l’ordre des substitutions sera utile pour établir l’égalité(∀yF )[x := t]= ∀y (F [x := t]) (avec x = y)0 0
entre formules obtenues par diverses substitutions (par exemple, dans la section 4.1,(∃x F )[x := t]= ∃x F0 0
page 92).(∃yF )[x := t]= ∃y (F [x := t]) (avec x = y)0 0
Lemme 1.1 Soit t un terme, x, y deux symboles de variable différents et t , t deux1 2Notons que dans cette définition, supposer que Bound(F)∩ϑ(t)=∅ peut conduire à
termes tels que x∈/ ϑ(t ) et y/∈ ϑ(t ),on a:2 1procéder, si nécessaire, aux opérations de renommage avant celle de substitution. Par
exemple, pour calculer :
t[x := t ][y := t ]= t[y := t ][x := t ]1 2 2 1
((∃yp(g(y,x)))∨(∀x p(h(x,z))))[x := f(k,y,z)]
Démonstration. Par induction sur t.
Si t est une variable, on distingue trois cas.on commence par effectuer un renommage de l’occurrence liée dey (puisquey apparaît
— Si t est la variable x, alorsdans le terme de remplacement f(k,y,z)) pour obtenir la formule :
t[x := t ][y := t ]= x[x := t ][y := t ]= t [y := t ]= t puisque y/∈ ϑ(t )1 2 1 2 1 2 1 1
(∃wp(g(w,x)))∨(∀x p(h(x,z))) et t[y := t ][x := t ]= x[y := t ][x := t ]= x[x := t ]= t .2 1 2 1 1 1



1.3. Substitution 25
dans laquelle on remplace les occurrences libres de x par le terme f(k,y,z) ce qui
donne :
(∃wp(g(w,f(k,y,z))))∨ (∀x p(h(x,z)))
On peut, en quelque sorte «internaliser» l’opération de renommage puisque
celleci se résume à la substitution d’un terme (un nouveau symbole de variable) à une
variable. Voici une définition alternative de F[x := t] qui adopte cette approche :
true[x := t]= true
false[x := t]= false
p(t ,··· ,t )[x := t]= p(t [x := t],··· ,t [x := t]) (p∈P )1 n 1 n n
(¬F )[x := t]= ¬(F [x := t])0 0
(F ∧F )[x := t]= F [x := t]∧F [x := t]1 2 1 2
(F ∨F )[x := t]= F [x := t]∨F [x := t]1 2 1 2
(F ⇒ F )[x := t]= F [x := t]⇒ F [x := t]1 2 1 2
(∀x F )[x := t]= ∀x F0 0
(∀yF )[x := t]= ∀y (F [x := t]) (avec x = y et y∈ ϑ(t))0 0
(∀yF )[x := t]= ∀z (F [y := z][x := t]) (avec x = y,y ∈ ϑ(t)0 0
et z ∈ ϑ(t)∪ϑ(F ))0
(∃x F )[x := t]= ∃x F0 0
(∃yF )[x := t]= ∃y (F [x := t]) (avec x = y et y∈ ϑ(t))0 0
(∃yF )[x := t]= ∃z (F [y := z][x := t]) (avec x = y,y ∈ ϑ(t)0 0
et z ∈ ϑ(t)∪ϑ(F ))0
Remarquez que la substitution F [y := z] est bien définie car si y est liée dans ∀yF ,0 0
elle est libre dans F . Notez également comment on détermine le choix du symbole0
de remplacement pour y lorsque y ∈ ϑ(t) en choisissant z ∈ ϑ(t) ∪ ϑ(F ), c-à-d,0
z ∈ X \ ϑ(t)∪ ϑ(F ). De plus, comme nous l’avions souligné au paragraphe 1.3.1,0
puisque X est infini alors que ϑ(t)∪ϑ(F ) est fini, l’ensemble X\ϑ(t)∪ϑ(F ) laisse0 0
une infinité de choix possibles pour le symbole de renommage z.
Propriétés de la substitution Dans des circonstances bien particulières, l’ordre des
substitutions peut être inversé. C’est ce que montrent les lemmes 1.1 et 1.2 ci-dessous.
Cette possibilité d’inverser l’ordre des substitutions sera utile pour établir l’égalité
entre formules obtenues par diverses substitutions (par exemple, dans la section 4.1,
page 92).
Lemme 1.1 Soit t un terme, x, y deux symboles de variable différents et t , t deux1 2
termes tels que x∈/ ϑ(t ) et y/∈ ϑ(t ),on a:2 1
t[x := t ][y := t ]= t[y := t ][x := t ]1 2 2 1
Démonstration. Par induction sur t.
Si t est une variable, on distingue trois cas.
— Si t est la variable x, alors
t[x := t ][y := t ]= x[x := t ][y := t ]= t [y := t ]= t puisque y/∈ ϑ(t )1 2 1 2 1 2 1 1
et t[y := t ][x := t ]= x[y := t ][x := t ]= x[x := t ]= t .2 1 2 1 1 1