pith. sign in

arxiv: 2606.31868 · v1 · pith:OJRXZ3M4new · submitted 2026-06-30 · 💻 cs.LO

Labelled Sequents for Inquisitive First-Order Modal Logic

Ivano Ciardelli (University of Padua) , Simone Conti (University of Padua) This is my paper

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

classification 💻 cs.LO
keywords inquisitive logicmodal logicsequent calculuslabelled sequentscompletenesscut admissibilityfirst-order logic
0
0 comments X

The pith

A labelled sequent calculus is complete for inquisitive first-order modal logic and admits cut.

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

The paper constructs a proof system for a logic that captures modal dependence relations such as global supervenience among predicate extensions across possibilities. It extends an existing labelled sequent calculus for a weaker inquisitive first-order logic by adding rules for modal operators. Strong completeness is shown for the full system, together with the invertibility of all rules and the admissibility of cut. This supplies a syntactic method for establishing validities in the logic without relying solely on semantic arguments.

Core claim

We provide a complete labelled sequent calculus for inquisitive first-order modal logic, extending a calculus developed for a weak version of inquisitive first-order logic. We prove strong completeness for the calculus and show that it enjoys desirable structural properties, including the invertibility of its rules and the admissibility of cut.

What carries the argument

The labelled sequent calculus that tracks accessibility and dependence via labels and extends prior rules to full modal operators.

If this is right

  • Every valid formula in the logic has a finite derivation in the calculus.
  • All rules can be applied in either direction during proof search.
  • Cut elimination holds, so derivations can be restricted to cut-free proofs.
  • The system supports systematic enumeration of theorems.

Where Pith is reading between the lines

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

  • The calculus could support implementation of a decision procedure or automated prover for dependence statements.
  • Similar labelled extensions might be attempted for other variants of inquisitive modal logics with different dependence atoms.

Load-bearing premise

Adding the modal rules to the existing calculus preserves completeness and does not create gaps or allow derivation of invalid formulas.

What would settle it

A concrete formula valid under inquisitive first-order modal semantics that the calculus fails to prove, or an invalid formula that the calculus derives.

read the original abstract

In recent work, an inquisitive first-order modal logic has been proposed to reason about relations of modal dependence, including the notion of global supervenience (functional dependence among the extensions of predicates relative to a space of possibilities). At present, no proof system exists for this logic. We provide a complete labelled sequent calculus, extending a calculus developed by Litak and Sano for a weak version of inquisitive first-order logic. We prove strong completeness for the calculus and show that it enjoys desirable structural properties, including the invertibility of its rules and the admissibility of cut.

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

1 major / 0 minor

Summary. The manuscript presents a labelled sequent calculus for inquisitive first-order modal logic by extending the calculus developed by Litak and Sano for a weak version of inquisitive first-order logic. It claims to prove strong completeness for the calculus and to establish structural properties including the invertibility of its rules and the admissibility of cut.

Significance. If the claimed results hold, the work would supply the first proof system for this logic, supporting formal reasoning about modal dependence relations such as global supervenience. Extending labelled sequent methods in this way aligns with standard techniques in modal logic and would be a useful addition if the completeness argument is verified.

major comments (1)
  1. [Abstract] Abstract: the abstract asserts proofs of strong completeness and structural properties, but without access to the full derivations, rule definitions, or any verification details, the support for the claims cannot be assessed.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. We address the single major comment below, clarifying that the full manuscript supplies the requested details.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the abstract asserts proofs of strong completeness and structural properties, but without access to the full derivations, rule definitions, or any verification details, the support for the claims cannot be assessed.

    Authors: The manuscript defines the labelled sequent rules in Section 3. Strong completeness (via canonical model construction and truth lemma) is proved in full in Section 4. Rule invertibility appears in Section 5.1 and cut admissibility in Section 5.2. These sections contain the complete derivations and verification details that support the abstract's summary. The full text is available on arXiv. revision: no

Circularity Check

0 steps flagged

No significant circularity; derivation extends external prior work

full rationale

The paper's core contribution is a labelled sequent calculus obtained by extending the system of Litak and Sano (distinct authors) for a weaker logic, followed by a standard strong-completeness proof and verification of structural properties such as rule invertibility and cut admissibility. No self-definitional equations, fitted inputs renamed as predictions, or load-bearing self-citations appear in the abstract or description. The cited foundation is external and the methods are conventional proof-theoretic extensions, rendering the derivation self-contained against the referenced prior calculus.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no specific free parameters, axioms, or invented entities can be identified from the provided text.

pith-pipeline@v0.9.1-grok · 5625 in / 989 out tokens · 40853 ms · 2026-07-01T03:07:33.395700+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

33 extracted references · 29 canonical work pages

  1. [1]

    Philosophy and Phenomenological Research 68(3), pp

    Karen Bennett (2004): Global supervenience and dependence. Philosophy and Phenomenological Research 68(3), pp. 501–529, doi:10.1111/j.1933-1592.2004.tb00364.x

    work page doi:10.1111/j.1933-1592.2004.tb00364.x 2004

  2. [2]

    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 , Springer International Publishing Switzerland, pp. 129–181, doi:10.1007/978-3-319-31803-5_8

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

  3. [3]

    In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe & Thomas Studer, editors: Advances in Modal Logic (AIML) , College Publi- cations, London, pp

    Ivano Ciardelli (2018): Dependence Statements Are Strict Conditionals. In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe & Thomas Studer, editors: Advances in Modal Logic (AIML) , College Publi- cations, London, pp. 123–142. Available at http://www.aiml.net/volumes/volume12/

    2018

  4. [4]

    Consequence and inference in the realm of questions

    Ivano Ciardelli (2023): Inquisitive Logic. Consequence and inference in the realm of questions. Springer, doi:10.1007/978-3-031-09706-5

    work page doi:10.1007/978-3-031-09706-5 2023

  5. [5]

    The Review of Symbolic Logic 18(2), p

    Ivano Ciardelli (2025): Global Supervenience in Inquisitive Modal Logic . The Review of Symbolic Logic 18(2), p. 589–615, doi:10.1017/S175502032500005X

    work page doi:10.1017/s175502032500005x 2025

  6. [6]

    Journal of Logic, Language and Information 34(5), p

    Ivano Ciardelli (2025): Inquisitive Neighborhood Logic. Journal of Logic, Language and Information 34(5), p. 419–461, doi:10.1007/s10849-025-09440-0

    work page doi:10.1007/s10849-025-09440-0 2025

  7. [7]

    Annals of Pure and Applied Logic 173(9), p

    Ivano Ciardelli & Gianluca Grilletti (2022): Coherence in inquisitive first-order logic. Annals of Pure and Applied Logic 173(9), p. 103155, doi:10.1016/j.apal.2022.103155

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

  8. [8]

    2003 , pages =

    Ivano Ciardelli, Jeroen Groenendijk & Floris Roelofsen (2018): Inquisitive Semantics. Oxford University Press, doi:10.1093/oso/9780198814788.001.0001

    work page doi:10.1093/oso/9780198814788.001.0001 2018

  9. [9]

    Synthese 192(6), pp

    Ivano Ciardelli & Floris Roelofsen (2015): Inquisitive dynamic epistemic logic. Synthese 192(6), pp. 1643– 1687, doi:10.1007/s11229-014-0404-7. 260 Labelled Sequents for Inquisitive First-Order Modal Logic

    work page doi:10.1007/s11229-014-0404-7 2015

  10. [10]

    In Valeria Gradimondo & Emil Rosina, editors: Proceedings of the ESSLLI 2025 Student Session , pp

    Simone Conti (2025): Completeness for Weak Inquisitive First-Order Logic . In Valeria Gradimondo & Emil Rosina, editors: Proceedings of the ESSLLI 2025 Student Session , pp. 70–79. Available at https: //philpapers.org/rec/GRAPOT-20

    2025

  11. [11]

    Annals of Pure and Applied Logic 163(1), pp

    Pietro Galliani (2012): Inclusion and exclusion dependencies in team semantics – on some logics of imperfect information. Annals of Pure and Applied Logic 163(1), pp. 68–84, doi:10.1016/j.apal.2011.08.005

    work page doi:10.1016/j.apal.2011.08.005 2012

  12. [12]

    In: 2012 27th Annual IEEE Symposium on Logic in Computer Science , IEEE, Dubrovnik, Croatia, pp

    Deepak Garg, Valerio Genovese & Sara Negri (2012): Countermodels from Sequent Calculi in Multi-Modal Logics. In: 2012 27th Annual IEEE Symposium on Logic in Computer Science , IEEE, Dubrovnik, Croatia, pp. 315–324, doi:10.1109/LICS.2012.42

    work page doi:10.1109/lics.2012.42 2012

  13. [13]

    Studia Logica 101(2), pp

    Erich Grädel & Jouko Väänänen (2013): Dependence and independence. Studia Logica 101(2), pp. 399–410, doi:10.1007/s11225-013-9479-2

    work page doi:10.1007/s11225-013-9479-2 2013

  14. [14]

    Studia Logica, pp

    Gianluca Grilletti (2017): Disjunction and Existence Properties in Inquisitive First-Order Logic . Studia Logica, pp. 1–36, doi:10.1007/s11225-018-9835-3

    work page doi:10.1007/s11225-018-9835-3 2017

  15. [15]

    Journal of Logic, Language, and Information 30, pp

    Gianluca Grilletti (2021): Completeness for the Classical Antecedent Fragment of Inquisitive First-Order Logic. Journal of Logic, Language, and Information 30, pp. 725–751, doi:10.1007/s10849-021-09341-y

    work page doi:10.1007/s10849-021-09341-y 2021

  16. [16]

    The Review of Symbolic Logic 16(1), pp

    Gianluca Grilletti & Ivano Ciardelli (2023): Games and cardinalities in inquisitive first-order logic . The Review of Symbolic Logic 16(1), pp. 241–267, doi:10.1017/S1755020321000198

    work page doi:10.1017/s1755020321000198 2023

  17. [17]

    Logic Journal of IGPL 5(4), pp

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

    work page doi:10.1093/jigpal/5.4.539 1997

  18. [18]

    Philosophy and phenomenological research 45(2), pp

    Jaegwon Kim (1984): Concepts of supervenience . Philosophy and phenomenological research 45(2), pp. 153–176, doi:10.2307/2107423

    work page doi:10.2307/2107423 1984

  19. [19]

    Studia Logica 101(2), pp

    Jarmo Kontinen (2013): Coherence and computational complexity of quantifier-free dependence logic for- mulas. Studia Logica 101(2), pp. 267–291, doi:10.1007/s11225-013-9481-8

    work page doi:10.1007/s11225-013-9481-8 2013

  20. [20]

    115–129, doi:10.1007/s11229-008-9360-4

    Stephan Leuenberger (2009): What is global supervenience? Synthese 170(1), pp. 115–129, doi:10.1007/s11229-008-9360-4

    work page doi:10.1007/s11229-008-9360-4 2009

  21. [21]

    Oxford University Press

    David Lewis (1986): Philosophical Papers Volume II. Oxford University Press

    1986

  22. [22]

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

    Tadeusz Litak & Katsuhiko Sano (2025): Bounded inquisitive logics: Sequent calculi and schematic valid- ity. In: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer, pp. 39–58, doi:10.1007/978-3-032-06085-3_3

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

  23. [23]

    McLaughlin (1997): Supervenience, Vagueness, and Determination

    Brian P. McLaughlin (1997): Supervenience, Vagueness, and Determination. Philosophical Perspectives 11, pp. 209–230. Available at http://www.jstor.org/stable/2216131

    arXiv 1997

  24. [24]

    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 , Springer Nature Switzerland, 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

  25. [25]

    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), p. exaf082, doi:10.1093/logcom/exaf082

    work page doi:10.1093/logcom/exaf082 2026

  26. [26]

    Journal of Philosophical Logic 34(5), p

    Sara Negri (2005): Proof Analysis in Modal Logic . Journal of Philosophical Logic 34(5), p. 507, doi:10.1007/s10992-005-2267-3

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

  27. [27]

    Logica Universalis 8(1), pp

    Sara Negri (2014): Proofs and Countermodels in Non-Classical Logics. Logica Universalis 8(1), pp. 25–60, doi:10.1007/s11787-014-0097-1

    work page doi:10.1007/s11787-014-0097-1 2014

  28. [28]

    Cambridge University Press, doi:10.1017/cbo9780511527340

    Sara Negri & Jan von Plato (2001): Structural Proof Theory . Cambridge University Press, doi:10.1017/cbo9780511527340

    work page doi:10.1017/cbo9780511527340 2001

  29. [29]

    Journal of Philosophical Logic 45(4), pp

    Vít Pun ˇcocháˇr (2016): A generalization of inquisitive semantics . Journal of Philosophical Logic 45(4), pp. 399–428, doi:10.1007/s10992-015-9379-1

    work page doi:10.1007/s10992-015-9379-1 2016

  30. [30]

    The Review of Symbolic Logic 12(2), pp

    Vít Pun ˇcocháˇr (2019): Substructural inquisitive logics. The Review of Symbolic Logic 12(2), pp. 296–330, doi:10.1017/S1755020319000017. I. Ciardelli, S. Conti 261

    work page doi:10.1017/s1755020319000017 2019

  31. [31]

    Philosophical perspectives 10, pp

    Robert Stalnaker (1996): Varieties of supervenience . Philosophical perspectives 10, pp. 221–241, doi:10.2307/2216245

    work page doi:10.2307/2216245 1996

  32. [32]

    Cambridge University Press, doi:10.1017/CBO9780511611193

    Jouko Väänänen (2007): Dependence Logic: A New Approach to Independence Friendly Logic. Cambridge University Press, doi:10.1017/CBO9780511611193

    work page doi:10.1017/cbo9780511611193 2007

  33. [33]

    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