En 1934, 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.

Para ello introduce el cálculo de consecuencias lógicas o secuentes.

Capturado por los soviéticos, murió como prisionero poco después de terminar la guerra.

Establece que toda derivación en el cálculo de consecuencias lógicas puede ser normalizada como una derivación con igual conclusión pero sin utilizar lemas auxiliares.