[PDF] Le Point Aveugle de la logique quoique maigre

View - Download Le Point Aveugle

Previous PDF

Next PDF

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:quotesdbs_dbs45.pdfusesText_45

[PDF] incomplétude définition

[PDF] introduction ? la calculabilité pdf

[PDF] indemnité prof principal 2017

[PDF] isoe prof principal

[PDF] hsa prof

[PDF] indemnite tuteur stagiaire education nationale

[PDF] prime prof principal contractuel

[PDF] evaluation anglais 6ème description physique

[PDF] indemnité prof principal agrégé terminale

[PDF] indemnités vacances éducation nationale

[PDF] enseignant contractuel vacances d'été

[PDF] entretien d'embauche la meilleure défense c'est d'être préparé

[PDF] cdi prof contractuel

[PDF] planification annuelle français secondaire 1

[PDF] planification annuelle français secondaire 3