Théorie de la démonstration
La théorie de la démonstration étudie les preuves formelles en tant qu'objets mathématiques à part entière, en analysant leur structure, leurs transformations et la force des théories qui les produisent.
Definition
La théorie de la démonstration est la branche de la logique mathématique qui considère les preuves dans les systèmes formels comme des objets combinatoires finis, étudiant comment elles peuvent être transformées et normalisées et ce que leur existence révèle sur la cohérence et la force des théories sous-jacentes.
Scope
Ce domaine couvre les calculs formels tels que la déduction naturelle et le calcul des séquents, les théorèmes d'élimination des coupures et de normalisation, les théorèmes d'incomplétude de Gödel, la mesure de la force des théories par l'analyse ordinale, ainsi que le contenu constructif et computationnel des preuves révélé par la correspondance entre preuves et programmes.
Sub-topics
Core questions
- Comment les preuves formelles peuvent-elles être représentées et manipulées comme des objets combinatoires ?
- Quels détours dans les preuves peuvent être systématiquement éliminés, et qu'est-ce que cela révèle ?
- Quelles sont les limites inhérentes à ce qu'une théorie formelle peut prouver sur elle-même ?
- Comment la force d'une théorie peut-elle être mesurée précisément ?
Key theories
- Théorème d'élimination des coupures
- Gentzen a montré que toute preuve dans le calcul des séquents peut être transformée en une preuve sans la règle de coupure, produisant des preuves avec la propriété de sous-formule et des résultats de cohérence directs.
- Théorèmes d'incomplétude de Gödel
- Toute théorie formelle cohérente suffisamment forte pour exprimer l'arithmétique contient des énoncés vrais qu'elle ne peut pas prouver et ne peut pas prouver sa propre cohérence, fixant des limites fondamentales à la formalisation.
- Correspondance de Curry-Howard
- Les preuves en déduction naturelle correspondent aux termes d'un calcul lambda typé et la normalisation des preuves correspond au calcul, reliant la théorie de la démonstration à la théorie des langages de programmation.
Clinical relevance
La théorie de la démonstration sous-tend l'analyse de la cohérence et du contenu constructif en mathématiques et fournit la base théorique pour la théorie des types, la programmation fonctionnelle et les assistants de preuve automatisés, où les preuves servent également de programmes vérifiables.
History
La théorie de la démonstration a été fondée par Hilbert dans le cadre de son programme visant à sécuriser les mathématiques par des preuves de cohérence finitaires. Les théorèmes d'incomplétude de Gödel de 1931 ont montré que le programme original ne pouvait pas réussir pleinement, et la preuve d'élimination des coupures et de cohérence de l'arithmétique par induction transfinie de Gentzen a réorienté le domaine vers l'analyse ordinale et, plus tard, le paradigme des preuves-comme-programmes.
Key figures
- David Hilbert
- Gerhard Gentzen
- Kurt Goedel
- Jean-Yves Girard
Related topics
Seminal works
- troelstra2000
- takeuti1987
- girard1989
Frequently asked questions
- En quoi la théorie de la démonstration diffère-t-elle de la théorie des modèles ?
- La théorie des modèles étudie les structures et la vérité des énoncés en leur sein, adoptant une perspective sémantique, tandis que la théorie de la démonstration étudie les dérivations formelles et leurs transformations syntaxiques. Le théorème de complétude de Gödel relie les deux, mais leurs méthodes et leurs questions sont distinctes.
- Qu'est-ce que le programme de Hilbert ?
- C'était la proposition de prouver la cohérence de toutes les mathématiques en utilisant uniquement un raisonnement finitaire et incontestable. Le second théorème d'incomplétude de Gödel a montré qu'aucune théorie suffisamment forte ne peut prouver sa propre cohérence, de sorte que le programme ne peut être réalisé dans sa forme originale, bien que des versions modifiées restent influentes.