Semantics of Multiplicative Propositional Signed Sequent Calculi with Structural Rules
Alexej P. Pynko
In this paper we study semantics of abstract propositional signed sequent calculi constituted by multiplicative rule schemas including structural rules (explicit Weakening and implicit Contraction and Permutation). Our semantic approach is based upon the concept of signed matrix that is a structure constituted by an algebra of the propositional language involved and subsets of its carrier corresponding to signs under consideration. Defining the notion of validity of a signed sequent in a signed matrix, we come to the conception of soundness of a signed sequent rule with respect to a signed matrix. Our main general result is that every calculus of the kind specified above has a class of signed matrices, viewed as its (essentially, many-valued) semantics, such that a signed sequent rule is derivable in the calculus iff it is sound with respect to each matrix in the class. We apply this general result to calculi associated with singular signed matrices according to [1]. Studying their matrix models, we obtain an algebraic description of their (finite) posets of deductively-complete extensions together with finite semantics and deductive bases with cutelimination property for each of their deductive extensions and also prove that any multiplicative rule schema is admissible in any of their extensions iff it is derivable in it.