Non-deterministic Matrices for Semi-canonical Deduction Systems

We use non-deterministic finite-valued matrices to provide uniform effective semantics for a large family of logics, emerging from "well-behaved" sequent systems in which the cut rule and/or the identity-axiom are not present. We exploit this semantics to obtain important proof-theoretic properties of systems of this kind, such as cut-admissibility. Non-determinism is shown to be essential for these purposes, since the studied logics cannot be characterized by ordinary finite-valued matrices. Our results shed light on the dual semantic roles of the cut rule and the identity-axiom, showing that they are crucial for having deterministic (truth-functional) finite-valued semantics.