Studying Sequent Systems via Non-deterministic Multiple-Valued Matrices
Ori Lahav
We consider a family of sequent systems with “well-behaved” logical rules in which the cut rule and/or the identity-axiom are not present. We provide a semantic characterization of the logics induced by these systems in the form of non-deterministic three-valued or four-valued matrices. The semantics is used to study some important proof-theoretic properties of these systems. These results shed light on the dual semantic roles of the cut rule and the identity-axiom, showing that they are both crucial for having deterministic finite-valued semantics.
Keywords: Proof theory, sequent systems, cut-elimination, semantic proofs, non-deterministic semantics, multiple-valued logics