Admissibility of structural rules for extensions of contraction-free sequent calculi (Q2743638)

The cut-free nature of the sequent calculus is easily destroyed by adding new rules. If it is not, however, the conservativity of the extension may be shown affirmatively as an immediate consequence. In fact, some conservativity problems with respect to apartness over equality and positive counterparts of order have been solved affirmatively from this approach by the second author and Jan von Plato. In this paper the authors extend the contraction-free sequent calculus G4 for intuitionistic logic by rules follwing a general rule-schema for nonlogical axioms and prove the admissibility of structural rules for them 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.