Abonnez-vous à Universalis pour 1 euro

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).

— Gabriel SABBAGH

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écouvrez nos offres

Déjà abonné ? Se connecter

Écrit par

  • : 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
    • 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
    • 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...