Gentzen Gerhard

En 1929, à Göttingen, Gerhard Gentzen commence une thèse de logique sous la direction de Paul Bernays. Son parcours le conduit à chercher une manière de décrire les preuves par les étapes de raisonnement elles-mêmes, plutôt que par une simple liste d'axiomes.

La déduction naturelle et le calcul des séquents donnent corps à cette idée. Une dérivation est l'enchaînement des étapes d'une preuve. Dans le calcul des séquents concerné, la règle de coupure fait intervenir une formule intermédiaire, établie dans une branche puis utilisée dans une autre, qui n'apparaît plus dans la conclusion. Gentzen montre qu'une dérivation qui emploie cette règle peut être transformée en une dérivation sans coupure : la preuve est réorganisée sans ce détour intermédiaire. Ce théorème d'élimination des coupures se distingue du théorème de normalisation en déduction naturelle.

Gerhard Gentzen est un mathématicien et logicien allemand, né en 1909 à Greifswald et mort en 1945 à Prague. Après des études dans plusieurs universités, il rejoint Göttingen en 1929 pour préparer sa thèse avec Paul Bernays. Bernays est destitué en 1933 en raison de ses origines juives ; Hermann Weyl reprend alors la direction de la thèse. Gentzen devient ensuite assistant de Hilbert.

Son apport majeur concerne la logique mathématique et les fondements des mathématiques. Il introduit deux systèmes formels fondés sur des règles d'inférence, la déduction naturelle et le calcul des séquents. En 1934, son théorème d'élimination des coupures établit, dans le calcul des séquents concerné, qu'une dérivation utilisant la règle de coupure peut être transformée en une dérivation sans coupure ; ce résultat se distingue du théorème de normalisation en déduction naturelle. En 1936, il démontre la cohérence de l'arithmétique de Peano à l'aide d'une induction transfinie allant jusqu'à l'ordinal ε₀, pour des formules de faible complexité logique. Ces méthodes deviennent essentielles à la théorie moderne de la démonstration.

Son parcours comporte aussi un engagement politique et militaire documenté : il adhère au parti national-socialiste en 1937, devient professeur à l'université de Prague en 1943 et participe aux travaux sur le missile V2. Arrêté par l'armée soviétique en mai 1945, il meurt de dénutrition après quelques mois d'internement. Ses travaux sont réunis en 1969 dans The Collected Papers of Gerhard Gentzen.

On veut reconstruire la succession de deux résultats de Gentzen sans attribuer la même date à des travaux distincts. Données : le théorème d'élimination des coupures date de 1934 ; la démonstration de cohérence de l'arithmétique de Peano date de 1936.

1. Associez 1934 au théorème d'élimination des coupures. Dans le calcul des séquents concerné, son résultat permet de transformer une dérivation avec coupure en une dérivation sans coupure ; il ne se confond pas avec le théorème de normalisation en déduction naturelle.

2. Associez 1936 à la cohérence de l'arithmétique de Peano. L'outil annoncé est une induction transfinie jusqu'à l'ordinal ε₀.

3. Ajoutez la restriction donnée par la source : le résultat de 1936 porte sur des formules de faible complexité logique.

Le contrôle est refaisable : 1934 renvoie à l'élimination des coupures dans le calcul des séquents, tandis que 1936 renvoie à la cohérence, à l'induction transfinie et à ε₀. Aucun des deux résultats n'absorbe l'autre.

Dans un cours de logique, le nom de Gentzen sert à situer la déduction naturelle et le calcul des séquents. Si le texte étudie la transformation des dérivations dans ce calcul des séquents, le théorème d'élimination des coupures est le repère le plus précis ; la normalisation en déduction naturelle constitue un résultat distinct, dans un autre cadre formel.

Dans une histoire des fondements, l'année 1936 appelle un autre repère : la cohérence de l'arithmétique de Peano par induction transfinie jusqu'à ε₀. La présence de cette induction distingue ce résultat de celui de 1934.

Dans une lecture biographique, les contributions scientifiques ne doivent pas effacer le contexte politique. L'adhésion de 1937 au parti national-socialiste et la participation au projet V2 font partie du portrait documenté.

Gerhard Gentzen et David Hilbert. Gentzen a été l'assistant de Hilbert, mais les deux noms ne désignent pas la même personne. Un texte qui attribue à Gentzen la déduction naturelle, le calcul des séquents ou l'élimination des coupures parle bien de Gentzen.

Élimination des coupures, normalisation et cohérence de l'arithmétique de Peano. Ce sont des résultats distincts. La date de 1934 et la transformation d'une dérivation en dérivation sans coupure signalent l'élimination des coupures dans le calcul des séquents ; la normalisation concerne notamment la déduction naturelle. L'année 1936, l'induction transfinie et ε₀ signalent le résultat de cohérence.

Une date ne résume pas toute l'œuvre. Le symptôme est une chronologie qui place l'élimination des coupures et la cohérence de l'arithmétique de Peano sous 1934. Il faut conserver 1934 pour le premier résultat et 1936 pour le second. L'élimination des coupures porte ici sur le calcul des séquents et ne doit pas être assimilée au théorème de normalisation en déduction naturelle.

La cohérence n'est pas présentée sans cadre. Omettre l'induction transfinie jusqu'à ε₀ ou la faible complexité logique des formules rend l'énoncé plus large que la source. Ces deux précisions doivent accompagner le résultat de 1936.

Le portrait ne se réduit pas à l'héritage scientifique. Une biographie qui s'arrête aux méthodes de preuve masque l'adhésion au parti national-socialiste et le travail sur le projet V2. Ces faits doivent être maintenus sans les confondre avec les résultats logiques.

La fiche déduction naturelle précise l'un des deux systèmes de logique introduits par Gentzen.

Le portrait Hilbert David situe le mathématicien dont Gentzen fut l'assistant.

L'article Cherche démonstration désespérément prolonge la réflexion sur la démonstration, au cœur des méthodes de Gentzen.