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

Dyckhoff, Roy; Negri, Sara

J. Symbolic Logic, Tome 65 (2000) no. 1, p. 1499-1518 / Harvested from Project Euclid

Résumé

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.

Publié le : 2000-12-14
Classification:

@article{1183746249,
     author = {Dyckhoff, Roy and Negri, Sara},
     title = {Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic},
     journal = {J. Symbolic Logic},
     volume = {65},
     number = {1},
     year = {2000},
     pages = { 1499-1518},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746249}
}

Dyckhoff, Roy; Negri, Sara. Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. J. Symbolic Logic, Tome 65 (2000) no. 1, pp.  1499-1518. http://gdmltest.u-ga.fr/item/1183746249/