A cut-elimination proof in intuitionistic predicate logic Original Research Article

In this paper we give a new proof of cut elimination in Gentzenʹs sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.