Pith. sign in

REVIEW 2 major objections 6 minor 23 references

Agent Interpolation for Knowledge

T0 review · 2 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Every valid implication in multi-agent epistemic logic S5n has an interpolant whose atoms, polarities, and agents all occur in both sides.

desk verdict A real new proof formalism for multi-agent S5 with a solid soundness/completeness/termination core, but the headline ALIP theorem rests on an unproved, non-routine Lemma 23 and a largely delegated interpolation method. read the letter →

arxiv 2505.23401 v1 pith:3PFPE3MJ submitted 2025-05-29 cs.LO math.LO

Marta Bílková , Wesley Fussner , Roman Kuznets This is my paper
classification cs.LOmath.LO MSC 03B4503F0503B70
keywords multi-agentS5agentinterpolationLyndoncrosswordsequentshypersequentsnesteddecidabilityfinitemodelproperty
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper establishes that the multi-agent epistemic logic S5n satisfies the Agent Lyndon Interpolation Property: whenever φ → ψ is valid, there is an interpolant δ whose propositional atoms, with their polarities, and whose agents all occur in both φ and ψ. To get there, the authors build a new proof calculus whose structures, called crossword sequents or cross-sequents, combine hypersequent layers for each agent's equivalence relation with nested-sequent nesting for alternations of different agents. They prove the calculus sound, complete, cut-free, and terminating; failed proof search yields finite countermodels, giving decidability and the finite model property. The interpolation proof runs by splitting every sequent into left and right sides, and it needs a separate lemma ensuring that agents introduced when removing modalities are already shared by both sides of the original implication. Since Lyndon interpolation implies Craig interpolation, the result is the strongest of the standard interpolation properties for multi-agent S5.

What carries the argument

The central object is the crossword sequent, or cross-sequent: a proof structure whose root is a single component and whose other components are arranged in agent-indexed brackets, so that all components inside an a-bracket behave like one hypersequent layer for agent a, while a-brackets can be nested inside other brackets to represent alternations of agents. The rules of ♯S5n act on each agent's component cluster, the set of components mutually accessible for that agent, and are all invertible; saturation conditions control proof search and make it terminate. The interpolation part splits every component at a semicolon and treats the left and right sides as the two sides of the implication; split versions of each rule come with transformations of multiformula interpolants, and Lemma 23 is the load-bearing auxiliary result that guarantees the agent added by a box- or diamond-like transformation already occurs on both sides of the original sequent. The whole argument gives one structure that supports proof search, countermodel extraction, and interpolation simultaneously.

What would settle it

Concretely, a reader could enumerate split proof searches for all depth-0 sequents over two agents with formulas of modal depth at most two; if any proof contains an a-box with a formula that is not a subformula of some $\heartsuit_a\psi$ on the same side of the root, Lemma 23 fails. Alternatively, any valid implication whose every interpolant mentions an agent absent from one side would refute Corollary 25.

Watch

Extended reading notes

Core claim

The central claim is Theorem 24 together with Corollary 25: the cut-free calculus ♯S5n is sound, complete, and strongly terminating for S5n, and every valid implication φ → ψ of multi-agent S5 has an interpolant δ satisfying Var+(δ) ⊆ Var+(φ) ∩ Var+(ψ), Var−(δ) ⊆ Var−(φ) ∩ Var−(ψ), and Ag(δ) ⊆ Ag(φ) ∩ Ag(ψ). The proof uses split cross-sequents, in which every component is divided into a left and right side, and a multiformula built from labelled formulas and conjunctions or disjunctions is carried up the derivation. The subtle point is that the standard multicomponent interpolation transformations, when applied to the modal rules, may introduce a modality for an agent that is not visibly common; the paper's Lemma 23 is the device that forces the agent to be common after all, provided the endsequent has depth 0, meaning it contains no brackets. The same calculus, through saturation and a finite countermodel construction, also yields decidability and the finite model property.

Load-bearing premise

The whole agent-interpolation argument rests on an unproved lemma saying that in any split proof of a bracket-free starting sequent, every formula appearing inside an agent-a box must come from a modal formula over agent a that was already in the corresponding side of that starting sequent.

Editorial extensions

If this is right

  • Every valid S5n implication φ → ψ has a Lyndon interpolant δ and hence a Craig interpolant, with the additional guarantee that Ag(δ) ⊆ Ag(φ) ∩ Ag(ψ).
  • S5n is decidable and has the finite model property, because terminating proof search either proves a sequent or produces a finite saturated leaf from which a finite countermodel is read off.
  • The calculus is cut-free and all its rules are invertible, so weakening, contraction, and cut are admissible and proof search can be made deterministic.
  • For the global consequence relation, the usual deduction-theorem route only yields a restricted deductive interpolation property in which the interpolant's agents are contained in the left-hand premise, not necessarily in the intersection.
  • The obstruction to S5-based distributed knowledge is tied to non-termination: adding group modalities whose knowledge is ordered by group inclusion lets one diamond-formula deposit material arbitrarily deep, breaking the termination argument.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An implicit consequence is that formulas speaking about disjoint sets of agents are separated by an interpolant mentioning no agent at all, giving a way to decompose epistemic specifications along agent signatures.
  • A testable extension would be to use the termination bounds of the calculus to extract explicit elementary decision procedures for S5n, since the paper only notes complexity as future work.
  • The distributed-knowledge obstruction suggests that a proof system for S5-based distributed knowledge needs a richer notion of cluster than the one cross-sequents provide, because ordering group modalities by inclusion makes naive nested proof search diverge.
  • If the stated auxiliary lemma can be proved in full, the same agent-interpolation argument should adapt to extensions of multi-agent K5 that share cluster-style semantics, a direction the paper names as future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper introduces crossword sequents, a proof formalism combining hypersequents and nested sequents, and a cut-free calculus ♯S5n for multi-agent S5. It proves soundness, completeness, cut-free admissibility, strong termination, decidability, and the finite model property for S5n. Its main new result is the Agent Lyndon Interpolation Property (ALIP) for S5n: every valid implication admits an interpolant whose atoms, polarities, and agents occur in both antecedent and consequent. The proof adapts the multicomponent Maehara method from [9] and adds a repair step for □-like and ♢-like rules, relying on a new Lemma 23 that is stated without proof. The paper closes with informal discussions of obstacles for distributed knowledge and for global/deductive interpolation.

Significance. If the missing proof of Lemma 23 is supplied, the ALIP result would be a substantial strengthening of known interpolation results for multi-agent S5, since it includes agents in the common language in addition to polarized atoms. The calculus itself is a valuable contribution: it is terminating and analytic, yields decidability and the finite model property, has admissible cut/weakening/contraction, and all rules are invertible. The paper is honest about its limitations and does not overclaim about distributed knowledge or global consequence. The main weakness is that the central interpolation theorem is conditional on an unproved lemma, so the result is not yet fully established as written.

major comments (2)
  1. [Section 4, Lemma 23] Lemma 23 is stated without proof; the text says only that it 'can be proved by induction on the split derivation.' This lemma is load-bearing for Theorem 24: in case 2 of the repair step, the argument that an agent introduced by a □-like or ♢-like rule is common to both sides of the depth-0 endsequent relies on the asserted existence of formulas ♡x_aψx in L(S) and ♡y_aψy in R(S). The promised induction is not routine, because the ♢-rules copy formulas between components of an a-bracket and each such case must preserve the invariant that every formula on side O inside the bracket has a modal ancestor ♡_aψ on side O in the original endsequent. As written, the ALIP theorem is conditional on this unverified proof obligation; a complete proof of Lemma 23, or an alternative argument, is required.
  2. [Section 4, Lemma 21] Lemma 21 is the engine of the SLIP part of Theorem 24, but its proof is delegated to [9] and only the □-like case is spelled out; the text says the remaining cases go 'along the lines' of Lemmas 4.18, 4.21, 4.24, and 4.27 of [9]. Because the definitions here are adapted to cross-sequents and because Definition 19 adds the new agent-commonality condition 4, the ♢-like case and the verification of condition 4 for all rule types are not actually established in the manuscript. The missing cases should be supplied, or the correspondence with [9] should be made precise enough for a reader to verify the adaptation.
minor comments (6)
  1. [References] Reference [20] misspells the second author's name as 'Scwichtenberg'; it should be 'Schwichtenberg'.
  2. [Section 1] The phrase 'PSPACE-compelete' should be 'PSPACE-complete'.
  3. [Theorem 24] The statement reads 'very split of S'; this should be 'every split of S'.
  4. [Lemma 10] Lemma 10 asserts soundness without giving the proof; a short argument or a pointer to a standard nested-sequent soundness proof would help the reader.
  5. [Definition 18] The symbols '7' and '6' for conjunction and disjunction are nonstandard and may be confused with labels; consider replacing them with ∧ and ∨.
  6. [Section 5] The claim that adding the hierarchy of distributed-knowledge modalities violates termination is supported only by an informal argument; since this section is explicitly future work, it would be clearer to label that discussion as a sketch or conjecture.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the cited multicomponent method is independent of the ALIP claim, and the agent-commonality step is new content, though Lemma 23 is an unproved proof obligation.

full rationale

The derivation chain is not circular. The interpolation proof imports the multicomponent Maehara-style interpolant transformations from [9] (Kuznets 2018), which is a self-citation by one of the present authors; however, [9] supplies an independent, published general method for multicomponent proof-theoretic interpolation and does not assert that S5n has the Agent Lyndon Interpolation Property. The ALIP-specific part of the argument is new: Lemma 23, stated as 'can be proved by induction on the split derivation,' is the load-bearing device that certifies the presence of a common agent modality, and Theorem 24's repair cases are argued in this paper rather than imported. Lemma 23 is indeed unproved and load-bearing for Case 2 of Theorem 24, so the correctness of Theorem 24 and Corollary 25 is conditional on an unverified proof obligation; but an omitted proof is a completeness/correctness risk, not a reduction of the conclusion to the premises. No equation is fitted and then renamed as a prediction, no known result is merely renamed, and no uniqueness theorem is invoked from the authors' prior work. The paper's own calculus, soundness, completeness, termination, and countermodel construction are developed self-containedly, and the interpolation transformation's dependence on [9] does not make the central ALIP claim equivalent to its inputs.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

No free parameters or data fitting. The central contribution is a syntactic formalism plus proofs. The axiomatic load is standard mathematics plus one unproved lemma, Lemma 23, and the assumed transfer of [9]'s method.

assumptions (4)
  • standard math Classical logic with standard induction and set theory
    Used for all proofs in the paper.
  • domain assumption S5_n semantics with equivalence relations and the Hilbert axiomatization (Theorem 2)
    The paper relies on the standard semantic completeness of S5_n without proving it.
  • domain assumption The multicomponent interpolation method of [9] transfers to cross-sequents as stated
    The paper says the method applies 'as is' but does not prove the transfer in detail.
  • ad hoc to paper Lemma 23 (Section 4)
    Stated without proof and load-bearing for the ALIP theorem.
invented entities (1)
  • Crossword sequents (cross-sequents)
    purpose: New proof formalism combining hypersequents for S5 clusters and nested sequents for alternating modalities
    A new syntactic structure. Its usefulness is demonstrated by the paper's theorems, but it makes no falsifiable predictions outside the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Agent Interpolation for Knowledge." pith.science (2026). https://pith.science/paper/3PFPE3MJ

@misc{pith2026250523401,
  author       = {Pith},
  title        = {Pith review of: Agent Interpolation for Knowledge},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3PFPE3MJ}},
  note         = {Machine review of arXiv:2505.23401}
}
read the original abstract

We define a new type of proof formalism for multi-agent modal logics with S5-type modalities. This novel formalism combines the features of hypersequents to represent S5 modalities with nested sequents to represent the T-like modality alternations. We show that the calculus is sound and complete, cut-free, and terminating and yields decidability and the finite model property for multi-agent S5. We also use it to prove the Lyndon (and hence Craig) interpolation property for multi-agent S5, considering not only propositional atoms but also agents to be part of the common language. Finally, we discuss the difficulties on the way to extending these results to the logic of distributed knowledge and to deductive interpolation.

Figures

Figures reproduced from arXiv: 2505.23401 by the authors.

Figure 1
Figure 1. Calculus ♯S5n. All cross-sequents are proper. Only one of the rules □ ∈ a, □ ↗ a, and □ ̸⇝ a can be applied (in the bottom-up direction) to any occurrence of □aφ, depending on its sequent component: □ ∈ a creates another a-sibling if the component already had a-siblings; □ ↗ a creates another a-child if the component already had a-children; □ ̸⇝ a creates the first a-child otherwise. The consolidation conditions mak… view at source ↗
Figure 2
Figure 2. Split calculus ♯S5n with labels. Here ℵ and ℵ ′ represent any number (possibly zero) of brackets indexed with pairwise distinct agents such that the resulting cross￾sequent is proper. 3. If r2 is a disjunctive rule and ℧i IP−→ Si for i = 1, 2, then ℧1 6 ℧2 IP−→ S. 4. If r1 is a □-like rule for k →a l and 7 m i=1(l:φi 6 ℧i) LIP −→ Sp, where l does not occur in any of ℧i, then 7 m i=1(k:□aφi 6 ℧i) LIP −→ S. 5. If r1 i… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

23 extracted references · 15 canonical work pages

  1. [9]

    R. Kuznets. Multicomponent proof-theoretic method for proving interpolation properties. Annals of Pure and Applied Logic, 169(12):1369–1418, December 2018. doi:10.1016/j.apal.2018.08.007

    work page doi:10.1016/j.apal.2018.08.007 2018

  2. [1]

    A. Avron. The method of hypersequents in the proof theory of propositional non- classical logics. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications: European Logic Colloquium, pages 1–32. Clarendon Press, 1996. doi:10.1093/oso/9780198538622.003.0001

    arXiv 1996

  3. [2]

    Brünnler

    K. Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, July 2009.doi:10.1007/s00153-009-0137-3

    doi:10.1007/s00153-009-0137-3 2009

  4. [3]

    W. Craig. Three uses of the Herbrand–Gentzen Theorem in relating model theory and proof theory.Journal of Symbolic Logic, 22(3):269–285, September 1957.doi: 10.2307/2963594

    doi:10.2307/2963594 1957

  5. [4]

    D’Agostino, D

    M. D’Agostino, D. M. Gabbay, R. Hähnle, and J. Posegga, editors. Hand- book of Tableau Methods. Kluwer Academic Publishers, 1999. doi:10.1007/ 978-94-017-1754-0

    work page 1999

  6. [5]

    Dyckhoff

    R. Dyckhoff. A deterministic terminating sequent calculus for Gödel–Dummett logic. Logic Journal of the IGPL, 7(3):319–326, May 1999.doi:10.1093/jigpal/ 7.3.319

    work page doi:10.1093/jigpal/ 1999

  7. [6]

    Fagin, J

    R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi.Reasoning About Knowledge. MIT Press, 1995. doi:10.7551/mitpress/5803.001.0001

    doi:10.7551/mitpress/5803.001.0001 1995

  8. [7]

    M. Fitting. Prefixed tableaus and nested sequents. Annals of Pure and Applied Logic, 163(3):291–313, March 2012.doi:10.1016/j.apal.2011.09.004

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

Show all 23 references
  1. [8]

    Fussner and W

    W. Fussner and W. Zuluaga Botero. Some modal and temporal translations of gen- eralized basic logic. In U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, editors, Relational and Algebraic Methods in Computer Science: 19th International Conference, RAMiCS 2021, Marseille...

    2021

  2. [10]

    Lellmann and F

    B. Lellmann and F. Poggiolesi. Nested sequents or tree-hypersequents—a survey. In Y. Weiss and R. Birman, editors,Saul Kripke on Modal Logic, volume 30 of Outstanding Contributions to Logic, pages 243–301. Springer, 2024.doi:10.1007/ 978-3-031-57635-5_11

    2024

  3. [11]

    R. C. Lyndon. An interpolation theorem in the predicate calculus.Pacific Journal of Mathematics, 9(1):129–142, March 1959.doi:10.2140/pjm.1959.9.129

    1959 doi

  4. [12]

    S. Maehara. On the interpolation theorem of Craig.Sugaku, 12(4):235–237, May

  5. [13]

    G. E. Minc. On some calculi of modal logic. In V. P. Orevkov, editor,The Calculi of Symbolic Logic. I, number 98 (1968) in Proceedings of the Steklov Institute of Mathematics, pages 97–124. American Mathematical Society, 1971. URL:https: //www.mathnet.ru/eng/tm/v98/p88

    1968

  6. [14]

    Murai and K

    R. Murai and K. Sano. Craig interpolation of epistemic logics with distributed knowledge. In A. Herzig and J. Kontinen, editors,Foundations of Information and Knowledge Systems: 11th International Symposium, FoIKS 2020, Dortmund, Ger- many, February 17–21, 2020, Proceedings, v...

    2020 doi

  7. [15]

    S. Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5– 6):507–544, October 2005. doi:10.1007/s10992-005-2267-3. Agent Interpolation for Knowledge 17

    2005 doi

  8. [16]

    Proof Analysis: A Contribution to Hilbert’s Last Problem

    S.NegriandJ.vonPlato. Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge University Press, 2011.doi:10.1017/CBO9781139003513

    2011 doi

  9. [17]

    Poggiolesi

    F. Poggiolesi. The method of tree-hypersequents for modal propositional logic. In D. Makinson, J. Malinowski, and H. Wansing, editors,Towards Mathematical Phi- losophy: Papers from the Studia Logica conferenceTrends in Logic IV, volume 28 of Trends in Logic, pages 31–51. Sprin...

    2009 doi

  10. [18]

    Poggiolesi

    F. Poggiolesi. From single agent to multi-agent via hypersequents.Logica Univer- salis, 7(2):147–166, June 2013.doi:10.1007/s11787-012-0047-8

    2013 doi

  11. [19]

    Pottinger

    G. Pottinger. Uniform, cut-free formulations ofT, S4, andS5. Journal of Symbolic Logic, 48(3):900, September 1983. Abstract.doi:10.2307/2273495

    1983 doi

  12. [20]

    A. S. Troelstra and H. Scwichtenberg.Basic Proof Theory, volume 43 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2nd edition,

  13. [1961]

    doi:10.11429/sugaku1947.12.235

    In Japanese. doi:10.11429/sugaku1947.12.235

    doi

  14. [2000]

    doi:10.1017/CBO9781139168717

    doi

  15. [2021]

    doi:10.1007/978-3-030-88701-8_11

    doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.