Admissibility of structural rules for contraction-free systems of intuitionistic logic

Journal of Symbolic Logic 65 (4):1499-1518 (2000)
  Copy   BIBTEX

Abstract

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
59 (#243,326)

6 months
3 (#439,386)

Historical graph of downloads
How can I increase my downloads?