Gerhard gentzen

Gerhard Gentzen (24 November 1909 in Greifswald, Germany - 4 August 1945 in Prague, Czech Republic) was a German mathematician and logician.

He was a student of Weyl at the University of Göttingen between 1929 and 1933. His main works were in fundamentals of mathematics and proof theory.

In 1934, Gentzen introduced the notion of a system of natural deduction for classical logic and intuitionistic logic. He shows that every test can be written in the normalized form without breaks . For this he introduces the calculation of logical consequences or sequent .

In 1936, Gentzen demonstrated the consistency of elementary number theory.

As part of the German war effort, he was appointed a professor at the German University in Prague. Captured by the Soviets, he died as a prisoner shortly after the war ended.

Cut Elimination Theorem

It establishes that any derivation in the calculation of logical consequences can be normalized as a derivation with the same conclusion but without using auxiliary lemmas.