Paper deep dive
Analytic Cut in Epistemic Logics with Distributed Knowledge
Ryo Murai, Sizhuo Liu, Katsuhiko Sano
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 98%
Last extracted: 7/5/2026, 1:37:51 AM
Summary
The paper investigates the analytic cut property in epistemic logics with distributed knowledge, specifically for the systems K45D, KD45D, and S5D. The authors demonstrate that while standard cut elimination fails for these systems, an analytic cut property (where the cut formula is a subformula of the conclusion) can be established by adapting Takano's (2018) strategy. This result implies the validity of the Craig interpolation theorem for these logics. Additionally, the paper shows that the distributed knowledge operator remains well-behaved when the empty group is allowed, acting as a global modality.
Entities (9)
Relation Signals (4)
Takano → developedstrategyfor → analytic cut
confidence 100% · adapting Takano's (2018) strategy, which restricts the cut formulas to the set of subformulas
K45D → hasproperty → analytic cut
confidence 100% · we establish the analytic cut property for all three systems [K45D, KD45D, S5D]
Ryo Murai → isauthorof → Analytic Cut in Epistemic Logics with Distributed Knowledge
confidence 100% · Ryo Murai Independent Researcher
K45D → satisfies → Craig interpolation theorem
confidence 100% · As a corollary, the Craig interpolation theorem holds for all logics considered.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2606.31886v1
- Canonical: https://arxiv.org/abs/2606.31886v1
Trouble viewing inline? Open PDF directly →
Full Text
55,226 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 636–654, doi:10.4204/EPTCS.447.36 © R. Murai & S. Liu & K. Sano This work is licensed under the Creative Commons Attribution License. Analytic Cut in Epistemic Logics with Distributed Knowledge Ryo Murai Independent Researcher ryo.murai11@gmail.com Sizhuo Liu Graduate School of Humanities and Human Sciences Hokkaido University Hokkaido, Japan liuliusizhuo@outlook.com Katsuhiko Sano Faculty of Humanities and Human Sciences Hokkaido University Hokkaido, Japan v-sano@let.hokudai.ac.jp Distributed knowledge is a notion of group knowledge studied in multi-agent epistemic logic. Se- mantically, 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 inves- tigates sequent calculi for epistemic logics of distributed knowledge based onK45,KD45, andS5. While cut elimination holds in existing sequent calculi for modal logicsK45andKD45, 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 con- sidered. 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. 1 Introduction Distributed knowledge is a notion of group knowledge in multi-agent epistemic logic [7] whose interpre- tation has varied in the literature. In this paper we follow the interpretation introduced in [2], i.e., a group Gis said to have distributed knowledge ofφif anexternalobserver with access to the epistemic states of all members ofGcan know thatφ. In Kripke semantics, while individual knowledge (notation:□ a φ, read as “agentaknows thatφ") is interpreted via an accessibility relationR a for each agenta, distributed knowledge for a groupGis interpreted via the intersection T a∈G R a of the epistemic accessibility rela- tions of the agents inG. Accordingly,D G φholds at a statewif and only ifφholds at all statesvsuch that(w,v)∈ T a∈G R a . Reflexivity, transitivity, Euclideanness, and symmetry are preserved when passing from the individual level to the group level, i.e., under intersection of epistemic accessibility relations, whereas seriality isnotpreserved (see [3, Lemma 3.2]). Sequent calculus, introduced by Gentzen in the 1930s, is a proof-theoretic framework where deriva- tions are formulated as sequentsΓ⇒∆(read as “if all formulas inΓhold, then some formula in∆ holds"), whereΓand∆are finite multisets of formulas [9, 10]. A crucial aspect of sequent calculus is the cut rule Γ⇒∆,φ φ,Π⇒Σ Γ,Π⇒∆,Σ (Cut) , and the associated cut elimination theorem (Gentzen’sHauptsatz), which states that every derivable sequent admits a cut-free derivation. As emphasized in [32], cut elimination is closely connected to proof normalization and the structural analysis of derivations. R. Murai & S. Liu & K. Sano637 For modal logics, Gentzen-style sequent calculiG(K45)andG(KD45)forK45andKD45, respec- tively, were shown to be cut-free in [27, Theorem 2]. However, as shown in [21, p. 116], cut elimination fails for the sequent calculusG(S5)corresponding to modal logicS5. As an alternative, Takano [28] showed that every application of the cut rule inG(S5)can be transformed into ananalyticcut, i.e., a cut rule in which the cut formula is a subformula of the conclusion. Moreover, Takano later provided a semantic analysis of sequent calculi for modal logics in [30], where cut-free sequent calculi such as G(K45)andG(KD45)were semantically shown to enjoy cut elimination, while sequent calculi that lack cut elimination such asG(S5)were shown to satisfy the extended subformula property. These results are established by proving the semantic completeness of sequent calculi where the cut rule is removed or restricted to an analytic cut. A key ingredient of the semantic proof is the notion ofΞ-partial valua- tion, i.e., a subformula-closed finite set of formulas, which originates from [29], that was later applied in [16, 15], [30], [23] and [33] to establish cut elimination or the analytic cut property for the sequent calculi for temporal epistemic logics, modal logics, bi-intuitionistic tense logic and awareness logic, respectively. Model-theoretic investigations of distributed knowledge have been extensively documented in, for example, [11, 25, 2, 3], whereas proof-theoretic studies, namely sequent calculi for logics with distributed knowledge, remain comparatively limited. A labelledG3-style sequent calculus, i.e., a calculus without structural rules in which each formula is equipped with a label, was introduced in [13]. A Gentzen- style sequent calculus based onS4was proposed in [24], in which the distributed knowledge operator isnotparameterized by a groupG. Gentzen-style and Kanger-style sequent calculi forS5were later studied in [12] in the same fashion. Label-free Gentzen-style sequent calculi for multi-agent epistemic propositional logicsK D ,KD D ,K4 D ,S4 D , andS5 D with group-parameterized distributed knowledge operators were introduced in [17]. Cut elimination was established for these systems except forG(S5 D ), which is the sequent calculus forS5 D . Moreover, the Craig interpolation theorem was obtained for the four systems via a method based on [26]. Furthermore, although groups are usually defined asnon- empty, the operatorD /0 corresponds naturally to the global modality when the empty set is allowed as a group. A sequent calculusG(S5 D )forS5 D was introduced in [17, 19]. This paper extends that line of research by introducing sequent calculiG(K45 D )andG(KD45 D )forK45 D andKD45 D , respectively, while also revisitingG(S5 D ). Surprisingly, although cut elimination holds forG(K45)andG(KD45), itfailsnot only forG(S5 D ), butalsoforG(K45 D )andG(KD45 D ). Therefore, by adapting Takano’s semantic approach [30], we establish the analytic cut property for all three systems. As a consequence, the Craig interpolation theorem is obtained via the method in [26]. We note that conditions onboth propositional variables andagentsare taken into account, which is a relatively new result for logics for distributed knowledge. To the best of the authors’ knowledge, such conditions have recently been considered only in [17, 34] and [5]. Although the Craig interpolation theorem in this paper has been established in [34], the proof is model-theoretic rather than proof-theoretic as in [26]. In fact, a proof- theoretic result was presented earlier by the first and third authors in [19]. As emphasized in [17], this result suggests that the logics with distributed knowledge are “good” expansions of basic modal logic, since the Craig interpolation theoremdoes nothold for some expansions of basic modal logic [31]. Moreover, we show that when the empty group is admitted, the operatorD /0 corresponds naturally to the global modality, and that the main proof-theoretic results are preserved under this extension. The paper is organized as follows. Section 2 introduces the syntax and semantics of distributed epistemic logics based onK45,KD45, andS5together with their Hilbert systems and pseudo-model semantics. Section 3 presents the sequent calculiG(K45 D ),G(KD45 D ), andG(S5 D ). Section 4 first demonstrates that cut elimination fails for these systems, then establishes the analytic cut property, while 638Analytic Cut in Epistemic Logics with Distributed Knowledge the Craig interpolation theorem is proved in Section 5. In Section 6, we extend the framework by in- troducing the global modality corresponding to distributed knowledge of the empty group and show that the analytic cut property and interpolation results are preserved under this extension. Finally, Section 7 concludes the paper. 2 Preliminaries LetPropbe a countably infinite set of propositional variables andAga non-empty finite set of agents. A groupis anon-emptysetG⊆Ago f agents and the set of all groups is denoted by Grp:= G∈P(Ag)|G̸=/0 . The syntaxLfor distributed epistemic logic is defined inductively as follows: L∋φ::=p|⊥|¬φ|φ→ψ|D G φ, wherep∈PropandG∈Grp. Boolean connectives∧,∨,↔and the truth constant⊤are defined in the usual manner. We also define the operator□ a φfor individual knowledge or belief as□ a φ:=D a φ. For a finite set∆, V ∆and W ∆are the conjunction or disjunction of all formulas in∆(when∆is empty, V ∆ :=⊤and W ∆:=⊥). As noted above, an expression of the formD /0 φis not a well-formed formula, since we have excluded /0 from our definition of groups. We move on to the semantics. Aframe Fis a tuple(W,(R a ) a∈Ag )whereWis a non-empty set of states andR a ⊆W×Wis a binary relation onWfor eacha∈Ag. Amodel Mis a tuple(W,(R a ) a∈Ag ,V) where(W,(R a ) a∈Ag )is a frame andV:Prop→P(W)is a valuation function. Given a modelM= (W,(R a ) a∈Ag ,V)and a statew∈W, the notion ofφbeing trueatwinM(notation:M,w|=φ) is defined inductively as follows: M,w|=piffw∈V(p), M,w|=⊥Never, M,w|=¬φiffM,w̸|=φ, M,w|=φ→ψiffM,w̸|=φorM,w|=ψ, M,w|=D G φiff for allv∈W,(w,v)∈ \ a∈G R a impliesM,v|=φ. A pair(M,w)of a modelMand a statewinMis called apointed model. A formulaφisvalidin a model M(notation:M|=φ) ifM,w|=φfor allw∈W. A formulaφisvalidin a frameF(notation:F|=φ) if(F,V)|=φfor all valuationsV. Given a classFof frames,φisvalidinFifF|=φfor every frame F∈F. To capture various aspects of individual knowledge operators, we consider a class of framesFin which all accessibility relationsR a fora∈Agsatisfy the same set of frame properties, defined as follows. Definition 2.1.We defineF K45 to be the class of all frames such that eachR a is transitive and Euclidean, F KD45 to be the class of all frames such that eachR a is transitive, Euclidean and serial (∀w∈W∃v(wR a v)), andF S5 to be the class of all frames such that eachR a is reflexive, transitive, and Euclidean (equivalently, symmetric). We define the distributed epistemic logicsK45 D ,KD45 D andS5 D to be the sets of allL- formulas that are valid in the class ofF K45 ,F KD45 andF S5 , respectively. R. Murai & S. Liu & K. Sano639 As proved in [3, Lemma 3.2], reflexivity, transitivity, Euclideanness and symmetry are preserved under taking the intersection T a∈G R a of binary relations 1 . It is well-known that all logics in Definition 2.1 can be axiomatized (see [7]). Table 1: Hilbert systemH(K D ),H(K45 D ),H(KD45 D )andH(S5 D ) All the Axioms and Rules ofH(K D ) (Taut)all instances of propositional tautologies (Incl)D G φ→D H φ(G⊆H) (K)D G (φ→ψ)→(D G φ→D G ψ) (MP)Fromφ→ψandφinferψ (Nec)FromφinferD G φ Additional Axiom Schemes (T)D G φ→φ (D)¬D a ⊥ (4)D G φ→D G D G φ (5)¬D G φ→D G ¬D G φ Definition 2.2.The Hilbert systemH(K D )is defined as in Table 1. The Hilbert systemH(K45 D )is defined as an axiomatic expansion ofH(K D )with(4)and(5)of Table 1. Moreover, the Hilbert systems H(KD45 D )andH(S5 D )are defined as axiomatic expansions ofH(K45 D )with(D)and(T)of Table 1, respectively. The following notion ofpseudo-modelis used in, for instance, [7, 11], as an intermediate step for semantic completeness proofs of epistemic logics with distributed knowledge. However, in this paper, we use pseudo-models to establish semantically the analytic property of sequent calculi in Section 4. Definition 2.3.Apseudo frame Fis a tuple(W,(R G ) G∈Grp )whereWis a set of states,R G ⊆W×Wis a binary relation onWsuch that for eachG,H∈GrpandG⊆HimpliesR H ⊆R G . Apseudo model M is a tuple(W,(R G ) G∈Grp ,V)where(W,(R G ) G∈Grp )is a pseudo frame andVis a function fromPropto P(W). Given a frameF= (W,(R a ) a∈Ag ), we defineR G := T a∈G R a . Then(W,(R G ) G∈Grp )is a pseudo frame. The notion ofφbeing trueatwinMis defined in the same way as at the beginning of Section 2 except that M,w|=D G φiff for allv∈W,wR G vimpliesM,v|=φ. Definition 2.4.We defineP K45 D to be the class of all pseudo frames such that eachR G is transitive and Euclidean,P KD45 D to be the class of all pseudo framesF=(W,(R G ) G∈Grp )such thatF∈P K45 D and each R a is serial,P S5 D to be the class of all pseudo frames such that eachR G is reflexive, transitive, and Euclidean (equivalently, symmetric). Fact 2.5.LetΛ∈K45 D ,KD45 D ,S5 D . The following are all equivalent: 1.φis a theorem ofH(Λ); 2.φis valid inP Λ ; 3.φis valid inF Λ . Proof.First, item 1 implies item 2 by the soundness ofH(Λ), which can be established straightforwardly. Moreover, item 2 implies item 3 sinceF Λ can be regarded as a subclass ofP Λ . So it remains to show that item 3 implies item 1, which is a result already established in the literature. A proof sketch forH(K D ) andH(K45 D )can be found in [7, Theorem 3.4.1] and [11, Theorem 3.30], respectively. Detailed proofs are provided in [3, Theorem 4.7] forH(KD45 D )and in [35, Theorem 10] forH(S5 D ). 1 However, seriality isnotpreserved. As shown in [3, Lemma 3.2], we can construct aKD45model in whichR a andR b are serial whileR a ∩R b is not. Thus, as discussed in [3], the axiom¬D G ⊥in [6] is not valid, hence the original axiomatization ofKD45 D in [6] is unsound. This axiomatization was subsequently corrected in [7], where completeness is reported, although without a detailed proof. 640Analytic Cut in Epistemic Logics with Distributed Knowledge 3 Sequent Calculi for Distributed Knowledge Logics In this section we introduce sequent calculiG(K45 D ),G(KD45 D )andG(S5 D )built onLK 0 (see [28]), which is the propositional fragment of a sequent calculusLK[9, 10] of the first-order classical logic. A sequentΓ⇒∆is a pair of finite multisetsΓand∆of formulas read as “if all formulas inΓhold, then at least one formula in∆holds". Moreover, we useD a Γto denote D a φ|φ∈Γ andΓ,∆to denote the multiset unionΓ∪∆. Definition 3.1.A sequent calculusLK 0 consists of the following. • Axioms: φ⇒φ (id) ⊥⇒ (⊥) • Structural Rules: Γ⇒∆ Γ⇒∆,φ (⇒w) Γ⇒∆ φ,Γ⇒∆ (w⇒) Γ⇒∆,φ,φ Γ⇒∆,φ (⇒c) φ,φ,Γ⇒∆ φ,Γ⇒∆ (c⇒) • Logical Rules: φ,Γ⇒∆ Γ⇒∆,¬φ (⇒¬) Γ⇒∆,φ ¬φ,Γ⇒∆ (¬⇒) φ,Γ⇒∆,ψ Γ⇒∆,φ→ψ (⇒→) Γ⇒∆,φ ψ,Π⇒Σ φ→ψ,Γ,Π⇒∆,Σ (→⇒) • Cut: Γ⇒∆,φ φ,Π⇒Σ Γ,Π⇒∆,Σ (Cut) φ The sequent calculusG(K45 D )isLK 0 expanded with the following rule: φ 1 ,...,φ m ,D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,χ D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,D G χ (⇒D K45 D ) , whereG i ,H j ⊆Gfor any 1≤i≤mand 1≤j≤n. The sequent calculusG(KD45 D )expandsG(K45 D ) with the following: Γ,D a Γ⇒D a ∆ D a Γ⇒D a ∆ (D KD45 D ) . Finally, the sequent calculusG(S5 D )expandsLK 0 with the following rules: φ,Γ⇒∆ D G φ,Γ⇒∆ (D⇒) D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,χ D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,D G χ (⇒D S5 D ) , whereG i ,H j ⊆Gfor any 1≤i≤mand 1≤j≤nin(⇒D S5 D ). Note thatmandnare possibly 0 in(⇒D K45 D )and(⇒D S5 D ). For each calculus, we define the notion of derivability of a sequent as a finite tree generated from axioms(id)and(⊥)by inference rules specific to the calculus. In addition, we use a double line=as an abbreviation of finite applications of structural rules. Given a derivationD, a sequent in the root node ofDis called theend-sequentand we use root(D)≡Γ⇒∆to mean that the end-sequent ofDisΓ⇒∆. Moreover we define theheightofDto be the maximum length of branches inDfrom the end-sequent to an axiom. Proposition 3.2.LetΛ∈K45 D ,KD45 D ,S5 D . IfΓ⇒∆is derivable inG(Λ)then V Γ→ W ∆is valid inF Λ . R. Murai & S. Liu & K. Sano641 Proof.By induction on the height of the derivationDto obtainΓ⇒∆. For base step, our goal is immediate. For inductive step, we divide the argument depending on the last rule applied. We only comment on the case of(⇒D K45 D )forG(K45 D ): φ 1 ,...,φ m ,D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,χ D G 1 φ 1 ,...,D G m φ m ⇒D H 1 ψ 1 ,...,D H n ψ n ,D G χ (⇒D K45 D ) , where S m i=1 G i ∪ S n j=1 H j ⊆G. Our goal is to showF K45 D |= V m i=1 D G i φ i → W n j=1 D H j ψ j ∨D G χ. Fix any modelMfromF K45 D and anyw∈W. SupposeM,w|= V m i=1 D G i φ i . We show thatM,w|= W n j=1 D H j ψ j ∨ D G χ. SupposeM,w̸|= W n j=1 D H j ψ j and we show thatM,w|=D G χ. Fix anyv∈Wsuch that(w,v)∈ T a∈G R a . It suffices to show thatM,v|=χ. By induction hypothesis, we obtainF K45 D |= V m i=1 φ i ∧ V m i=1 D G i φ i → W n j=1 D H j ψ j ∨χ. SinceG i ⊆G,(w,v)∈ T a∈G R a ⊆ T b∈G i R b . HenceM,v|= V m i=1 φ i by our assumptionM,w|= V m i=1 D G i φ i . Moreover by transitivity we obtainF K45 D |= V m i=1 D G i φ i , since for everyu∈Wsuch that(v,u)∈ T b∈G i R b ,(w,u)∈ T b∈G i R b . ThereforeM,v|= W n j=1 D H j ψ j ∨χ. For our goal, it suffices to showM,v̸|= W n j=1 D H j ψ j . ByM,w̸|= W n j=1 D H j ψ j , there exists a stateu j ∈W for every 1≤j≤nsuch that(w,u j )∈ T c∈H j R c andM,u j ̸|=ψ j . Then by Euclideanness, we obtain (v,u j )∈ T c∈H j R c , which implies our goalM,v̸|= W n j=1 D H j ψ j together withM,u j ̸|=ψ j . Proposition 3.3.LetΛ∈K45 D ,KD45 D ,S5 D . Ifφis a theorem ofH(Λ), then⇒φis derivable in G(Λ). Proof.We note that(Cut)is necessary to simulate(MP). We only check the derivability of(Incl) in each system. SupposeG⊆H. ForΛ∈K45 D ,KD45 D ,S5 D , the following derivations (left for K45 D ,KD45 D and right forS5 D ) witness(Incl), where the side conditions are satisfied by the assump- tionG⊆H. φ⇒φ φ,D G φ⇒φ (w⇒) D G φ⇒D H φ (⇒D K45 D ) ⇒D G φ→D H φ (⇒→) φ⇒φ D G φ⇒φ (D⇒) D G φ⇒D H φ (⇒D S5 D ) ⇒D G φ→D H φ (⇒→) . As shown in [27], sequent calculiG(K45)andG(KD45)for modal logicK45andKD45, respec- tively, are cut-free, while sequent calculusG(S5)for modal logicS5is not [21, p. 116]. A sequent ⇒D a ¬D a p,D a,b pis derivable inG(K45 D )andG(KD45 D )as follows: D a p⇒D a p ⇒¬D a p,D a p (⇒¬) ⇒D a ¬D a p,D a p (⇒D K45 D ) p⇒p p,D a p⇒p (w⇒) D a p⇒D a,b p (⇒D K45 D ) ⇒D a ¬D a p,D a,b p (Cut) D a p , Similarly, we can construct a derivation with(Cut)of the same sequent inG(S5 D ): D a p⇒D a p ⇒¬D a p,D a p (⇒¬) ⇒D a ¬D a p,D a p (⇒D S5 D ) p⇒p D a p⇒p (D⇒) D a p⇒D a,b p (⇒D S5 D ) ⇒D a ¬D a p,D a,b p (Cut) D a p . It is noted that the cut formulaD a pis a subformula of the conclusion of the cut. SinceG(S5)is not cut-free, it is not surprising thatG(S5 D )is also not cut-free. In what follows, however, we show that ⇒D a ¬D a p,D a,b pisnotderivable inG(K45 D ),G(KD45 D )andG(S5 D )without the cut rule either. 642Analytic Cut in Epistemic Logics with Distributed Knowledge Theorem 3.4.LetΛ∈K45 D ,KD45 D ,S5 D . The sequent⇒D a ¬D a p,D a,b p isnotderivable in G − (Λ), whereG − (Λ)is the same calculus asG(Λ)except that the cut rule is dropped. Proof.Letφ m denotemoccurrences ofφ. We comment on the case whereΛ=KD45 D . We can prove the following statements by simultaneous induction onDofG − (KD45 D ). (1)∀m,n,l∈N(root(D)̸≡⇒(D a ¬D a p) m ,(D a,b p) n ,p l ), (2)∀x 1 ,x 2 ,y,z∈N(root(D)̸≡p x 1 ,(D a p) x 2 ⇒(D a ¬D a p) y ,(¬D a p) z ). Then the statement of the lemma is a special case of (1) wherem=n=1 andl= 0. 4 Analytic Cut Property ofG(K45 D ),G(KD45 D )andG(S5 D ) This section establishes the analytic cut property, i.e., every application of the cut rule inG(Λ)can be replaced with an application of the cut rule such that the cut formula is in the set ofsubformulasof the conclusion of the cut. The setSub(φ)of subformulas of anL-formulaφis defined as usual. In particular, Sub(D G φ) =Sub(φ)∪D G φ. For any multisetΓof formulas,Sub(Γ)is defined as S φ∈Γ Sub(φ). Moreover, we say thatΞissubformula-closedifSub(Ξ)⊆Ξ. LetΛ∈K45 D ,KD45 D ,S5 D in this section. Definition 4.1.A cut Γ⇒∆,φ φ,Π⇒Σ Γ,Π⇒∆,Σ (Cut) φ isanalyticifφ∈Sub(Γ,Π,∆,Σ). The sequent calculusG a (Λ)is the same calculus asG(Λ)except that (Cut)is always analytic. In what follows, whenΓ⇒∆is derivable inG a (Λ), we denoteG a (Λ)⊢Γ⇒∆. LetΞbe a subformula-closed finite set of formulas in what follows. The following definition is taken from [30], whose notion originates from [29]. Definition 4.2.A pair(Γ,∆)is aΞ-partial valuationinG a (Λ)if all the following hold: (1)G a (Λ)̸⊢Γ⇒∆; (2)Sub(Γ,∆) =Γ∪∆; (3)Γ∪∆⊆Ξ. Remark 4.3.It is worth noting that the condition forSub(Γ,∆)highlights the distinction between se- mantically eliminating only non-analytic cuts and eliminating all cuts. In fully cut-free sequent calculi (for example,S4), the equalitySub(Γ,∆) =Γ∪∆maynothold; instead, the inclusionΓ∪∆⊆Sub(Γ,∆) is utilized. This is precisely the difference between the approach used in this paper to establish the an- alytic cut property and the one applied in [30] to prove semantic completeness for completely cut-free systems. The following lemma can be established similarly to Lindenbaum’s Lemma (cf. [33, Lemma 1]). Lemma 4.4.LetΓ∪∆⊆Ξ. IfG a (Λ)̸⊢Γ⇒∆, then there exists aΞ-partial valuation(Γ + ,∆ + )such thatΓ⊆Γ + ,∆⊆∆ + andSub(Γ,∆) =Γ + ∪∆ + . Proof.Letφ 1 ,...,φ m be an enumeration of all formulas inSub(Γ,∆). In what follows we inductively construct a sequence(Γ k ,∆ k )(1≤k≤m)such thatG a (Λ)̸⊢Γ k ⇒∆ k ,Γ k ⊆Γ k+1 and∆ k ⊆∆ k+1 for all R. Murai & S. Liu & K. Sano643 1≤k≤m. For base step, let(Γ 0 ,∆ 0 ):= (Γ,∆). It is clear thatG a (Λ)̸⊢Γ⇒∆. For inductive step, we define(Γ k+1 ,∆ k+1 )as follows: ( Γ k+1 =Γ k and∆ k+1 =∆ k ∪φ k ifG a (Λ)̸⊢Γ k ⇒∆ k ,φ k Γ k+1 =Γ k ∪φ k and∆ k+1 =∆ k otherwise Moreover, it is not the case thatG a (Λ)⊢Γ k ⇒∆ k ,φ k andG a (Λ)⊢φ k ,Γ k ⇒∆ k . Suppose it is the case for contradiction. Then we can deriveΓ k ⇒∆ k by Γ k ⇒∆ k ,φ k φ k ,Γ k ⇒∆ k Γ k ,Γ k ⇒∆ k ,∆ k (Cut) a φ k Γ k ⇒∆ k (w) , whereφ k ∈Sub(Γ k ,∆ k )holds clearly sinceφ k ∈Sub(Γ,∆)andΓ⊆Γ k ,∆⊆∆ k . Hence we haveG a (Λ)⊢ Γ k ⇒∆ k , which contradicts the induction hypothesis. Therefore, eitherΓ k ⇒∆ k ,φ k orφ k ,Γ k ⇒∆ k is underivable inG a (Λ). Finally, let(Γ + ,∆ + ):= (Γ m+1 ,∆ m+1 ). It holds clearly thatSub(Γ,∆) = Sub(Γ + ,∆ + ) =Γ + ∪∆ + . MoreoverΓ⊆Γ + ,∆⊆∆ + andG a (Λ)̸⊢Γ + ⇒∆ + by our definition. The following definition ofR Λ G is based on the definitions of accessibility relations for individual agents given in [16, Section 5.3] for individual agents, but is modified here to the group level to accom- modate the semantics of distributed knowledge. Definition 4.5.The pseudo modelM Λ Ξ = (W Λ Ξ ,(R Λ G ) G∈Grp ,V Λ Ξ )derived fromΞis defined as follows: •W Λ Ξ = (Γ,∆)|(Γ,∆)is aΞ-partial valuation inG a (Λ) ; •R Λ G is defined depending on the choice ofΛ: –Λ=K45 D :(Γ,∆)R K45 D G (Π,Σ)iff ∀H⊆G( φ,D H φ|D H φ∈Γ ⊆Πand D H φ|D H φ∈Π ⊆Γ), –Λ=KD45 D :R KD45 D G :=R K45 D G ; –Λ=S5 D :(Γ,∆)R S5 D G (Π,Σ)iff∀H⊆G( D H φ|D H φ∈Γ = D H φ|D H φ∈Π ); •(Γ,∆)∈V Λ Ξ (p)iffp∈Γ. SinceΞis finite, we note thatW Λ Ξ is finite. The following proposition shows thatM Λ Ξ is indeed a pseudo model. Proposition 4.6.The following hold for the pseudo frame F Λ Ξ = (W Λ Ξ ,(R Λ G ) G∈Grp )derived fromΞ: 1. G⊆H implies R Λ H ⊆R Λ G ; 2. F Λ Ξ satisfies the corresponding properties ofΛ. Proof.1. Fix anyG,H∈Grpsuch thatG⊆H. SinceR KD45 D G :=R K45 D G , we only comment on the cases where(Λ=K45 D )and(Λ=S5 D ). • LetΛ=K45 D . Fix any(Γ,∆),(Π,Σ)∈W Λ Ξ such that(Γ,∆)R K45 D H (Π,Σ). We show that (Γ,∆)R K45 D G (Π,Σ). Fix anyI⊆G. It suffices to show (i) φ,D I φ|D I φ∈Γ ⊆Πand (i) D I φ|D I φ∈Π ⊆Γ. By assumption,I⊆G⊆H, hence our goal follows from (Γ,∆)R K45 D H (Π,Σ). • LetΛ=S5 D . Fix any(Γ,∆),(Π,Σ)∈W Λ Ξ such that(Γ,∆)R S5 D H (Π,Σ). We show that (Γ,∆)R S5 D G (Π,Σ). Fix anyI⊆G. It suffices to show D I φ|D I φ∈Γ = D I φ|D I φ∈Π . By assumption,I⊆G⊆H, hence our goal follows from(Γ,∆)R S5 D H (Π,Σ). 644Analytic Cut in Epistemic Logics with Distributed Knowledge 2.• LetΛ=K45 D . We show thatR K45 D G is transitive and Euclidean. Transitivity Fix any(Γ,∆),(Π,Σ),(Θ,Ω)∈W K45 D Ξ . Suppose (Γ,∆)R K45 D G (Π,Σ)and(Π,Σ)R K45 D G (Θ,Ω). We show(Γ,∆)R K45 D G (Θ,Ω). Fix anyH⊆G. It suffices to show (i) φ,D H φ|D H φ∈Γ ⊆ Θand (i) D H φ|D H φ∈Θ ⊆Γ. First, we show (i). Let us fix anyD H ψ∈Γ. We show ψ,D H ψ∈Θ. By assumption, φ,D H φ|D H φ∈Γ ⊆Π. Then we haveD H ψ∈Π. Again by assumption, φ,D H φ|D H φ∈Π ⊆Θ. Therefore our goal ofψ,D H ψ∈Θfollows from D H ψ∈Π. Second, we move to (i). By assumption we have D H φ|D H φ∈Θ ⊆Πand D H φ|D H φ∈Π ⊆Γ, which implies our goal D H φ|D H φ∈Θ ⊆Γ. Euclideanness Fix any(Γ,∆),(Π,Σ),(Θ,Ω)∈W K45 D Ξ . Suppose(Γ,∆)R K45 D G (Π,Σ)and (Γ,∆)R K45 D G (Θ,Ω). We show(Π,Σ)R K45 D G (Θ,Ω). Fix anyH⊆G. It suffices to show (i) φ,D H φ|D H φ∈Π ⊆Θand (i) D H φ|D H φ∈Θ ⊆Π. First, we establish (i). Fix anyD H ψ∈Π. We show thatψ,D H ψ∈Θ. By(Γ,∆)R K45 D G (Π,Σ) we haveD H ψ∈Γ. Then our goal holds by(Γ,∆)R K45 D G (Θ,Ω). Second, we move to (i). Fix anyD H ψwithD H ψ∈Θ. We show thatD H ψ∈Π. By (Γ,∆)R K45 D G (Θ,Ω), we haveD H ψ∈Γ. Then our goal holds by(Γ,∆)R K45 D G (Π,Σ). Seriality We prove the seriality ofR KD45 D a . Fix any(Γ,∆)∈W KD45 D Ξ . We show that there exists(Π,Σ)∈W KD45 D Ξ such that(Γ,∆)R KD45 D a (Π,Σ). We defineΠ:= φ|D a φ∈Γ , Σ:= D a ψ|D a ψ∈∆ . ThenΠ,D a Π⇒Σis underivable inG a (KD45 D ). Otherwise Γ⇒∆is derivable fromΠ,D a Π⇒Σvia(D KD45 D )and weakening rules, which contradicts G a (Λ)̸⊢Γ⇒∆. By Lemma 4.4, there exists(Π + ,Σ + )∈W KD45 D Ξ such thatΠ∪D a Π⊆Π + , Σ⊆Σ + andSub(Π,D a Π,Σ) =Π + ∪Σ + . Then it suffices to show(Γ,∆)R KD45 D a (Π + ,Σ + ). Fix anyD a χ∈Ξ. First, we supposeD a χ∈Γ. We show thatχ,D a χ∈Π + . Then χ∈Π⊆Π + . MoreoverD a χ∈D a Π⊆Π + . Therefore, our goalχ∈Π + andD a χ∈Π + holds. Second, we supposeD a χ∈Π. Our goal is to showD a χ∈Γ. SupposeD a χ/∈Γ for contradiction. ByD a χ∈Π,D a χ∈Π + ∪Σ + =Sub(Π,D a Π,Σ)⊆Sub(Γ,∆) = Γ∪∆. SinceD a χ/∈Γ, we haveD a χ∈∆, i.e.,D a χ∈Σ⊆Σ + . ThenΠ + ⇒Σ + is derivable fromD a χ⇒D a χby weakening rules, which is contradicted to(Π + ,Σ + )being aΞ-partial valuation. Therefore, our goalD a χ∈Γholds. • LetΛ=S5 D . We show thatR S5 D G is reflexive, symmetric and transitive. Fix any(Γ,∆),(Π,Σ), (Θ,Ω)∈W S5 D Ξ . First, we show that(Γ,∆)R S5 D G (Γ,∆), which holds clearly by D H φ|D H φ∈Γ = D H φ|D H φ∈Γ . Second, suppose(Γ,∆)R S5 D G (Π,Σ). We show that(Π,Σ)R S5 D G (Γ,∆). It suffices to show that D H φ|D H φ∈Π = D H φ|D H φ∈Γ , which follows from our assumption (Γ,∆)R S5 D G (Π,Σ), i.e., D H φ|D H φ∈Γ = D H φ|D H φ∈Π . Finally, suppose (Γ,∆)R S5 D G (Π,Σ)and(Π,Σ)R S5 D G (Θ,Ω). R. Murai & S. Liu & K. Sano645 We show(Γ,∆)R S5 D G (Θ,Ω). Fix anyH⊆G. It suffices to show D H φ|D H φ∈Γ = D H φ|D H φ∈Θ . By assumption, we have D H φ|D H φ∈Γ = D H φ|D H φ∈Π and D H φ|D H φ∈Π = D H φ|D H φ∈Θ . Therefore, our goal holds. Lemma 4.7.Let(Γ,∆)be aΞ-partial valuation inG a (Λ). Then(Γ,∆)satisfies the following: (¬⇒)¬φ∈Γimpliesφ∈∆; (⇒¬)¬φ∈∆impliesφ∈Γ; (→⇒)φ→ψ∈Γimpliesφ∈∆orψ∈Γ; (⇒→)φ→ψ∈∆impliesφ∈Γandψ∈∆; (D)D G φ∈∆impliesφ∈Σfor some(Π,Σ)∈W Λ Ξ such that(Γ,∆)R Λ G (Π,Σ). Proof.We comment on item (D) forK45 D andS5 D , because the other conditions are established easily (cf. [33, Lemma 2]). • LetΛ=K45 D . SupposeD G φ∈∆. DefineΠ:= ψ,D H ψ|D H ψ∈ΓandH⊆G and Σ:= D I γ|D I γ∈∆andI⊆G . It follows thatΠ⇒Σ,φis underivable inG a (K45 D ). Suppose not. Then we obtain the following: Π⇒Σ,φ Π ′ ⇒Σ,D G φ (⇒D K45 D ) , whereΠ ′ = S H⊆G D H ψ|D H ψ∈Γ , which is contradicted to(Γ,∆)being aΞ-partial valuation by weakening rules. So,G a (K45 D )̸⊢Π⇒Σ,φ. By Lemma 4.4, there exists aΞ-partial valuation (Π + ,Σ + )such thatΠ⊆Π + ,Σ∪φ⊆Σ + andSub(Π,Σ,φ) =Π + ∪Σ + . Then it suffices to show (Γ,∆)R K45 D G (Π + ,Σ + ), which can be proved similarly to the proof of Proposition 4.6 (2). • LetΛ=S5 D . SupposeD G φ∈∆. LetΠandΣbe defined as: Π:= D H ψ|D H ψ∈ΓandH⊆G Σ:= D I γ|D I γ∈∆andI⊆G . It follows thatΠ⇒Σ,φis underivable inG a (S5 D ), otherwiseΓ⇒∆is derivable by(⇒D S5 D ) and weakening rules. Then by Lemma 4.4, there exists aΞ-partial valuation(Π + ,Σ + )such that Π⊆Π + ,Σ∪φ⊆Σ + andSub(Π,Σ,φ) =Π + ∪Σ + . Then it suffices to show(Γ,∆)R S5 D G (Π + ,Σ + ). Fix anyC⊆Gandχ∈Ξ. We show thatD C χ∈ΓiffD C χ∈Π + . (⇒) SupposeD C χ∈Γ. By definition ofΠ,D C χ∈Π. Therefore our goalD C χ∈Π + holds byΠ⊆Π + . (⇐) Suppose D C χ∈Π + . ThenD C χ∈Π + ∪Σ + =Sub(Π,Σ,φ)⊆Sub(Γ,∆) =Γ∪∆. Our goal is to show that D C χ∈Γ. Suppose not. ThenD C χ∈∆, i.e.,D C χ∈Σ⊆Σ + . ThenΠ + ⇒Σ + is derivable from D C φ⇒D C φ. Therefore our goalD C χ∈Γholds. By Lemma 4.7, we obtain the following. Lemma 4.8.The following holds for all formulasφ∈Ξand(Γ,∆)∈W Λ Ξ ; 1.φ∈Γimplies M Λ Ξ ,(Γ,∆)|=φ; 2.φ∈∆implies M Λ Ξ ,(Γ,∆)̸|=φ. Proof.By induction onφ. We comment on the case whereφ≡D G ψ. 1. SupposeD G ψ∈Γ. We show thatM Λ Ξ ,(Γ,∆)|=D G ψ. Fix any(Π,Σ)∈W Λ Ξ and suppose (Γ,∆)R Λ G (Π,Σ). We show thatM Λ Ξ ,(Π,Σ)|=ψ. We comment on the case forK45 D andS5 D . 646Analytic Cut in Epistemic Logics with Distributed Knowledge •(K45 D )We showM K45 D Ξ ,(Π,Σ)|=ψ. By induction hypothesis, it suffices to showψ∈Π, which follows from Definition 4.5 andD G ψ∈Γ. •(S5 D )We showM S5 D Ξ ,(Γ,∆)|=D G ψ. Fix any(Π,Σ)∈W S5 D Ξ and suppose(Γ,∆)R S5 D G (Π,Σ). ThenD G ψ∈ΓimpliesD G ψ∈Π. Thenψ∈Sub(D G ψ)⊆Sub(Π,Σ) =Π∪Σ. Ifψ∈ Π, our goalM K45 D Ξ ,(Π,Σ)|=ψfollows from induction hypothesis. So supposeψ/∈Πfor contradiction. Thenψ∈Σ, henceΠ⇒Σis derivable by φ⇒φ D G φ⇒φ (D⇒) Π⇒Σ (w) , which contradicts(Π,Σ)being aΞ-partial valuation. Therefore our goalψ∈Πholds. 2. SupposeD G ψ∈∆. We showM Λ Ξ ,(Γ,∆)̸|=D G ψ. By Lemma 4.7, we can find some(Π,Σ)∈W Λ Ξ such that(Γ,∆)R Λ G (Π,Σ)andψ∈Σ. By induction hypothesis,ψ∈ΣimpliesM Λ Ξ ,(Π,Σ)̸|=ψ. Therefore our goalM Λ Ξ ,(Γ,∆)̸|=D G ψholds. Theorem 4.9(Completeness ofG a (Λ)).For any sequentΓ⇒∆, if V Γ→ W ∆is valid inallpseudo frames which satisfies the corresponding properties toΛ, thenG a (Λ)⊢Γ⇒∆. Proof.We show the contraposition. SupposeG a (Λ)̸⊢Γ⇒∆. LetΞ:=Sub(Γ,∆). By Lemma 4.4, there exists aΞ-partial valuation(Γ + ,∆ + )such thatΓ⊆Γ + ,∆⊆∆ + andSub(Γ,∆) =Γ + ∪∆ + . By Lemma 4.8,M Λ Ξ ,(Γ + ,∆ + )̸|= V Γ→ W ∆. Therefore our goal holds. As a corollary of Theorem 4.9, we can show thatG(Λ)enjoys the analytic cut property. Corollary 4.10.If a sequentΓ⇒∆is derivable inG(Λ), then it is also derivable inG a (Λ). Proof.SupposeG(Λ)⊢Γ⇒∆. By Proposition 3.2, V Γ→ W ∆is valid inF Λ . Therefore, our goal G a (Λ)⊢Γ⇒∆holds by Theorem 4.9. 5 Craig Interpolation Theorem This section establishes the Craig interpolation theorem forG(Λ)using the analytic cut property via Maehara’s method, originally introduced in [26]. An application of this method to basic modal logic can also be found in [22]. First, we introduce some necessary syntactic notions. As in the previous section, we assume in what follows thatΛ∈K45 D ,KD45 D ,S5 D . Definition 5.1.Apartitionfor a sequentΓ⇒∆is defined as a tuple⟨(Γ 1 :∆ 1 );(Γ 2 :∆ 2 )⟩such that Γ=Γ 1 ,Γ 2 and∆=∆ 1 ,∆ 2 . Definition 5.2.For a formulaφ∈L, we defineProp(φ)as the set of all propositional variables appearing inφandAgt(φ)as the set of all agents appearing inφ. For any multisetΓof formulas,Prop(Γ)and Agt(Γ)are defined as S φ∈Γ Prop(φ)and S φ∈Γ Agt(φ), respectively. In particular, it is noted thatAgt(D G φ) =Agt(φ)∪G. The following lemma is immediate. Lemma 5.3.Ifφ∈Sub(ψ), thenProp(φ)⊆Prop(ψ)andAgt(φ)⊆Agt(ψ). The following is the key lemma for the Craig interpolation theorem. Lemma 5.4.SupposeG(Λ)⊢Γ⇒∆. Then for any partition⟨(Γ 1 :∆ 1 );(Γ 2 :∆ 2 )⟩for the sequentΓ⇒∆, there exists a formulaφ(calledinterpolant)that satisfies the following: R. Murai & S. Liu & K. Sano647 (1)G(Λ)⊢Γ 1 ⇒∆ 1 ,φandG(Λ)⊢φ,Γ 2 ⇒∆ 2 ; (2)Prop(φ)⊆Prop(Γ 1 ,∆ 1 )∩Prop(Γ 2 ,∆ 2 ); (3)Agt(φ)⊆Agt(Γ 1 ,∆ 1 )∩Agt(Γ 2 ,∆ 2 ). Proof.In what follows, we letΛbeK45 D . This is because the cases whereΛisKD45 D orS5 D can be handled using an argument similar to that forK45 D . By Corollary 4.10, we can assume thatΓ⇒∆has a derivationDinG a (Λ). We prove Lemma 5.4 by induction onD. Let the height ofDben. For the base case, our argument is standard (the reader is referred to [22, Lemma 36]). For the inductive step, letn>0. First, we supposeΓ 1 =∆ 1 =/0 orΓ 2 =∆ 2 =/0. Then the interpolant is¬⊥or⊥. Hence, in what follows, we suppose it is not the case thatΓ 1 =∆ 1 =/0 orΓ 2 =∆ 2 =/0, i.e.,Γ 1 ∪∆ 1 ̸=/0 and Γ 2 ∪∆ 2 ̸=/0. We divide our argument depending on the last applied rule to obtainΓ⇒∆. We comment on the cases where the last applied rule is an analytic cut or(⇒D K45 D ). Although an argument for the case of analytic cut is discussed already in [22, Section 6.4], we provide the details here in order to make the proof self-contained. For other cases, the reader is referred to [22, Lemma 34] for propositional connectives. • Suppose that the last applied rule is an analytic cut: Γ 1 ,Γ 2 ⇒∆ 1 ,∆ 2 ,φ φ,Π 1 ,Π 2 ⇒Σ 1 ,Σ 2 Γ 1 ,Γ 2 ,Π 1 ,Π 2 ⇒∆ 1 ,∆ 2 ,Σ 1 ,Σ 2 (Cut) φ , whereφ∈Sub(Γ 1 ,Γ 2 ,Π 1 ,Π 2 ,∆ 1 ,∆ 2 ,Σ 1 ,Σ 2 ). The partition is of the form ⟨(Γ 1 ,Π 1 :∆ 1 ,Σ 1 );(Γ 2 ,Π 2 :∆ 2 ,Σ 2 )⟩. We divide the argument into the following cases: φ∈Sub(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 )andφ∈Sub(Γ 2 ,Π 2 ,∆ 2 ,Σ 2 ). We focus only on the former case. Supposeφ∈Sub(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 ). By induction hypothesis, we can find formulasψ 1 andψ 2 such that –bothΓ 1 ,⇒∆ 1 ,φ,ψ 1 andψ 1 ,Γ 2 ⇒∆ 2 are derivable inG(Λ)andX(ψ 1 )⊆X(Γ 1 ,∆ 1 ,φ)∩ X(Γ 2 ,∆ 2 )for allX∈ Prop,Agt ; –bothφ,Π 1 ,⇒Σ 1 ,ψ 2 andψ 2 ,Π 2 ⇒Σ 2 are derivable inG(Λ)andX(ψ 2 )⊆X(φ,Π 1 ,Σ 1 )∩ X(Π 2 ,Σ 2 )for allX∈ Prop,Agt . We show thatψ 1 ∨ψ 2 :=¬ψ 1 →ψ 2 is a desired interpolant. The derivability condition is obtained as follows: Γ 1 ,⇒∆ 1 ,φ,ψ 1 φ,Π 1 ,⇒Σ 1 ,ψ 2 Γ 1 ,Π 1 ⇒∆ 1 ,Σ 1 ,ψ 1 ,ψ 2 (Cut) a φ ¬ψ 1 ,Γ 1 ,Π 1 ⇒∆ 1 ,Σ 1 ,ψ 2 (¬⇒) Γ 1 ,Π 1 ⇒∆ 1 ,Σ 1 ,¬ψ 1 →ψ 2 (⇒→) , ψ 1 ,Γ 2 ⇒∆ 2 Γ 2 ⇒∆ 2 ,¬ψ 1 (⇒¬) ψ 2 ,Π 2 ⇒Σ 2 ¬ψ 1 →ψ 2 ,Γ 2 ,Π 2 ⇒∆ 2 ,Σ 2 (→⇒) , where the(Cut)is analytic by our assumptionφ∈Sub(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 ). Moreover the variable and agent conditions are verified as follows. LetX∈Prop,Agt. We proceed as follows: X(¬ψ 1 →ψ 2 ) =X(ψ 1 )∪X(ψ 2 ), ⊆(X(Γ 1 ,∆ 1 ,φ)∩X(Γ 2 ,∆ 2 ))∪(X(φ,Π 1 ,Σ 1 )∩X(Π 2 ,Σ 2 )) ⊆X(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 ,φ)∩X(Γ 2 ,Π 2 ,∆ 2 ,Σ 2 ). By Lemma 5.3,φ∈Sub(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 )impliesX(φ)⊆X(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 ). Therefore, we obtain X(¬ψ 1 →ψ 2 )⊆X(Γ 1 ,Π 1 ,∆ 1 ,Σ 1 )∩X(Γ 2 ,Π 2 ,∆ 2 ,Σ 2 ). 648Analytic Cut in Epistemic Logics with Distributed Knowledge • Suppose that the last applied rule is(⇒D K45 D ): −→ φ 1x , −→ φ 2y , −→ D G 1x φ 1x , −→ D G 2y φ 2y ⇒ −→ D H 1a ψ 1a , −→ D H 2b ψ 2b ,χ −→ D G 1x φ 1x , −→ D G 2y φ 2y ⇒ −→ D H 1a ψ 1a , −→ D H 2b ψ 2b ,D G χ (⇒D K45 D ) , where −→ γ iz denotes a listγ i1 ,...,γ im z of formulas andG 1x ,H 1a ,G 2y ,H 2b ⊆Ghold for all indices. There are the following two possible forms of the partitions of the conclusion of the rule: (a)⟨( −→ D G 1x φ 1x : −→ D H 1a ψ 1a ,D G χ);( −→ D G 2y φ 2y : −→ D H 2b ψ 2b )⟩, (b)⟨( −→ D G 1x φ 1x : −→ D H 1a ψ 1a );( −→ D G 2y φ 2y : −→ D H 2b ψ 2b ,D G χ)⟩. Due to space limitations, we focus on case (a) alone. By induction hypothesis, we can find a for- mulaψsuch that both −→ φ 1x , −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,χ,ψandψ, −→ φ 2y , −→ D G 2y φ 2y ⇒ −→ D H 2b ψ 2b are derivable inG a (K45 D )andψsatisfiesX(ψ)⊆X( −→ φ 1x , −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,χ)∩X( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ), where X∈ Prop,Agt . We show that¬D H ¬ψis a desired interpolant, whereH= S −→ G 2y ∪ S −→ H 2b . We note thatH̸=/0 since we have assumedΓ 2 ∪∆ 2 ̸=/0. It follows thatH⊆G. −→ φ 1x , −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,χ,ψ ¬ψ, −→ φ 1x , −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,χ (¬⇒) ¬ψ,D H ¬ψ, −→ φ 1x , −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,χ (w⇒) D H ¬ψ, −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,D G χ (⇒D K45 D ) −→ D G 1x φ 1x ⇒ −→ D H 1a ψ 1a ,D G χ,¬D H ¬ψ (⇒¬) ψ, −→ φ 2y , −→ D G 2y φ 2y ⇒ −→ D H 2b ψ 2b −→ φ 2y , −→ D G 2y φ 2y ⇒ −→ D H 2b ψ 2b ,¬ψ (⇒¬) −→ D G 2y φ 2y ⇒ −→ D H 2b ψ 2b ,D H ¬ψ (⇒D K45 D ) ¬D H ¬ψ, −→ D G 2y φ 2y ⇒ −→ D H 2b ψ 2b (¬⇒) , where both applications of(⇒D K45 D )are eligible. Since the condition for propositional vari- ables is easily satisfied, we comment on the condition for agents. Our goal is to show that Agt(¬D H ¬ψ)⊆Agt( −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,D G χ)∩Agt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ). However, note that this argument isnotpossible whenΓ 2 =∆ 2 =/0, in which caseAgt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ) =/0. The same situation happens whenΓ 1 =∆ 1 =/0 for case (b). This is precisely why we made the assumption Γ 1 =∆ 1 =/0 orΓ 2 =∆ 2 =/0 in the first place. Fix anya∈Agt(¬D H ¬ψ) =H∪Agt(ψ). We divide the argument into the following two cases:a∈Agt(ψ)anda/∈Agt(ψ). –Supposea∈Agt(ψ). Then our goal a∈Agt( −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,D G χ)∩Agt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ) follows fromAgt(ψ)⊆Agt( −→ φ 1x , −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,χ)∩Agt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ). Note that it is possible that −→ φ 1x = −→ D G 1x φ 1x =/0, in which case the argument remains valid. –Supposea/∈Agt(ψ). Thena∈H. Our goal is to show a∈Agt( −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,D G χ)∩Agt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ), i.e.,a∈Agt( −→ D G 1x φ 1x , −→ D H 1a ψ 1a ,D G χ)anda∈Agt( −→ D G 2y φ 2y , −→ D H 2b ψ 2b ). The first condition is satisfied bya∈H⊆G⊆Agt(D G χ), and the second condition is satisfied byH= S −→ G 2y ∪ S −→ H 2b . Theorem 5.5.SupposeG(Λ)⊢⇒φ→ψ. Then there exists a formulaχsatisfying the following: R. Murai & S. Liu & K. Sano649 (1)G(Λ)⊢⇒φ→χandG(Λ)⊢⇒χ→ψ; (2)Prop(χ)⊆Prop(φ)∩Prop(ψ); (3)Agt(χ)⊆Agt(φ)∩Agt(ψ). Proof.SupposeG(Λ)⊢⇒φ→ψ. Then we can showG(Λ)⊢φ⇒ψby ⇒φ→ψ φ⇒φ ψ⇒ψ φ,φ→ψ⇒ψ (→⇒) φ⇒ψ (Cut) φ→ψ . By Corollary 4.10, we haveG a (Λ)⊢φ⇒ψ. Take a partition⟨(φ: /0);(/0 :ψ)⟩. Then by Lemma 5.4, we can find an interpolantχthat satisfies the required conditions. 6 Adding Global Modality In this section, we introduce the framework with the global modalityA. The syntaxL + with the global modality is defined inductively as follows: L + ∋φ::=p|⊥|¬φ|φ→ψ|D G φ|Aφ wherep∈PropandG⊆Ag. The notion ofAφbeing true atwin a modelMor a pseudo modelMis defined as: M,w|=Aφiff for allv∈W,M,v|=φ. As the readers may notice, though we have definedG̸=/0, the motivation for the global modality is to obtain the distributed knowledge of an empty group of agents, namelyD /0 φ. This is because T a∈/0 = W×W. Under the semantics defined above,D /0 φ:=Aφ. Now we introduce sequent calculiG(K45 DA ),G(KD45 DA )andG(S5 DA ), which are also expansions ofLK 0 . For a finite multisetΓof formulas, we useAΓto denote Aφ|φ∈Γ . The sequent calculus G(K45 DA )isLK 0 expanded with the following rules: φ 1 ,...,φ m ,D G 1 φ 1 ,...,D G m φ m ,AΠ⇒AΣ,D H 1 ψ 1 ,...,D H n ψ n ,χ D G 1 φ 1 ,...,D G m φ m ,AΠ⇒AΣ,D H 1 ψ 1 ,...,D H n ψ n ,D G χ (⇒D K45 DA ) , AΓ⇒A∆,φ AΓ⇒A∆,Aφ (⇒A) φ,Γ⇒∆ Aφ,Γ⇒∆ (A⇒) where S m i=1 G i ∪ S n j=1 H j ⊆Gin(⇒D K45 DA ). The sequent calculusG(KD45 DA )expandsG(K45 D )with the following rule: Γ,D a Γ,AΠ⇒AΣ,D a ∆ D a Γ,AΠ⇒AΣ,D a ∆ (D KD45 DA ) . Finally, the sequent calculusG(S5 DA )expandsLK 0 with(⇒A),(A⇒)and the following rules: D G 1 φ 1 ,...,D G m φ m ,AΠ⇒AΣ,D H 1 ψ 1 ,...,D H n ψ n ,χ D G 1 φ 1 ,...,D G m φ m ,AΠ⇒AΣ,D H 1 ψ 1 ,...,D H n ψ n ,D G χ (⇒D S5 DA ) φ,Γ⇒∆ D G φ,Γ⇒∆ (D⇒) . where S m i=1 G i ∪ S n j=1 H j ⊆Gin(⇒D S5 DA ). The following proposition can be established similarly as Proposition 3.2. 650Analytic Cut in Epistemic Logics with Distributed Knowledge Proposition 6.1.IfΓ⇒∆is derivable inG(Λ)then V Γ→ W ∆is valid in the corresponding classP Λ of pseudo frames toΛ. In what remains in this section, letΛ∈K45 DA ,KD45 DA ,S5 DA , and explain that the proof-theoretic results, namely the analytic cut property and Craig interpolation theorem forG(Λ)can be obtained in a similar way as in Theorems 4.9 and 5.5, respectively, except that a modification of the pseudo-model is required to establish the analytic cut property. Definition 6.2.DefineM Λ Ξ = (W Λ Ξ ,(R Λ G ) G∈Grp ,V Λ Ξ )to be the pseudo model derived fromΞin the same way as in Definition 4.5. Define∼ A onW Λ Ξ as follows: (Γ,∆)∼ A (Π,Σ)iff Aφ|Aφ∈Γ = Aφ|Aφ∈Π . It follows that∼ A is reflexive, transitive, symmetric and Euclidean. Definition 6.3.Let(Φ,Ψ)be aΞ-partial valuation. The pseudo model M Λ Ξ(Φ,Ψ) = (W Λ Ξ(Φ,Ψ) ,(R Λ G ) G∈Grp ,V Λ Ξ(Φ,Ψ) ) derived fromΞand(Γ,∆)is defined as: •W Λ Ξ(Φ,Ψ) = (Γ,∆)∈W Λ Ξ |(Φ,Ψ)∼ A (Γ,∆) ; •R Λ G is defined depending on the choice ofΛ: –Λ=K45 DA :(Γ,∆)R K45 DA G (Π,Σ)iff ∀H⊆G( φ,D H φ|D H φ∈Γ ⊆Πand D H φ|D H φ∈Π ⊆Γ) and Aφ|Aφ∈Γ = Aφ|Aφ∈Π , –Λ=KD45 DA :R KD45 DA G :=R K45 DA G , –Λ=S5 DA :(Γ,∆)R S5 DA G (Π,Σ)iff∀H⊆G( D H φ|D H φ∈Γ = D H φ|D H φ∈Π ) and Aφ|Aφ∈Γ = Aφ|Aφ∈Π ; •(Γ,∆)∈V Λ Ξ(Φ,Ψ) (p)iffp∈Γ. The above definition ofW Λ Ξ(Φ,Ψ) ensures that the global modalityAmeans “for all states” by specifying the root(Φ,Ψ). All the necessary lemmas can be proved in a manner similar to those for distributed knowledge logic without the global modality, with the exception of the following: Lemma 6.4.Let(Γ,∆)be aΞ-partial valuation inG a (Λ). Then(Γ,∆)satisfies the following: (A⇒)Aφ∈Γimpliesφ∈Πfor all(Π,Σ)∈W Λ Ξ(Φ,Ψ) ; (⇒A)Aφ∈∆impliesφ∈Σfor some(Π,Σ)∈W Λ Ξ(Φ,Ψ) ; (D)D G φ∈∆impliesφ∈Σfor some(Π,Σ)∈W Λ Ξ(Φ,Ψ) such that(Γ,∆)R Λ G (Π,Σ); For item(D), to find a desired witness(Π,Σ)∈W Λ Ξ(Φ,Ψ) reachable from(Φ,Ψ), adding the contexts AΠandAΣto the inference rules(⇒D K45 D ),(D KD45 D )and(⇒D S5 D )ofD G plays a crucial role. By applying this lemma, we can prove the semantic completeness theorem, following the same line of argument as in the case without the global modality: Theorem 6.5.For any sequentΓ⇒∆, if V Γ→ W ∆is valid in the classP Λ of all pseudo frames which satisfy the properties corresponding toΛ, thenG a (Λ)⊢Γ⇒∆. Corollary 6.6.For any sequentΓ⇒∆, ifG(Λ)⊢Γ⇒∆, thenG a (Λ)⊢Γ⇒∆. R. Murai & S. Liu & K. Sano651 For the rules(⇒A)and(A⇒), we can employ the same argument in terms of Maehara’s method as used for the modal logicS5(see, e.g., [22]). Moreover, adding the contextsAΠandAΣto the inference rules(⇒D K45 D ),(D KD45 D )and(⇒D S5 D )ofD G does not change the outline of Maehara’s argument or the information regarding the common vocabulary. Therefore, we obtain the following: Theorem 6.7.LetΛ∈K45 DA ,KD45 DA ,S5 DA . SupposeG(Λ)⊢Γ⇒∆. Then for any partition⟨(Γ 1 : ∆ 1 );(Γ 2 :∆ 2 )⟩for the sequentΓ⇒∆, there exists a formulaφthat satisfies the following:Γ 1 ⇒∆ 1 ,φand φ,Γ 2 ⇒∆ 2 are derivable inG(Λ)andX(φ)⊆X(Γ 1 ,∆ 1 )∩X(Γ 2 ,∆ 2 )for allX∈Agt,Prop. Therefore, the Craig interpolation theorem holds forG(Λ). The reader may wonder if all the sequent calculi equipped with the global modality are semantically complete in terms of models, i.e., pseudo modelsM=(W,(R G ) G∈Grp ,V)such thatR G = T a∈G R a holds for allG∈Grp. This can be done in terms of a technique called “tree unraveling”, which transforms a pseudo-model into one that satisfies T a∈G R a =R G . Theorem 6.8.LetΛ∈K45 DA ,KD45 DA ,S5 DA . If a formulaφis valid in the classF Λ of all frames that satisfy the corresponding properties toΛthenφis valid in the classP Λ of all pseudo frames that satisfy the properties corresponding toΛ. Therefore, for any sequentΓ⇒∆, if V Γ→ W ∆is valid in the classF Λ , thenG a (Λ)⊢Γ⇒∆. Proof.(Outline) The latter part follows immediately from the former part by Theorem 6.5. In what follows, we outline the proof of the former part. The following definitions and arguments are adapted from [8, 3, 18]. Suppose that a formulaφis valid in the classF Λ . To show thatφis valid in the pseudo- frame classP Λ , let us fix an arbitrary pseudo-frameF= (W,(R G ) G∈Grp )inP Λ . Our goal is to establish the validity ofφonF. Let us fix an arbitrary valuationVand a statew∈W. We will show thatM,w|=φ, whereM:= (F,V). Without loss of generality, we assume thatMis point-generated bywwith respect to the binary relations(R G ) G∈Grp . We define the tree unravelingTree Λ (M,w)ofMaroundwas follows: •Finpath(M,w)is defined as follows: Finpath(M,w):=⟨w 0 ,G 1 ,w 1 ,...,G m ,w m ⟩| m≥0,G i ∈Grp,w 0 =w,w i−1 R G i w i for all 1≤i≤m. We refer to an element ofFinpath(M,w)as a “path (from statew)” and denote it by −→ v, −→ u, etc. • We define a binary relationR G onFinpath(M,w)as follows: −→ wR G −→ viff −→ v= −→ w ⌢ (H,tail( −→ w)) for someH⊇G, wheretail( −→ w)denotes the last element of −→ w, and ⌢ denotes concatenation. We useR + G (orR ∗ G ) to mean the transitive closure (or the reflexive and transitive closure) ofR G . • Depending on our choice ofΛ, we defineR Λ G as follows: –ForΛ∈ K45 DA ,KD45 DA , define −→ wR Λ G −→ viff there exists −→ u∈Finpath(M,w)such that −→ uR ∗ G −→ wand −→ uR + G −→ v; –ForΛ=S5 DA , define −→ wR Λ G −→ viff there exists −→ u∈Finpath(M,w)such that −→ uR ∗ G −→ wand −→ uR ∗ G −→ v. •V(p) = −→ v∈Finpath(M,w)|tail( −→ v)∈V(p) for everyp∈Prop. • DefineTree Λ (M,w):= (Finpath(M,w),(R Λ G ) G∈Grp ,V). It is straightforward to verify that the frame part(Finpath(M,w),(R Λ G ) G∈Grp )ofTree Λ (M,w)still belongs toP Λ . Moreover, we note thatR Λ G = T a∈G R Λ a holds. We can also establish that the mapping tail:Finpath(M,w)→W, which sends each −→ vto its last elementtail( −→ v), is a surjective bounded 652Analytic Cut in Epistemic Logics with Distributed Knowledge morphism between pseudo-models. Here, surjectivity is necessary for preserving the truth of formulas of the formAψ(along the bounded morphism). Then we obtainTree Λ (M,w),⟨w⟩|=φiffM,tail(⟨w⟩)|= φ, wheretail(⟨w⟩) =w. SinceR Λ G = T a∈G R Λ a holds,(Finpath(M,w),(R Λ a ) a∈Ag )∈F Λ . Sinceφ is valid inF Λ , we obtain(Finpath(M,w),(R Λ a ) a∈Ag ,V),⟨w⟩|=φ, henceTree Λ (M,w),⟨w⟩|=φin terms of pseudo models. Therefore, it follows from the above equivalence thatM,w|=φ, as desired. 7 Conclusion There are several directions for further research. First, there have been attempts to combine epistemic logic with coalition logicCL, which is a logic that concerns coalitional power (see [1]). It would be interesting to develop sequent calculi forCLwith distributed knowledge and to investigate whether analytic cut properties can be established. Second, to the best of the authors’ knowledge, a syntactic proof of the analytic cut property in the style of [28] isnotavailable for our sequent calculi. The main obstacle appears to lie in the parameterization of the operator by a groupG. However, a Gentzen-style sequent calculus forS5was introduced in [12], in which the operator is not parameterized by groups. It would therefore be interesting to investigate whether Takano’s syntactic strategy can be adapted to systems combining this calculus withCL. Third, Hilbert systems and cut-free sequent calculi for intuitionistic K,KT,KD,K4,K4D, andS4with distributed knowledge were introduced in [18]. Building on this line of work, public announcement expansions of intuitionisticK,KT,K4, andS4with distributed knowledge were studied in [20]. It would therefore be worthwhile to investigate intuitionistic versions ofK45,KD45, andS5with distributed knowledge, and to examine whether these intuitionistic systems can be expanded with public announcement logic via the approach used in [14], as well as whether the main proof-theoretic results are preserved under such extensions. Finally, an axiomatization for comparative knowledge was introduced in [4], which allows one to express that one group’s (distributed) knowledge includesallof another group’s (distributed) knowledge. It would therefore be interesting to develop sequent calculi for this expansion of distributed knowledge and examine whether the main proof-theoretic results established in this paper still hold. Acknowledgements The authors would like to thank the three reviewers for their constructive comments and suggestions, which have helped improve the quality of the manuscript. The work of the second author is supported by the China Scholarship Council (CSC). The work of the third author was partially supported by JSPS KAKENHI Grant-in-Aid for Scientific Research (B) Grant Number JP22H00597 and Grant-in-Aid for Scientific Research (C) JP25K03537. References [1] Thomas Ågotnes & Natasha Alechina (2016):Coalition Logic with Individual, Distributed and Common Knowledge.Journal of Logic and Computation29(7), p. 1041–1069, doi:10.1093/logcom/exv085. [2] Thomas Ågotnes & Yì N. Wáng (2017):Resolving Distributed Knowledge.Artificial Intelligence252, p. 1–21, doi:10.1016/j.artint.2017.07.002. [3] Thomas Ågotnes & Yì N Wáng (2021):Group Belief.Journal of Logic and Computation31(8), p. 1959– 1978, doi:10.1093/logcom/exaa068. R. Murai & S. Liu & K. Sano653 [4] 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 Computing73, EasyChair, Manchester, UK, p. 90–119, doi:10.29007/plm4. [5] 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, p. 95–113, doi:10.1007/978-3-032-22469-9_6. [6] Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1995):Reasoning About Knowledge. The MIT Press, doi:10.7551/mitpress/5803.001.0001. [7] 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. [8] Ronald Fagin, Joseph Y. Halpern & Moshe Y. Vardi (1992):What Can Machines Know? On the Properties of Knowledge in Distributed Systems.J. ACM39(2), p. 328–376, doi:10.1145/128749.150945. [9] Gerhard Gentzen (1964):Investigations into Logical Deduction.American Philosophical Quarterly1(4), p. 288–306. [10] Gerhard Gentzen (1965):Investigations into Logical Deduction: I.American Philosophical Quarterly2(3), p. 204–218. [11] J. D. Gerbrandy (1999):Bisimulations on Planet Kripke. Amsterdam ILLC Dissertation Series, Amsterdam, The Netherlands. [12] Haroldas Giedra (2010):Cut Free Sequent Calculus for Logic S5n(ED).Lietuvos matematikos rinkinys51, doi:10.15388/LMR.2010.61. [13] 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, p. 100–116, doi:10.1007/978-3-540-88833-8_6. [14] 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, p. 190–206, doi:10.1007/978-3-031-45558-2_15. [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. [16] Akio Maruyama, Satoshi Tojo & Hiroakira Ono (2003):Temporal epistemic logics for multi-agent mod- els and their efficient proof-search procedure (in Japanese).Computer Software20(1), p. 51–65, doi:10.11309/jssst.20.51. [17] 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, p. 211–221, doi:10.1007/978-3-030-39951-1_13. [18] Ryo Murai & Katsuhiko Sano (2022):Intuitionistic Epistemic Logic with Distributed Knowledge.Com- putación y Sistemas26(2), doi:10.13053/cys-26-2-4259. [19] 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. [20] Ryo Murai & Katsuhiko Sano (2024):Intuitionistic Public Announcement Logic with Distributed Knowledge. Studia Logica112(3), p. 661–691, doi:10.1007/s11225-023-10066-1. [21] Masao Ohnishi & Kazuo Matsumoto (1959):Gentzen Method in Modal Calculi. I.Osaka Mathematical Journal11(2), p. 115–120. [22] Hiroakira Ono (1998):Proof-Theoretic Methods in Nonclassical Logic – an Introduction.In: Theories of Types and Proofs, 2, Mathematical Society of Japan, Tokyo, Japan, p. 207–255, doi:10.2969/msjmemoirs/00201C060. 654Analytic Cut in Epistemic Logics with Distributed Knowledge [23] 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, p. 601–623. [24] Regimantas Pliuškevi ˇ cius & Aida Pliuškevi ˇ cien ̇ e (2008):Termination of Derivations in a Fragment of Tran- sitive Distributed Knowledge Logic.Informatica19(4), p. 597–616, doi:10.15388/Informatica.2008.232. [25] Floris Roelofsen (2007):Distributed Knowledge.Journal of Applied Non-Classical Logics17(2), p. 255– 273, doi:10.3166/jancl.17.255-273. [26] Maehara Shoji (1961):Craig No Interpolation Theorem (On Craig’s Interpolation Theorem).Sugaku12(4), p. 235–237, doi:10.11429/sugaku1947.12.235. [27] 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, p. 245–256, doi:10.1007/3-540-51237-3_20. [28] Mitio Takano (1992):Subformula Property as a Substitute for Cut-Elimination in Modal Propositional Log- ics.Mathematica Japonica37(6), p. 1129–1145. [29] Mitio Takano (2001):A Modified Subformula Property for the Modal Logics K5 and K5D.Bulletin of the Section of Logic30(2), p. 115–122. [30] Mitio Takano (2018):A Semantical Analysis of Cut-Free Calculi for Modal Logics.Reports on Mathematical Logic53, p. 43–65, doi:10.4467/20842589RM.18.003.8836. [31] Balder Ten Cate (2005):Interpolation for Extended Modal Languages.Journal of Symbolic Logic70(1), p. 223–234, doi:10.2178/jsl/1107298517. [32] A. S. Troelstra & Helmut Schwichtenberg (2000):Basic Proof Theory.Cambridge Tracts in Theoretical Computer Science43, Cambridge University Press, Cambridge, doi:10.1017/CBO9781139168717. [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, p. 233–246, doi:10.1007/978-3-031-89610-1_17. [34] 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. [35] Yì N. Wáng & Thomas Ågotnes (2013):Public Announcement Logic with Distributed Knowledge: Expres- sivity, Completeness and Complexity.Synthese190(S1), p. 135–162, doi:10.1007/s11229-012-0243-3.