Article contents
Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
Published online by Cambridge University Press: 12 March 2014
Abstract
There is a simple technique, due to Dragalin. for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop's ι-translation and perpetual reductions.
These tools are of independent interest and have proved useful in a variety of settings; it is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2008
References
REFERENCES
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20151019083351860-0135:S0022481200004254_inline1.gif?pub-status=live)
- 2
- Cited by