Institut de Mathématiques de Luminy

Abstract 2000

Girard Jean-Yves
From the why to the how: proof theory from 1950 to date.
Du pourquoi au comment : la théorie de la démonstration de 1950 à nos jours.

The author presents the evolution of Proof Theory during the second halfof the 20th century. His introduction replaces in their historical context the works of Goedel, Herbrand and Gentzen as well as the constructivist tradition (Brouwer's intuitions), the introduction by Church, Curry and Kleene of the lambda-calculus and the pivotal role played by Keisel. By stressing thepermanent interactions between the theoretic and algorithmic aspects, his text describes side by side the "why" - what is, the fundamentalist aspect - and the "how" - that is the pragmatic aspect - of Proof Theory.

L'auteur présente l'évolution de la théorie de la démonstration durant la seconde moitié du XXème siècle. Son introduction replace dans leur contexte historique d'une part les travaux de Goedel, Herbrand et Gentzen, et d'autre part la tradition constructive (intuitionnisme de Brouwer), l'introduction du lambda-calculpar Church, Curry, Kleene, ainsi que le rôle charnière de Kreisel. Soulignant les interactions permanentes entre aspects théoriques et algorithmiques, ce texte décrit parallèlement le "pourquoi" - c'est-a-dire l'aspect fondamentaliste - et le "comment" - c'est-a-dire l'aspect pragmatique - de la théorie de la démonstration. Il s'agit d'un domaine en pleine expansion (lambda-calcul type, sémantique dénotationnelle, logique linéaire) dont on connait les liens étroits avec les développements de l'informatique, et qui pourrait permettre d'établir dans un avenir proche des ponts solides avec la géometrie et la physique.

Keywords : Proving; Contemporary Mathematics.

MATHDI

 




Publis 2000
Last update : september 19, 2001, EL.