Christian Urban - Strong Normalisation of Cut-Elimination in Classical Logic
The talk will concentrate on a sequent-calculus formulation for classical logic where the cut-elimination procedure is strongly normalising. Gentzen has shown in 1934 that all cuts can be eliminated from proofs in LK and LJ. Since then many cut-elimination theorems have appeared for various sequent-calculus formulations. Most of them, including Gentzen's original, provide a cut-elimination procedure which is only weakly normalising.
In intuitionistic logic we know by the Curry-Howard correspondence that the notion of cut-elimination is closely related to the notion of reduction of typed lambda-terms. As a consequence we have a precise computational meaning for the corresponding cut-elimination procedure and strong normalisation results become desirable. Recent approaches attempt to extend the Curry-Howard correspondence to classical logic. However, it is rather difficult to design a reduction system for classical logic which is strongly normalising. Therefore all those approaches impose some from of restriction on the cut-elimination rules to ensure strong normalisation. In my talk I shall present a term-calculus for classical logic and the cut-elimination steps will be given as rewrite rules. The cut-elimination procedure adapts the standard cut-transformations and no additional information is required to guide the cut-elimination process. The talk will conclude with some remarks on the computational meaning of the presented cut-elimination procedure.