Labelled Sequent Calculi for Propositional Team Logics
This work provides the first labelled sequent calculi for team logics, addressing a gap in proof-theoretic foundations for these logics, though it is limited to finitely many propositional atoms.
The authors present sound and complete labelled sequent calculi for four propositional team logics, including basic inquisitive logic and propositional intuitionistic dependence logic, with admissible weakening, contraction, and cut rules, and provide terminating proof search procedures for simplified label variants.
Team semantics is a general framework where formulas are not interpreted with respect to a single point of evaluation, but with respect to sets of such points. Team semantics is used in dependence logic, to reason about dependencies between variables, and in inquisitive logic, to formalize the meaning of questions. We provide sound and complete labelled sequent calculi for four logics based on team semantics: basic inquisitive logic, propositional intuitionistic dependence logic, and their respective extensions with tensor disjunction. For technical reasons, we restrict ourselves to languages with finitely many propositional atoms. The rules of weakening, contraction and cut are shown to be admissible in each of our calculi. In the last part of the paper, we present terminating proof search procedures for variants of our proof systems, in which labels have a simplified structure.