Strong Normalisation for a Gentzen-like Cut-Elimination Procedure

Abstract

In this paper we introduce a cut-elimination procedure for classical logic, which is both strongly normalising and consisting of local proof transformations. Traditional cut-elimination procedures, including the one by Gentzen, are formulated so that they only rewrite neighbouring inference rules; that is they use local proof transformations. Unfortunately, such local proof transformation, if defined naïvely, break the strong normalisation property. Inspired by work of Bloo and Geuvers concerning the λx-calculus, we shall show that a simple trick allows us to preserve this property in our cut-elimination procedure. We shall establish this property using the recursive path ordering by Dershowitz.

I should like to thank Roy Dyckhoff for many helpful discussions. I am currently funded with a research fellowship from Corpus Christi College, Cambridge.