Théorie de la preuve

Théorie de la preuve

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 XXe siècle.

Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2e 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 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 :


Bibliographie

  • Buss S. R. (ed.), Handbook of Proof Theory, Amsterdam, Elsevier, 1998.


  • Portail des mathématiques Portail des mathématiques
  • Portail de la logique Portail de la logique
  • Portail de l’informatique Portail de l’informatique
Ce document provient de « Th%C3%A9orie de la d%C3%A9monstration ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Théorie de la preuve de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • PREUVE (épistémologie) — Une proposition est dite prouvée si, ayant été établie par une méthode reconnue, elle fait l’objet d’une croyance. Cette formulation permet de distinguer quatre versants dans la théorie de la preuve: 1o un élément sémantico formel, la proposition …   Encyclopédie Universelle

  • Theorie de la demonstration — 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 XXe siècle …   Wikipédia en Français

  • Théorie la démonstration — 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 XXe siècle …   Wikipédia en Français

  • 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 XXe siècle. Hilbert a proposé cette… …   Wikipédia en Français

  • Theorie axiomatique — Théorie axiomatique Quand on parle de théorie mathématique on fait référence à une somme d énoncés, de définitions, de méthodes de preuve etc. Par exemple, quand dans cet article on parle de théorie de la calculabilité c est en ce sens. Par… …   Wikipédia en Français

  • Theorie des nombres — Théorie des nombres Traditionnellement, la théorie des nombres est une branche des mathématiques qui s occupe des propriétés des nombres entiers, qu ils soient entiers naturels ou entiers relatifs, et contient beaucoup de problèmes ouverts qu il… …   Wikipédia en Français

  • Theorie des graphes — Théorie des graphes  Pour la notion mathématique utilisée en Théorie des ensembles, voir Graphe d une fonction. La théorie des graphes est une branche commune à l informatique et aux mathématiques étudiant les graphes et les objets qui lui… …   Wikipédia en Français

  • Theorie de Galois a l'origine — Théorie de Galois à l origine Le travail de Galois proprement dit est fondé sur l étude des « substitutions » des racines des polynômes appelées aujourd hui permutations. Les permutations possibles sur une équation algébrique forment… …   Wikipédia en Français

  • Théorie de galois à l'origine — Le travail de Galois proprement dit est fondé sur l étude des « substitutions » des racines des polynômes appelées aujourd hui permutations. Les permutations possibles sur une équation algébrique forment des groupes de… …   Wikipédia en Français

  • Theorie de l'invasion aryenne — Théorie de l invasion aryenne La théorie de l invasion aryenne (TIA) a été proposée pour la première fois par l abbé Jean Antoine Dubois, un indianiste français, et développée par l indianiste germano britannique Max Müller durant le… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”