pith. sign in

arxiv: 2606.31860 · v1 · pith:X5S3K5KMnew · submitted 2026-06-30 · 💻 cs.LO

Labelled Sequent Calculi for Propositional Team Logics

Fausto Barbero , Marianna Girlando , Valentin M\"uller , Fan Yang This is my paper

Pith reviewed 2026-07-01 02:31 UTC · model grok-4.3

classification 💻 cs.LO
keywords team semanticsinquisitive logicdependence logicsequent calculilabelled systemstensor disjunction
0
0 comments X

The pith

Sound and complete labelled sequent calculi exist for basic inquisitive logic, propositional intuitionistic dependence logic, and their tensor disjunction extensions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs labelled sequent calculi that capture the team-based semantics of four propositional logics. Soundness and completeness are proved for basic inquisitive logic and for propositional intuitionistic dependence logic, together with the versions obtained by adding tensor disjunction. All development is carried out in languages that contain only finitely many propositional atoms, which is required for the termination arguments. The calculi admit weakening, contraction and cut, and variants with simplified labels support terminating proof search.

Core claim

We provide sound and complete labelled sequent calculi for basic inquisitive logic, propositional intuitionistic dependence logic, and their respective extensions with tensor disjunction. 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.

What carries the argument

Labelled sequent calculi whose labels denote teams of worlds and whose rules directly encode the team-semantic clauses for dependence atoms, inquisitive disjunction, and tensor disjunction.

If this is right

  • Validity in the four logics can be checked by searching for derivations in the labelled systems.
  • The admissibility results allow proofs to be written without explicit weakening, contraction or cut steps.
  • The terminating proof-search procedures decide the logics in the finite-atom case.
  • The same labelled framework uniformly treats both inquisitive and dependence logics and their tensor extensions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The finite-atom restriction may be removable by replacing the termination argument with a different well-founded order.
  • The calculi could be extended to first-order team logics by adding rules for quantifiers over teams.
  • Similar labelled systems might be constructed for other team-semantic logics such as inclusion logic.

Load-bearing premise

The language contains only finitely many propositional atoms.

What would settle it

A formula that is valid under team semantics in a language with infinitely many atoms but has no derivation in one of the labelled calculi, or a derivation of a formula that is not valid.

Figures

Figures reproduced from arXiv: 2606.31860 by Fan Yang, Fausto Barbero, Marianna Girlando, Valentin M\"uller.

Figure 1
Figure 1. Figure 1: Hilbert-style axiomatizations. Let now L be any of the logics from [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Labelled sequent calculi. A labelled formula is an expression of the form π : ϕ, where π is a label and ϕ is a formula. Labelled formulas internalise the satisfaction relation into our calculi, so π : ϕ may be read as “The team π satisfies the formula ϕ”. A relational atom is an expression of the form π ⊆ σ, where π and σ are labels, meaning that π is a subset of σ. A sequent is an expression of the form Γ… view at source ↗
Figure 3
Figure 3. Figure 3: The substitution rules and the structural rules of weakening, contraction and cut. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Axioms and rules of our terminating labelled sequent calculi. [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper develops labelled sequent calculi for basic inquisitive logic (InqB), propositional intuitionistic dependence logic (PID), and their tensor-disjunction extensions (InqB^⊗, PID^⊗). It claims to establish soundness, completeness, admissibility of weakening/contraction/cut, and terminating proof search, all under the explicit restriction to languages with finitely many propositional atoms.

Significance. If the rule definitions, cut-elimination arguments, and termination proofs hold as stated, the work supplies the first cut-free labelled systems for these team-semantics logics together with decision procedures. The explicit disclosure of the finiteness restriction and the provision of machine-checkable-style admissibility results (where present) strengthen the contribution; the limitation is treated as a technical boundary rather than concealed.

minor comments (2)
  1. Abstract and introduction should cross-reference the specific sections containing the rule sets, soundness/completeness theorems, and the termination arguments for the simplified-label variants.
  2. Notation for team satisfaction and label semantics is introduced early; a consolidated table of all label operations and their interpretations would improve readability for readers unfamiliar with team semantics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation of minor revision. The report correctly identifies the scope of our results, including the explicit finiteness restriction on the language. Since no specific major comments or requested changes were raised, we have no points to address in detail.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper develops labelled sequent calculi for inquisitive and dependence logics via direct syntactic constructions, followed by explicit proofs of soundness, completeness, admissibility of weakening/contraction/cut, and termination of proof search under the finite-atom restriction. All load-bearing steps are standard proof-theoretic arguments internal to the calculi; the finite-atom limitation is disclosed upfront as required for termination and does not mask any reduction. No self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations appear. The work is a conventional sequent-calculus construction whose central claims rest on the provided proofs rather than on prior results by the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The development rests on the standard definition of team semantics and the usual properties of labelled sequent systems; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Team semantics interprets formulas over sets of assignments rather than single assignments.
    Invoked in the abstract as the semantic foundation for all four logics.
  • ad hoc to paper Finiteness of the propositional atom set is assumed to ensure termination and technical tractability.
    Explicitly stated as a restriction required for the calculi.

pith-pipeline@v0.9.1-grok · 5669 in / 1219 out tokens · 37201 ms · 2026-07-01T02:31:08.621827+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 24 canonical work pages

  1. [1]

    Bulletin of Symbolic Logic 32(1), pp

    Samson Abramsky, Joni Puljujärvi & Jouko Väänänen (2026): Team semantics and independence notions in quantum physics. Bulletin of Symbolic Logic 32(1), pp. 82–135, doi:10.1017/bsl.2025.10089

    work page doi:10.1017/bsl.2025.10089 2026

  2. [2]

    Annals of Pure and Applied Logic 173(10), pp

    Rafael Albert & Erich Grädel (2022): Unifying hidden-variable problems from quantum mechanics by logics of dependence and independence . Annals of Pure and Applied Logic 173(10), pp. 103088:1–30, doi:10.1016/j.apal.2022.103088

    work page doi:10.1016/j.apal.2022.103088 2022

  3. [3]

    Semantics and Pragmatics 15(5), pp

    Maria Aloni (2022): Logic and conversation: The case of free choice. Semantics and Pragmatics 15(5), pp. 5:1–60, doi:10.3765/sp.15.5

    work page doi:10.3765/sp.15.5 2022

  4. [4]

    arXiv:2508.07509

    Aleksi Anttila, Rosalie Iemhoff & Fan Yang (2025): A deep-inference sequent calculus for basic proposi- tional team logic (without delving too deep). arXiv:2508.07509

    arXiv 2025

  5. [5]

    Belnap (1982): Display logic

    Nuel D. Belnap (1982): Display logic . Journal of Philosophical Logic 11, pp. 375–417, doi:10.1007/ BF00284976

    1982

  6. [6]

    In Alexandru Baltag, Jeremy Seligman & Tomoyuki Yamada, editors: Logic, Rationality, and Interaction

    Jinsheng Chen & Minghui Ma (2017): Labelled sequent calculus for inquisitive logic. In Alexandru Baltag, Jeremy Seligman & Tomoyuki Yamada, editors: Logic, Rationality, and Interaction. LORI 2017 , Lecture F. Barbero, M. Girlando, V . Müller & F. Y ang 135 Notes in Computer Science 10455, Springer, Berlin and Heidelberg, pp. 526–540, doi:10.1007/978-3-662...

    work page doi:10.1007/978-3-662- 2017

  7. [7]

    In Samson Abramsky, Juha Kontinen, Jouko Väänänen & Heribert V ollmer, editors: Dependence Logic: theory and applications , Springer International Publishing Switzerland, pp

    Ivano Ciardelli (2016): Dependency as question entailment . In Samson Abramsky, Juha Kontinen, Jouko Väänänen & Heribert V ollmer, editors:Dependence Logic: Theory and Applications , Birkhäuser, Cham, pp. 129–181, doi:10.1007/978-3-319-31803-5_8

    work page doi:10.1007/978-3-319-31803-5_8 2016

  8. [8]

    Ivano Ciardelli (2016): Questions in Logic . Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam. Available at https://eprints.illc.uva.nl/id/eprint/2131/

    2016

  9. [9]

    Notre Dame Journal of Formal Logic 61(1), pp

    Ivano Ciardelli, Rosalie Iemhoff & Fan Yang (2020): Questions and dependency in intuitionistic logic. Notre Dame Journal of Formal Logic 61(1), pp. 75–115, doi:10.1215/00294527-2019-0033

    work page doi:10.1215/00294527-2019-0033 2020

  10. [10]

    Journal of Philosophical Logic 40, pp

    Ivano Ciardelli & Floris Roelofsen (2011): Inquisitive logic. Journal of Philosophical Logic 40, pp. 55–94, doi:10.1007/s10992-010-9142-6

    work page doi:10.1007/s10992-010-9142-6 2011

  11. [11]

    Annals of Pure and Applied Logic 170(9), pp

    Jukka Corander, Antti Hyttinen, Juha Kontinen, Johan Pensar & Jouko Väänänen (2019): A logical approach to context-specific independence . Annals of Pure and Applied Logic 170(9), pp. 975–992, doi:10.1016/j.apal.2019.04.004

    work page doi:10.1016/j.apal.2019.04.004 2019

  12. [12]

    Archive for Mathematical Logic 51, pp

    Roy Dyckhoff & Sara Negri (2012): Proof analysis in intermediate logics. Archive for Mathematical Logic 51, pp. 71–92, doi:10.1007/s00153-011-0254-7

    work page doi:10.1007/s00153-011-0254-7 2012

  13. [13]

    In Jouko Väänänen, Åsa Hirvonen & Ruy de Queiroz, editors:Logic, Language, Information, and Computation

    Sabine Frittella, Giuseppe Greco, Alessandra Palmigiano & Fan Yang (2016): A multi-type calculus for in- quisitive logic. In Jouko Väänänen, Åsa Hirvonen & Ruy de Queiroz, editors:Logic, Language, Information, and Computation. WoLLIC 2016, Lecture Notes in Computer Science 9803, Springer, Berlin and Heidelberg, pp. 215–233, doi:10.1007/978-3-662-52921-8_14

    work page doi:10.1007/978-3-662-52921-8_14 2016

  14. [14]

    Journal of Computer and System Sciences 82(5), pp

    Miika Hannula, Juha Kontinen & Sebastian Link (2016): On the finite and general implication prob- lems of independence atoms and keys . Journal of Computer and System Sciences 82(5), pp. 856–877, doi:10.1016/j.jcss.2016.02.007

    work page doi:10.1016/j.jcss.2016.02.007 2016

  15. [15]

    Logic Journal of IGPL 5(4), pp

    Wilfrid Hodges (1997): Compositional semantics for a language of imperfect information. Logic Journal of the IGPL 5(4), pp. 539–563, doi:10.1093/jigpal/5.4.539

    work page doi:10.1093/jigpal/5.4.539 1997

  16. [16]

    In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer, pp

    Tadeusz Litak & Katsuhiko Sano (2026): Bounded inquisitive logics: Sequent calculi and schematic validity. In Gian Luca Pozzato & Tarmo Uustalu, editors: Automated Reasoning with Analytic Tableaux and Re- lated Methods. TABLEAUX 2025, Lecture Notes in Computer Science 15980, Springer, Cham, pp. 39–58, doi:10.1007/978-3-032-06085-3_3

    work page doi:10.1007/978-3-032-06085-3_3 2026

  17. [17]

    Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam

    Valentin Müller (2023): On the Proof Theory of Inquisitive Logic . Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam. Available at https://eprints.illc.uva.nl/ id/eprint/2278/1/MoL-2023-26.text.pdf

    2023

  18. [18]

    In George Metcalfe, Thomas Studer & Ruy de Queiroz, editors: Logic, Language, Information, and Computation , Springer Nature Switzerland, Cham, pp

    Valentin Müller (2024): Labelled sequent calculi for inquisitive modal logics. In George Metcalfe, Thomas Studer & Ruy de Queiroz, editors: Logic, Language, Information, and Computation. WoLLIC 2024 , Lecture Notes in Computer Science 14672, Springer, Cham, pp. 122–139, doi:10.1007/978-3-031-62687-6_9

    work page doi:10.1007/978-3-031-62687-6_9 2024

  19. [19]

    Journal of Logic and Computation 36(3), p

    Valentin Müller (2026): Geometric theories in inquisitive modal logic . Journal of Logic and Computation 36(3), doi:10.1093/logcom/exaf082

    work page doi:10.1093/logcom/exaf082 2026

  20. [20]

    Archive for Mathematical Logic 42, pp

    Sara Negri (2003): Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Archive for Mathematical Logic 42, pp. 389–401, doi:10.1007/s001530100124

    work page doi:10.1007/s001530100124 2003

  21. [21]

    Journal of Philosophical Logic 34(5), p

    Sara Negri (2005): Proof analysis in modal logic . Journal of Philosophical Logic 34, pp. 507–544, doi:10.1007/s10992-005-2267-3

    work page doi:10.1007/s10992-005-2267-3 2005

  22. [22]

    Bulletin of Symbolic Logic 4(4), pp

    Sara Negri & Jan von Plato (1998): Cut elimination in the presence of axioms . Bulletin of Symbolic Logic 4(4), pp. 418–435, doi:10.2307/420956

    work page doi:10.2307/420956 1998

  23. [23]

    Cambridge University Press, doi:10.1017/cbo9780511527340

    Sara Negri & Jan von Plato (2001): Structural Proof Theory . Cambridge University Press, Cambridge, doi:10.1017/CBO9780511527340. 136 Labelled Sequent Calculi for Team-Based Logics

    work page doi:10.1017/cbo9780511527340 2001

  24. [24]

    In Samson Abramsky, Juha Kontinen, Jouko Väänänen & Heribert V ollmer, editors: Dependence Logic: Theory and Applications, Birkhäuser, Cham, pp

    Eric Pacuit & Fan Yang (2016): Dependence and independence in social choice: Arrow’s theorem. In Samson Abramsky, Juha Kontinen, Jouko Väänänen & Heribert V ollmer, editors: Dependence Logic: Theory and Applications, Birkhäuser, Cham, pp. 235–260, doi:10.1007/978-3-319-31803-5_11

    work page doi:10.1007/978-3-319-31803-5_11 2016

  25. [25]

    Cambridge University Press, Cambridge, doi:10.1017/CBO9781139168717

    Anne Sjerp Troelstra & Helmut Schwichtenberg (1996): Basic Proof Theory. Cambridge University Press, Cambridge, doi:10.1017/CBO9781139168717

    work page doi:10.1017/cbo9781139168717 1996

  26. [26]

    London Mathematical Society Student Texts 70, Cambridge University Press, Cambridge

    Jouko Väänänen (2007): Dependence Logic: A New Approach to Independence Friendly Logic . London Mathematical Society Student Texts 70, Cambridge University Press, Cambridge

    2007

  27. [27]

    In Krzysztof R

    Jouko Väänänen (2008): Modal dependence logic. In Krzysztof R. Apt & Robert van Rooij, editors: New Perspectives on Games and Interaction , Texts in Logic and Games 4, Taylor & Francis, pp. 237–254

    2008

  28. [28]

    Annals of Pure and Applied Logic 173(6), pp

    Fan Yang (2022): Propositional union closed team logics . Annals of Pure and Applied Logic 173(6), pp. 103102:1–35, doi:10.1016/j.apal.2022.103102

    work page doi:10.1016/j.apal.2022.103102 2022

  29. [29]

    Annals of Pure and Applied Logic 167(7), pp

    Fan Yang & Jouko Väänänen (2016): Propositional logics of dependence. Annals of Pure and Applied Logic 167(7), pp. 557–589, doi:10.1016/j.apal.2016.03.003

    work page doi:10.1016/j.apal.2016.03.003 2016

  30. [30]

    Annals of Pure and Applied Logic 168(7), pp

    Fan Yang & Jouko Väänänen (2017): Propositional team logics. Annals of Pure and Applied Logic 168(7), pp. 1406–1441, doi:10.1016/j.apal.2017.01.007

    work page doi:10.1016/j.apal.2017.01.007 2017