[PDF] formulaire declaration trimestrielle ppa
[PDF] exercice représentation de lewis paces
[PDF] demande de prime d'activité
[PDF] prime d activité 18 25 ans caf
[PDF] rsa et prime d activité 2017
[PDF] prime d activité jusqu ? quel age
[PDF] qlweb caf fr
[PDF] caf prime activité
[PDF] contrat d'option sur action
[PDF] les options cours pdf
[PDF] cours sur les options call put pdf
[PDF] exercice construction de phrase ce2
[PDF] option bourse exemple
[PDF] accord sujet verbe cm2 leçon
[PDF] clases de español para extranjeros material
Le Point Aveugle
Cours de logique.
Tome 1 : vers la perfection.
Jean-Yves Girard
Institut de Mathématiques de Luminy, UMR 6206 -CNRS
163, Avenue de Luminy, Case 930, F-13288 Marseille Cedex 09
girard@iml.univ-mrs.fr
Table des matières
Avant-Proposxiii
I Les bases1
1 Existence contre essence3
1.1 L"opposition existence/essence . . . . . . . . . . . . . . . . . . . . .. 3
1.2 Projets essentialistes et existentialistes . . . . . . . . .. . . . . . . . . 5
1.2.1 La théorie des ensembles . . . . . . . . . . . . . . . . . . . . . . 5
1.2.2 Le projet Hilbertien . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2.3 Le projet de Brouwer . . . . . . . . . . . . . . . . . . . . . . . 7
1.3.1 Échecs et décadence . . . . . . . . . . . . . . . . . . . . . . . . 9
1.3.2 Relectures et renouveau . . . . . . . . . . . . . . . . . . . . . . 11
1.3.3 Et demain? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.A Essentialisme et platonisme . . . . . . . . . . . . . . . . . . . . . . .. 13
1.A.1 Le platonisme . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.A.2 Une question de morphologie . . . . . . . . . . . . . . . . . . . 13
1.B Parfait/imparfait et les catégories . . . . . . . . . . . . . . . . .. . . . 15
1.B.1 Parfait/imparfait . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.B.2 Logique linéaire et catégories . . . . . . . . . . . . . . . . . . . 15
2 Le théorème d"incomplétude17
2.1 Énoncé technique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.1 La difficulté du théorème . . . . . . . . . . . . . . . . . . . . . 17
2.1.2 L"argument diagonal . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.3 Le codage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.1.4 L"expansivité et la récessivité . . . . . . . . . . . . . . . . . . .20
2.1.5 Le premier théorème . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.6 Le second théorème . . . . . . . . . . . . . . . . . . . . . . . . 22
2.1.7 Version rapide . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.2 Hilbert face à l"incomplétude . . . . . . . . . . . . . . . . . . . . . . . 23
2.2.1 Le programme . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2.2 Le coup de grâce . . . . . . . . . . . . . . . . . . . . . . . . . . 24
iii ivTABLE DES MATIÈRES
2.3 L"incomplétude n"est pas un manque . . . . . . . . . . . . . . . . . . .25
2.3.1 Manque de rigueur? . . . . . . . . . . . . . . . . . . . . . . . . 25
2.3.2 Manque d"imagination? . . . . . . . . . . . . . . . . . . . . . . 26
2.3.3 Manque cognitif? . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3.4 Manque d"axiomes? . . . . . . . . . . . . . . . . . . . . . . . . 27
2.3.5 Manque de vérité? . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.4 Lectures métaphoriques . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.1 Le théorème de Blair . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.2 L"anti-mécanisme . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.3 Digression : l"intelligence artificielle . . . . . . . . . . . .. . . . 30
2.4.4 L"extinction du popperisme . . . . . . . . . . . . . . . . . . . . 31
2.4.5 Divers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.A Davantage sur la classification des prédicats . . . . . . . . . . . .. . . 32
2.A.1 Au premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.A.2 Au second ordre . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.A.3 Complétude vs. incomplétude . . . . . . . . . . . . . . . . . . . 33
2.A.4 Expansivité et récessivité . . . . . . . . . . . . . . . . . . . . . 34
2.B L"arithmétique formelle . . . . . . . . . . . . . . . . . . . . . . . . . .35
2.B.1 Le système RR . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.B.2 L"arithmétique de Peano . . . . . . . . . . . . . . . . . . . . . . 36
2.B.3 Systèmes plus généraux . . . . . . . . . . . . . . . . . . . . . . 37
2.C Techniques de l"incomplétude . . . . . . . . . . . . . . . . . . . . . . .38
2.C.1 Le point fixe : Russell . . . . . . . . . . . . . . . . . . . . . . . 38
2.C.3 Le codage des suites . . . . . . . . . . . . . . . . . . . . . . . . 39
2.D Incomplétude et vérité . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.D.1 Le théorème de Tarski . . . . . . . . . . . . . . . . . . . . . . . 40
2.D.2 La1-cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.D.3 La variante de Rosser . . . . . . . . . . . . . . . . . . . . . . . 41
2.E L"indécidabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.E.1 L"indécidable . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.E.2 L"inséparabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.E.3 Fonctions ambiguës . . . . . . . . . . . . . . . . . . . . . . . . . 43
3 Les séquents classiques : LK45
3.1 Généralités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.1.1 Séquents vs. systèmes à la Hilbert . . . . . . . . . . . . . . . . 45
3.1.2 Les séquents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.3 Signification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.2 Le calcul classique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.2.1 Identité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.2.2 Groupe structurel . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.2.3 Groupe logique . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.2.4 La symétrie gauche/droite . . . . . . . . . . . . . . . . . . . . . 52
3.2.5 Calcul droit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3 Le système sans coupures . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.3.1 La propriété de la sous-formule . . . . . . . . . . . . . . . . . . 53
TABLE DES MATIÈRESv
3.3.2 Sous-formule et décision . . . . . . . . . . . . . . . . . . . . . . 54
3.3.3 La signature . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.4 Démonstration duHauptsatz. . . . . . . . . . . . . . . . . . . . . . . 56
3.4.1 Les cas-clefs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.4.2 Commutations . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.4.3 Règles structurelles . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.4.4 Finalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.A Autour du calcul des séquents . . . . . . . . . . . . . . . . . . . . . . . 59
3.A.1 Théorème de déduction dans les séquents . . . . . . . . . . . . 59
3.A.2 Achille et la Tortue . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.A.3 Le théorème de Herbrand . . . . . . . . . . . . . . . . . . . . . 61
3.A.4 L"unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.A.5 Davantage sur Herbrand . . . . . . . . . . . . . . . . . . . . . . 62
3.A.6 L"égalité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.A.7 Éliminations partielles . . . . . . . . . . . . . . . . . . . . . . . 63
3.B Aspects sémantiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
3.B.1 Le théorème de complétude . . . . . . . . . . . . . . . . . . . . 64
3.B.2 La conjecture de Takeuti . . . . . . . . . . . . . . . . . . . . . 65
3.B.3 Prédicats de vérité bornés . . . . . . . . . . . . . . . . . . . . . 68
3.B.4 Le schéma de réflexion . . . . . . . . . . . . . . . . . . . . . . . 69
3.C La théorie de la démonstration infinie . . . . . . . . . . . . . . . .. . 70
3.C.1 La deuxième démonstration de Gentzen . . . . . . . . . . . . . 70
3.C.2 Laω-règle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.C.3 L"école de Munich . . . . . . . . . . . . . . . . . . . . . . . . . 72
3.C.4 Les
?reverse mathematics?. . . . . . . . . . . . . . . . . . . . 73
4 Cas intuitionniste : LJ et NJ75
4.1 Le calcul intuitionniste des séquents LJ . . . . . . . . . . . . . . .. . 75
4.1.1 Séquents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.1.2 Le calcul intuitionniste . . . . . . . . . . . . . . . . . . . . . . . 75
4.2 LeHauptsatzdans LJ . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.2.1 Démonstration . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.2.2 Propriété de la sous-formule . . . . . . . . . . . . . . . . . . . . 79
4.2.3 Existence et disjonction intuitionnistes . . . . . . . . . . .. . . 79
4.3 La déduction naturelle NJ . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.3.1 Le système . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.3.2 Coupures et normalisation . . . . . . . . . . . . . . . . . . . . . 83
4.3.3 Réductions immédiates . . . . . . . . . . . . . . . . . . . . . . 84
4.3.4 Théorème de Church-Rosser . . . . . . . . . . . . . . . . . . . . 86
4.3.5 Théorème de normalisation faible . . . . . . . . . . . . . . . . .86
4.4 La signature en déduction naturelle . . . . . . . . . . . . . . . . . .. . 87
4.4.1 L"hypothèse principale . . . . . . . . . . . . . . . . . . . . . . . 87
4.4.2 La sous-formule en déduction naturelle . . . . . . . . . . . . .. 88
4.4.3 Relation avec LJ . . . . . . . . . . . . . . . . . . . . . . . . . . 89
4.A Existence et disjonction dans NJ . . . . . . . . . . . . . . . . . . . . . 90
4.A.1 Les éliminations
?directes?. . . . . . . . . . . . . . . . . . . 90 viTABLE DES MATIÈRES
4.A.2 Les coupures commutatives . . . . . . . . . . . . . . . . . . . . 91
4.A.3 Normalisation faible . . . . . . . . . . . . . . . . . . . . . . . . 92
4.B Déduction naturelle vs. calcul des séquents . . . . . . . . . . . . .. . 92
4.B.1 Petite comparaison . . . . . . . . . . . . . . . . . . . . . . . . . 92
4.B.2 Démonstrations duHauptsatz. . . . . . . . . . . . . . . . . . . 93
4.B.3 La méthode Gandy . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.C Autour de la contraction . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4.C.1 La déduction naturelle classique . . . . . . . . . . . . . . . . . 94
4.C.2 Prawitz et la compréhension naïve . . . . . . . . . . . . . . . . 94
4.C.3 Contraction et répétitions d"hypothèses . . . . . . . . . . .. . 95
4.C.4 Bornes effectives . . . . . . . . . . . . . . . . . . . . . . . . . . 95
4.D La programmation logique . . . . . . . . . . . . . . . . . . . . . . . . . 96
4.D.1 La méthode de résolution . . . . . . . . . . . . . . . . . . . . . 96
4.D.2 PROLOG, sa grandeur . . . . . . . . . . . . . . . . . . . . . . . 96
4.D.3 PROLOG, sa misère . . . . . . . . . . . . . . . . . . . . . . . . 97
4.D.4 La négation dans PROLOG . . . . . . . . . . . . . . . . . . . . 97
4.E Modèles de Kripke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
II Autour de Curry-Howard 101
5 Interprétations fonctionnelles103
5.1 Les démonstrations comme fonctions . . . . . . . . . . . . . . . . . . .103
5.1.1 La
?sémantique des preuves?. . . . . . . . . . . . . . . . . . 103
5.1.2 L"interprétation fonctionnelle . . . . . . . . . . . . . . . . . .. 104
5.1.3 Points aveugles . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
5.1.4 NJ revu en fonctionnel . . . . . . . . . . . . . . . . . . . . . . . 106
5.1.5 Occurrences, aspects locatifs . . . . . . . . . . . . . . . . . . . 108
5.2 Leλ-calcul pur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.2.1 Une théorie naïve des fonctions . . . . . . . . . . . . . . . . . . 109
5.2.2 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.2.3 Le théorème de Church-Rosser . . . . . . . . . . . . . . . . . . 111
5.3 L"isomorphisme de Curry-Howard . . . . . . . . . . . . . . . . . . . .. 114
5.3.1 Leλ-calcul simplement typé . . . . . . . . . . . . . . . . . . . . 114
5.3.2 Somme, produit, exponentielle . . . . . . . . . . . . . . . . . . 114
5.3.3 L"isomorphisme . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
5.3.4 Normalisation forte . . . . . . . . . . . . . . . . . . . . . . . . . 116
5.A Kreisel et l"interprétation fonctionnelle . . . . . . . . . . . .. . . . . . 116
5.B La logique combinatoire . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.C Autres connecteurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.C.1 Conjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.C.2 Disjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.C.3 Absurdité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.C.4 Quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.C.5 Normalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
TABLE DES MATIÈRESvii
6 Le système F123
6.1 Le système F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
6.1.1 Généralités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
6.1.2 Le foncteur d"oubli . . . . . . . . . . . . . . . . . . . . . . . . . 124
6.1.3 Traduction des connecteurs . . . . . . . . . . . . . . . . . . . . 124
6.1.4 Un autre foncteur d"oubli . . . . . . . . . . . . . . . . . . . . . 126
6.1.5 Traduction des structures libres . . . . . . . . . . . . . . . . . . 126
6.1.6 Traduction des types de données . . . . . . . . . . . . . . . . . 127
6.1.7 Propriétés des traductions . . . . . . . . . . . . . . . . . . . . . 128
6.2 Le théorème de normalisation . . . . . . . . . . . . . . . . . . . . . . .130
6.2.1 Cas simplement typé . . . . . . . . . . . . . . . . . . . . . . . . 130
6.2.2 Une généralisation fautive . . . . . . . . . . . . . . . . . . . . . 132
6.2.3 La faute . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
6.2.4 Candidats de réductibilité . . . . . . . . . . . . . . . . . . . . . 133
6.2.5 La
?vraie?réductibilité . . . . . . . . . . . . . . . . . . . . . 134
6.2.6 La démonstration . . . . . . . . . . . . . . . . . . . . . . . . . . 135
6.A Théories des types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
6.A.1 La conjecture de Takeuti . . . . . . . . . . . . . . . . . . . . . 136
6.A.2 Retour sur la quantification du premier ordre . . . . . . . . .. 136
6.A.3 La théorie des types à la Russell . . . . . . . . . . . . . . . . . 137
6.A.4 Gentzen à son pire . . . . . . . . . . . . . . . . . . . . . . . . . 137
6.B L"arithmétique de Heyting . . . . . . . . . . . . . . . . . . . . . . . . .138
6.B.1 Traduction au second ordre . . . . . . . . . . . . . . . . . . . . 138
6.B.2 Existence et disjonction dans AH . . . . . . . . . . . . . . . . . 139
6.C Le système T . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
6.C.1 L"interprétation
?Dialectica?. . . . . . . . . . . . . . . . . . 139
6.C.2 Le système T . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
6.C.3 Réalisabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
6.D Pouvoir expressif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
6.D.1 Fonctions récursives prouvables . . . . . . . . . . . . . . . . . . 141
6.D.2 Peano vs. Heyting . . . . . . . . . . . . . . . . . . . . . . . . . 142
6.D.3 Formalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
6.D.4 La méthode Gandy . . . . . . . . . . . . . . . . . . . . . . . . . 145
6.E Le sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
6.E.1 Le polymorphisme . . . . . . . . . . . . . . . . . . . . . . . . . 145
6.E.2 Sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
6.E.3 Sous-typage etspin. . . . . . . . . . . . . . . . . . . . . . . . 146
6.F Essence, existence et typage . . . . . . . . . . . . . . . . . . . . . . . . 147
6.F.1 Phénomènes locatifs . . . . . . . . . . . . . . . . . . . . . . . . 147
6.F.2 Le typage comme essence . . . . . . . . . . . . . . . . . . . . . 147
6.F.3 Typage et calcul . . . . . . . . . . . . . . . . . . . . . . . . . . 148
6.F.4 Réductibilité et essence . . . . . . . . . . . . . . . . . . . . . . 149
viiiTABLE DES MATIÈRES
7 L"interprétation catégorique151
7.1 Les trois niveaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
7.1.1 Le premier sous-sol . . . . . . . . . . . . . . . . . . . . . . . . . 151
7.1.2 Le deuxième sous-sol . . . . . . . . . . . . . . . . . . . . . . . . 153
7.1.3 Le troisième sous-sol . . . . . . . . . . . . . . . . . . . . . . . . 156
7.2 Catégories cartésiennes fermées . . . . . . . . . . . . . . . . . . . .. . 158
7.2.1 Catégories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
7.2.2 Catégories cartésiennes . . . . . . . . . . . . . . . . . . . . . . 159
7.2.3 Catégories cartésiennes fermées . . . . . . . . . . . . . . . . . .160
7.2.4 Isomorphismes intuitionnistes . . . . . . . . . . . . . . . . . .. 162
7.3 Exemples de CCC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
7.3.1 CCC dégénérées . . . . . . . . . . . . . . . . . . . . . . . . . . 162
7.3.2 Les ensembles . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
7.3.3 Les domaines de Scott . . . . . . . . . . . . . . . . . . . . . . . 163
7.4 La logique dans une CCC . . . . . . . . . . . . . . . . . . . . . . . . . 164
7.4.1 Interprétation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
7.4.2 Laη-conversion . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
7.A La logique classique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
7.A.1 Sommes directes . . . . . . . . . . . . . . . . . . . . . . . . . . 166
7.A.2 Isomorphismes . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
7.A.3 Eta et disjonction . . . . . . . . . . . . . . . . . . . . . . . . . 167
7.A.4 La logique classique est dégénérée . . . . . . . . . . . . . . . . 167
7.A.5 Digression : les catégories du Loch Ness . . . . . . . . . . . . .168
7.A.6 Interprétation polarisée . . . . . . . . . . . . . . . . . . . . . . 169
7.B Interprétations diverses . . . . . . . . . . . . . . . . . . . . . . . . .. 170
7.B.1 Leλ-calcul pur . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
7.B.2 La majorabilité à la Howard . . . . . . . . . . . . . . . . . . . . 170
7.B.3 Le module de continuité . . . . . . . . . . . . . . . . . . . . . . 171
7.B.4 Kreisel et la prédicativité . . . . . . . . . . . . . . . . . . . . . 172
III La logique linéaire 173
8 Espaces cohérents175
8.1 Splendeurs et misère des domaines de Scott . . . . . . . . . . . . .. . 175
8.1.1 Les fonctionnelles récursives . . . . . . . . . . . . . . . . . . . . 175
8.1.2 Splendeurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
8.1.3 Misère . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
8.2 Les espaces cohérents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
8.2.1 Espaces cohérents . . . . . . . . . . . . . . . . . . . . . . . . . 177
8.2.2 Une intuition catégorique . . . . . . . . . . . . . . . . . . . . . 177
8.2.3 Limites directes . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
8.2.4 Redondance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
8.2.5 Les produits fibrés . . . . . . . . . . . . . . . . . . . . . . . . . 179
8.2.6 Fonctions stables et ordre stable . . . . . . . . . . . . . . . . . 180
8.2.7 Les espaces cohérents comme CC . . . . . . . . . . . . . . . . . 181
8.2.8 Les espaces cohérents comme CCC . . . . . . . . . . . . . . . . 182
TABLE DES MATIÈRESix
8.3 Interprétation du système F . . . . . . . . . . . . . . . . . . . . . . . .184
8.3.1 Plongements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
8.3.2 Le
?modèle de Scott?. . . . . . . . . . . . . . . . . . . . . . 185
8.3.3 Produits fibrés . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
8.3.4 Espaces et cliques variables . . . . . . . . . . . . . . . . . . . . 186
8.3.5 Cliques variables . . . . . . . . . . . . . . . . . . . . . . . . . . 187
8.3.6 Finalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
8.A Interprétations asymétriques . . . . . . . . . . . . . . . . . . . . .. . . 188
8.A.1 Généralités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
8.A.2 Interprétation quantitative . . . . . . . . . . . . . . . . . . . .188
8.A.3 Hexagones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189
9 La logique linéaire191
9.1 La linéarité dans les espaces cohérents . . . . . . . . . . . . . . . .. . 191
9.1.1 Définition et exemples . . . . . . . . . . . . . . . . . . . . . . . 191
9.1.2 La catégorie COH . . . . . . . . . . . . . . . . . . . . . . . . . 192
9.1.3 L"implication linéaire . . . . . . . . . . . . . . . . . . . . . . . . 192
9.1.4 La négation linéaire . . . . . . . . . . . . . . . . . . . . . . . . 193
9.1.5 Cohérence et dualité . . . . . . . . . . . . . . . . . . . . . . . . 194
9.2 Connecteurs linéaires parfaits . . . . . . . . . . . . . . . . . . . . .. . 195
9.2.1 Multiplicatifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195
9.2.2 Additifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
9.2.3 Digression : les notations . . . . . . . . . . . . . . . . . . . . . 197
9.3 Connecteurs imparfaits . . . . . . . . . . . . . . . . . . . . . . . . . . . 198
9.3.1 Stabilité, le retour . . . . . . . . . . . . . . . . . . . . . . . . . 198
9.3.2Pons Asinorum. . . . . . . . . . . . . . . . . . . . . . . . . . . 199
9.4 Le système logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200
9.4.1 Généralités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200
9.4.2 Le langage de LL . . . . . . . . . . . . . . . . . . . . . . . . . . 201
9.4.3 Le calcul LL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202
9.4.4 Interprétation des démonstrations . . . . . . . . . . . . . . .. 203
9.4.5 Calcul mixte . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
9.4.6 Interprétation, suite et fin . . . . . . . . . . . . . . . . . . . . . 206
9.4.7 Élimination des coupures . . . . . . . . . . . . . . . . . . . . . 207
9.A Catégories monoïdales . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
9.A.1 Le produit tensoriel selon Bourbaki . . . . . . . . . . . . . . . .208
9.A.2 Catégories monoïdales symétriques . . . . . . . . . . . . . . .. 208
9.A.3 Catégories?-autonomes . . . . . . . . . . . . . . . . . . . . . . 209
9.A.4 Le non-commutatif . . . . . . . . . . . . . . . . . . . . . . . . . 209
10 Perfection et imperfection211
10.1 La sémantique des phases . . . . . . . . . . . . . . . . . . . . . . . . . 211
10.1.1 Généralités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
10.1.2 Modèles de phases . . . . . . . . . . . . . . . . . . . . . . . . . 211
10.1.3 Interprétation de la logique . . . . . . . . . . . . . . . . . . . .212
10.1.4 Correction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 212
10.1.5 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213
xTABLE DES MATIÈRES
10.1.6 LeHauptsatz. . . . . . . . . . . . . . . . . . . . . . . . . . . . 214
10.1.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
10.2 Un monde parfait? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
10.2.1 Implication et causalité . . . . . . . . . . . . . . . . . . . . . . 217
10.2.2 Les ressources . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
10.3 Le monde est imparfait . . . . . . . . . . . . . . . . . . . . . . . . . . 223
10.3.1 L"imparfait . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
10.3.2 Bien sûr! . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
10.3.3 Modalités . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
10.3.4Il Menù del Cavaliere. . . . . . . . . . . . . . . . . . . . . . . 224
10.A La focalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225
10.A.1 La programmation logique linéaire . . . . . . . . . . . . . . .. 225
10.A.2 Connecteurs négatifs . . . . . . . . . . . . . . . . . . . . . . . . 226
10.A.3 La focalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
10.A.4 La polarité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
10.A.5 Connecteurs synthétiques . . . . . . . . . . . . . . . . . . . . . 229
10.A.6 Exponentielles et polarité . . . . . . . . . . . . . . . . . . . . .230
11 Réseaux de démonstration231
11.1 LL intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
11.1.1 Une régression . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
11.1.2 Un résultat de conservation . . . . . . . . . . . . . . . . . . . . 232
11.1.3 Logique cyclique et calcul de Lambek . . . . . . . . . . . . . . 232
11.1.4 Digression : logique non associative . . . . . . . . . . . . . .. . 234
11.1.5 Une déduction naturelle . . . . . . . . . . . . . . . . . . . . . . 235
11.2 Réseaux multiplicatifs . . . . . . . . . . . . . . . . . . . . . . . . . . .236
11.2.1 Critique des règles . . . . . . . . . . . . . . . . . . . . . . . . . 236
11.2.2 La remise à l"endroit . . . . . . . . . . . . . . . . . . . . . . . . 236
11.2.3 Traduction du calcul des séquents . . . . . . . . . . . . . . . . 238
11.2.4 Réseaux et structures . . . . . . . . . . . . . . . . . . . . . . . 239
11.2.5 Normalisation dans les structures . . . . . . . . . . . . . . . .. 240
11.2.6 Un
?théorème?de normalisation . . . . . . . . . . . . . . . . 241
11.2.7 Digression :
?logique?linéaire compacte . . . . . . . . . . . . 242
11.3 Le critère de correction . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
11.3.1 Séquentialisation . . . . . . . . . . . . . . . . . . . . . . . . . . 243
11.3.2 Interrupteurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244
11.3.3 Théorème de séquentialisation . . . . . . . . . . . . . . . . . .244
11.3.4 Les empires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
11.3.5 Démonstration du théorème . . . . . . . . . . . . . . . . . . . . 247
11.3.6 Une anecdote . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249
11.A Davantage sur le multiplicatif . . . . . . . . . . . . . . . . . . . . .. . 249
11.A.1ηdans les réseaux . . . . . . . . . . . . . . . . . . . . . . . . . 249
11.A.2 Euler-Poincaré . . . . . . . . . . . . . . . . . . . . . . . . . . . 250
11.A.3 Éléments neutres . . . . . . . . . . . . . . . . . . . . . . . . . . 251
11.A.4 La règle
?mix?. . . . . . . . . . . . . . . . . . . . . . . . . . 253
11.A.5 Réseaux d"interaction . . . . . . . . . . . . . . . . . . . . . . . 254
11.A.6 Déduction naturelle pour le calcul de Lambek . . . . . . . . . .254
TABLE DES MATIÈRESxi
11.B La syllogistique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
11.B.1 La scolastique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
11.B.2 Barbara . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
11.B.3 Scolastique ancienne . . . . . . . . . . . . . . . . . . . . . . . . 255
11.B.4 Le respect du passé . . . . . . . . . . . . . . . . . . . . . . . . 256
11.C Réseaux généraux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
11.C.1 Boîtes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
11.C.2 Réseaux exponentiels . . . . . . . . . . . . . . . . . . . . . . . . 258
11.C.3 Réseaux avec quantificateurs . . . . . . . . . . . . . . . . . . . 259
11.C.4 Réseaux additifs . . . . . . . . . . . . . . . . . . . . . . . . . . 262
11.C.5 L"
?état de l"art?. . . . . . . . . . . . . . . . . . . . . . . . . 264
Bibliographie265
Index269
xii
Plan du tome 2 : vers l"imperfection
IV Interprétations polarisées
12 Une hypothèse : la polarisation
13 Desseins et comportements
14 Ludique : la reconstruction
15 Les exponentielles orthodoxes
V Iconoclasme
16 Les exponentielles hétérodoxes
17 Espaces cohérents quantiques
18 Encore des réseaux!
19 Géométrie de l"interaction
20 GdI finie et hyperfinie
Avant-Propos
Ce petit cours de théorie de la démonstration s"adressea prioriaussi bien aux mathématiciens qu"aux informaticiens, aux physiciensqu"aux philosophes et aux linguistes; et, comme nous ne sommes plus au XVI esiècle - ni même au XVIII e-, il est bien évidemment voué à l"échec. À l"inverse d"un cours sur des sous-domaines qui fonctionnent bien (théorie des modèles, théorie des en- sembles), très moyennement (logique temporelle, logique modale), voire pas du tout (logique quantique, logique épistémique) et qui s"enracinerait alors dans une excellence technique, ou, plus prosaïquement, dans un cercle d"entraide bien comprise. Cela dit, on peut se donner d"autres objectifs que la réussite pure et simple, par exemple, la révélation d"un désordre dans cet univers ap- paremment bien rangé, au sein duquel la logique a finalement pris place entre deux pots de confiture et l"almanach des postes et ne dérange plus, ne dérange surtout pas, comme un gros chat qui ronronnerait dans son coin. Au début du siècle dernier, le chat était plutôt chien-loup etaboyait très fort : le XX esiècle fut celui des totalitarismes en tous genres et en particu- lier celui du totalitarisme (rebaptisé ?tournant?) linguistique. Cette forme extrême descientismeconsistait à ramener toute question mathématique (et donc, tout étant supposé mathématisable, toute question) àun problème de protocoles formels, langagiers, bureaucratiques : on attendait Kafka. Moins lit- térairement, le même scientisme s"attaquait dès 1904 à l"amélioration de la race en Namibie, que de pendus dans ce pays sans arbre! La logique moderne reste fondamentalement imprégnée de ?l"esprit 1900?, cette espèce de prétention à tout simplifier, puisqu"on peut tout résoudre. Quand, après 1930, l"incom- plétude viendra secouer cette morgue, on n"observera guèrequ"une complexi- fication du discours : au lieu d"expliquer à partir de plus simple, on expliquera
à partir du
?méta?; commencera alors le temps de la fausse monnaie. C"est aussi à partir de ce moment que la logique, incapable de se réformer, se coupera des mathématiques, de la physique, etc. Un sophisme typique : a quoi bon chercher de belles structuresmathéma- tiques pour la logique? Il ne peut pas y en avoir, puisque les mathématiques, les bonnes comme les mauvaises, se traduisent en logique : sastructure doit refléter le pire, i.e., ne pas exister, ou, du moins, rester très molle. Donc, si l"on xiii xivAvant-propos cherche une interprétation topologique, continue, de la logique, on ira directe- ment au pire (e.g., les domaines de Scott) et on en sera même fier! Parmi les détails révélateurs, cette insistance des logiciens à choisir des symboles contre- intuitifs, pour surtout ne pas suggérer que certaines propriétés, par exemple la distributivité, pourraient être plus importantes que d"autres1: ?Plus impor- tantes, vraiment? Ça se définit comment, l"importance? ?. Je pense à cette remarque de ma fille Isabelle - alors très jeune : ?Pourquoi ne pas appeler la porte "cuiller" et la cuiller "porte" ? ?, à laquelle j"avais répondu :?Quand on dit "prends la porte", ce ne doit pas être pris comme une invitation à dî- ner ?. Parmi les erreurs magistrales de la logique, on mentionnera la logique quantique, dont le ridicule ne s"explique que par un sentiment de supériorité du langage - et des idées, même mauvaises, dès qu"elles prennent la forme écrite - sur le monde physique. La logique quantique est, en effet, une espèce de punition infligée à la nature, coupable de ne pas obéir aux préjugés des logiciens... on pense à Xerxes faisant fouetter la mer qui avait emporté son pont de bateaux. Il y a cent ans, bien rares étaient ceux qui osaient s"opposeraux certitudes scientistes. Après un siècle de massacres, c"est devenu plusfacile : bien que les mêmes âneries reviennent sempiternellement - telle quel"idée d"un robot intelligent, fantasme de l"intelligence artificielle, prothèse improbable pour ceux qui en auraient tant besoin -, il est permis de nos jours de se moquer des Jivarosde la science. Par exemple de H. Simon, celui qui a fait retrouver la troisième loi de Kepler (les carrés et les cubes) par une machine, oubliant que ce n"est pas la loi qui lie la période au demi-grand axe, mais l"idée-même d"une telle loi, qui est difficile à trouver. Surtout quand on est...astrologue comme
Kepler.
Il faudrait aussi remarquer que, malgré son lourd passif scientiste, le bilan de la logique, quoique maigre, n"est pas nul. La théorie des modèles et la théorie des ensembles se portent plutôt bien; même la théorie de la démonstration a un bilan non négligeable et d"ailleurs de quoi partirais-jesinon, puisque c"est essentiellement dethéorie de la démonstrationqu"il va s"agir? Au début du siècle passé, la relativité d"Einstein et, de façon plus radicale, la mécanique quantique, remirent en cause nos ?intuitions fondamentales?. La logique, par ses outrances, choisit alors de déboucher sur le vide : la non- structure, le non-signifiant ?tout est codable en tout2?. Pourtant, dans le ?tournant linguistique?, l"idée de la prégnance du langage était tout à fait géniale et ne méritait pas de devenir cettemachine à décervelerque je viens d"évoquer. Si l"on y regarde de plus près, elle contient en germe une autre
1Voir par exemple, au début de la logique linéaire, le point d"honneur mis par certains à
quotesdbs_dbs8.pdfusesText_14
[PDF] La description: point aveugle de la recherche qualitative