Introduction à la logique
Théorie de la démonstration
Cours et exercices corrigés 2e édition
René David
Karim Nour
Christophe Raffali
Pierre-Louis Curien
Dunod
Introduction
1
Chapitre 1 · Formules et démonstrations de la logique du premier ordre9
1.1 Introduction9
1.2 Les formules
11
1.2.1 Le langage11
1.2.2 Les termes12
1.2.3 Les formules15
1.2.4 Variables libres et variables liées19
1.2.5 Substitutions21
1.2.6 Le calcul propositionnel
22
1.3 Les démonstrations en déduction naturelle
23
1.3.1 Introduction23
1.3.2 Les séquents24
1.3.3 Les règles de démonstration25
1.3.4 Exemples de démonstration33
1.3.5 Quelques démonstrations fausses36
1.3.6 Déduction naturelle sans séquents37
1.3.7 Une autre présentation des démonstrations40
1.3.8 Règles dérivées42
1.3.9 Simplification de la notation linéaire
46
1.4 Exemples
48
1.4.1 A propos d'involutions48
1.4.2 Un théorème de commutation49
1.4.3 Une propriété de N
49
1.5 Démonstrations formelles et informelles
50
1.5.1 Retour sur les exemples précédents50
1.5.2 Rédaction formelle - rédaction «en français»51
1.5.3 Pour conclure
52
1.6 Premiers résultats théoriques
52
1.6.1 Un problème de formalisation53
1.6.2 Quelques résultats sur la substitution54
1.6.3 Choisir correctement la récurrence
57
1.7 Systèmes alternatifs de démonstration
58
1.7.1 Le calcul des séquents58
1.7.2 Les systèmes de Hilbert58
1.7.3 Les systèmes utilisés en démonstration automatique60
1.7.4 Quelques commentaires
60
Chapitre 2 · Complétude de la logique du premier ordre
67
2.1 Introduction67
2.2 Interprétations68
2.3 Le cas du calcul propositionnel73
2.4 Un peu de théorie des modèles75
2.5 Théorème de complétude
79
2.5.1 non contradictoire · consistante81
2.5.2 consistante · non contradictoire83
2.5.3 Théorème de compacité
86
2.6 Formes canoniques
87
2.6.1 Formules conjonctives et disjonctives87
2.6.2 Formules prénexes
88
2.7 Skolémisation
89
Chapitre 3 · Exemples de théories
103
3.1 Introduction103
3.2 Quelques théories algébriques
104
3.2.1 La théorie de l'égalité104
3.2.2 La théorie des groupes105
3.2.3 La théorie des anneaux et des corps106
3.2.4 La théorie des espaces vectoriels
107
3.3 Exemples d'analyse
108
3.3.1 Unicité de la limite108
3.3.2 Une propriété des fonctions continues109
3.3.3 Un exemple de topologie
109
3.4 L'arithmétique de Peano
111
3.4.1 Les axiomes111
3.4.2 Quelques propriétés théoriques de PA112
3.4.3 Exemples de preuves dans PA
113
3.5 La théorie des ensembles de Zermelo Fraenkel
116
3.5.1 Les axiomes116
3.5.2 Modélisation des mathématiques119
3.5.3 Autres axiomes
121
3.6 Les phénomènes d'incomplétude
123
3.6.1 Quelques paradoxes123
3.6.2 Indécidabilité de PA et de ZF124
3.6.3 Incomplétude et non-contradiction de PA et ZF127
3.6.4 Un exemple concret de l'incomplétude de PA
128
3.7 Quelques théories et structures décidables
129
3.7.1 Élimination des quantificateurs129
3.7.2 La théorie des ordres denses130
3.7.3 La théorie de l'égalité132
3.7.4 Le théorème de Tarski133
3.7.5 L'arithmétique de Presburger
136
Chapitre 4 · Logique intuitionniste et modèles de kripke
145
4.1 Introduction145
4.2 Logique minimale, intuitionniste et classique147
4.3 Traductions entre ces logiques
149
4.3.1 Quelques lemmes utiles149
4.3.2 Traduction de Gödel152
4.3.3 Traduction de Kuroda155
4.3.4 Problèmes de décision
158
4.4 Sémantique du calcul propositionnel
158
4.4.1 Modèles de Kripke propositionnels158
4.4.2 Théorème de complétude160
4.4.3 Autres théorèmes de complétude
162
4.5 Sémantique de la logique du premier ordre
166
4.5.1 Un cas particulier166
4.5.2 Le cas général167
4.5.3 Théorème de complétude169
4.5.4 Les théories à égalité décidable171
4.5.5 Constructivité
172
4.6 Sémantique de la logique minimale
173
4.6.1 Théorème de complétude173
4.6.2 Traduction de LM dans LI
173
4.7 L'arithmétique de Heyting
175
4.7.1 Relations entre PA et HA175
4.7.2 Constructivité de HA
176
Chapitre 5 · Calcul des séquents
185
5.1 Introduction185
5.2 Les systèmes LK et LJ
186
5.2.1 Le système LK186
5.2.2 Exemples dans LK188
5.2.3 Formulation alternative des règles191
5.2.4 Le système LJ192
5.2.5 Exemples dans LJ
194
5.3 Déduction naturelle et calcul des séquents
195
5.3.1 "formule mathématique non exprimable en texte html"195
5.3.2 "formule mathématique non exprimable en texte html"
197
5.4 Élimination des coupures
200
5.4.1 Réductions immédiates203
5.4.2 Réductions commutatives204
5.4.3 Réductions essentielles207
5.4.4 Commentaires
209
5.5 Conséquences de l'élimination des coupures
211
5.5.1 Consistance des systèmes LK et LJ211
5.5.2 Constructivité de la logique intuitionniste212
5.5.3 Propriété de la sous-formule215
5.5.4 Le théorème d'interpolation
216
Chapitre 6 · Logiques d'ordre supérieur
223
6.1 Introduction223
6.2 Le système
224
6.2.1 Les sortes224
6.2.2 Les expressions225
6.2.3 Beta-équivalence228
6.2.4 Démonstrations
229
6.3 Exemples de logiques et de théories
230
6.3.1 Les logiques multisortes du premier ordre231
6.3.2 Les logiques du second ordre233
6.3.3 L'arithmétique du second ordre234
6.3.4 Les nombres réels236
6.3.5 La théorie des types simples
237
6.4 Extensionnalité et axiome du choix238
6.5 Sémantique
241
Chapitre 7 · Démonstration automatique
247
7.1 Introduction247
7.2 L'unification
248
7.2.1 L'algorithme élémentaire d'unification248
7.2.2 Un algorithme plus performant
252
7.3 La méthode des tableaux
255
7.3.1 La structure des preuves255
7.3.2 La méthode257
7.3.3 Exemples260
7.3.4 Correction de la méthode
262
7.4 La résolution
264
7.4.1 La méthode264
7.4.2 Mise sous forme clausale268
7.4.3 Optimisations
270
Annexe · Le logiciel phox275
Corrigés des exercices
281
Exercices du chapitre 1281
Exercices du chapitre 2293
Exercices du chapitre 3303
Exercices du chapitre 4311
Exercices du chapitre 5322
Exercices du chapitre 6333
Exercices du chapitre 7
339
Bibliographie
347
Index
349