Théorie de la démonstration

La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XX^e siècle.

Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2^e congrès international des mathématiciens en 1900 avec pour objectif de démontrer la cohérence des mathématiques. Cet objectif a été invalidé par le non moins célèbre théorème d'incomplétude de Gödel en 1931, ce qui n'a toutefois pas empêché la théorie de la démonstration de se développer, notamment grâce aux travaux de Jacques Herbrand et de Gerhard Gentzen. Ce dernier a démontré l'un des résultats principaux de la théorie de la démonstration, connu sous le nom de Hauptsatz (théorème principal) ou théorème d'élimination des coupures. Gentzen a ensuite utilisé ce théorème pour donner la première démonstration purement syntaxique de la cohérence de l'arithmétique.

Après une période de calme, qui a tout de même permis d'établir un certain nombre d'autres résultats de cohérence relative et d'esquisser une classification des théories axiomatiques, la théorie de la démonstration a connu une renaissance spectaculaire au cours des années 1960 avec la découverte de la correspondance de Curry-Howard qui a exhibé un lien structurel nouveau et profond entre logique et informatique : essentiellement, la procédure d'élimination des coupures définie par Gentzen peut être vue comme un processus de calcul, si bien que les démonstrations formelles deviennent alors des programmes dont le type est la proposition à démontrer. Depuis, la théorie de la démonstration s'est développée en étroite symbiose avec d'autres domaines de la logique et de l'informatique théorique, notamment le lambda-calcul, et a donné naissance à de nouveaux modèles du calcul, le plus récent étant la logique linéaire de Jean-Yves Girard en 1986. Aujourd'hui, une partie de la théorie de la démonstration se confond avec la sémantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique théorique :

• Calcul des prédicats
• Calcul des propositions
• Calcul des séquents
• Déduction naturelle (voir aussi Style de Fitch pour la déduction naturelle)
• Système à la Hilbert
• Lambda-calcul
• Logique combinatoire
• Logique linéaire
• Automate cellulaire
• Programmation fonctionnelle
• Réalisabilité
• Théorie des catégories
• Sémantique dénotationnelle
• Théorème de Herbrand
• Théorie des domaines
• Théorie des types
• Complexité des preuves

Voir aussi

• Démonstration (logique et mathématique)

Bibliographie

• (en) Buss S. R. (ed.), Handbook of Proof Theory, Amsterdam, Elsevier, 1998.
• (en) A. S. Troelstra (en), H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, (ISBN 0-521-77911-1).
• Karim Nour, René David, Christophe Raffalli Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés, ed. Dunod.
• J.-Y. Girard, Le Point Aveugle, Cours de Logique, ed. Hermann, Paris, collection « Visions des Sciences »:
  • Tome 1 : Vers la Perfection, 280 pp., mai 2006. Cours de théorie de la démonstration s'ouvre sur une réflexion sur l'état actuel de la logique (essentialisme et existentialisme, théorème d'incomplétude de Gödel, calcul des séquents), poursuit sur la correspondance de Curry-Howard (système F, interprétation catégorique) puis motive et décrit la logique linéaire (espaces cohérents, système LL, réseaux de preuves).
  • Tome 2 : Vers l'imperfection, 288 pp., mars 2007. Le cours continue en exposant l'« hypothèse de la polarisation » (les « desseins », la « ludique » et les systèmes LC et LLP), puis décrit les systèmes expérimentaux LLL et ELL et les « espaces cohérents quantiques », et enfin s'achève sur la « géométrie de l'interaction » .
• J.-Y. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, 1989