GENTZEN GERHARD (1909-1945)
Logicien allemand, né à Greifswald et mort à Prague lors de son emprisonnement par les Soviétiques. Gentzen a développé l'étude des systèmes de déduction naturelle et établi un théorème d'élimination des coupures. Gerhard Gentzen a également donné une démonstration de consistance de l'arithmétique du premier ordre fondée sur l'induction transfinie jusqu'au premier nombre ordinal inaccessible pour l'exponentiation (et strictement supérieur à Ω). Ses méthodes et ses résultats ont profondément influé sur la théorie de la démonstration depuis 1945 et ont été péniblement et considérablement étendus à divers systèmes d'ordre supérieur. Ses travaux sont regroupés dans l'ouvrage The Collected Papers of Gerhard Gentzen (1969).
La suite de cet article est accessible aux abonnés
- Des contenus variés, complets et fiables
- Accessible sur tous les écrans
- Pas de publicité
Déjà abonné ? Se connecter
Écrit par
- Gabriel SABBAGH : docteur ès sciences, professeur de mathématiques à l'université de Paris-VII
Classification
Autres références
-
DÉMONSTRATION THÉORIE DE LA
- Écrit par Jean-Yves GIRARD
- 6 140 mots
- 1 média
...démonstration n'est pas élémentaire ! Σ01 est la complexité logique de la démonstrabilité dans les systèmes de logique usuelle (finitaire). Les travaux de Gentzen, vers 1935, ont permis de démontrer un principe de pureté des méthodes pour le calcul des prédicats, c'est-à-dire la logique pure, sans axiomes.... -
GÖDEL KURT (1906-1978)
- Écrit par Daniel ANDLER
- 2 292 mots
Dès 1936, Gentzen donnait une démonstration de la consistance de l'arithmétique ; d'autres allaient suivre. Mais chacune met (nécessairement) en jeu des mécanismes déductifs non formalisables dans le système dont la consistance est étudiée. Dans son article de 1958, où il livre notamment une nouvelle...
