Cut-elimination and a permutation-free sequent calculus for intuitionistic logic

Abstract

We describe a sequent calculus, based on work of Herbelin's, of which the cut-free derivations are in 1-1 correspondence with normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path oredering theorem of Dershowitz.