A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION
Jan von Plato · The Review of Symbolic Logic · 2010
Gentzen’s thesis proved the equivalence of natural deduction, sequent calculus, and axiomatic logic through a cycle of translations. Mysteriously, even normal derivations in natural deduction got translated into sequent derivations with cuts. It is shown that the insertion of special cuts, whenever left conjunction, left implication, or left universal quantification in sequent calculus is used, results in sequent calculus derivations isomorphic to those in Gentzen’s natural deduction. Thereby the appearance of the cuts in translation is explained.