Premium
Translations from natural deduction to sequent calculus
Author(s) -
von Plato Jan
Publication year - 2003
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200310047
Subject(s) - sequent , sequent calculus , natural deduction , cut elimination theorem , mathematics , translation (biology) , calculus (dental) , property (philosophy) , pure mathematics , discrete mathematics , proof calculus , philosophy , geometry , mathematical proof , medicine , dentistry , biochemistry , chemistry , epistemology , messenger rna , gene
Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut‐free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut‐free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the cuts in Gentzen's translation. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination.