Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions

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

Full description

Saved in:
Bibliographic Details
Published in:The Journal of symbolic logic 2008-09, Vol.73 (3), p.919-932
Main Authors: Sørensen, Morten Heine, Urzyczyn, PaweŁ
Format: Article
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0022-4812
1943-5886
DOI:10.2178/jsl/1230396755