Théorie de la démonstration

Code APOGÉE : MA2CE030 | 6 ECTS | Enseignant : Thierry Joly | Validation : examen
Horaires hebdomadaires : 2h CM, 2h TD | Mutualisé avec : M2 LMFI

Programme

Théorème de complétude

• Théorème de complétude du calcul des séquents égalitaire LK par les témoins de Henkin

Calcul des séquents

• Élimination des coupures et théorème du séquent médian dans LK
• Théorème de Herbrand
• Sous-calcul LJ : la logique intuitionniste et son interprétation BHK
• Propriétés de la sous-formule et du témoin existentiel dans LJ

Déduction naturelle

• Systèmes NK et NJ
• Élimination des coupures de NJ
• Propriétés de la sous-formule et du témoin existentiel dans NJ, puis dans HA (arithmétique intuitionniste)

Lambda-calcul

• Propriétés de confluence et de standardisation
• Représentation des fonctions récursives
• Système T
• Correspondance de Curry-Howard
• Réalisabilité, normalisation forte et correction des programmes

Bibliographie

• Cori, R. & Lascar, D. (2003). Logique mathématique, tomes 1 & 2. Paris : Dunod.
• David, R., Nour, K. & Raffalli, C. (2004). Introduction à la logique – Théorie de la démonstration. Paris : Dunod.
• Troelstra, A. S. & van Dalen, D. (1988). Constructivism in mathematics, Vol. I. Amsterdam : North-Holland.
• Girard, J.-Y., Lafont, Y. & Taylor, P. (1989). Proofs and Types. Cambridge : Cambridge University Press. Disponible sur la page de P. Taylor.
• Krivine, J.-L. (1990). Lambda-calcul : Types et Modèles. Paris : Masson. Existe en version anglaise et augmentée, disponible sur la page de l’auteur.