Gerhard Gentzen
Gerhard Gentzen (24 novembre 1909 à Greifswald - 4 août 1945 à Prague) fut un mathématicien et logicien allemand.
Il fut l'un des étudiants de Weyl à l'université de Göttingen de 1929 à 1933. Il a inventé les méthodes formelles de déduction naturelle avec un calcul de séquences, pour lequel 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. (Recherches sur la déduction logique, aperçu d'ensemble, p.4-5)
Il a ensuite démontré la consistance de l'arithmétique (1936) en appliquant une logique minimale à une structure plus riche que celle des nombres naturels, à savoir les ordinaux inférieurs à ε0, qui est un petit ordinal dénombrable. Son œuvre a fondé la théorie de la preuve et a une grande importance pour la logique et les fondements des mathématiques.
Il est mort dans un camp de prisonnier de guerre, après avoir été arrêté par les soviets à cause de ses loyautés nazies.