Structural Cut Elimination

We present new variants of known proofs of cut elimination for intuitionistic and classical sequent calculi. In both cases the proofs proceed by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. This makes them amenable to elegant and concise representations in LF, which are given in full detail.

Authors

• Frank Pfenning

Keywords

No keywords are indexed for this paper.