Applied Modal Logic

Epistemic Logics

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Editorial

This chapter covers the metatheory of epistemic logics. It is structured in a similar way to Aldo Antonelli's notes on classical basic modal logic, but has been rewritten by Audrey Yap in order to add material on bisimulation and dynamic epistemic logics.

Introduction

Just as modal logic deals with modal propositions and the entailment relations among them, epistemic logic deals with epistemic propositions and the entailment relations among them. Rather than interpreting the modal operators as representing possibility and necessity, the unary connectives are interpreted in epistemic or doxastic ways, to model knowledge and belief. For example, we might want to express claims like the following:

  1. Richard knows that Calgary is in Alberta.

  2. Audrey thinks it is possible that a dog is on the couch.

  3. Richard knows that Audrey knows that her class is on Tuesdays.

  4. Everyone knows that a year has 12 months.

Contemporary epistemic logic is often traced to Jaako Hintikka's Knowledge and Belief, from 1962, and it was written at a time when possible worlds semantics were becoming increasingly more used in logic. In fact, epistemic logics use most of the same semantic tools as other modal logics, but will interpret them differently. The main change is in what we take the accessibility relation to represent. In epistemic logics, they represent some form of epistemic possibility. We'll see that the epistemic notion that we're modelling will affect the constraints that we want to place on the accessibility relation. And we'll also see what happens to correspondence theory when it is given an epistemic interpretation. You'll notice that the examples above mention two agents: Richard and Audrey, and the relationship between the things that each one knows. The epistemic logics we'll consider will be multi-agent logics, in which such things can be expressed. In contrast, a single-agent epistemic logic would only talk about what one individual knows or believes.

The Language of Epistemic Logic

Definition of the multi-agent epistemic language

Let GGsource be a set of agent-symbols. The basic language of multi-agent epistemic logic contains

  1. The propositional constant for falsity ⊥\lfalsesource.

  2. A denumerables set of propositional variables: p0\Obj p_0source, p1\Obj p_1source, p2\Obj p_2source, dots

  3. The propositional connectives: ¬\lnotsource (negation) , ∧\landsource (conjunction) , ∨\lorsource (disjunction) , →\lifsource (conditional) .

  4. The knowledge operator Ka\Knows_asource where a∈Ga \in Gsource.

If we are only concerned with the knowledge of a single agent in our system, we can drop the reference to the set GGsource, and individual agents. In that case, we only have the basic operator K\Knowssource.

Inductive definition of epistemic formulas

Formulas of the epistemic language are inductively defined as follows:

  1. ⊥\lfalsesource is an atomic formula.

  2. Every propositional variable pi\Obj p_isource is an (atomic) formula.

  3. If A!Asource is a formula, then ¬A\lnot !Asource is a formula.

  4. If A!Asource and B!Bsource are formulas, then (A∧B)(!A \land !B)source is a formula.

  5. If A!Asource and B!Bsource are formulas, then (A∨B)(!A \lor !B)source is a formula.

  6. If A!Asource and B!Bsource are formulas, then (A→B)(!A \lif !B)source is a formula.

  7. If A!Asource is a formula and a∈Ga \in Gsource, then KaA\Knows_a !Asource is a formula.

  8. Nothing else is a formula.

If a formula A!Asource does not contain Ka\Knows_asource, we say it is modal-free.

Definition of everybody knows

While the K\Knowssource operator is intended to symbolize individual knowledge, E\EKnowssource, often read as “everybody knows,” symbolizes group knowledge. Where G′⊆GG' \subseteq Gsource, we define EG′A\EKnows_{G'} !Asource as an abbreviation for

⋀b∈G′KbA.\bigwedge_{b \in G'} \Knows_b !A.source

We can also define an even stronger sense of knowledge, namely common knowledge among a group of agents GGsource. When a piece of information is common knowledge among a group of agents, it means that for every combination of agents in that group, they all know that each other knows that each other knows dots ad infinitum. This is significantly stronger than group knowledge, and it is easy to come up with relational models in which a formula is group knowledge, but not common knowledge. We will use CGA\CKnows_G !Asource to symbolize “it is common knowledge among GGsource that A!Asource.”

Relational Models

The basic semantic concept for epistemic logics is the same as that of ordinary modal logics. Relational models still consist of a set of worlds, and an assignment that determines which propositional variables count as “true” at which worlds. And if we are only dealing with a single agent, we have a single accessibility relation as usual. However, if we have a multi-agent epistemic logic, then our single accessibility relation becomes a set of accessibility relations, one for each aasource in our set of agent symbols GGsource.

A relational model consists of a set of worlds, which are related by binary accessibility relations---one for each agent---together with an assignment which determines which propositional variables are true at which worlds.

Definition of a multi-agent epistemic model

A model for the multi-agent epistemic language is a triple M=⟨W,R,V⟩\mModel{M} = \tuple{W, R, V}source, where

  1. WWsource is a nonempty set of “worlds,”

  2. For each a∈Ga \in Gsource, Ra{R}_asource is a binary accessibility relation on WWsource, and

  3. VVsource is a function assigning to each propositional variable ppsource a set V(p)V(p)source of possible worlds.

When Raww′R_a ww'source holds, we say that w′w'source is accessible by a from wwsource. When w∈V(p)w \in V(p)source we say ppsource is true at wwsource.

The mechanics are just like the mechanics for normal modal logic, just with more accessibility relations added in. For a given agent, we will generally interpret their accessibility relation as representing something about their informational states. For example, we often treat Raww′R_a ww'source, as expressing that w′w'source is consistent with aasource's information at wwsource. Or to put it another way, at wwsource, they cannot tell the difference between world wwsource and world w′w'source.

Truth at a World

Just as with normal modal logic, every epistemic model determines which formulas count as true at which worlds in it. We use the same notation “model M\mModel{M}source makes formula A!Asource true at world wwsource” for the basic notion of relational semantics. The relation is defined inductively and is identical to the normal modal case for all non-modal operators.

Definition of truth at a world in an epistemic model

Truth of a formula A!Asource at wwsource in a M\mModel Msource, in symbols: M⊩A[w]\mSat{M}{!A}[w]source, is defined inductively as follows:

  1. Case: A≡⊥!A \ident \lfalsesource

    Never M⊩⊥[w]\mSat{M}{\lfalse}[w]source.

  2. M⊩p[w]\mSat{M}{p}[w]source iff w∈V(p)w \in V(p)source

  3. Case: A≡¬B!A \ident \lnot !Bsource

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊮B[w]\mSat/{M}{!B}[w]source.

  4. Case: A≡(B∧C)!A \ident (!B \land !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w]\mSat{M}{!B}[w]source and M⊩C[w]\mSat{M}{!C}[w]source.

  5. Case: A≡(B∨C)!A \ident (!B \lor !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w]\mSat{M}{!B}[w]source or M⊩C[w]\mSat{M}{!C}[w]source (or both).

  6. Case: A≡(B→C)!A \ident (!B \lif !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊮B[w]\mSat/{M}{!B}[w]source or M⊩C[w]\mSat{M}{!C}[w]source.

  7. Case: A≡KaB!A \ident \Knows_a !Bsource

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w′]\mSat{M}{!B}[w']source for all w′∈Ww' \in Wsource with Raww′R_a ww'source

Here's where we need to think about restrictions on our accessibility relations, though. After all, by clause the knowledge clause in the definition of truth at a world, a formula KaB\Knows_a !Bsource is true at wwsource whenever there are no w′w'source with Raww′R_a ww'source. This is the same clause as in normal modal logic; when a world has no successors, all □\Boxsource-formulas are vacuously true there. This seems extremely counterintuitive if we think about K\Knowssource as representing knowledge. After all, we tend to think that there are no circumstances under which an agent might know both A!Asource and ¬A\lnot !Asource at the same time.

One solution is to ensure that our accessibility relation in epistemic logic will always be reflexive. This roughly corresponds to the idea that the actual world is consistent with an agent's information. In fact, epistemic logics typically use S5, but others might use weaker systems depending on what exactly they want the Ka\Knows_asource relation to represent.

Figure containing a simple epistemic model

The outer figure captions a three-world, two-agent model. Its inner TikZ object records every printed valuation, bidirectional relation, and loop.

Source transcription

Simple three-world epistemic model graph

Simple epistemic model graph. The first node prints p is true and q is false, then labels the world world w subscript one. The second node prints p is true and q is true, then labels the world world w subscript two. The third node prints p is false and q is false, then labels the world world w subscript three. Source-ordered relations: a bidirectional link labelled agent a between w one and w two; a loop at w one for agents a and b; a bidirectional link labelled agent b between w one and w three; a loop at w two for agents a and b; and a loop at w three for agents a and b. End graph.

Nodes

  1. Node 1: world w subscript onep\mTrue{p}source¬q\mFalse{q}sourcew1w_1source
  2. Node 2: world w subscript twop\mTrue{p}sourceq\mTrue{q}sourcew2w_2source
  3. Node 3: world w subscript three¬p\mFalse{p}source¬q\mFalse{q}sourcew3w_3source

Edges

  1. Edge 1: w1 to w2; accessibility relation for agent a.
  2. Edge 2: w2 to w1; accessibility relation for agent a.
  3. Edge 3: w1 to w1; accessibility relation for agent a; loop.
  4. Edge 4: w1 to w1; accessibility relation for agent b; loop.
  5. Edge 5: w1 to w3; accessibility relation for agent b.
  6. Edge 6: w3 to w1; accessibility relation for agent b.
  7. Edge 7: w2 to w2; accessibility relation for agent a; loop.
  8. Edge 8: w2 to w2; accessibility relation for agent b; loop.
  9. Edge 9: w3 to w3; accessibility relation for agent a; loop.
  10. Edge 10: w3 to w3; accessibility relation for agent b; loop.
aasource
a,ba,bsource
bbsource
a,ba,bsource
a,ba,bsource
source 61

captionA simple epistemic model.

Exercise evaluating six epistemic formulas

Consider which of the following hold in the simple three-world epistemic model:

  1. M⊩¬q[w1]\mSat{M}{\lnot q}[w_1]source;

  2. M⊩Ka¬q[w1]\mSat{M}{\Knows_a \lnot q}[w_1]source;

  3. M⊩Kb¬q[w1]\mSat{M}{\Knows_b \lnot q}[w_1]source;

  4. M⊩Kbq∨Kb¬q[w2]\mSat{M}{\Knows_b q \lor \Knows_b \lnot q}[w_2]source;

  5. M⊩Ka(Kbq∨Kb¬q)[w2]\mSat{M}{\Knows_a( \Knows_b q \lor \Knows_b \lnot q)}[w_2]source;

  6. M⊩E{a,b}¬q[w3]\mSat{M}{\EKnows_{\{a,b\}} \lnot q}[w_3]source;

Now that we have given our basic definition of truth at a world, the other semantic concepts from normal modal logic, such as modal validity and entailment, simply carry over, applied to this new way of thinking about the interpretation for the modal operators.

We are now also in a position to give truth conditions for the common knowledge operator CG\CKnows_Gsource. Recall from the section defining operations on relations that the transitive closure R+R^+source of a relation RRsource is defined as

R+=⋃n∈NRn,whereR0=R andRn+1={⟨x,z⟩:∃y(Rnxy∧Ryz)}.R^+ &= \bigcup_{ n \in \mathbb{N}} R^n, \intertext{where} R^0 & = R \text{ and}\\ R^{n+1} & = \Setabs{\tuple{x, z}}{\exists y (R^n xy \land Ryz)}.source

Then, where GGsource is a group of agents, we define RG=(⋃b∈GRb)+R_G = ( \bigcup_{b \in G} R_b )^+source to be the transitive closure of the union of all agents' accessibility relations.

Truth condition for common knowledge

If G′⊆GG' \subseteq Gsource, we let M⊩CG′A[w]\mSat{M}{\CKnows_{G'} !A}[ w]source iff for every w′w'source such that RG′ww′R_{G'} w w'source, M⊩A[w′]\mSat{M}{!A}[w']source.

Accessibility Relations and Epistemic Principles

Given what we already know about frame correspondence in normal modal logics, we might want to see what the characteristic formulas look like given epistemic interpretations. We have already said that epistemic logics are typically interpreted in S5. So let's take a look at how various epistemic principles are represented, and consider how they correspond to various frame conditions.

Recall from normal modal logic, that different modal formulas characterized different properties of accessibility relations. This table picks out a few that correspond to particular epistemic principles.

Figure containing four epistemic correspondence principles

[t]

Four epistemic correspondence rows

Epistemic correspondence table. Column headers: if accessibility relation R has the stated property; then the displayed principle is true in model M. Row one has an intentionally blank frame-condition cell; Closure: if it is known that p implies q, then, if p is known, q is known. Row two, reflexive: for every world w, w is accessible from itself under relation R; Veridicality: if p is known, then p is true. Row three, transitive: for every u, v, and w, if v is accessible from u and w is accessible from v, then w is accessible from u; Positive Introspection: if p is known, then it is known that p is known. Row four, euclidean: for every w, u, and v, if u and v are each accessible from w, then v is accessible from u; Negative Introspection: if p is not known, then it is known that p is not known. End table.

Four epistemic correspondence rows
If RRsource has this propertyThen this epistemic principle is true in M\mModel{M}source
blank source cellClosure K(p→q)→(Kp→Kq)\Knows (p \lif q) \lif (\Knows p \lif \Knows q)source
reflexive ∀wRww\forall w RwwsourceVeridicality Kp→p\Knows p \lif psource
transitive ∀u∀v∀w((Ruv∧Rvw)→Ruw)\forall u \forall v \forall w ((Ruv \land Rvw) \lif Ruw)sourcePositive Introspection Kp→KKp\Knows p \lif \Knows \Knows psource
euclidean ∀w∀u∀v((Rwu∧Rwv)→Ruv)\forall w \forall u \forall v ((Rwu \land Rwv) \lif Ruv)sourceNegative Introspection ¬Kp→K¬Kp\lnot \Knows p \lif \Knows \neg \Knows psource
source 26

captionFour epistemic principles.

Veridicality, corresponding to the TTsource axiom, is often treated as the most uncontroversial of these principles, as it represents that claim that if a formula is known, then it must be true. Closure, as well as Positive and Negative Introspection are much more contested.

Closure, corresponding to the KKsource axiom, represents the idea that an agent's knowledge is closed under implication. This might seem plausible to us in some cases. For instance, I might know that if I am in Victoria, then I am on Vancouver Island. Barring odd skeptical scenarios, I do know that I am in Victoria, and this should also suggest that I know I am on Vancouver Island. So in this case, the logical closure of my knowledge might seem relatively intuitive. On the other hand, we do not always think through the consequences of our knowledge, and so this might lead to less intuitive results in other cases.

Positive Introspection, sometimes known as the KK-principle, is sometimes articulated as the statement that if I know something, then I know that I know. It is the epistemic counterpart of the 4 axiom. Correspondingly, negative introspection is articulated as the statement that if I don't know something, then I know that I don't know it, which is the counterpart of the 5 axiom. Both of these seem to admit of relatively ordinary counterexamples, in which I am unsure whether or not I know something that I do in fact know.

Bisimulations

One remaining question that we might have about the expressive power of our epistemic language has to do with the relationship between models and the formulas that hold in them. We have seen from our frame correspondence results that when certain formulas are valid in a frame, they will also ensure that those frames satisfy certain properties. But does our modal language, for example, allow us to distinguish between a world at which there is a reflexive arrow, and an infinite chain of worlds, each of which leads to the next? That is, is there any formula AAsource that might hold at only one of these two worlds?

Bisimulation is a relationship that we can define between relational models to say that they have effectively the same structure. And as we will see, it will capture a sense of equivalence between models that can be captured in our epistemic language.

Definition of bisimulation

[Bisimulation] Let M1=⟨W1,R1,V1⟩M_1 = \tuple{W_1, R_1, V_1}source and M2=⟨W2,R2,V2⟩M_2 = \tuple{W_2, R_2, V_2}source be two relational models. And let R⊆W1×W2\mathcal{R} \subseteq W_1 \times W_2source be a binary relation. We say that R\mathcal{R}source is a bisimulation when for every ⟨w1,w2⟩∈R\tuple{w_1, w_2} \in \mathcal{R}source, we have:

  1. w1∈V1(p)w_1 \in V_1(p)source iff w2∈V2(p)w_2 \in V_2(p)source for all propositional variables ppsource.

  2. For all agents a∈Aa \in Asource and worlds v1∈W1v_1 \in W_1source, if R1aw1v1R_{1_a} w_1 v_1source then there is some v2∈W2v_2 \in W_2source such that R2aw2v2R_{2_a} w_2 v_2source, and ⟨v1,v2⟩∈R\tuple{v_1, v_2} \in \mathcal{R}source.

  3. For all agents a∈Aa \in Asource and worlds v2∈W2v_2 \in W_2source, if R2aw2v2R_{2_a} w_2 v_2source then there is some v1∈W1v_1 \in W_1source such that R1aw1v1R_{1_a} w_1 v_1source, and ⟨v1,v2⟩∈R\tuple{v_1, v_2} \in \mathcal{R}source.

When there is a bisimulation between M1M_1source and M2M_2source that links worlds w1w_1source and w2w_2source, we can also write ⟨M1,w1⟩=↔⟨M2,w2⟩\tuple{M_1, w_1} \leftrightarroweq \tuple{M_2, w_2}source, and call ⟨M1,w1⟩\tuple{M_1, w_1}source and ⟨M2,w2⟩\tuple{M_2, w_2}source bisimilar.

The different clauses in the bisimulation relation ensure different things. Clause 1 ensures that bisimilar worlds will satisfy the same modal-free formulas, since it ensures agreement on all propositional variables. The other two clauses, sometimes referred to as “forth” and “back,” respectively, ensure that the accessibility relations will have the same structure.

Theorem on invariance under bisimulation

If ⟨M1,w1⟩=↔⟨M2,w2⟩\tuple{M_1, w_1} \leftrightarroweq \tuple{M_2, w_2}source, then for every formula A!Asource, we have that M1⊩A[w1]\mSat{M_1}{!A}[w_1]source iff M2⊩A[w2]\mSat{M_2}{!A}[w_2]source.

Figure containing two bisimilar models

The outer figure captions two source graphs and three dotted bisimulation links. The inner TikZ structure retains every world, directed accessibility edge, loop, and dotted correspondence.

Source transcription

Two bisimilar model graphs

Bisimilar model graphs. Left-world declarations: world w subscript one, world w subscript two, and world w subscript three. Left accessibility, in source order: a bidirectional w one to w two link for agent a; a w one loop for agent a; a bidirectional w one to w three link for agent a; a w two loop for agent a; and a w three loop for agent a. Right-world declarations: world v subscript one and world v subscript two. Right accessibility: a bidirectional v one to v two link for agent a; a v one loop for agent a; and a v two loop for agent a. Unlabelled dotted bisimulation links connect w one with v one, w two with v two, and w three with v two. No valuation is printed. End graphs.

Nodes

  1. Node 1: world w subscript onew1w_1source
  2. Node 2: world w subscript twow2w_2source
  3. Node 3: world w subscript threew3w_3source
  4. Node 4: world v subscript onev1v_1source
  5. Node 5: world v subscript twov2v_2source

Edges

  1. Edge 1: w1 to w2; accessibility relation for agent a.
  2. Edge 2: w2 to w1; accessibility relation for agent a.
  3. Edge 3: w1 to w1; accessibility relation for agent a; loop.
  4. Edge 4: w1 to w3; accessibility relation for agent a.
  5. Edge 5: w3 to w1; accessibility relation for agent a.
  6. Edge 6: w2 to w2; accessibility relation for agent a; loop.
  7. Edge 7: w3 to w3; accessibility relation for agent a; loop.
  8. Edge 8: v1 to v2; accessibility relation for agent a.
  9. Edge 9: v2 to v1; accessibility relation for agent a.
  10. Edge 10: v1 to v1; accessibility relation for agent a; loop.
  11. Edge 11: v2 to v2; accessibility relation for agent a; loop.
  12. Edge 12: w1 to v1; unlabelled dotted bisimulation correspondence.
  13. Edge 13: w2 to v2; unlabelled dotted bisimulation correspondence.
  14. Edge 14: w3 to v2; unlabelled dotted bisimulation correspondence.
aasource
aasource
aasource
aasource
aasource
aasource
aasource
aasource
source 70

captionTwo bisimilar models.

Even though the two models pictured in the figure of two bisimilar models aren't quite the same as each other, there is a bisimulation linking worlds w1w_1source and v1v_1source. This bisimulation will also link both w2w_2source and w3w_3source to v2v_2source, with the idea being that there is nothing expressible in our modal language that can really distinguish between them. The situation would be different if w2w_2source and w3w_3source satisfied different propositional variables, however.

Public Announcement Logic

Dynamic epistemic logics allow us to represent the ways in which agents' knowledge changes over time, or as they gain new information. Many of these represent changes in knowlege using informational events or updates. The most basic kind of update is a public announcement in which some formula is truthfully announced and all of the agents witness this taking place together. To do this, we expand the language as follows

Definition of the language with public announcements

Let GGsource be a set of agent-symbols. The basic language of multi-agent epistemic logic with public announcements contains

  1. The propositional constant for falsity ⊥\lfalsesource.

  2. A denumerables set of propositional variables: p0\Obj p_0source, p1\Obj p_1source, p2\Obj p_2source, dots

  3. The propositional connectives: ¬\lnotsource (negation) , ∧\landsource (conjunction) , ∨\lorsource (disjunction) , →\lifsource (conditional)

  4. The knowledge operator Ka\Knows_asource where a∈Ga \in Gsource.

  5. The public announcement operator [B][!B]source where B!Bsource is a formula.

The public announcement operator functions as a box operator, and our inductive definition of the language is given accordingly:

Inductive definition of public-announcement formulas

Formulas of the epistemic language are inductively defined as follows:

  1. ⊥\lfalsesource is an atomic formula.

  2. Every propositional variable pi\Obj p_isource is an (atomic) formula.

  3. If A!Asource is a formula, then ¬A\lnot !Asource is a formula.

  4. If A!Asource and B!Bsource are formulas, then (A∧B)(!A \land !B)source is a formula.

  5. If A!Asource and B!Bsource are formulas, then (A∨B)(!A \lor !B)source is a formula.

  6. If A!Asource and B!Bsource are formulas, then (A→B)(!A \lif !B)source is a formula.

  7. If A!Asource is a formula and a∈Ga \in Gsource, then KaA\Knows_a !Asource is a formula.

  8. If A!Asource and B!Bsource are formulas, then [A]B[!A] !Bsource is a formula.

  9. Nothing else is a formula.

The intended reading of the formula [A]B[!A] !Bsource is “After A!Asource is truthfully announced, B!Bsource holds. It will sometimes also be useful to talk about common knowledge in the context of public announcements, so the language may also include the common knowledge operator CGA\CKnows_G !Asource.

Semantics of Public Announcement Logic

Relational models for public announcement logics are the same as they were in epistemic logics. However, the semantics for the public announcement operator are something new.

Truth definition for public announcement logic

Truth of a formula A!Asource at wwsource in a M=⟨W,R,V⟩\mModel M = \tuple{W, R, V}source, in symbols: M⊩A[w]\mSat{M}{!A}[w]source, is defined inductively as follows:

  1. Case: A≡⊥!A \ident \lfalsesource

    Never M⊩⊥[w]\mSat{M}{\lfalse}[w]source.

  2. M⊩p[w]\mSat{M}{p}[w]source iff w∈V(p)w \in V(p)source

  3. Case: A≡¬B!A \ident \lnot !Bsource

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊮B[w]\mSat/{M}{!B}[w]source.

  4. Case: A≡(B∧C)!A \ident (!B \land !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w]\mSat{M}{!B}[w]source and M⊩C[w]\mSat{M}{!C}[w]source.

  5. Case: A≡(B∨C)!A \ident (!B \lor !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w]\mSat{M}{!B}[w]source or M⊩C[w]\mSat{M}{!C}[w]source (or both).

  6. Case: A≡(B→C)!A \ident (!B \lif !C)source

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊮B[w]\mSat/{M}{!B}[w]source or M⊩C[w]\mSat{M}{!C}[w]source.

  7. Case: A≡KaB!A \ident \Knows_a !Bsource

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w′]\mSat{M}{!B}[w']source for all w′∈Ww' \in Wsource with Raww′R_a ww'source

  8. Case: A≡[B]C!A \ident [!B] !Csource

    M⊩A[w]\mSat{M}{\indfrm}[w]source iff M⊩B[w]\mSat{M}{!B}[w]source implies M∣B⊩C[w]\mSat{M \mid !B}{!C}[w]source

    Where M∣B=⟨W′,R′,V′⟩\mModel M \mid !B = \tuple{W', R', V'}source is defined as follows:

    1. W′={u∈W:M⊩B[u]}W' = \Setabs{ u \in W}{\mSat{M}{!B}[u]}source. So the worlds of M∣B\mModel M \mid !Bsource are the worlds in M\mModel Msource at which B!Bsource holds.

    2. Ra′=Ra∩(W′×W′)R'_a = R_a \cap (W' \times W')source. Each agent's accessibility relation is simply restricted to the worlds that remain in W′W'source.

    3. V′(p)={u∈W′:u∈V(p)}V'(p) = \Setabs{ u \in W'}{u \in V(p) }source. Similarly, the propositional valuations at worlds remain the same, representing the idea that informational events will not change the truth value of propositional variables.

What is distinctive, then, about public announcement logics, is that the truth of a formula at M\mModel Msource can sometimes only be decided by referring to a model other than M\mModel Msource itself.

Notice also that our semantics treats the announcement operator as a □\Boxsource operator, and so if a formula A!Asource cannot be truthfully announced at a world, then [A]B[!A]Bsource will hold there trivially, just as all □\Boxsource formulas hold at endpoints.

Figure before and after a public announcement

The outer figure compares model M with its restriction after announcing p. The inner TikZ structure retains both graphs, all printed valuations and relation loops, both model labels, and the dotted announcement connection.

Source transcription

Public-announcement update graph

Public-announcement update graph. Left node one prints p is true and q is false and is labelled world w subscript one. Left node two prints p is false and q is false and is labelled world w subscript two. Left node three prints p is true and q is true and is labelled world w subscript three. Left relations, in source order: a bidirectional b link agent b; a loop at w one for agents a and b; a bidirectional a link agent a; a loop at w two for agents a and b; and a loop at w three for agents a and b. Right node one prints p is true and q is false and is labelled world w prime subscript one. Right node three prints p is true and q is true and is labelled world w prime subscript three. Right relations: a bidirectional a link agent a; a loop at w one prime for agents a and b; and a loop at w three prime for agents a and b. The source labels the left graph model M and the right graph model M restricted by p. An unarrowed dotted update connection from w one to w one prime is labelled announcement of p. End graph.

Nodes

  1. Node 1: world w subscript onew1w_1sourcetruefalse
  2. Node 2: world w subscript twow2w_2sourcefalsefalse
  3. Node 3: world w subscript threew3w_3sourcetruetrue
  4. Node 4: world w prime subscript onew1′w'_1sourcetruefalse
  5. Node 5: world w prime subscript threew3′w'_3sourcetruetrue

Edges

  1. Edge 1: w1 to w2; accessibility relation for agent b.
  2. Edge 2: w2 to w1; accessibility relation for agent b.
  3. Edge 3: w1 to w1; accessibility relation for agent a; loop.
  4. Edge 4: w1 to w1; accessibility relation for agent b; loop.
  5. Edge 5: w1 to w3; accessibility relation for agent a.
  6. Edge 6: w3 to w1; accessibility relation for agent a.
  7. Edge 7: w2 to w2; accessibility relation for agent a; loop.
  8. Edge 8: w2 to w2; accessibility relation for agent b; loop.
  9. Edge 9: w3 to w3; accessibility relation for agent a; loop.
  10. Edge 10: w3 to w3; accessibility relation for agent b; loop.
  11. Edge 11: w1p to w3p; accessibility relation for agent a.
  12. Edge 12: w3p to w1p; accessibility relation for agent a.
  13. Edge 13: w1p to w1p; accessibility relation for agent a; loop.
  14. Edge 14: w1p to w1p; accessibility relation for agent b; loop.
  15. Edge 15: w3p to w3p; accessibility relation for agent a; loop.
  16. Edge 16: w3p to w3p; accessibility relation for agent b; loop.
  17. Edge 17: w1 to w1p; public announcement of p.
p,¬qp, \lnot qsource
¬p,¬q\lnot p, \lnot qsource
p,qp, qsource
bbsource
a,ba, bsource
aasource
a,ba, bsource
a,ba, bsource
p,¬qp, \lnot qsource
p,qp,qsource
aasource
a,ba,bsource
a,ba,bsource
M\mModel Msource
M∣p\mModel M \mid psource
ppsource
source 71

captionBefore and after the public announcement of ppsource.

We can see the public announcement of a formula as shrinking a model, or restricting it to the worlds at which the formula was true. the before-and-after public-announcement model gives an example of the effects of publicly announcing ppsource. One notable thing about that model is that agent bbsource learns that ppsource as a result of the announcement, while agent aasource does not (since aasource already knew that ppsource was true).

More formally, we have M⊩¬Kbp[w1]\mSat{M}{\lnot \Knows_b p}[w_1]source but M∣p⊩Kbp[w1′]\mSat{M \mid p}{\Knows_b p}[w'_1]source. This implies that M⊩[p]Kbp[w1]\mSat{M}{[p] \Knows_b p}[w_1]source. But we have some even stronger claims that we can make about the result of the announcement. In fact, it is the case that M⊩[p]C{a,b}p[w1]\mSat{M}{[p]\CKnows_{\{a,b\}} p}[w_1]source. In other words, after ppsource is announced, it becomes common knowledge.

We might wonder, though, whether this holds in the general case, and whether a truthful announcement of A!Asource will always result in A!Asource becoming common knowledge. It may be surprising that the answer is no. And in fact, it is possible to truthfully announce formulas that will no longer be true once they are announced. For example, consider the effects of announcing p∧¬Kbpp \land \lnot \Knows_b psource at w1w_1source in the before-and-after public-announcement model. In fact, M∣p\mModel M \mid psource and M∣(p∧¬Kbp)\mModel M \mid (p \land \lnot \Knows_b p)source are the same model. However, as we have already noted, M∣p⊩Kbp[w1′]\mSat{M \mid p}{\Knows_b p}[w'_1]source. Therefore, M∣(p∧¬Kbp)⊩¬(p∧¬Kbp)[w1′]\mSat{M \mid (p \land \lnot \Knows_b p)}{\lnot (p \land \lnot \Knows_b p)}[w'_1]source, so this is a formula that becomes false once it has been announced.

Source disclosures