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

TL;DR

This paper develops a deep-inference sequent calculus for propositional team logic, combining classical logic with inquisitive disjunction, and proves key properties including cut elimination and interpolation.

Contribution

It introduces a novel G3-like deep-inference calculus for propositional team logic with inquisitive disjunction, establishing foundational proof-theoretic properties.

Findings

Supports height-preserving weakening, contraction, and inversion

Allows construction of cutfree proofs and countermodels

Proves a Lyndon's interpolation theorem for the logic

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.