Strong cut-elimination in sequent calculus using Klop’s \(\iota \)-translation and perpetual reductions. (English) Zbl 1168.03041

The strong cut-elimination theorem (all sufficiently long reduction sequences terminate) is obviously false: one can infinitely permute two adjacent cuts. A. Dragalin [Mathematical intuitionism. Introduction to proof theory. Translations of Mathematical Monographs, 67. Providence, RI: American Mathematical Society (AMS) (1988; Zbl 0634.03054), Supplement 5] gave a simple proof of a strong cut-elimination with two restrictions. 1. Permuting two adjacent cuts is prohibited. 2. Essential reduction (replacing a cut by smaller cuts) is allowed only when the cut formula does not have predecessors in the premises of the cut.
The present paper treats intuitionistic implicational propositional calculus and proves strong cut elimination for a more complicated set of cut reductions when the second restriction is weakened. The proof transfers to the sequent calculus a strong normalization proof for natural deduction (simply typed \(\lambda\)-calculus) due to W. Klop using a translation to \(\lambda I\)-calculus to take account of the derivations “lost” in \(\beta\)-reduction.


03F05 Cut-elimination and normal-form theorems


Zbl 0634.03054
Full Text: DOI


[1] DOI: 10.1007/3-540-62688-3_48
[2] DOI: 10.1007/978-3-540-24754-8_18
[3] DOI: 10.1016/j.ipl.2006.03.009 · Zbl 1185.68625
[4] Computer science logic 1994 933 pp 61– (1995)
[5] DOI: 10.1023/A:1025693307470 · Zbl 1074.68010
[6] Journal of Logic and Computation 13 pp 59– (2003)
[7] International conference on functional programming pp 233– (2000)
[8] DOI: 10.1017/S0960129500003248 · Zbl 0972.68027
[9] DOI: 10.1016/S0304-3975(01)00012-3 · Zbl 0983.68029
[10] The lambda calculus: Its syntax and semantics (1984)
[11] DOI: 10.1017/S0956796800000186 · Zbl 0941.68542
[12] Fundamenta Informaticae 45 pp 123– (2001)
[13] Lectures on the Curry-Howard isomorphism (2006) · Zbl 1183.03004
[14] DOI: 10.1006/inco.1996.2622 · Zbl 0878.03010
[15] DOI: 10.1006/inco.1998.2750 · Zbl 0920.03024
[16] DOI: 10.1007/978-3-540-24727-2_30
[17] Induction principles as the foundation of the theory of normalisation: Concepts and techniques (2005)
[18] Electronic notes in theoretical computer science 86 (2003)
[19] International conference on foundations of software science and computation structures 4962 pp 380– (2008)
[20] DOI: 10.1007/11916277_9 · Zbl 1165.03345
[21] DOI: 10.1017/S0960129500003273 · Zbl 0972.68102
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.