A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)

Abstract

We introduce a sequent calculus for the propositional team logic with both the split disjunction and the inquisitive disjunction consisting of a Gentzen-style system (G3-like) for classical propositional logic together with two deep-inference rules for the inquisitive disjunction. We show that the system satisfies various desirable properties: it admits height-preserving weakening, contraction and inversion; it supports a procedure for constructing cutfree proofs and countermodels similar to that for G3cp; and cut elimination holds as a corollary of cut elimination for the G3-style subsystem together with a normal form theorem for cutfree derivations. We also prove a sequent interpolation theorem for the system that yields a novel Lyndon's interpolation theorem for the logic as a corollary.