zbMATH — the first resource for mathematics

Strong normalisation of cut-elimination in classical logic. (English) Zbl 0982.03032
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.
References: 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); V. Danos, J.-B. Joinet, and H. Schellinx, “A new deconstructive logic: Linear logic”, J. Symb. Log. 62, No. 3, 755-807 (1997; Zbl 0895.03023).

MSC:
 03F05 Cut-elimination and normal-form theorems 03B40 Combinatory logic and lambda calculus 68Q42 Grammars and rewriting systems 03F52 Proof-theoretic aspects of linear logic and other substructural logics 03F07 Structure of proofs