Strong normalisation of cut-elimination in classical logic (Q2708321)

In this article first the fact that cut-elimination for classical propositional sequent calculus is, in the presence of explicit contraction rules, not strongly normalising, is revisited. The authors look at various attempts in the literature to remedy this by adding suitable restrictions to the cut-elimination procedure, and criticize them as being too restrictive. Then an interesting notation system for denoting sequent calculus proofs is introduced. This system is some kind of lambda calculus, with the possibility to abstract both on the left and the right side of a sequent. Reductions are introduced, which correspond to cut-elimination steps and are similar to \(\beta\)-reductions in the lambda calculus. It is then shown that the resulting term-rewriting system is strongly normalising. Finally the notation system is extended to the classical first-order sequent calculus, but the proof of strong normalisation is only sketched for that system.NEWLINENEWLINENEWLINEReferences: \textit{J. Gallier}, ``Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)-calculi'', Theor. Comput. Sci. 110, No. 2, 249-339 (1993; Zbl 0772.03026); \textit{V. Danos}, \textit{J.-B. Joinet}, and \textit{H. Schellinx}, ``A new deconstructive logic: Linear logic'', J. Symb. Log. 62, No. 3, 755-807 (1997; Zbl 0895.03023).