2025/08/10 by A. Anttila, Anttila, Aleksi, Rosalie Iemhoff +3
Computer Science · #03B60 #03F03 (Primary) 03F05 #03F07 (Secondary) #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2508.07509
openalex publication_date 2025/08/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.