Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic

Roy Dyckhoff, S Negri

Research output: Contribution to journalArticlepeer-review

17 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)1499-1518
Number of pages20
JournalJournal of Symbolic Logic
Volume65
Publication statusPublished - Dec 2000

Keywords

  • PROPOSITIONAL LOGIC
  • CALCULI
  • MODELS

Fingerprint

Dive into the research topics of 'Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic'. Together they form a unique fingerprint.

Cite this