informações gerais
anterior próximo
Translations between Natural Deduction and Sequent Calculus

Abstract: Gentzen's "Untersuchungen" gave a translation from natural deduction to sequent calculus with the property, not commented on by Gentzen, that normal derivations may translate into derivations with cuts. Prawitz 1965 gave a translation that instead produced cut-free derivations. It is shown that by writing all the elimination rules of natural deduction in the manner of disjunction elimination, with an arbitrary consequence, isomorphism between normal derivations and cut-free derivations is achieved. The cuts in Gentzen's translation are thereby explained. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination.