Biografía de Gerhard Gentzen

Establece que toda derivación en el cálculo de consecuencias lógicas puede ser normalizada como una derivación igual conclusión pero sin utilizar lemas auxiliares. Sus principales trabajos fueron en fundamentos de la matemática y la teoría de la demostración, Gentzen introduce la noción de sistema de deducción natural para lógica clásica y lógica intuicionista. Demuestra que toda prueba puede escribirse de manera normalizada sin cortes por ello introduce el cálculo de consecuencias lógicas o se cuentes.