Introduction à la logique : théorie de la démonstration, cours et exercices corrigés : licence 3e année, master, Capes, agrégation

Auteur(s) :

David, René (1906-1990) Découvrir l'auteur

Résumé

Les premiers chapitres présentent les bases du raisonnement mathématique et la syntaxe associée au calcul des énoncés. La deuxième partie traite de la théorie de la démonstration. Des énoncés d'exercices sont proposés en fin de chapitres : certains sont corrigés, d'autres réalisables sur Internet. Une annexe présente un assistant de démonstration, le logiciel PhoX.

Autre(s) auteur(s)
- Raffalli, Christophe
- Nour, Karim
Éditeur(s)
- Dunod
Date
- 2004
Notes
- Bibliogr. Index
Langues
- Français
Description matérielle
- XIII-352 p. ; 24 x 17 cm
Collections
- Sciences sup
Sujet(s)
ISBN
- 2-10-006796-6
Indice
- 510.1 Fondements des mathématiques, axiomatique, logique mathématique
Quatrième de couverture
- Cet ouvrage, entièrement révisé dans cette seconde édition, est un cours introductif à la logique mathématique et, en particulier, la théorie de la démonstration. On y donne la réponse du mathématicien aux questions «qu'est-ce qu'un énoncé? une démonstration?» ou plus fondamentalement, «qu'est-ce que les mathématiques?», en l'illustrant par de nombreux exemples de mathématiques courantes. Il aborde également la logique intuitionniste qui donne des preuves constructives et les techniques de base de la démonstration automatique. Ces notions sont essentielles en informatique.
  Pour aider le lecteur dans sa compréhension, ce cours contient de nombreux exemples et près de 170 exercices corrigés. Une annexe présente un assistant de démonstration, le logiciel PhoX, écrit par l'un des auteurs. Des compléments aux corrigés (preuves complètement formalisées ou réalisées avec le logiciel PhoX) ainsi que le logiciel Phox, sont disponibles sur le site des auteurs.
  Ce livre, qui ne suppose aucun prérequis en logique, s'adresse plus particulièrement aux étudiants en troisième année de Licence ou en Master. Il pourra également intéresser les candidats au CAPES et à l'agrégation.
  Mathématiques
  Physique
  Chimie
  Sciences de l'ingénieur
  Informatique
  Sciences de la vie
  Sciences de la terre
Tables des matières
- - 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
Origine de la notice:
- Electre