zbMATH — the first resource for mathematics

Semantic cut elimination in the intuitionistic sequent calculus. (English) Zbl 1114.03044
Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 221-233 (2005).
Summary: Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, which relies on completeness of the cut-free calculus with respect to Kripke models. The proof defines a general framework to extend the cut elimination result to other intuitionistic deduction systems, in particular to deduction modulo provided the rewrite system verifies some properties. We also give an example of a rewrite system for which cut elimination holds but that doesn’t enjoy proof normalization.
For the entire collection see [Zbl 1070.03001].

03F05 Cut-elimination and normal-form theorems
03B20 Subsystems of classical logic (including intuitionistic logic)
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
68Q42 Grammars and rewriting systems
Full Text: DOI