On a local-step cut-elimination procedure for the intuitionistic sequent calculus

In this paper we investigate, for intuitionistic implicational logic, the relationship between normalization in natural deduction and cut-elimination in a standard sequent calculus. First we identify a subset of proofs in the sequent calculus that correspond to proofs in natural deduction. Then we define a reduction relation on those proofs that exactly corresponds to normalization in natural deduction. The reduction relation is simulated soundly and completely by a cut-elimination procedure which consists of local proof transformations. It follows that the sequent calculus with our cut-elimination procedure is a proper extension that is conservative over natural deduction with normalization.