Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Gerhard Gentzen
Résumé
Gerhard Gentzen ( à Greifswald - à Prague) est un mathématicien et logicien allemand, dont l'œuvre est fondamentale en théorie de la démonstration. Il fut l’un des étudiants de Weyl à l'université de Göttingen de 1929 à 1933. Il est mort dans un camp de prisonniers de guerre en 1945, après avoir été arrêté par les soviets à cause de ses loyautés nazies.
Gentzen est un élève de Paul Bernays à l'université de Göttingen. Mais ce dernier ayant été renvoyé comme « non- aryen » en , Hermann Weyl devient formellement son directeur de thèse. Gentzen rejoint les sections d'assaut en novembre 1933 alors qu'il n'en était nullement obligé. Néanmoins, il reste en contact avec Bernays jusqu'au début de la Seconde Guerre mondiale. En 1935, il correspond avec Abraham Fraenkel à Jérusalem et est reconnu par le syndicat des enseignants nazis comme celui qui « entretient des contacts avec le Peuple élu ». En 1935 et 1936, Hermann Weyl, directeur du département de mathématiques de Göttingen de 1933 jusqu'à sa démission sous la pression nazie, fait de gros efforts pour le faire aller à l'Institute for Advanced Study à Princeton.
Entre et 1939, il est assistant de David Hilbert à Göttingen. Gentzen rejoint le parti nazi en 1937. En , Gentzen prête serment de loyauté envers Adolf Hitler dans le cadre de son poste à l'Université. À partir de 1943, il est professeur à l'université de Prague. Dans le cadre d'un contrat avec la SS, Gentzen travaille pour le projet V-2.
Après la guerre, il meurt de faim dans un camp après avoir été arrêté à Prague, le .
Gentzen a inventé deux systèmes de déduction pour la logique du premier ordre, la déduction naturelle et le calcul des séquents. Pour ce dernier, il a démontré son Hauptsatz (théorème principal), appelé plus explicitement « théorème d'élimination des coupures », publié en 1934 dans ses Recherches sur la déduction logique.
Gentzen a d'autre part démontré la cohérence de l'arithmétique de Peano (en 1936) en utilisant un principe d'induction jusqu'à l'ordinal dénombrable ε0, mais pour des formules de faible complexité logique.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.