Gentzen, Gerhard

matematico e logico tedesco (Greifswald 1909-Praga 1945). È noto soprattutto per l'elaborazione (1935) di calcoli formali, detti di deduzione naturale, che gli consentirono di ottenere notevoli risultati nella teoria della dimostrazione. Gentzen sviluppò due tipi di calcoli, che ha chiamato N e L; i calcoli L derivano dai calcoli N mediante l'applicazione di altre regole, tra le quali è peculiare quella di sezione, consistente in una forma generalizzata del modus ponens. Grazie a questi metodi poté dimostrare la consistenza della logica dei predicati classica e intuizionista, definire un nuovo metodo di decisione per il calcolo proposizionale intuizionista e da ultimo dimostrare la consistenza dell'aritmetica (1936) per la quale utilizzò, però, un principio di induzione transfinita irriducibile all'induzione ordinaria all'interno del sistema considerato.