Théorie de la démonstration

Infos
La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve, est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du . Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2 Congrès international de mathématiques en 1900 avec pour objectif de résoudre le problème de la cohérence des mathématiques. Cet objectif a été invalidé par le non moins célèbre théor
Théorie de la démonstration

La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve, est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du . Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2 Congrès international de mathématiques en 1900 avec pour objectif de résoudre le problème de 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 preuve 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. 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
- lambda-calcul ;
- linguistique ;
- logique linéaire ;
- modèles graphiques du calcul ;
- programmation fonctionnelle ;
- réalisabilité ;
- sémantique catégorique ;
- sémantique dénotationnelle ;
- sémantique des jeux ;
- théorème de Herbrand ;
- théorie des domaines ;
- théorie des types ;
- ...

Bibliographie

- Buss S. R. (ed.), Handbook of Proof Theory, Amsterdam, Elsevier, 1998. Catégorie:Logique mathématique ar:نظرية البرهان bn:প্রমাণ তত্ত্ব de:Beweistheorie en:Proof theory es:Teoría de la demostración fa:نظریه برهان he:תורת ההוכחות ko:증명이론 pl:Teoria dowodu zh:证明论
Sujets connexes
Arithmétique   Calcul des propositions   Calcul des prédicats   Calcul des séquents   Congrès international de mathématiques   Correspondance de Curry-Howard   David Hilbert   Déduction naturelle   Gerhard Gentzen   Jacques Herbrand   Jean-Yves Girard   Lambda-calcul   Linguistique   Logique linéaire   Logique mathématique   Problèmes de Hilbert   Programmation fonctionnelle   Réalisabilité   Sémantique   Sémantique dénotationnelle   Théorie des domaines   Théorie des types   Théorème d'incomplétude de Gödel   Théorème de Herbrand  
#
Accident de Beaune   Amélie Mauresmo   Anisocytose   C3H6O   CA Paris   Carole Richert   Catherinettes   Chaleur massique   Championnat de Tunisie de football D2   Classement mondial des entreprises leader par secteur   Col du Bonhomme (Vosges)   De viris illustribus (Lhomond)   Dolcett   EGP  
^