Admissibility of structural rules for extensions of contraction-free sequent calculi

&
Logic Journal of the IGPL 9 (4):541-548 (2001)
  Copy   BIBTEX

Abstract

The contraction-free sequent calculus G4 for intuitionistic logic is extended by rules following a general rule-scheme for nonlogical axioms. Admissibility of structural rules for these extensions is proved in a direct way by induction on derivations. This method permits the representation of various applied logics as complete, contraction- and cut-free sequent calculus systems with some restrictions on the nature of the derivations. As specific examples, intuitionistic theories of apartness and order are treated.

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/9.4.541

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

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

Through your library

My notes

Similar books and articles

Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
A minimal classical sequent calculus free of structural rules.Dominic Hughes - 2010 - Annals of Pure and Applied Logic 161 (10):1244-1253.
Contraction-free sequent calculi for geometric theories with an application to Barr's theorem.Sara Negri - 2003 - Archive for Mathematical Logic 42 (4):389-401.
Sequent Calculi And Quasivarieties.Katarzyna Palasinska - 2000 - Reports on Mathematical Logic:107-131.
Distributive-lattice semantics of sequent calculi with structural rules.Alexej P. Pynko - 2009 - Logica Universalis 3 (1):59-94.
Sequent calculus proof theory of intuitionistic apartness and order relations.Sara Negri - 1999 - Archive for Mathematical Logic 38 (8):521-547.
Investigations into a left-structural right-substructural sequent calculus.Lloyd Humberstone - 2007 - Journal of Logic, Language and Information 16 (2):141-171.
Modular Sequent Calculi for Classical Modal Logics.David R. Gilbert & Paolo Maffezioli - 2015 - Studia Logica 103 (1):175-217.
Lambek calculus with restricted contraction and expansion.Andreja Prijatelj - 1992 - Studia Logica 51 (1):125 - 143.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
Intuitionistic sequent calculi for finitely many-valued logics.E. Reznik & P. Curmin - 2001 - Logic Journal of the IGPL 9 (6):793-812.
Labeled sequent calculi for modal logics and implicit contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
A purely syntactic and cut-free sequent calculus for the modal logic of provability.Francesca Poggiolesi - 2009 - Review of Symbolic Logic 2 (4):593-611.
Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics.A. Avellone, M. Ferrari & P. Miglioli - 1999 - Logic Journal of the IGPL 7 (4):447-480.

Analytics

Added to PP
2015-02-04

Downloads
8 (#1,287,956)

6 months
1 (#1,510,037)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references