Gentzen

Gentzen

Gerhard Gentzen

Gerhard Gentzen (24 novembre 1909 à Greifswald - 4 août 1945 à Prague) fut un mathématicien et logicien allemand. Son œ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 prisonnier de guerre en 1945, après avoir été arrêté par les soviets à cause de ses loyautés nazies.

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), publié en 1934 dans ses Recherches sur la déduction logique.

Le théorème fondamental affirme que toute démonstration purement logique peut se ramener à une forme normale déterminée, qui n'est d'ailleurs nullement univoque. On peut formuler les propriétés essentielles d'une telle démonstration normale à peu près de la façon suivante : elle ne comporte pas de détours. On n'y introduit aucun concept qui ne soit pas contenu dans son résultat final et qui, par conséquent, ne doive pas nécessairement être utilisé pour obtenir ce résultat.[1]


Gentzen a aussi 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. Les méthodes utilisées pour cette démonstration se sont révélées essentielles pour la théorie de la démonstration moderne.

La théorie dans laquelle cette preuve peut se formaliser est nécessairement plus forte que l'arithmétique de Peano d'après le second théorème d'incomplétude de Gödel (au sens où si elle permet de prouver la cohérence de l'arithmétique de Peano, sa cohérence ne pourra donc se prouver dans cette arithmétique). On a pu voir cette preuve, à laquelle Gödel s'est beaucoup intéressé, comme une tentative pour réhabiliter le programme de Hilbert, en élargissant la notion de méthodes finitaires à des inductions jusqu'à certains ordinaux comme ε0. La cohérence de la théorie utilisée par Gentzen pour sa preuve, bien que plus forte, serait moins douteuse que la cohérence de l'arithmétique de Peano, parce que l'induction, bien que jusqu'à un ordinal (forcément supérieur à celui des entiers), se fait sur des formules simples. Cela n'est plus guère soutenu tel quel. De façon plus objective, cette preuve permet d'analyser la cohérence de l'arithmétique de Peano ; par exemple le résultat de cohérence permet d'en mesurer la "force" par l'ordinal ε0. En généralisant, on a pu ainsi engager une classification des théories arithmétiques.

Théorèmes de Gentzen

Gentzen est connu pour deux théorèmes:

  1. le théorème d'élimination des coupures en calcul des séquents, voir Calcul des séquents
  2. le théorème de cohérence de l'arithmétique

Références

  1. Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France, 1955, p. 4-5.
    Traduit et commenté
     


Voir aussi

  • Portail de l’informatique Portail de l’informatique
  • Portail de la logique Portail de la logique
  • Portail des mathématiques Portail des mathématiques
Ce document provient de « Gerhard Gentzen ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Gentzen de Wikipédia en français (auteurs)

Regardez d'autres dictionnaires:

  • GENTZEN (G.) — 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.… …   Encyclopédie Universelle

  • Gentzen — ist der Familienname folgender Personen: Felix Heinrich Gentzen (1914–1969), deutscher Historiker Gerhard Gentzen (1909–1945), deutscher Mathematiker und Logiker Horst Gentzen (1930–1985), deutscher Schauspieler Siehe auch: Gentzenscher Hauptsatz …   Deutsch Wikipedia

  • Gentzen's — Gentzen, Gerhard …   Philosophy dictionary

  • Gentzen — Gẹntzen,   Gerhard Karl Erich, Mathematiker und Logiker, * Greifswald 24. 11. 1909, ✝ Prag 4. 8. 1945; ab 1943 Dozent in Prag, wo er in der Internierung starb. Gentzen entwickelte in seiner Dissertation den »Kalkül des natürlichen Schließens«,… …   Universal-Lexikon

  • Gentzen's consistency proof — Gentzen s theoremIn 1936 Gerhard Gentzen proved the consistency of first order arithmetic using combinatorial methods. Gentzen s proof shows much more than merely that first order arithmetic is consistent. Gentzen showed that the consistency of… …   Wikipedia

  • Gentzen, Gerhard — (1909–1945) German mathematician, who proved the consistency of classical arithmetic in 1936, relying, however, on transfinite induction . Gentzen was also responsible for the first natural deduction approach to formal logic …   Philosophy dictionary

  • Gerhard Karl Erich Gentzen — (* 24. November 1909 in Greifswald; † 4. August 1945 in Prag) war ein deutscher Mathematiker und Logiker. Inhaltsverzeichnis 1 Mathematische Leistungen 2 Leben 3 Zitat …   Deutsch Wikipedia

  • Gerhard Gentzen — Gerhard Karl Erich Gentzen (* 24. November 1909 in Greifswald; † 4. August 1945 in Prag) war ein deutscher Mathematiker und Logiker. Inhaltsverzeichnis …   Deutsch Wikipedia

  • Felix-Heinrich Gentzen — (* 19. Mai 1914 in Rastenburg; † 2. August 1969) war ein deutscher Historiker. Inhaltsverzeichnis 1 Familie und Kriegsdienst 2 Heimkehr und Studium 3 Lehrtätigkeit …   Deutsch Wikipedia

  • Théorème de Gentzen — Gerhard Gentzen Gerhard Gentzen (24 novembre 1909 à Greifswald 4 août 1945 à Prague) fut un mathématicien et logicien allemand. Son œuvre est fondamentale en théorie de la démonstration. Il fut l un des étudiants de Weyl à l… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”