pith. sign in

arxiv: 2606.31886 · v1 · pith:VOEAZIBXnew · submitted 2026-06-30 · 💻 cs.MA · cs.LO

Analytic Cut in Epistemic Logics with Distributed Knowledge

Ryo Murai (Independent Researcher) , Sizhuo Liu (Hokkaido University) , Katsuhiko Sano (Hokkaido University) This is my paper

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

classification 💻 cs.MA cs.LO
keywords epistemic logicdistributed knowledgesequent calculusanalytic cutCraig interpolationmodal logicK45S5
0
0 comments X

The pith

Sequent calculi for epistemic logics with distributed knowledge admit analytic cut, which yields Craig interpolation.

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

The paper establishes that sequent calculi for epistemic logics of distributed knowledge based on K45, KD45, and S5 satisfy the analytic cut property even though full cut elimination fails. Distributed knowledge is interpreted through the intersection of individual accessibility relations, and the authors adapt a restriction of cut formulas to subformulas of the conclusion sequent to prove the property. If this holds, the Craig interpolation theorem follows directly as a corollary for each system. The same analytic cut results continue to hold when the empty group is permitted, in which case distributed knowledge for the empty group acts as the global modality.

Core claim

We establish the analytic cut property for all three systems by adapting a strategy that restricts the cut formulas to the set of subformulas of the conclusion of the cut rule. As a corollary, the Craig interpolation theorem holds for all logics considered. We also show that all proof-theoretic results remain valid when the empty group is allowed for the distributed-knowledge operator, in which case the distributed knowledge for the empty group is interpreted as the global modality.

What carries the argument

Analytic cut rule restricting cut formulas to subformulas of the conclusion sequent, applied to sequent calculi whose distributed-knowledge rules encode intersection semantics.

If this is right

  • Craig interpolation holds for the three systems based on K45, KD45, and S5.
  • All proof-theoretic results, including analytic cut, continue to hold when the empty group is allowed and distributed knowledge becomes the global modality.
  • The subformula property follows from analytic cut and supports decision procedures for these logics.
  • The sequent systems remain sound and complete with respect to the intersection semantics.

Where Pith is reading between the lines

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

  • The same restriction technique could be tested on other group modalities whose semantics involve intersections or unions of relations.
  • Analytic cut may supply a uniform route to interpolation in related multi-agent logics that currently lack cut elimination.
  • The results suggest that proof search algorithms for these logics can safely limit attention to subformulas once analytic cut is in place.

Load-bearing premise

The restriction of cut formulas to subformulas can be carried over to these calculi without extra complications from the intersection semantics of distributed knowledge.

What would settle it

A concrete sequent in one of the three systems for which every cut-free proof requires a cut formula outside the subformulas of the conclusion, or a pair of formulas in one logic for which no interpolant exists.

read the original abstract

Distributed knowledge is a notion of group knowledge studied in multi-agent epistemic logic. Semantically, the distributed knowledge of a group is interpreted via an accessibility relation given by the intersection of the epistemic accessibility relations of the agents in that group. This paper investigates sequent calculi for epistemic logics of distributed knowledge based on K45, KD45, and S5. While cut elimination holds in existing sequent calculi for modal logics K45 and KD45, it fails in all the systems mentioned above. Instead, we establish the analytic cut property for all three systems by adapting Takano' s (2018) strategy, which restricts the cut formulas to the set of subformulas of the conclusion of the cut rule. As a corollary, the Craig interpolation theorem holds for all logics considered. We also show that all proof-theoretic results remain valid when the empty group is allowed for the distributed-knowledge operator, in which case the distributed knowledge for the empty group is interpreted as the global modality.

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

2 major / 1 minor

Summary. The paper develops sequent calculi for epistemic logics with distributed knowledge extending K45, KD45 and S5. It observes that standard cut elimination fails in these systems but establishes the analytic cut property by adapting Takano's (2018) strategy of restricting cut formulas to subformulas of the cut conclusion. Craig interpolation is obtained as a corollary. The results are claimed to remain valid when the empty group is permitted, interpreting D_∅ as the global modality.

Significance. If the adaptation is shown to succeed without extra lemmas or enlargement of the subformula set, the work supplies a uniform proof-theoretic treatment of distributed knowledge that yields interpolation for these systems. Interpolation is a valuable property for epistemic logics in multi-agent settings. The explicit treatment of the empty-group case is a useful extension.

major comments (2)
  1. [analytic cut proof (adaptation of Takano 2018)] The central claim rests on a direct adaptation of Takano's subformula restriction to the D_G rules. The manuscript must explicitly verify that the intersection-semantics rules for D_G do not generate principal-formula interactions in cut reduction that fall outside the subformula closure of the conclusion; otherwise the restriction fails to be analytic.
  2. [extension to empty group] The extension to the empty group requires a separate check that the global-modality rule does not force additional cut-formula cases beyond those already covered by the subformula property; the manuscript should list the relevant reduction cases.
minor comments (1)
  1. The abstract would be clearer if it briefly indicated the form of the sequent rules adopted for the distributed-knowledge operators.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. The positive assessment of the significance of the results is appreciated. We respond to each major comment below.

read point-by-point responses

  1. Referee: The central claim rests on a direct adaptation of Takano's subformula restriction to the D_G rules. The manuscript must explicitly verify that the intersection-semantics rules for D_G do not generate principal-formula interactions in cut reduction that fall outside the subformula closure of the conclusion; otherwise the restriction fails to be analytic.

    Authors: We agree that an explicit verification strengthens the argument. Although the adaptation of Takano's strategy is direct and the subformula property is preserved by the intersection semantics in our case analysis, the revised manuscript will add a dedicated lemma enumerating the principal-formula interactions for the D_G rules and confirming that all resulting formulas lie within the subformula closure of the cut conclusion. revision: yes

  2. Referee: The extension to the empty group requires a separate check that the global-modality rule does not force additional cut-formula cases beyond those already covered by the subformula property; the manuscript should list the relevant reduction cases.

    Authors: We concur that a separate, explicit listing improves clarity. The revised version will include an additional paragraph or subsection that lists the cut-reduction cases involving the global-modality rule for D_∅ and verifies that no new cut formulas outside the subformula set are generated. revision: yes

Circularity Check

0 steps flagged

No circularity: analytic-cut result obtained by direct adaptation of external Takano (2018) strategy

full rationale

The paper's central claim is a proof-theoretic result obtained by adapting an external reference (Takano 2018) to the new sequent rules for distributed knowledge. No equations, fitted parameters, self-definitional constructions, or load-bearing self-citations appear. The derivation chain consists of standard sequent-calculus manipulations whose validity is established relative to an independent prior result rather than reducing to the paper's own inputs by construction. The empty-group extension is likewise shown to preserve the same external adaptation. This is the normal case of a self-contained proof paper.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the standard modal axioms for K45, KD45, and S5 together with the intersection semantics for distributed knowledge; no free parameters, no new entities, and no ad-hoc axioms are introduced in the abstract.

axioms (2)
  • standard math Standard axioms and rules of K45, KD45, and S5 modal logics
    The paper builds sequent calculi on these established modal bases.
  • domain assumption Distributed knowledge interpreted via intersection of individual accessibility relations
    This is the standard Kripke semantics for the distributed-knowledge operator.

pith-pipeline@v0.9.1-grok · 5714 in / 1338 out tokens · 48639 ms · 2026-07-01T02:23:09.166609+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

34 extracted references · 24 canonical work pages

  1. [1]

    Journal of Logic and Computation 29(7), pp

    Thomas Ågotnes & Natasha Alechina (2016): Coalition Logic with Individual, Distributed and Common Knowledge. Journal of Logic and Computation 29(7), pp. 1041–1069, doi:10.1093/logcom/exv085

    work page doi:10.1093/logcom/exv085 2016

  2. [2]

    Wáng (2017): Resolving Distributed Knowledge

    Thomas Ågotnes & Yì N. Wáng (2017): Resolving Distributed Knowledge. Artificial Intelligence 252, pp. 1–21, doi:10.1016/j.artint.2017.07.002

    work page doi:10.1016/j.artint.2017.07.002 2017

  3. [3]

    Journal of Logic and Computation 31(8), pp

    Thomas Ågotnes & Yì N Wáng (2021): Group Belief. Journal of Logic and Computation 31(8), pp. 1959– 1978, doi:10.1093/logcom/exaa068. R. Murai & S. Liu & K. Sano 653

    work page doi:10.1093/logcom/exaa068 2021

  4. [4]

    In: LPAR23

    Alexandru Baltag & Sonja Smets (2020): Learning What Others Know . In: LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning , EPiC Series in Computing 73, EasyChair, Manchester, UK, pp. 90–119, doi:10.29007/plm4

    work page doi:10.29007/plm4 2020

  5. [5]

    In Uli Fahrenberg, Wesley Fussner & Luigi Santocanale, editors: Relational and Algebraic Methods in Computer Science, 16526, Springer Nature Switzerland, Cham, pp

    Marta Bílková, Wesley Fussner & Roman Kuznets (2026): Agent Interpolation in Distributed Systems. In Uli Fahrenberg, Wesley Fussner & Luigi Santocanale, editors: Relational and Algebraic Methods in Computer Science, 16526, Springer Nature Switzerland, Cham, pp. 95–113, doi:10.1007/978-3-032-22469-9_6

    work page doi:10.1007/978-3-032-22469-9_6 2026

  6. [7]

    Halpern, Yoram Moses & Moshe Y

    Ronald Fagin, Joseph Y . Halpern, Yoram Moses & Moshe Y . Vardi (2003): Reasoning about Knowledge . MIT Press, Cambridge, Mass, doi:10.7551/mitpress/5803.001.0001

    work page doi:10.7551/mitpress/5803.001.0001 2003

  7. [8]

    Halpern & Moshe Y

    Ronald Fagin, Joseph Y . Halpern & Moshe Y . Vardi (1992):What Can Machines Know? On the Properties of Knowledge in Distributed Systems. J. ACM 39(2), pp. 328–376, doi:10.1145/128749.150945

    work page doi:10.1145/128749.150945 1992

  8. [9]

    American Philosophical Quarterly 1(4), pp

    Gerhard Gentzen (1964): Investigations into Logical Deduction. American Philosophical Quarterly 1(4), pp. 288–306

    1964

  9. [10]

    American Philosophical Quarterly 2(3), pp

    Gerhard Gentzen (1965): Investigations into Logical Deduction: II. American Philosophical Quarterly 2(3), pp. 204–218

    1965

  10. [11]

    J. D. Gerbrandy (1999): Bisimulations on Planet Kripke. Amsterdam ILLC Dissertation Series, Amsterdam, The Netherlands

    1999

  11. [12]

    Lietuvos matematikos rinkinys 51, doi:10.15388/LMR.2010.61

    Haroldas Giedra (2010): Cut Free Sequent Calculus for Logic S5n(ED). Lietuvos matematikos rinkinys 51, doi:10.15388/LMR.2010.61

    work page doi:10.15388/lmr.2010.61 2010

  12. [13]

    In Fariba Sadri & Ken Satoh, editors: Computational Logic in Multi-Agent Systems, 5056, Springer Berlin Heidelberg, Berlin, Heidelberg, pp

    Raul Hakli & Sara Negri (2008): Proof Theory for Distributed Knowledge . In Fariba Sadri & Ken Satoh, editors: Computational Logic in Multi-Agent Systems, 5056, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 100–116, doi:10.1007/978-3-540-88833-8_6

    work page doi:10.1007/978-3-540-88833-8_6 2008

  13. [14]

    In Natasha Alechina, Andreas Herzig & Fei Liang, editors: Logic, Rationality, and Interaction, 14329, Springer Nature Switzerland, Cham, pp

    Sizhuo Liu & Katsuhiko Sano (2023): Non-Labelled Sequent Calculi of Public Announcement Expansions of K45 and S5. In Natasha Alechina, Andreas Herzig & Fei Liang, editors: Logic, Rationality, and Interaction, 14329, Springer Nature Switzerland, Cham, pp. 190–206, doi:10.1007/978-3-031-45558-2_15

    work page doi:10.1007/978-3-031-45558-2_15 2023

  14. [15]

    Akio Maruyama (2003): Towards Combined Systems of Modal Logics - a Syntactic and Semantic Study . Ph.D. thesis, School of Information Science, Japan Advanced Institute of Science and Technology

    2003

  15. [16]

    Computer Software 20(1), pp

    Akio Maruyama, Satoshi Tojo & Hiroakira Ono (2003): Temporal epistemic logics for multi-agent mod- els and their efficient proof-search procedure (in Japanese) . Computer Software 20(1), pp. 51–65, doi:10.11309/jssst.20.51

    work page doi:10.11309/jssst.20.51 2003

  16. [17]

    In Andreas Herzig & Juha Kontinen, editors: Foundations of Information and Knowledge Systems , 12012, Springer International Publishing, Cham, pp

    Ryo Murai & Katsuhiko Sano (2020): Craig Interpolation of Epistemic Logics with Distributed Knowledge. In Andreas Herzig & Juha Kontinen, editors: Foundations of Information and Knowledge Systems , 12012, Springer International Publishing, Cham, pp. 211–221, doi:10.1007/978-3-030-39951-1_13

    work page doi:10.1007/978-3-030-39951-1_13 2020

  17. [18]

    Com- putación y Sistemas 26(2), doi:10.13053/cys-26-2-4259

    Ryo Murai & Katsuhiko Sano (2022): Intuitionistic Epistemic Logic with Distributed Knowledge . Com- putación y Sistemas 26(2), doi:10.13053/cys-26-2-4259

    work page doi:10.13053/cys-26-2-4259 2022

  18. [19]

    Presentation slide

    Ryo Murai & Katsuhiko Sano (2023): Subformula Property for Sequent Calculus of Epistemic Logics with Distributed Knowledge S5, K45 and K45D. Presentation slide. The 57th MLG Mathematical Logic Research Meeting

    2023

  19. [20]

    Studia Logica 112(3), pp

    Ryo Murai & Katsuhiko Sano (2024): Intuitionistic Public Announcement Logic with Distributed Knowledge. Studia Logica 112(3), pp. 661–691, doi:10.1007/s11225-023-10066-1

    work page doi:10.1007/s11225-023-10066-1 2024

  20. [21]

    Masao Ohnishi & Kazuo Matsumoto (1959): Gentzen Method in Modal Calculi. II . Osaka Mathematical Journal 11(2), pp. 115–120

    1959

  21. [22]

    In: Theories of Types and Proofs , 2, Mathematical Society of Japan, Tokyo, Japan, pp

    Hiroakira Ono (1998): Proof-Theoretic Methods in Nonclassical Logic – an Introduction . In: Theories of Types and Proofs , 2, Mathematical Society of Japan, Tokyo, Japan, pp. 207–255, doi:10.2969/msjmemoirs/00201C060. 654 Analytic Cut in Epistemic Logics with Distributed Knowledge

    work page doi:10.2969/msjmemoirs/00201c060 1998

  22. [23]

    In: Advances in Modal Logic , 14, College Publications, Rennes, France, pp

    Hiroakira Ono & Katsuhiko Sano (2022): Analytic Cut and Mints’ Symmetric Interpolation Method for Bi- intuitionistic Tense Logic . In: Advances in Modal Logic , 14, College Publications, Rennes, France, pp. 601–623

    2022

  23. [24]

    Informatica 19(4), pp

    Regimantas Pliuškevi ˇcius & Aida Pliuškeviˇcien˙e (2008): Termination of Derivations in a Fragment of Tran- sitive Distributed Knowledge Logic. Informatica 19(4), pp. 597–616, doi:10.15388/Informatica.2008.232

    work page doi:10.15388/informatica.2008.232 2008

  24. [25]

    Journal of Applied Non-Classical Logics 17(2), pp

    Floris Roelofsen (2007): Distributed Knowledge. Journal of Applied Non-Classical Logics 17(2), pp. 255– 273, doi:10.3166/jancl.17.255-273

    work page doi:10.3166/jancl.17.255-273 2007

  25. [26]

    Maehara (1961): Craig no Interpolation Theorem

    Maehara Shoji (1961): Craig No Interpolation Theorem (On Craig’s Interpolation Theorem). Sugaku 12(4), pp. 235–237, doi:10.11429/sugaku1947.12.235

    work page doi:10.11429/sugaku1947.12.235 1961

  26. [27]

    Shvarts (1989): Gentzen Style Systems for K45 and K45D

    Grigori F. Shvarts (1989): Gentzen Style Systems for K45 and K45D . In Albert R. Meyer & Taitslin Michael A., editors: Logic at Botik ’89, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 245–256, doi:10.1007/3-540-51237-3_20

    work page doi:10.1007/3-540-51237-3_20 1989

  27. [28]

    Mathematica Japonica 37(6), pp

    Mitio Takano (1992): Subformula Property as a Substitute for Cut-Elimination in Modal Propositional Log- ics. Mathematica Japonica 37(6), pp. 1129–1145

    1992

  28. [29]

    Bulletin of the Section of Logic 30(2), pp

    Mitio Takano (2001): A Modified Subformula Property for the Modal Logics K5 and K5D . Bulletin of the Section of Logic 30(2), pp. 115–122

    2001

  29. [30]

    Reports on Mathematical Logic 53, pp

    Mitio Takano (2018): A Semantical Analysis of Cut-Free Calculi for Modal Logics. Reports on Mathematical Logic 53, pp. 43–65, doi:10.4467/20842589RM.18.003.8836

    work page doi:10.4467/20842589rm.18.003.8836 2018

  30. [31]

    Journal of Symbolic Logic 70(1), pp

    Balder Ten Cate (2005): Interpolation for Extended Modal Languages. Journal of Symbolic Logic 70(1), pp. 223–234, doi:10.2178/jsl/1107298517

    work page doi:10.2178/jsl/1107298517 2005

  31. [32]

    A. S. Troelstra & Helmut Schwichtenberg (2000): Basic Proof Theory . Cambridge Tracts in Theoretical Computer Science 43, Cambridge University Press, Cambridge, doi:10.1017/CBO9781139168717

    work page doi:10.1017/cbo9781139168717 2000

  32. [33]

    Kosuke Udatsu & Katsuhiko Sano (2025): Craig Interpolation for Awareness Logics. In C. Aiswarya, Pra- bal Kumar Sen & Shashi Mohan Srivastava, editors: Logic and Its Applications , 15402, Springer Nature Switzerland, Cham, pp. 233–246, doi:10.1007/978-3-031-89610-1_17

    work page doi:10.1007/978-3-031-89610-1_17 2025

  33. [34]

    In Abhishek Anant Nowbagh, Ramanujam & Sujata Ghosh, editors: Proceedings of the 7th Asian Workshop on Philosophical Logic (AWPL 2025) , Logic in Asia, Springer

    Wataru Umemura & Katsuhiko Sano (2025): Craig Interpolation for Logics of Distributed Knowledge via Bisimulation Products. In Abhishek Anant Nowbagh, Ramanujam & Sujata Ghosh, editors: Proceedings of the 7th Asian Workshop on Philosophical Logic (AWPL 2025) , Logic in Asia, Springer. Accepted for publication

    2025

  34. [35]

    Wáng & Thomas Ågotnes (2013): Public Announcement Logic with Distributed Knowledge: Expres- sivity, Completeness and Complexity

    Yì N. Wáng & Thomas Ågotnes (2013): Public Announcement Logic with Distributed Knowledge: Expres- sivity, Completeness and Complexity. Synthese 190(S1), pp. 135–162, doi:10.1007/s11229-012-0243-3

    work page doi:10.1007/s11229-012-0243-3 2013