Strong Normalisation of Cut-Elimination in Classical Logic

Abstract

. In this paper a strongly normalising cut-elimination procedure is presented for classical logic. The procedure adapts the standard cut transformations, see for example [12]. In particular our cutelimination procedure requires no special annotations on formulae. We design a term calculus for a variant of Kleene's sequent calculus G3 via the Curry-Howard correspondence and the cut-elimination steps are given as rewrite rules. In the strong normalisation proof we adapt the symmetric reducibility candidates developed by Barbanera and Berardi. 1 Introduction Gentzen has shown in his seminal paper [10] that all cuts can be eliminated from proofs in LK and LJ. Since then many Hauptsatze (cut-elimination theorems) have appeared for various sequent calculus formulations. Most of them, including Gentzen's original, provide a cut-elimination procedure which is weakly normalising, i.e., they employ a particular reduction strategy (for example an inner-most reduction strategy or the elimination...