Paper deep dive
Common Belief Revisited
Thomas Ågotnes
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 7/21/2026, 3:39:53 AM
Summary
This paper investigates the logical properties of common belief in multi-agent systems where individual belief follows the KD45 axiomatization. It demonstrates that common belief is not simply KD4, but possesses additional properties, specifically shift-reflexivity (C(Cφ→φ)) and a property dependent on the number of agents (C^n). The author provides a complete axiomatization for common belief over KD45, showing that the logic varies depending on the number of agents, thereby settling an open problem in epistemic logic.
Entities (9)
Relation Signals (6)
Thomas Ågotnes → authored → Common Belief Revisited
confidence 98% · Thomas Ågotnes University of Bergen and Shanxi University Abstract
Common Belief → dependson → Number of Agents
confidence 95% · there is one additional axiom, and, furthermore, it relies on the number of agents.
Common Belief → hasproperty → C(Cφ→φ)
confidence 95% · But it has another property: C(C\phi\rightarrow\phi) -- corresponding to so-called shift-reflexivity
Hans van Ditmarsch → collaboratedwith → Thomas Ågotnes
confidence 90% · Many thanks to Hans van Ditmarsch for significant input on this work.
Andreas Herzig → collaboratedwith → Thomas Ågotnes
confidence 85% · This paper is identical to the version appearing in the Festscrift in honour of Andreas Herzig’s 65th birthday
Common Belief → hasproperty → KD4
confidence 80% · Contrary to common belief, common belief is not KD4.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Contrary to common belief, common belief is not KD4. If individual belief is KD45, common belief does indeed lose the 5 property and keep the D and 4 properties -- and it has none of the other commonly considered properties of knowledge and belief. But it has another property: $C(C\phi \rightarrow \phi)$ -- corresponding to so-called shift-reflexivity (reflexivity one step ahead). This observation begs the question: is KD4 extended with this axiom a complete characterisation of common belief in the KD45 case? If not, what \emph{is} the logic of common belief? In this paper we show that the answer to the first question is ``no'': there is one additional axiom, and, furthermore, it relies on the number of agents. We show that the result is a complete characterisation of common belief, settling the open problem.
Tags
Links
- Source: https://arxiv.org/abs/2602.15403v1
- Canonical: https://arxiv.org/abs/2602.15403v1
Trouble viewing inline? Open PDF directly →
Full Text
41,522 characters extracted from source content.
Expand or collapse full text
Common Belief Revisited111This paper is identical to the version appearing in the Festscrift in honour of Andreas Herzig’s 65th birthday, published by College Publications (2025). Many thanks to Hans van Ditmarsch for significant input on this work. I also thank the anonymous reviewers for helpful comments. Thomas Ågotnes University of Bergen and Shanxi University Abstract Contrary to common belief, common belief is not KD4. If individual belief is KD45, common belief does indeed lose the 5 property and keep the D and 4 properties – and it has none of the other commonly considered properties of knowledge and belief. But it has another property222This was pointed out to me by Hans van Ditmarsch who knew it from Andreas Herzig who knew it from Giacomo Bonanno.: C(Cϕ→ϕ)C(Cφ→φ) – corresponding to so-called shift-reflexivity (reflexivity one step ahead). This observation begs the question333First raised, to me at least, by Andreas Herzig. This is typical: Andreas is a genuinely curious researcher who has a gift for asking the right questions and is generous with sharing his ideas. No wonder he is one of the most influential researchers in the area of (multi-)agent logic in general and epistemic logic in particular. Andreas has conjectured (personal communication) that the answer to the question is “yes”. He has also referred to it as (to him) “the most important open problem in epistemic logic” (personal communication, Hans van Ditmarsch). I am happy to be able to settle this problem in this paper, in honour of Andreas’ 65th birthday. I know that he would be absolutely delighted if the answer is “yes” and the conjecture is correct. I also know that he would be even more delighted if the answer is “no”. : is KD4 extended with this axiom a complete characterisation of common belief in the KD45 case? If not, what is the logic of common belief? In this paper we show that the answer to the first question is “no”: there is one additional axiom, and, furthermore, it relies on the number of agents. We show that the result is a complete characterisation of common belief, settling the open problem. 1 Introduction In standard (modal) logics of knowledge and belief [5, 11, 12], common knowledge and belief [9] are defined by taking the transitive closure of the union of the accessibility relations for the individual agents. It is well known that if the latter are equivalence relations, so is the former – when individual knowledge has the S5 properties then so does common knowledge. What about weaker notions of belief? The most commonly used model of belief is KD45. It is also well known that common belief in that case “inherits” the D and 4 properties, but not the negative introspection property 5. Indeed, among the most commonly considered properties, D and 4 (in addition to the standard properties of normal modalities) are in a certain sense the only properties of common belief over KD45 [2]. That doesn’t necessarily mean that common belief on KD45 is KD4, and that there are not other properties. And indeed there are. The formula C(Cϕ→ϕ)C(Cφ→φ) (CcCc) (where CϕCφ means that ϕφ is common belief by the grand coalition of all agents) is valid on KD45444This observation is attributed to Giacomo Bonanno (personal communication, Andreas Herzig).. To see this, observe that Euclidicity implies shift-reflexivity555A relation R is shift-reflexive iff RxyRxy implies RyyRyy for all x and y., and thus individual Eucludicity ensures that the common belief relation is reflexive in any state that is accessible by any agent from any other state. This again begs the question: are there any other properties, or is KD4Cc a complete characterisation of common belief? Consider the case that there are only two agents, and a formula of the form: (C^ϕ1∧C^ϕ2∧C^ϕ3)→C^((C^ϕ1∧C^ϕ2)∨(C^ϕ1∧C^ϕ3)∨(C^ϕ2∧C^ϕ3))( C _1 C _2 C _3)→ C(( C _1 C _2) ( C _1 C _3) ( C _2 C _3)) (C^2 C2) where C^ϕ=¬C¬ϕ Cφ= C φ. It is not too hard to see that this formula is valid: since there are only two agents, the first step on two of the paths to the three formulas must be for the same agent, and by individual Euclidicity there is a path to two of those formulas after one step. This means, first, that KD4Cc is not a complete characterisation (it is not too hard to see that C^2 C2 cannot be derived). Second, observe that C^2 C2 is not valid if there are three or more agents, so that means that a complete characterisation would be different for different numbers of agents. In this paper we show that that’s it: KD4 + CcCc + C^2 C2 is a sound and complete characterisation of common belief over KD45 for the language where the only modality is a common belief operator for the grand coalition, in the case of two agents – and similarly for any number of agents. Existing axiomatisations of common (knowledge and) belief are for languages that also have individual belief modalities, and common belief is characterised in terms of individual belief by fixed-point axioms666See also [6] for an intuitively elegant alternative axiom in terms of knowing-whether, that works only for logics with the T axiom. [8, 4, 10] like (where KiK_i is the individual knowledge modality for agent i and N is the set of all agents) C(ϕ→⋀i∈NKiϕ)→(⋀i∈NKiϕ→Cϕ)C(φ→ _i∈ NK_iφ)→( _i∈ NK_iφ→ Cφ) (sometimes an induction rule is used instead [5]). While this, together with axioms describing the properties of individual belief, indirectly gives us a precise and complete characterisation of common belief, it obfuscates the properties of common belief since they are entangled with individual belief in the description. By leaving individual belief out of the picture on the syntactic level and having only a single modality, for common belief of the grand coalition, in the language, in this paper we get a direct and explicit complete characterisation of the core properties of common belief. The rest of the paper is organised as follows. In the next section we formally define the language and the semantics, and the axiomatisations are presented and shown to be sound in Section 3. The main result, completeness, is shown in Section 4. We briefly discuss taking the reflexive transitive closure instead of the transitive closure in Section 5, and conclude in Section 6. 2 Language and Semantics The language ℒCL_C is defined as follows, given a set of atomic propositions P. ϕ::=p∣¬ϕ∣ϕ∧ϕ∣Cϕφ::=p φ φ φ Cφ where p∈Pp∈ P. We write C^ϕ Cφ for ¬C¬ϕ C φ, in addition to using the usual derived propositional connectives. The language is interpreted in multi-agent Kripke models M=(W,R,V)M=(W,R,V) over P and a finite set of agents N (without loss of generality we assume that N=1,…,nN=\1,…,n\): • W is a non-empty set of states; • Ri⊆W×WR_i W× W is an accessibility relation for each agent i∈Ni∈ N; • V:P→WV:P→ W is a valuation function. A KD45 model is a model where each accessibility relation is serial, transitive and Euclidian. The class of all KD45 models for n agents (|N|=n|N|=n) is denoted KD45nKD45_n. Let R∗=(⋃i∈NRi)∗R^*=( _i∈ NR_i)^* where Q∗Q^* is the transitive closure of the binary relation Q on W. The language is interpreted in these models as follows: M,s⊧p⇔s∈V(p)M,s⊧¬ϕ⇔M,s⊧̸ϕM,s⊧ϕ∧ψ⇔M,s⊧ϕ and M,s⊧ψM,s⊧Cϕ⇔∀t∈W:R∗st⇒M,t⊧ϕ array[]lclM,s p& &s∈ V(p)\\ M,s φ& &M,s φ\\ M,s φ ψ& &M,s φ and M,s ψ\\ M,s Cφ& &∀ t∈ W:R^*st M,t φ array 3 Axiomatisation As discussed in the introduction, common belief in the KD45 case has the 4 and D properties but (as in most cases with individual negative introspection with the exception of S5 [2]) loses the 5 property. A simple example illustrating the latter is shown in Figure 1. ∙s ^s 1 12 2∙t ^t 1 1∙u ^u 2 2 Figure 1: Simple KD45 model. As mentioned in the introduction, we also get the additional property C(Cϕ→ϕ)C(Cφ→φ) (CcCc) This is perhaps easiest seen by observing that in a KD45 model the R∗R^* relation is shift-reflexive, since any state that is accessible from some other state by at least one agent has a reflexive loop for that agent due to individual Euclidicity. In particular, if a formula ϕφ is satisfied in some state s of a model then every state with the possible exception of the initial state s in the generated submodel of that model from s is reflexive. Of course, this property is not “new” – as just argued it is implied by (is a sub-property of) Euclidicity. So, we don’t lose 5 completely, only partially. The second “new” class of properties we get are the following: C(⋀1≤i<j≤n+1(Cϕi∨Cϕj))→⋁1≤i≤n+1CϕiC ( _1≤ i<j≤ n+1(C _i C _j) )→ _1≤ i≤ n+1C _i (CnCn) where n is the number of agents. It might be instructive to observe that the following is equivalent: ⋀1≤i≤n+1C^ϕi→C^⋁1≤i<j≤n+1(C^ϕi∧C^ϕj) _1≤ i≤ n+1 C _i→ C _1≤ i<j≤ n+1( C _i C _j) (C^n Cn) Lemma 1. CnCn is canonical for the (FOL) property ∀xy1…yn+1((⋀1≤i≤n+1Rxyi)→∃z(Rxz∧⋁1≤i<j≤n+1(Rzyi∧Rzyj)))∀ xy_1… y_n+1 (( _1≤ i≤ n+1Rxy_i)→∃ z (Rxz _1≤ i<j≤ n+1(Rzy_i Rzy_j) ) ) Proof. C^n Cn is a (“very simple”) Sahlqvist formula, and it can be shown that the property in the lemma is its first-order correspondent (see [3, Theorem 3.42]). Thus, the formula is canonical for that property (see [3, Theorem 4.42]). ∎ In other words, this property says that if I can see n+1n+1 states, then I can see a state that can see two of them. Again, this property is not “new” – it is implied by the 55 axiom (Euclidicity, in which case all of those n+1n+1 states can see each other). Thus, instead of just dropping the 5 axiom we replace it with two weaker axioms: CnCn and CcCc. By adding those axioms to KD4, we get the axiomatisation CBnCB_n shown in Table 1. all instances of propositional tautologies PropProp C(ϕ→ψ)→(Cϕ→Cψ)C(φ→ψ)→(Cφ→ Cψ) K Cϕ→¬C¬ϕCφ→ C φ D Cϕ→CCϕCφ→ Cφ 44 C(Cϕ→ϕC(Cφ→φ) CcCc (C⋀1≤i<j≤n+1(Cϕi∨Cϕj))→⋁1≤i≤n+1Cϕi(C _1≤ i<j≤ n+1(C _i C _j))→ _1≤ i≤ n+1C _i CnCn From ϕ→ψφ→ψ and ϕφ, derive ψ MPMP From ϕφ, derive CϕCφ NecNec Table 1: Axiomatisation CBnCB_n over the language ℒCL_C. Lemma 2. For any n≥2n≥ 2, CBnCB_n is sound wrt. the class of KD45nKD45_n models. Proof. Validity (preservation) for K and NecNec follow from the fact that C is normal (has standard relational semantics). Validity of D and 44 is well known [2]. For CcCc, for any state w and agent j, by Euclidicity of RjR_j, if RjwvR_jwv then RjvvR_jv. Then also R∗vvR^*v. Thus, if M,v⊧CϕM,v Cφ then M,v⊧ϕM,v φ. For CnCn, we use the equivalent C^n Cn. Let t1,…,tn+1t_1,…,t_n+1 be such that (s,ti)∈R∗(s,t_i)∈ R^* and M,ti⊧ϕiM,t_i _i, for each 1≤i≤n+11≤ i≤ n+1. In other words, for each i there is an R∗R^*-path ti0ti1⋯tinit_i^0t_i^1·s t_i^n_i, such that ti0=st_i^0=s and tini=tit_i^n_i=t_i. Since ti0R∗ti1t_i^0R^*t_i^1 for each 1≤i≤n+11≤ i≤ n+1 and there are only n agents, two of those first steps on those n+1n+1 paths must be for the same agent j: sRjtj1sR_jt_j^1 and sRjtk1sR_jt_k^1 for some j≠kj≠ k. By Euclidicy of RjR_j then we also have that tj1Rjtk1t_j^1R_jt_k^1. Then M,tj1⊧C^ϕj∧C^ϕkM,t_j^1 C _j C _k, and M,s⊧C^(C^ϕj∧C^ϕk)M,s C( C _j C _k). ∎ Note that CnCn does not hold for the case of m>nm>n agents. For example, C2C2 holds in the case of two agents but not in the case of three. We thus get different systems CBnCB_n for different numbers of agents. These two additional axioms are all we need, as we now show. 4 Completeness We construct a satisfying KD45nKD45_n model for any CBnCB_n-consistent formula. Two be able to focus on the key ideas we give the proof in full detail for the case n=2n=2; in Section 4.1 we describe how it is generalised. Thus, henceforth assume that n=2n=2. The main ideas are as follows, with some pointers to the technical details that follow: • We take the standard canonical uni-modal model for CBnCB_n (with a single relation interpreting the C modality) as the starting point (Def. 1 below). • We need a model where the transitions in the relation are “labeled” by agent names. However, we cannot just label all the transitions in the canonical model by some agent – some of them correspond not to single agents but to sequences of agents due to transitivity of the common belief relation. • Also, if we label two outgoing transitions from the same state by the same agent, we need to make sure that the two incoming states are also related, due to individual Euclidicity. • Key idea number one: if a state (1) is reflexive and (2) has at most one other incoming transition already labeled by an agent name, say agent 1, we can do the following: if the state has k777This also works when the number of outgoing transitions is not finite. outgoing transitions, split it into k copies with universal access between them for agent 1, each with one outgoing transition for agent 2. This does not affect satisfaction of any ℒCL_C formulas; in fact the resulting model will be bisimilar when we take the transitive closure of union of the new accessibility relations (Lemma 7 below). • If we take the generated submodel of the canonical uni-modal model, then all reachable states will be reflexive, taking care of condition (1). • .. and we can also make it into a tree-like model in (pretty much) the standard way, taking care of condition (2). • This transformation can be done recursively, for each state, possibly except the initial state which might not be reflexive, by alternating the agent names: states with ingoing transitions for agent 2 get split into an agent 2 cluster. • The transformation takes care of individual Euclidicity, since each new state only has one outgoing transition in addition to the reflexive loop. It also takes care of individual transitivity by alternating between agents. • Key idea number two: this leaves us with the initial state, and this is where the C2C2 axiom is needed. The initial state might have infinitely many directly accessible states, but to satisfy a (finite) formula we only need finitely many of them, at most corresponding to each subformula C^ψ Cψ we need to satisfy. For each triple of those states, the C2C2 axiom ensures that the initial state can access some state that can access two of them (possibly not among the already identified states). That state then acts as a “proxy” for those two states since they can be reached by transtitive closure, and therefore we no longer need to be able to access those two states directly by the relation for some agent. We can thus replace those two states with the new one, and by repeating the process we can get down to at most two states that can access all the other needed states which thus can be reached through transitive closure. The transitions from the initial state to those two states can each be labeled with one of the two agents. (The set XwX^cl_w defined below, where cl gives us the set of C^ψ Cψ subformulas and w is the initial state, is the set of those two states). • The model construction proceeds recursively, building up a tree-like model level by level. Start with the initial node w and its two successors identified above; make one copy of those successors for each outgoing transition (in the canonical model) each receiving an ingoing transition from w for the same agent; add universal access for the same agent inside the cluster; repeat for the outgoing transitions in the new nodes but for the other agent. The construction is illustrated in Figure 2. Y0: Y_0:w w 1 12 2Y1: Y_1:… … 2 22 2… … 1 11 1Y2: Y_2:… … 1 1… … 1 1… … 2 2… …Y3: Y_3:… … … …⋮ Figure 2: Part of the model construction. Each cluster (denoted ⋯·s) has incoming transitions of only one type, has internal universal access for the same type, and has one outgoing transition of the opposite type for each node in the cluster. We proceed with the details. It might be helpful to keep an eye on Figure 2. A uni-modal model is a structure M=(W,R,V)M=(W,R,V) where W and V are like in a (multi-agent) model, and R⊆W×WR W× W is a single accessibility relation. The ℒCL_C language is interpreted in uni-modal models by letting M,s⊧CϕM,s Cφ iff M,t⊧ϕM,t φ for all t∈Wt∈ W such that RstRst (and letting the other clauses be as in the interpretation in a model). Definition 1 (Canonical uni-modal model). The canonical uni-modal model Mc=(Wc,Rc,Vc)M^c=(W^c,R^c,V^c) is defined as follows: • WcW^c is the set of all maximal CBnCB_n-consistent sets; • RcwvR^cwv iff for all formulas ψ, if ψ∈vψ∈ v then C^ψ∈w Cψ∈ w; • V(p)=w:p∈WV(p)=\w:p∈ W\. We say that an MCS Γ is branching if ΓRcΔ R^c and ΓRcΔ′ R^c for some MCSs Δ≠Δ′ ≠ . We say that a set of formulas cl is proper iff it is finite, is closed under subformulas, contains C^⊤ C , and contains C^¬ψ C ψ whenever it contains CψCψ. Let w be a branching MCS and cl be proper set of formulas. We now define a finite set Xw⊆WcX^cl_w W^c of states. We start with recursively defining Xi(,w)X^(cl,w)_i for each natural number i. X0(,w)X^(cl,w)_0 Let ψ0,…,ψk _0,…, _k be the (finitely many) different formulas of the form C^χ Cχ in cl. For each ψi=C^χi _i= C _i, if Mc,w⊧C^χiM^c,w C _i let ui∈Wcu_i∈ W^c be such that RcwuiR^cwu_i and Mc,ui⊧χiM^c,u_i _i. Finally let X0(,w)=u0,…,ukX^(cl,w)_0=\u_0,…,u_k\. Xi+1(,w)X^(cl,w)_i+1 If Xi(,w)X^(cl,w)_i contains less than three nodes we are done, and let Xi+1(,w)=Xi(,w)X^(cl,w)_i+1=X^(cl,w)_i. Otherwise, let t,u,vt,u,v be three (pair-wise) different nodes in Xi(,w)X^(cl,w)_i. By Lemma 1 (with x=wx=w) there is a z∈Wcz∈ W^c such that RcwzR^cwz that can see two of those three states. Without loss of generality assume that those are t and u, i.e., that RcztR^czt and RczuR^czu. Let Xi+1(,w)=(Xi(,w)∖t,u)∪zX^(cl,w)_i+1=(X^(cl,w)_i \t,u\)∪\z\. Lemma 3. For some i≥0i≥ 0, Xi+1(,w)=Xi(,w)X^(cl,w)_i+1=X^(cl,w)_i. Proof. X0(,w)X^(cl,w)_0 is finite by definition. Xi+1(,w)=Xi(,w)∖t,u∪zX^(cl,w)_i+1=X^(cl,w)_i \t,u\∪\z\ has at least one state less than Xi(,w)X^(cl,w)_i (two if z is already in Xi(,w)X^(cl,w)_i). ∎ Thus, let X(,w)=Xi(,w)X^(cl,w)=X^(cl,w)_i, where i is the lowest number such that Xi+1(,w)=Xi(,w)X^(cl,w)_i+1=X^(cl,w)_i. Lemma 4. 1. |X(,w)|>0|X^(cl,w)|>0 2. |X(,w)|<3|X^(cl,w)|<3 3. for any t∈X0(,w)t∈ X^(cl,w)_0 there is a u∈X(,w)u∈ X^(cl,w) such that RcutR^cut Proof. 1. By the D axiom, C^⊤∈w C ∈ w, so there is at least one state u such that RcwuR^cwu. Each step in the elimination process removes at most two states when there is at least three states left. 2. By definition, Xi+1(,w)X^(cl,w)_i+1 contains at least one state less than Xi(,w)X^(cl,w)_i when the latter has more than two states. 3. Let t∈X0(,w)t∈ X^(cl,w)_0. We show that for any i, there is a u∈Xi(,w)u∈ X^(cl,w)_i such that RcutR^cut. For the base case let u=tu=t: RcttR^ct due to RcwtR^cwt and the CcCc axiom. For the inductive case, let Xi+1(,w)=(Xi(,w)∖t′,u′)∪zX^(cl,w)_i+1=(X^(cl,w)_i \t ,u \)∪\z\ where RcwzR^cwz and Rczt′R^czt and Rczu′R^czu . By the inductive hypothesis there is a u∈Xi(,w)u∈ X^(cl,w)_i such that RcutR^cut. If u≠t′u≠ t and u≠u′u≠ u then also u∈Xi+1(,w)u∈ X^(cl,w)_i+1. Consider the case that u=t′u=t . Since Rczt′R^czt and RcutR^cut, we have that RcztR^czt by transitivity (axiom 44). Thus, let u=zu=z. ∎ Finally, we define the set XwX^cl_w (given cl and the branching MCS w). If |X(,w)|=2|X^(cl,w)|=2, let Xw=X(,w)X^cl_w=X^(cl,w). Otherwise, let u∈Wcu∈ W^c be such that RcwuR^cwu and u∉X(,w)u ∈ X^(cl,w) (it exists since w is branching), and let Xw=X(,w)∪uX^cl_w=X^(cl,w)∪\u\. In either case |Xw|=2|X^cl_w|=2, so henceforth assume that Xw=x0,y0X^cl_w=\x_0,y_0\. Given a proper cl and a branching MCS w, we are now going to build a model M(,w)=(W,R,V)M_(cl,w)=(W,R,V). We first define a set of states YiY_i and a set of paths Πi _i, for each natural number i, by mutual recursion (keeping in mind that these sets are parameterised by cl and w). The former is in turn defined in terms of sets YiπY^π_i where π∈Πiπ∈ _i is a path. The empty path is denoted ϵε (as usual we write πxπ x for the concatination of path π with state x, and when π=ϵπ=ε we omit π in the concatination and write just x for ϵxε x). Any non-empty path888We slightly abuse the word “path” here, as a sequence of symbols representing states. In fact, a path is actually a path in the resulting model, with the exception of the possible initial states w1w^1 or w2w^2 in the path which both represent the root node w. We use w1w^1 and w2w^2 to distinguish between left paths and right paths. starts with either w1w^1 or w2w^2. A path that starts with w1w^1 is called a left path; a path that starts with w2w^2 is called a right path. The model construction is illustrated in Figure 2. • i=0i=0: Y0=Y0ϵ=wY_0=Y^ε_0=\w\. Π0=ϵ _0=\ε\. • i=1i=1 (recall that Xw=x0,y0)X^cl_w=\x_0,y_0\): – Π1=w1,w2 _1=\w^1,w^2\ – Y1w1=xzw1:Rcx0zY^w^1_1=\x^w^1_z:R^cx_0z\ and Y1w2=yzw2:Rcy0zY^w^2_1=\y^w^2_z:R^cy_0z\ – Y1=Y1w1∪Y1w2Y_1=Y^w1_1∪ Y^w2_1 • i≥2i≥ 2, i=j+1i=j+1: – Πi=πv:π∈Πj,v∈Yjπ _i=\π v:π∈ _j,v∈ Y_j^π\ – For each π∈Πjπ∈ _j and v=tsπ∈Yjπv=t^π_s∈ Y^π_j, Yiπv=szπv:RcszY^π v_i=\s^π v_z:R^csz\ – Yi=⋃π∈ΠiYiπY_i= _π∈ _iY^π_i Finally, let the model M(,w)=(W,R,V)M_(cl,w)=(W,R,V) be defined as follows: • W=⋃i≥0YiW= _i≥ 0Y_i • R1uvR_1uv iff v∈Yiπv∈ Y_i^π for i≥1i≥ 1 and – if π is a left path: * i=1i=1 and u=wu=w, or * i≠1i≠ 1 is odd and u∈Yi−1π′u∈ Y^π _i-1 such that π=π′uπ=π u, or * i is odd and u∈Yiπu∈ Y^π_i. – if π is a right path: * i is even and u∈Yi−1π′u∈ Y^π _i-1 such that π=π′uπ=π u, or * i is even and v∈Yiπv∈ Y^π_i. • R2uvR_2uv iff v∈Yiπv∈ Y_i^π for i≥1i≥ 1 and (just swap “left” and “right” above): – if π is a right path: * i=1i=1 and u=wu=w, or * i≠1i≠ 1 is odd and u∈Yi−1π′u∈ Y^π _i-1 such that π=π′uπ=π u, or * i is odd and u∈Yiπu∈ Y^π_i. – if π is a left path: * i is even and u∈Yi−1π′u∈ Y^π _i-1 such that π=π′uπ=π u, or * i is even and v∈Yiπv∈ Y^π_i. • V(p)=szπ∈W:s∈Vc(p)∪(w∩Vc(p))V(p)=\s^π_z∈ W:s∈ V^c(p)\∪(\w\∩ V^c(p)) Lemma 5. For any branching w∈Wcw∈ W^c and proper cl, M(,w)M_(cl,w) is a KD452KD45_2 model. Proof. For seriality, consider the case for R1R_1. For w, we have that R1wxz′w1R^1wx^w^1_z for some z′z such that Rcx0zR^cx_0z (exists since RcR^c is serial). Let x′=szπ∈Yiπx =s^π_z∈ Y^π_i. First assume that π is a left path. If i is odd then R1x′x′R_1x x . If i≠0i≠ 0 is even, let z′z be such that Rczz′R^cz (it exists since RcR^c is serial). We have that z′πszπ∈Yi+1πszπz^π s^π_z_z ∈ Y_i+1^π s^π_z, and R1szπz′πszπR_1s^π_zz^π s^π_z_z by definition. The cases for the right path, and for R2R_2, are similar. For transitivity, consider frist R1R_1. Assume that R1abR_1ab and R1bcR_1bc, where b∈Yiπb∈ Y^π_i for some π and i. If π is a left path, R1abR_1ab can only hold if i is odd. Then R1bcR_1bc implies that also c∈Yiπc∈ Y^π_i since the only outgoing transitions from YiπY^π_i when i is odd and π is left is to other nodes inside YiπY^π_i. Then, by definition, also R1acR_1ac. If π is a right path the argument is symmetric: then R1abR_1ab can only hold if i is even. Then R1bcR_1bc implies that also c∈Yiπc∈ Y^π_i since the only outgoing transitions from YiπY^π_i when i is even and π is right is to other nodes inside YiπY^π_i. Then, by definition, also R1acR_1ac. Thus, R1R_1 is transitive. Transitivity of R2R_2 can be shown in exactly the same way. For euclidicity, by construction, all outgoing transitions for RkR_k (k∈1,2k∈\1,2\) from any state goes to the same set YiπY^π_i, and RkR_k has universal accessibility inside that set. ∎ Let M(,w)∗=(W,R∗,V)M^*_(cl,w)=(W,R^*,V) be the uni-modal variant of M(,w)M_(cl,w), which has the same state space and valuation function and where R∗=(R1∪R2)∗R^*=(R_1∪ R_2)^*. The following is immediate from the definition: Lemma 6. For any formula ϕφ and state v∈Wv∈ W, M(,w),v⊧ϕM_(cl,w),v φ iff M(,w)∗,v⊧ϕM^*_(cl,w),v φ In the constructed model we have several copies szπs^π_z of states s in the canonical model, for each path π and for each outgoing transition from s to state z in the canonical model. We show that every state in (the uni-modal) model M(,w)∗M^*_(cl,w), except the inital state w, is bisimilar (see the appendix for definitions) to the corresponding state in the (uni-modal) canonical model. Lemma 7. For any szπ∈Ws^π_z∈ W, M(,w)∗,szπ⇆Mc,sM^*_(cl,w),s^π_z M^c,s. Proof. Let the relation Z⊆(W∖w)×WcZ (W \w\)× W^c be defined by: szπZs^π_zZs. We show that it is a bisimulation: • Atoms: immediate. • Forth: Let szπZs^π_zZs and szπR∗sz′π′s^π_zR^*s π _z . If s′=s =s, then sRcs′sR^cs (since s≠ws≠ w). Assume that s′≠s ≠ s. The path from szπs^π_z to sz′π′s π _z in M(,w)M_(cl,w) consists of a sequence of steps some of which are inside the same cluster YiπY_i^π (where all nodes correspond to the same node in McM^c) and some that go from one cluster Yiπ′Y_i^π to the next Yi+1πtxπ′Y_i+1^π t^π _x such that RctxR^ctx. Simply disregard the former, and we are left with a path from s to s′s in McM^c. Thus, Rcss′R^cs , and we have that sz′π′Zs′s π _z Zs . • Back: Let szπZs^π_zZs and Rcss′R^cs . Assume that szπ∈Yiπs^π_z∈ Y^π_i. Then also s′π∈Yiπs^π_s ∈ Y^π_i, and szπRks′πs^π_zR_ks^π_s for k=1k=1 or k=2k=2. By construction, s′πRk¯s′z′πs′πs^π_s R_ ks ^π s^π_s _z for some z′z , where 1¯=2 1=2 and 2¯=1 2=1. Thus, szπR∗sz′π′s^π_zR^*s π _z . ∎ Lemma 8. For any branching w∈Wcw∈ W^c and any proper cl, for any formula ϕ∈φ , M(,w),w⊧ϕM_(cl,w),w φ iff Mc,w⊧ϕM^c,w φ. Proof. The proof is by induction on the structure of ϕ∈φ . • ϕ=p∈Pφ=p∈ P: M(,w),w⊧pM_(cl,w),w p iff w∈V(p)w∈ V(p) iff w∈Vc(p)w∈ V^c(p) iff Mc,w⊧pM^c,w p. • Boolean connectives: straightforward. • ϕ=Cψφ=Cψ: for the implication towards the left, we show the contrapositive. Assume that M(,w),w⊧̸ϕM_(cl,w),w φ. M(,w),w⊧C^¬ψM_(cl,w),w C ψ, i.e., there is a szπ∈Ws^π_z∈ W such that R∗wszπR^*ws^π_z and M(,w),szπ⊧¬ψM_(cl,w),s^π_z ψ. The path from w to szπs^π_z in M(,w)M_(cl,w) consists of a sequence of steps some of which are inside the same cluster YiπY^π_i (where all nodes correspond to the same node in McM^c) and some that go from one cluster Yiπ′Y_i^π to the next Yi+1πtzπ′Y_i+1^π t^π _z such that RctzR^ctz. Simply disregard the former, and we are left with a path from w to s in McM^c. By Lemmas 6 and 7, Mc,s⊧¬ψM^c,s ψ. Thus, Mc,w⊧C^¬ψM^c,w C ψ. For the direction towards the right, we show the contrapositive. Assume that Mc,w⊧C^¬ψM^c,w C ψ. Since C^¬ψ∈ C ψ , there is a v∈X0(,w)v∈ X_0^(cl,w) such that Mc,v⊧¬ψM^c,v ψ. By Lemma 4.3, there is a u∈X(,w)u∈ X^(cl,w) such that RcuvR^cuv. By construction of M(,w)M_(cl,w) that means that RkuvwxvzwxuvwxR_ku^w^x_vv^w^xu^w^x_v_z (for some x∈1,2x∈\1,2\ and z) for some k∈1,2k∈\1,2\, and since we also have that RjwuvwxR_jwu^w^x_v (for some j), we get that R∗wvzwxuvwxR^*wv^w^xu^w^x_v_z. By Lemma 7, M(,w)∗,vzwxuvwx⊧¬ψM_(cl,w)^*,v^w^xu^w^x_v_z ψ and by Lemma 6 M(,w),vzwxuvwx⊧¬ψM_(cl,w),v^w^xu^w^x_v_z ψ. Thus, M(,w),w⊧C^¬ψM_(cl,w),w C ψ. ∎ Theorem 1. CB2CB_2 is complete wrt. the class of all KD452KD45_2 models. Proof. Assume that ϕφ is consistent. Let ϕ′=ϕ∧C^p∧C^¬pφ =φ Cp C p, for some p not occurring in ϕφ. It is easy to see that ϕ′φ is consistent. By the standard Lindenbaum construction ϕφ is included in some branching MCS Φ . We have that Mc,Φ⊧ϕM^c, φ by the standard truth lemma for canonical (in this case uni-modal) models. Let cl be the smallest set containing all subformulas of ϕ′φ as well as C^⊤ C and that is closed under the rule: if Cψ∈Cψ then C^¬ψ∈ C ψ (this set is finite). By Lemma 8 M(,Φ),Φ⊧ϕM_(cl, ), φ. Thus, ϕφ is satisfiable on a KD452KD45_2 model (Lemma 5). ∎ 4.1 The general case The proof for the case that n>2n>2 is almost identical, with only two minor differences: • n outgoing transitions from the initial state: in the first step of the model construction, we use the CnCn axiom in exactly the same way to get the set XwX^cl_w, now consisting of n (instead of 2) states. • Choice of alternating agents and seriality: we only need two agents for alternation, so for each of those n outgoing transitions from the initial state we can chose one other agent to alternate with along the path. To take care of seriality for the other agents, within each cluster also add reflexive access for any other agent, different from those two (those states all have incoming transitions and thus are reflexive so adding reflexive access for some agents doesn’t change anything). We get the following. Theorem 2. For any n≥2n≥ 2, CBnCB_n is sound and complete wrt. the class of all KD45nKD45_n models. 5 Reflexive transitive closure Sometimes (e.g., in [13, 7, 12]), the reflexive transitive closure is used instead of transitive closure – albeit mostly in the case of S5 knowledge when the two definitions coincide. We still give the following result for the KD45 case, with reflexive transitive closure. Recall that S4 = KT4. Theorem 3. S4 over the language ℒCL_C, where CϕCφ is interpreted by taking the reflexive transitive closure, is sound and complete wrt. all KD45nKD45_n models, for any n≥1n≥ 1. Proof. Proof sketch: this can be shown exactly like in the transitive case. Note that both CcCc and CnCn follow from reflexivity (the T axiom). In this case the proof can be simplified, since also the initial state is reflexive. ∎ 6 Conclusions Not only is common belief based on individual KD45 belief not merely KD4, but the additional properties are different for different numbers of agents. This is obfuscated by the standard axiomatisations in terms of individual belief and induction axioms/rules. It is also similar to the case for somebody-knows [1]. By adding the CcCc and CnCn axioms to KD4, we get a family of logics, and we showed that each of them is a complete characterisation of common belief for n KD45 agents, in the language with only one common belief operator for the grand coalition. The proof depends crucially on the ability to alternate agents between the clusters, which is why n≥2n≥ 2 is required: the corresponding result for one agent does not hold (otherwise KD45 would be equal to KD4CcC1, which it is not). This depends on the standard interpretation in a class of models with a finite and fixed number of agents. Of course, since we (unlike in the case of one common belief operator for each group of agents) don’t have agent names in the syntax, that is not necessary – we could, alternatively, interpret the language in the broader classes of (1) all models with any finite number of agents, or (2) all models with countably infinitely many agents. We have to leave out details due to the restricted space but in both cases the resulting logic is completely axiomatised by KD4Cc (i.e., by dropping the counting axiom). We also get a corresponding result for the case when individual belief is K45, by adapting the proof for the KD45 case (again, we have to leave out the details): the resulting logic is K4CcCn. Other cases, like K5 and KB, are left for future work. References [1] T. Ågotnes and Y. N. Wáng (2021) Somebody knows. In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, November 3-12, 2021, M. Bienvenu, G. Lakemeyer, and E. Erdem (Eds.), p. 2–11. External Links: Link, Document Cited by: §6. [2] T. Ågotnes and Y. N. Wáng (2021) Group belief. Journal of Logic and Computation 31 (8), p. 1959–1978. Cited by: §1, §3, §3. [3] P. Blackburn, M. de Rijke, and Y. Venema (2001) Modal logic. Cambridge Tracts in Theoretical Computer Science, Vol. 53, Cambridge University Press, Cambridge University Press. Cited by: §3. [4] G. Bonanno (1996) On the logic of common belief. Mathematical Logic Quarterly 42 (1), p. 305–311. Cited by: §1. [5] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi (1995) Reasoning about knowledge. The MIT Press, Cambridge, Massachusetts. Cited by: §1, §1. [6] A. Herzig and E. Perrotin (2020) On the axiomatisation of common knowledge.. In AiML, p. 309–328. Cited by: footnote 6. [7] W. Jamroga and W. van der Hoek (2004-05) Agents that know how to play. Fundamenta Informaticae 63 (2–3), p. 185–219. External Links: Document Cited by: §5. [8] D. Lehmann (1984) Knowledge, common knowledge and related puzzles (extended summary). In Proceedings of the third annual ACM symposium on Principles of distributed computing, p. 62–67. Cited by: §1. [9] D. K. Lewis (1969) Convention: a philosophical study. Harvard University Press. Cited by: §1. [10] L. Lismont and P. Mongin (1994) On the logic of common belief and common knowledge. Theory and Decision 37, p. 75–106. Cited by: §1. [11] J.-J. Ch. Meyer and W. van der Hoek (1995) Epistemic logic for ai and computer science. Cambridge University Press. Cited by: §1. [12] H. van Ditmarsch, W. van der Hoek, and B. Kooi (2007) Dynamic epistemic logic. Synthese Library, Vol. 337, Springer. Cited by: §1, §5. [13] H. van Ditmarsch, W. van der Hoek, and B. Kooi (2003) Concurrent dynamic epistemic logic. In Knowledge Contributors, V.F. Hendricks, K.F. Jørgensen, and S.A. Pedersen (Eds.), Synthese Library Series, p. 105–143. Cited by: §5. Appendix Definition 2 (Bisimulations). Let M1=(S1,R1,V1)M^1=(S^1,R^1,V^1) and M2=(S2,R2,V2)M^2=(S^2,R^2,V^2) be two models. We say that M1M^1 and M2M^2 are bisimilar (denoted M1⇆M2M^1 M^2) if there is a non-empty relation Z⊆S1×S2Z S^1× S^2, called a bisimulation, such that for all sZtsZt: Atoms for all p∈Pp∈ P: s∈V1(p)s∈ V^1(p) if and only if t∈V2(p)t∈ V^2(p), Forth for all i∈Ni∈ N and u∈S1u∈ S^1 s.t. sRi1usR^1_iu, there is a v∈S2v∈ S^2 s.t. tRi2vtR^2_iv and uZvuZv, Back for all i∈Ni∈ N and v∈S2v∈ S^2 s.t tRi2vtR^2_iv, there is a u∈S1u∈ S^1 s.t. sRi1usR^1_iu and uZvuZv. We say that M1,sM^1,s and M2,tM^2,t are bisimilar and denote this by M1,s⇆M2,tM^1,s M^2,t if there is a bisimulation linking states s and t. We have that for any modal language with a normal (relational) semantics, including ℒCL_C, if M1,s⇆M2,tM^1,s M^2,t then for any formula ϕφ, M1,s⊧ϕM^1,s φ iff M2,t⊧ϕM^2,t φ.