Meeting Strength in Substructural Logics

Abstract

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only a limited possibility to use structural rules. Following the literature, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as the meet of the marked formula with a special type Q. In this way we can make the specific structural behaviour of marked formulas more explicit. The main motivation for our approach is that we can provide a nice intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the 'strong' system in the hybrid one.