Strong normalisation of cut-elimination in classical logic

MaRDI QIDQ2708321zbMATH OpenFDO

Authors C. Urban, Gavin M. Bierman

Publication date 14 March 2002

Published in Fundamenta Informaticae (Search for Journal in Brave)

zbMATH Keywords

contraction rulecut-eliminationlambda calculuslinear logicnormalisationnotation systemsterm-rewriting

Mathematics Subject Classification ID

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

Review text

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).

Recommendations

• scientific article; zbMATH DE number 1342291
• scientific article; zbMATH DE number 1722668
• A short proof of the strong normalization of classical natural deduction with disjunction
• A strong normalization result for classical logic
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction

Cited in

(23)

• The computational content of arithmetical proofs
• A strong normalization result for classical logic
• Some general results about proof normalization
• Proof nets for classical logic
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• scientific article; zbMATH DE number 1302675 (Why is no real title available?)
• scientific article; zbMATH DE number 1342291 (Why is no real title available?)
• SN and CR for free-style LK^tq: linear decorations and simulation of normalization
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• Cut elimination, substitution and normalisation
• Expansion trees with cut
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Proof theory in the abstract
• Strong normalisation in the \(\pi\)-calculus
• A minimal classical sequent calculus free of structural rules
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Invertibility in Sequent Calculi
• Categorical proof theory of classical propositional calculus
• On the form of witness terms

This page was built for publication: Strong normalisation of cut-elimination in classical logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2708321)