Strong normalization proofs for cut elimination in Gentzen's sequent calculi
Volume 46 / 1999
Banach Center Publications 46 (1999), 179-225
DOI: 10.4064/-46-1-179-225
Abstract
We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $
