We study the modal logic K42C of common belief for normal agents. We study Kripke completeness and show that the logic has tree model property. As a main result we prove that K42C is the modal logic of all TD-intersection closed, bi-topological spaces with derived set interpretation of modalities. Based on the splitting translation we discuss connections with S42C, the logic of common knowledge.
In logics for knowledge representation and reasoning, the study of epistemic and
doxastic properties of agents with certain, intuitively acceptable, restrictions on their
knowledge and belief is a well-developed area. Smullyan [
Agreement technologies is a newly emerging domain where iterative concepts of belief and knowledge of agents are of special interest. To achieve successful communication and agreement it is important for agents to reason about themselves and what others know or believe. Among the more interesting cases are the notions of common knowledge and common belief. We denote the operators for common knowledge and common belief by CK and CB respectively. We have: CK ' iff ' is common knowledge in the group K and CB ' iff ' is a common belief in the group B.
Following the analysis of common knowledge as originally defined by Lewis [
In light of [
As stated, we focus on the common belief of normal agents, and for ease of exposition
we restrict ourselves to the two agent case. We thus consider two agents whose
individual beliefs satisfy the axioms of K4. In other respects we adopt the main principles of
the logic of common knowledge, S42C. This can be seen as a formalization of the idea
that common knowledge is equivalent to an infinite conjunction of iterated individual
knowledge: ' ^ 21' ^ 22' ^ 2121' ^ 2122' ^ 2221' ^ 2222' ^ 212121' ^
212122'::. Later we shall see that a variation of this formula is ‘true’ for common
belief under the relational semantics. We shall also show that the topological semantics
for K42C is compatible with the idea of common belief as a fixpoint equilibrium, a
notion used by Barwise [
Our approach to providing a topological semantics follows the work of Esakia [
We turn to the syntax and Kripke semantics of the logic K42C. The interpretation of
common belief operator CB on bi-relational Kripke frames is similar to the
interpretation of the common knowledge operator CK ; and is based on the notion of transitive
closure of a relation. In this section we show that the logic K42C is sound and complete
with respect to the class of all bi-relational transitive Kripke structures. The proof is a
slight modification of the completeness proof for the logic S42C given in [
There are different notions of common belief [
B
C0 p = 21p ^ 22p;
B Cn+1p = 21CBnp ^ 22CBnp;
B
CB!p = Vn2! CBnp: C! exactly formalizes the intuition behind the former idea of common belief. However,
B since CB! is an infinite intersection, it cannot be expressed as an ordinary formula of modal logic and hence studied in the usual approaches to standard modal logic. Nevertheless it turns out that we can capture the infinitary behavior of CB! in a finitary sense. This idea is made more precise via the modal logic K42C. 2.2
Throughout we work in the modal language LC with an infinite set P rop of propositional letters and symbols ^; :; 21; 22; CB . The set of formulas F orm is constructed in a standard way: P rop F orm. If ; 2 F orm then : ; ^ ; 21 ; 22 ; CB 2 F orm. We will use standard abbreviations for disjunction and implication, _ :(: ^ : ) and ! : _ .
The axioms of the logic K42C are all classical tautologies, each box satisfies all K4 axioms, ie. we have: (K) 2i(p ! q) ! (2ip ! 2iq), (4) 2ip ! 2i2ip, for each i 2 f1; 2g and in addition we have the equilibrium axiom for the common belief operator:
(equi) : CB p $ 21p ^ 22p ^ 21CB p ^ 22CB p:
The rules of inference are: Modus-Ponens, Substitution, Necessitation for 21 and 22 and the induction rule for the common belief operator: (ind) : ` ' ! 21(' ^ ` ' ! CB ) ^ 22(' ^ ) where ' and
are arbitrary formulas of the language. 2.3
The Kripke semantics for the modal logic K42C is provided by transitive, bi-relational Kripke frames. The triple (W; R1; R2), with W an arbitrary set and Ri W W where i 2 f1; 2g, is a bi-transitive Kripke frame if both R1 and R2 are transitive relations. A quadruple (W; R1; R2; V ) is a bi-transitive Kripke model if (W; R1; R2) is a bitransitive Kripke frame and V : P rop ! P (W ) is a valuation function. Observe that we only have two relations, which give a semantics for 21 and 22. To interpret the common belief operator, CB , we construct a new relation, which is a transitive closure of the union of R1 and R2.
relation containing the relation R.
Two points x and y are related by the transitive closure of the relation if there exists a finite path hx1; ::; xni starting at x and ending at y.
Definition 2. For a given bi-relational Kripke model M = (W; R1; R2; V ) the satisfaction of a formula at a point w 2 W is defined inductively as follows: w p iff w 2 V (p), w ^ iff w and w , w : iff w 1 , w 2i' iff (8v)(wRiv ) v '), w CB ' iff (8v)(w(R1 [ R2)+v ) v ').
A formula is valid in a model M, in symbols M , if for every point w 2 W we have w . is valid in a bi-relational frame F = (W; R1; R2), in symbols F , iff is valid in every model M = (F ; V ) based on the frame. is valid in a class of bi-relational frames K if for every frame F 2 K we have F .
Proposition 1. (Completeness) Modal logic K42C is sound and complete with respect to the class of all finite, bi-transitive Kripke frames.
Proof. (Sketch) The proof follows the pattern of [
According to proposition 1 every non-theorem of K42C is falsified on a finite, bitransitive frame. The following theorem shows that every non-theorem of K42C can be falsified on a frame (W t; R1t; R2t; V t), where for each k 2 f1; 2g the pair (W t; Rkt) is a transitive tree.
Definition 3. A frame (W; R) is called a tree if: 1) it is rooted, ie. there is a unique point (the root) r 2 W such that for every v 2 W it holds that v 6= r ) rR+v, 2) every element distinct from r has a unique immediate predecessor; that is, for every v 6= r there is a unique v0 such that v0Rv and for every v00 we have that v00Rv ) v00Rv0, 3) R is acyclic; that is, for every v 2 W it is not the case that vR+v.
If in addition R is transitive, ie. R = R+, then (W; R) is called a transitive tree. Theorem 1. The modal logic K42C has tree model property.
Proof. (Sketch) We start with a bi-relational countermodel M = (W; R1; R2; V ) for
the formula '. The proof follows a standard unravelling technique [
Note 1. Observe that the relation (R1t [ R2t)+ does not contain cycles and in particular it is irreflexive.
The mains reason for introducing K42C was to mimic the infinitary operator CB! by finitary CB . Though we cannot claim that on a logical level CB and CB! are equivalent, we can establish a semantical equivalence, in particular on Kripke structures. Theorem 2. For any transitive bi-relational Kripke model M point w: M; w CB ' iff M; w CB! : Proof. The proof follows easily from Definitions 1 and 2. = (W; R1; R2; V ) and 2.4
We mentioned that common belief can also be understood as an equilibrium concept1.
On Kripke structures the equilibrium conception coincides with common belief by
infinite iteration, while in general the equilibrium conception has a much closer connection
1 For the remainder of this section and later on for Theorem 9 we assume some familiarity with
the modal -calculus. Lack of space hinders a fuller treatment, however for more details on
the modal -calculus we refer to [
C ' = :p(21' ^ 22' ^ 21p ^ 22p): The greatest fixpoint is defined as the fixpoint of a descending approximation sequence defined over the ordinals. Denote by j'j the truth set of ' in the appropriate model M where evaluation occurs: jC0'j = j21' ^ 22'j; jCk+1'j = j21' ^ 22' ^ 21Ck' ^ 22Ck'j; jC 'j = j T k<
Ck'j, for a limit ordinal.
We obtain jC 'j = jC 'j, where is a least ordinal for which the approximation procedure halts: ie. jC 'j = jC +1'j. Halting is guaranteed because the occurrence of the propositional variable p in operator F (p), where F (p) = 21'^22'^21p^22p, is positive. Hence by the Knaster-Tarski theorem the sequence will always reach a greatest fixpoint. Then the semantics of the operator C is defined in the following way:
M; w C ' iff w 2 jC 'j In general this procedure may take more than ! steps, but in case of Kripke structures the situation is simpler. The following property relates the different operators on Kripke models.
Theorem 3. For every bi-relational Kripke model M = (W; R1; R2; V ) and a point w 2 W the following condition holds: M; w CB! ' iff M; w C '. Proof. Observe that we can rewrite C! ' = 21' ^ 22' ^ 2121' ^ 2122' ^ 2221' ^
B
2222'^212121'^212122'::: in the following way: 21'^22'^21(21'^22')^
22(21' ^ 22') ^ ::. Hence jCB! 'j = jC! 'j. It is known that on Kripke structures
stabilization process does not need more than ! steps [
It follows that on transitive bi-relational Kripke structures the three operators CB ; CB! and C coincide. 3
The idea of a derived set topological semantics originates with the McKinsey-Tarski
paper [
Definition 4. A pair (X; ) is called a topological space if X is a set and collection of subsets of X with the following properties: 1) X; ? 2 , 2) A; B 2 implies A \ B 2 , 3) Ai 2 implies S Ai 2 .
Elements of are called opens or open sets of the topological space. Definition 5. A topological space (X; ) is called an Alexandroff space if an arbitrary intersection of opens is open, that is Ai 2 implies T Ai 2 . (X; ) is called a TD-space if every point x 2 X can be represented as an intersection of some open set A and some closed set B.
We now define the colimit operator (or the set of all colimit points [
Definition 6. Given a topological space (X; ) and a set A X we will say that x 2 X is a colimit point of A if there exists an open neighborhood Ux of x such that Ux fxg A. The set of all colimit points of A will be denoted by (A) and will be called the colimit set of A.
The colimit set provides a semantics for the box modality, consequently the semantics for diamond is provided by the dual of the colimit set, which is called the derived set. The derived set of A is denoted by der(A). So we have (A) = X der(X A). Below we list some properties of the colimit operator.
Fact 4 [
The following links TD-spaces and irreflexive transitive relational structures. This
result is a special case of a more general correspondence between weakly-transitive and
irreflexive relational structures and all Alexandroff spaces [
Fact 5 ([
Let us briefly describe the correspondence. We first introduce the downset operator. Let (X; R) be a Kripke frame. The downset operator R 1 is defined in the following way: for any A X we set R 1(A) := fxj(9y)(y 2 A ^ xRy)g. Now if we are given an irreflexive, transitive order (X; R) it is possible to prove that the downset operator R 1 satisfies all the properties of the topological derivative operator for TDspaces. Hence we get a TD-space (X; R), where R is the topology obtained from the derivative operator R 1. Conversely with every Alexandroff TD-space (X; ), one can associate an irreflexive and transitive relational structure (X; R ), where xR y iff x 2 der(fyg). Moreover we have that (X; R ) is homeomorphic to (X; ) and (X; R R ) is order isomorphic to (X; R).
Fact 6 [
This correspondence can be directly generalized to Kripke frames with more than one transitive and irreflexive relation. Of course then we will have one Alexandroff TDspace for each irreflexive and transitive order. Below we prove the proposition which builds a bridge between Kripke and topological semantics for K42C.
Proposition 2. If R1 and R2 are two irreflexive and transitive orders on X and (R1 [ R2)+ is also irreflexive and transitive, then R2 . (R1[R2)+ =
R1 \ Before starting the proof, observe that (R1 [ R2)+ may not be irreflexive even if both R1 and R2 are. For example: Let X = fx; yg and R1 = f(x; y)g and R2 = f(y; x)g then (R1 [ R2)+ = f(x; y); (y; x); (x; x); (y; y)g. On the topological side this example shows that TD-spaces do not form a lattice. That is why in Proposition 2 we require (R1 [ R2)+ to be a irreflexive and transitive.
Proof. Assume that A 2 (R1[R2)+ . By Fact 6 this means that if x 2 A then for every y such that x(R1 [ R2)+y it holds that y 2 A. Since Ri (R1 [ R2)+ for each i 2 f1; 2g, it holds that xR1y ) y 2 A and xR2y ) y 2 A for every y 2 X. Hence A 2 1 \ 2 according to Fact 6.
Conversely assume A 2 1 \ 2. This means that x 2 A ) (x(R1 [ R2)y ) y 2 A). Now take arbitrary y such that x(R1 [ R2)+y. By definition this means that there is a (R1 [ R2)-path hx1; x2; ::xni starting at x going to y. But this means that each member of this path is in A because A is open in the intersection of the two topologies. Hence y 2 A and hence A 2 (R1[R2)+
Next we give a definition of the satisfaction relation of modal formulas in the derived set topological semantics. Observe that this definition is given in a standard modal language ie., without the common belief operator. Recall that a topological model is a tuple M = (W; ; V ) where V : P rop ! P (W ) is a valuation function. Definition 7. The satisfaction of a modal formula in a topological model M = (W; ; V ) at a point w 2 W is defined in the following way: – M; w p iff w 2 V (p), – Boolean cases are standard, – M; w 2' iff w 2 (V (')), where is a colimit operator of .
Fact 7 [
Note that in Fact 7, the symbol on the left hand side denotes the satisfaction relation on Kripke models, while on the right hand side it denotes the satisfaction relation on topological frames in the derived set semantics. Now we extend the satisfaction relation to the language with the common belief operator.
Definition 8. The satisfaction of a modal formula on a bi-topological model M = (W; 1; 2; V ) at a point w 2 W is defined in the following way: M; w p iff w 2 V (p), M; w ^ iff M; w and M; w , M; w : iff M; w 1 , M; w 2i' iff w 2 i(V (')), where i is a colimit operator of i, i 2 f1; 2g, M; w CB ' iff w 2 1^2(V (')), where 1^2 is a colimit operator in 1 \ 2:
As an immediate corollary of the proposition 2 and a many-modal version of the Fact 7, we get the following proposition.
Proposition 3. If R1 and R2 are two irreflexive and transitive orders and (R1 [ R2)+ is also topological then for every formula in K42C the following holds: (W; R1; R2; V ); x iff (W; R1 ; R2 ; V ); x .
Now it is clear that we can reduce the topological completeness problem to Kripke completeness if for every non-theorem K42C 6` ' we can find a bi-relational topological counter-model (W; R1; R2; V ) with (R1 [ R2)+ being also a topological relation.
1 \ Definition 9. The triple (X; 1; 2) is a TD-intersection closed bi-topological space if each of the topologies 1, 2 and 2, satisfies the TD-separation axiom. Theorem 8. K42C is sound and complete with respect to the class of all TD-intersection closed, bi-topological, Alexandroff spaces.
Proof. (Soundness) Take an arbitrary TD-intersection closed, bi-topological model M = (X; 1; 2; V ). From 2) and 3) of Fact 4 it follows that K4-axioms are valid for each box. Let us show that at each point x 2 X, the equilibrium axiom is satisfied. Assume that M; x CB p. Hence by Definition 8 we have x 2 1^2jpj. By 4) of Fact 4 we get x 2 1jpj and x 2 2jpj. By 3) we have 1^2jpj 1^2 1^2jpj 1 1^2jpj. Analogously 1^2jpj 2 1^2jpj. Hence we have x 21p ^ 22p ^ 21CB p ^ 22CB p:
For the other direction assume that x 2 1 1^2jpj \ 1jpj \ 2 1^2jpj \ 2jpj. By 2) of Fact 4 we get x 2 1( 1^2jpj \ jpj) \ 2( 1^2jpj \ jpj). By 1) of Fact 4 we conclude x 2 1(Int1^2jpj)\ 2(Int1^2jpj), where Int1^2 denotes the interior operator in the intersection topology. By definition of colimit there exists Ux1 2 1 such that x 2 Ux1 and Ux1 fxg Int1^2jpj and there exists Ux2 2 2 such that x 2 Ux2 and Ux2 fxg Int1^2jpj. Hence (Ux1 [ Ux2) fxg Int1^2jpj. Let us show that Int1^2jpj [ fxg is open in 1 \ 2. Since Ux1 2 1 and Int1^2jpj 2 1 we have Ux1 [ Int1^2jpj = Int1^2jpj [ fxg 2 1. Analogously we show that Int1^2jpj [ fxg 2 2. Hence x 2 1^2jpj.
Let us show that the induction rule is valid in the class of all TD-intersection closed bi-topological spaces. The proof goes by contraposition. Assume not ` p ! CB q. This means that for some TD-intersection closed, bi-topological model M = (X; 1; 2; V ) and a point x 2 X it holds that: x p while x 1 CB q. We want to show that not ` p ! 21(p ^ q) ^ 22(p ^ q). It suffices to find a TD-intersection closed bi-topological model which falsifies the formula. For such a model one could take M0 = (X; 1 \ 2; 1 \ 2; V ). Indeed as (X; 1; 2; V ) is TD-intersection closed, the topology 1 \ 2 satisfies the TD-separation axiom. Besides since in M0 both topologies are the same, their intersection is also 1 \ 2 and hence again is a TD-space. Now it is immediate that M0; x 1 p ! 21(p ^ q) ^ 22(p ^ q). This is because by construction of M0 we have M0; x 1 2iq iff M; x 1 CB q for every x 2 X and i 2 f1; 2g.
(Completeness) Assume K42C 6` '. According to Theorem 1 there exist a tree model M t = (W t; R1t; R2t; V ) which falsifies '. We know that (R1[R2)+ is irreflexive and transitive order (see Note 1). By applying Proposition 3 we get that the formula ' is falsified in the corresponding bi-topological model (W t; R1t ; R2t ; V ), which is TDintersection closed because of Fact 5, Proposition 2 and Note 1.
We can now show how the semantical definition of common belief CB ' as a colimit of the intersection topology meshes with the general equilibrium concept: on topological models the two operators CB and C coincide.
Theorem 9. For every bi-topological model M = (X; 1; 2; V ) and an arbitrary formula ' the following equality holds: :p( 1(j'j) \ 2(j'j) \ 1(p) \ 2(p)) = Proof. That 1^2(j'j) is a fixpoint of the operator F (p) = 1(j'j) \ 2(j'j) \ 1(p) \ 2(p) follows from the soundness proof of the equilibrium axiom, see Theorem 8. Now let us show that 1^2(j'j) is the greatest fixpoint of F (p). Take an arbitrary fixpoint B of the operator F (p). That B is a fixpoint immediately implies that B 1(j'j) \ 2(j'j) \ 1(B) \ 2(B). By 1) of Fact 4 we have B Inti(B) = i(B) \ B for each i 2 f1; 2g. Hence B = Int1^2(B) where Int1^2 is the interior operator in the intersection topology of the two topologies. Now let us show that for every x 2 B the set fxg [ (B \ j'j) is open in the intersection of the two topologies. Take an arbitrary point y 2 fxg [ (B \ j'j). Since y 2 B 1(j'j) we know that there exists an open neighborhood Uy1 2 1 of y such that Uy1 fyg j'j. This means that B \ Uy1 2 1 and B \Uy1 fxg[(B \j'j). This means that for every point y 2 fxg[(B \j'j) there is an open neighborhood B \ Uy1 2 1 of y such that B \ Uy1 fxg [ (B \ j'j) hence fxg [ (B \ j'j) 2 1: In exactly the same way we show that fxg [ (B \ j'j) 2 2. Hence fxg [ (B \ j'j) 2 1 \ 2. This means that x 2 1^2(j'j) since there exists an open neighborhood U1^2 = fxg [ (B \ j'j) 2 1 \ 2 with U1^2 fxg 2 j'j. 4
In this section we discuss the connection between the logics of common knowledge S42C and common belief K42C. This connection generalizes the existing splitting translation between S4-logics and K4-logics. As a result we obtain a validity preserving translation from S42C formulas to K42C formulas in which common knowledge is expressed in terms of common belief.
Definition 10. The normal modal logic S42C is defined in a modal language with infinite set of propositional letters p; q; r:: and connectives _; ^; :; 21; 22; CK , where the formulas are constructed in a standard way.
The axioms are all classical tautologies, each box satisfies all S4 axioms and in addition we have equilibrium axiom for common knowledge operator: (equi) : CK p $ p ^ 21CK p ^ 22CK p
The rules of inference are: Modus-ponens, Substitution, Necessitation for 21 and 22 and the induction rule:
in the following way: R? = R+ [ f(w; w)jw 2 W g:
The satisfaction of formulas is definition in the following way.
W
W is defined Definition 12. For a given bi-relational Kripke model M = (W; R1; R2; V ) the satisfaction of a formula at a point w 2 W is defined inductively as follows: w p iff w 2 V (p), w ^ iff w and w , w : iff w 1 , w 2i' iff (8v)(wRiv ) v '), w CK ' iff (8v)(w(R1 [ R2)?v ) v ').
Fact 10 [
Definition 13. Consider the following function from the set of formulas in S42C to the set of formulas in K4C.
2 Sp(p) = p for every propositional letter p, Sp(: _ ) = :Sp( ) _ Sp( ), Sp(2i ) = 2iSp( ) ^ Sp( ), Sp(CK ) = CB Sp( ) ^ Sp( ).
Theorem 11. `S42C ' iff `K42C Sp(').
Proof. We prove the theorem by a semantical argument using the Kripke completeness results, see Proposition 1 and Fact 10. Let us first show by induction on the length of formula that for every bi-relational Kripke model M = (W; R1; R2; V ) and every w 2 W the following holds: (a)
M? = (W; R1?; R2?; V ); w ' iff M+ = (W; R1+; R2+; V ); w
The only nonstandard case is when ' = CK . Assume M?; w CK . By the definition of (R1 [ R2)? this means that M?; w and for every w0 such that w(R1 [ R2)?w0, we have M?; w0 . Now by the induction hypotheses we have that M+; w and M+; w0 . Since w0 was arbitrary (R1 [ R2)? successor of w we have M+; w CB . This is because (R1 [ R2)? (R1 [ R2)+. Hence we get M+; w CB ^ . The converse direction follows by the same argument.
Now assume `S42C '. By fact 10 this means that ' is valid in every reflexive and transitive, bi-relational model. Take arbitrary transitive, bi-relational model M. Then by assumption we have M? '. Hence by (a) we have that M Sp('). As M was arbitrary transitive, bi-relational model from Proposition 1 we get that `K42C Sp('). Conversely assume `K4C Sp('). Then by Proposition 1, Sp(') is valid in the class of 2 all transitive, bi-relational models. Take arbitrary reflexive and transitive, bi-relational model N . Then N Sp(') because N = N +. So by (a) we have that N ? '. Now as N was reflexive and transitive, N ? = N , hence N '. Sinse N was arbitrary reflexive and transitive, bi-relational model, by Fact 10 we have `S42C '. 5
Our main aim in this paper has been to extend the work of [
While preparing the final draft of this work, we came across the article [27] by Lismont and Mongin. This paper treats several logics of common belief including one that is equivalent to K42C. Besides a relational semantics, the authors also consider a more general neighborhood semantics and discuss the equilibrium conception of common belief in this setting. While the semantics and methods of [27] are formally different to ours, there are obvious similarities. Though it is beyond the scope of this paper, a detailed comparison of our topological approach with the neighborhood systems of [27] would be a worthwhile exercise for the future. Another direction for future work is to look for concrete topological structures which would fully capture the behavior of the logic K42C or some of it’s extensions. 6
The authors are grateful to anonymous reviewers whose comments helped to improve the readability of the paper. This research has been partially supported by the Spanish Ministry of Science and Innovation through the AT project CSD2007-0022 and MCICINN project TiN2009-14562-CO5. 24. David Pearce and Levan Uridia., Minimal Knowledge and Belief via Minimal Topology. In T.
Janhunen, I. Niemela (eds), Logics in Artificial Intelligence, Proc. JELIA 2010, LNAI 6341, Springer, pp. 273-285, 2010. 25. David Pearce and Levan Uridia., The Godel and the Splitting Translations. In G. Brewka, V.
Marek & M. Truszczynski (eds), Nonmonotonic Reasoning, Studies in Logic, pp. 335-360, Vol. 31, College Publications, 2011. 26. David Pearce and Levan Uridia., An Approach to Minimal Belief via Objective Belief. In T.
Walsh (ed), Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 11, pp. 1045-1050, 2011. 27. Luc Lismont and Philippe Mongin., On the Logic of Common Belief and Common Knowledge. Theory and Decision, pp. 75–106, Vol. 37, 1994.