Cut Elimination Revisited

Jeremy Avigad

Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented. A variation of the double-negation translation is also discussed: if φ is provable classically, then ¬(¬φ)^{nf} is provable in minimal logic, where θ^{nf} denotes the negation-normal form of θ. The translation is used to show that the cut-elimination theorem for classical logic can be viewed as a special case of the cutelimination theorem for intuitionistic logic.

Address: Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, 15213, USA

E-mail: avigad@cmu.edu, www.andrew.cmu.edu/∼avigad