|
|
 |
 |
 |
|
 |
|
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.
|
|
|
|
 |
|
 |