Applied Modal Logic

Epistemic Logics

Equation form expr-00c5e11c728e184c

⟨M1,w1⟩\tuple{M_1, w_1}

Read as: the ordered pair model M subscript one, then world w subscript one

Means: the ordered pair model M subscript one, then world w subscript one

1 occurrence in this chapter

Equation form expr-01208e159d2aec8c

∧\land

Read as: the conjunction connective

Means: the conjunction connective

2 occurrences in this chapter

Equation form expr-0928828231e90719

a∈Aa \in A

Read as: agent a belongs to agent set A

Means: agent a belongs to agent set A

2 occurrences in this chapter

Equation form expr-0b8a0483d529e6e3

R1aw1v1R_{1_a} w_1 v_1

Read as: world v subscript one is accessible from world w subscript one under the agent a accessibility relation in model one

Means: world v subscript one is accessible from world w subscript one under the agent a accessibility relation in model one

2 occurrences in this chapter

Equation form expr-0bc2eaa80c0355be

M⊩[p]C{a,b}p[w1]\mSat{M}{[p]\CKnows_{\{a,b\}} p}[w_1]

Read as: model M satisfies after p is truthfully announced, it is common knowledge among the group containing agent a and agent b that p holds at world w subscript one

Means: model M satisfies after p is truthfully announced, it is common knowledge among the group containing agent a and agent b that p holds at world w subscript one

1 occurrence in this chapter

Equation form expr-139c9f29b4e3d712

M∣(p∧¬Kbp)⊩¬(p∧¬Kbp)[w1′]\mSat{M \mid (p \land \lnot \Knows_b p)}{\lnot (p \land \lnot \Knows_b p)}[w'_1]

Read as: model M restricted by open scope, p and not agent b knows that p, close scope satisfies not open scope, p and not agent b knows that p, close scope at world w prime subscript one

Means: model M restricted by open scope, p and not agent b knows that p, close scope satisfies not open scope, p and not agent b knows that p, close scope at world w prime subscript one

1 occurrence in this chapter

Equation form expr-141a788a845573ec

M⊩A[w]\mSat{M}{\indfrm}[w]

Read as: model M satisfies the formula in the current induction case at world w

Means: model M satisfies the formula in the current induction case at world w

11 occurrences in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

9 occurrences in this chapter

Equation form expr-16c92dc0c5be3daf

⟨v1,v2⟩∈R\tuple{v_1, v_2} \in \mathcal{R}

Read as: the ordered pair world v subscript one, then world v subscript two belongs to bisimulation relation script R

Means: the ordered pair world v subscript one, then world v subscript two belongs to bisimulation relation script R

2 occurrences in this chapter

Equation form expr-1a53000974926187

V(p)V(p)

Read as: valuation V of p

Means: valuation V of p

1 occurrence in this chapter

Equation form expr-1e7b56fbe18aca77

⟨M2,w2⟩\tuple{M_2, w_2}

Read as: the ordered pair model M subscript two, then world w subscript two

Means: the ordered pair model M subscript two, then world w subscript two

1 occurrence in this chapter

Equation form expr-1eb7c54d52831bbf

a,ba,b

Read as: agents a and b

Means: agents a and b

5 occurrences in this chapter

Equation form expr-1ef6557e970094ed

w1′w'_1

Read as: world w prime subscript one

Means: world w prime subscript one

1 occurrence in this chapter

Equation form expr-20a508e46929e0de

M1=⟨W1,R1,V1⟩M_1 = \tuple{W_1, R_1, V_1}

Read as: model M subscript one equals the ordered triple world set W subscript one, then accessibility relation R subscript one, then valuation V subscript one

Means: model M subscript one equals the ordered triple world set W subscript one, then accessibility relation R subscript one, then valuation V subscript one

1 occurrence in this chapter

Equation form expr-22fcce974c4bdb33

M\mModel M

Read as: model M

Means: model M

5 occurrences in this chapter

Equation form expr-234ef32b30394a54

(A∨B)(!A \lor !B)

Read as: open scope, formula A or formula B, close scope

Means: open scope, formula A or formula B, close scope

2 occurrences in this chapter

Equation form expr-23fac266c08cc34b

pi\Obj p_i

Read as: propositional variable p subscript i

Means: propositional variable p subscript i

2 occurrences in this chapter

Equation form expr-24fc9b5857acc732

v2∈W2v_2 \in W_2

Read as: world v subscript two belongs to world set W subscript two

Means: world v subscript two belongs to world set W subscript two

2 occurrences in this chapter

Equation form expr-2846ed9b15800931

Raww′R_a ww'

Read as: world w prime is accessible from world w under the agent a accessibility relation

Means: world w prime is accessible from world w under the agent a accessibility relation

5 occurrences in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: the negation connective

Means: the negation connective

2 occurrences in this chapter

Equation form expr-28e1e9860f569480

R⊆W1×W2\mathcal{R} \subseteq W_1 \times W_2

Read as: bisimulation relation script R is a subset of world set W subscript one cross world set W subscript two

Means: bisimulation relation script R is a subset of world set W subscript one cross world set W subscript two

1 occurrence in this chapter

Equation form expr-2ad30c5ca4cc976f

w2∈V2(p)w_2 \in V_2(p)

Read as: world w subscript two belongs to valuation V subscript two of p

Means: world w subscript two belongs to valuation V subscript two of p

1 occurrence in this chapter

Equation form expr-2c9c7d19c365a2ce

∀w∀u∀v((Rwu∧Rwv)→Ruv)\forall w \forall u \forall v ((Rwu \land Rwv) \lif Ruv)

Read as: for every w, u, and v, if u and v are each accessible from w, then v is accessible from u

Means: for every w, u, and v, if u and v are each accessible from w, then v is accessible from u

1 occurrence in this chapter

Equation form expr-3106fac3e3c8f992

w2w_2

Read as: world w subscript two

Means: world w subscript two

6 occurrences in this chapter

Equation form expr-318f93b8c3835cd2

p1\Obj p_1

Read as: propositional variable p subscript one

Means: propositional variable p subscript one

2 occurrences in this chapter

Equation form expr-3233a452a01c815c

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

Read as: model M satisfies agent a knows that open scope, agent b knows that q or agent b knows that not q, close scope at world w subscript two

Means: model M satisfies agent a knows that open scope, agent b knows that q or agent b knows that not q, close scope at world w subscript two

1 occurrence in this chapter

Equation form expr-333e0a1e27815d0c

GG

Read as: agent set G

Means: agent set G

7 occurrences in this chapter

Equation form expr-3565225c19d3bc52

v1v_1

Read as: world v subscript one

Means: world v subscript one

2 occurrences in this chapter

Equation form expr-376d5037f2a5b8b0

p0\Obj p_0

Read as: propositional variable p subscript zero

Means: propositional variable p subscript zero

2 occurrences in this chapter

Equation form expr-387d2431d07391c1

[B][!B]

Read as: the public announcement operator indexed by formula B

Means: the public announcement operator indexed by formula B

1 occurrence in this chapter

Equation form expr-3b524d8b1a1063d9

M⊩C[w]\mSat{M}{!C}[w]

Read as: model M satisfies formula C at world w

Means: model M satisfies formula C at world w

6 occurrences in this chapter

Equation form expr-3b681c5e2fc6313b

w1∈V1(p)w_1 \in V_1(p)

Read as: world w subscript one belongs to valuation V subscript one of p

Means: world w subscript one belongs to valuation V subscript one of p

1 occurrence in this chapter

Equation form expr-3e23e8160039594a

bb

Read as: agent b

Means: agent b

3 occurrences in this chapter

Equation form expr-3e5db243d8a756fd

a∈Ga \in G

Read as: agent a belongs to agent set G

Means: agent a belongs to agent set G

5 occurrences in this chapter

Equation form expr-3f8a924ce1a3552c

W′={u∈W:M⊩B[u]}W' = \Setabs{ u \in W}{\mSat{M}{!B}[u]}

Read as: remaining world set W prime equals the set of all world u in world set W such that model M satisfies formula B at world u

Means: remaining world set W prime equals the set of all world u in world set W such that model M satisfies formula B at world u

1 occurrence in this chapter

Equation form expr-438757f12dd8c3fc

w1w_1

Read as: world w subscript one

Means: world w subscript one

6 occurrences in this chapter

Equation form expr-464ff395ff571fb1

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

Read as: model M satisfies agent b knows that q or agent b knows that not q at world w subscript two

Means: model M satisfies agent b knows that q or agent b knows that not q at world w subscript two

1 occurrence in this chapter

Equation form expr-476c8e0d7ccdebf0

M1⊩A[w1]\mSat{M_1}{!A}[w_1]

Read as: model M subscript one satisfies formula A at world w subscript one

Means: model M subscript one satisfies formula A at world w subscript one

1 occurrence in this chapter

Equation form expr-4a479db6af79906e

a,ba, b

Read as: agents a and b

Means: agents a and b

3 occurrences in this chapter

Equation form expr-4b7232319bafe577

RG=(⋃b∈GRb)+R_G = ( \bigcup_{b \in G} R_b )^+

Read as: group relation R subscript G is the transitive closure of the union of relation R subscript b over agents b in G

Means: group relation R subscript G is the transitive closure of the union of relation R subscript b over agents b in G

1 occurrence in this chapter

Equation form expr-4f61516118e61d9a

EG′A\EKnows_{G'} !A

Read as: every agent in agent group G prime knows that formula A

Means: every agent in agent group G prime knows that formula A

1 occurrence in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: world w

Means: world w

9 occurrences in this chapter

Equation form expr-525a1d0e8bb940a9

w′∈Ww' \in W

Read as: world w prime belongs to world set W

Means: world w prime belongs to world set W

2 occurrences in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: the disjunction connective

Means: the disjunction connective

2 occurrences in this chapter

Equation form expr-52d7448aebc51481

M⊩⊥[w]\mSat{M}{\lfalse}[w]

Read as: model M satisfies falsity at world w

Means: model M satisfies falsity at world w

2 occurrences in this chapter

Equation form expr-559aead08264d579

AA

Read as: A

Means: A

1 occurrence in this chapter

Equation form expr-55a2a39b9f6de118

[A]B[!A]B

Read as: after formula A is truthfully announced, formula B holds

Means: after formula A is truthfully announced, formula B holds

1 occurrence in this chapter

Equation form expr-57c1d36e705bef36

M=⟨W,R,V⟩\mModel M = \tuple{W, R, V}

Read as: model M equals the ordered triple world set W, then accessibility relation R, then valuation V

Means: model M equals the ordered triple world set W, then accessibility relation R, then valuation V

1 occurrence in this chapter

Equation form expr-5805b13f114f5cb0

E\EKnows

Read as: the everybody-knows operator

Means: the everybody-knows operator

1 occurrence in this chapter

Equation form expr-5a9cf23220f8d4cd

M⊩Ka¬q[w1]\mSat{M}{\Knows_a \lnot q}[w_1]

Read as: model M satisfies agent a knows that not q at world w subscript one

Means: model M satisfies agent a knows that not q at world w subscript one

1 occurrence in this chapter

Equation form expr-5aa658699a9c38ee

M⊩Kb¬q[w1]\mSat{M}{\Knows_b \lnot q}[w_1]

Read as: model M satisfies agent b knows that not q at world w subscript one

Means: model M satisfies agent b knows that not q at world w subscript one

1 occurrence in this chapter

Equation form expr-5cbf77da4b1832e3

CG\CKnows_G

Read as: the common-knowledge operator for group G

Means: the common-knowledge operator for group G

1 occurrence in this chapter

Equation form expr-62cb695074593661

M⊩¬Kbp[w1]\mSat{M}{\lnot \Knows_b p}[w_1]

Read as: model M satisfies not agent b knows that p at world w subscript one

Means: model M satisfies not agent b knows that p at world w subscript one

1 occurrence in this chapter

Equation form expr-69ef9ee2c45eb3b7

M⊩A[w′]\mSat{M}{!A}[w']

Read as: model M satisfies formula A at world w prime

Means: model M satisfies formula A at world w prime

1 occurrence in this chapter

Equation form expr-73e53e33a083878b

M2=⟨W2,R2,V2⟩M_2 = \tuple{W_2, R_2, V_2}

Read as: model M subscript two equals the ordered triple world set W subscript two, then accessibility relation R subscript two, then valuation V subscript two

Means: model M subscript two equals the ordered triple world set W subscript two, then accessibility relation R subscript two, then valuation V subscript two

1 occurrence in this chapter

Equation form expr-753933d219dca076

M2⊩A[w2]\mSat{M_2}{!A}[w_2]

Read as: model M subscript two satisfies formula A at world w subscript two

Means: model M subscript two satisfies formula A at world w subscript two

1 occurrence in this chapter

Equation form expr-7972c7311ed14dbc

R2aw2v2R_{2_a} w_2 v_2

Read as: world v subscript two is accessible from world w subscript two under the agent a accessibility relation in model two

Means: world v subscript two is accessible from world w subscript two under the agent a accessibility relation in model two

2 occurrences in this chapter

Equation form expr-7aef8fc57799f0c7

Ra′=Ra∩(W′×W′)R'_a = R_a \cap (W' \times W')

Read as: agent a accessibility relation R prime equals agent a accessibility relation R intersected with open scope, remaining world set W prime cross remaining world set W prime, close scope

Means: agent a accessibility relation R prime equals agent a accessibility relation R intersected with open scope, remaining world set W prime cross remaining world set W prime, close scope

1 occurrence in this chapter

Equation form expr-7b70cfd9956e081e

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

Read as: the conjunction, over every agent b in group G prime, that agent b knows formula A

Means: the conjunction, over every agent b in group G prime, that agent b knows formula A

1 occurrence in this chapter

Equation form expr-7c75ecfdd8a1dd83

⟨w1,w2⟩∈R\tuple{w_1, w_2} \in \mathcal{R}

Read as: the ordered pair world w subscript one, then world w subscript two belongs to bisimulation relation script R

Means: the ordered pair world w subscript one, then world w subscript two belongs to bisimulation relation script R

1 occurrence in this chapter

Equation form expr-7cc21a3bda17828d

M⊩B[w]\mSat{M}{!B}[w]

Read as: model M satisfies formula B at world w

Means: model M satisfies formula B at world w

5 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: formula A

Means: formula A

22 occurrences in this chapter

Equation form expr-8282de19f2fd6f74

M∣p⊩Kbp[w1′]\mSat{M \mid p}{\Knows_b p}[w'_1]

Read as: model M restricted by p satisfies agent b knows that p at world w prime subscript one

Means: model M restricted by p satisfies agent b knows that p at world w prime subscript one

2 occurrences in this chapter

Equation form expr-86053f6920c00ebe

[A]B[!A] !B

Read as: after formula A is truthfully announced, formula B holds

Means: after formula A is truthfully announced, formula B holds

2 occurrences in this chapter

Equation form expr-86be9a55762d316a

KK

Read as: axiom K

Means: axiom K

1 occurrence in this chapter

Equation form expr-88f9e11bcc0503c0

KaA\Knows_a !A

Read as: agent a knows that formula A

Means: agent a knows that formula A

2 occurrences in this chapter

Equation form expr-89224ea9484e3018

CGA\CKnows_G !A

Read as: it is common knowledge among agent set G that formula A

Means: it is common knowledge among agent set G that formula A

2 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: accessibility relation R

Means: accessibility relation R

2 occurrences in this chapter

Equation form expr-8c90cb56cd9a3747

v2v_2

Read as: world v subscript two

Means: world v subscript two

2 occurrences in this chapter

Equation form expr-93b63b5612c3bd91

¬p,¬q\lnot p, \lnot q

Read as: p is false and q is false

Means: p is false and q is false

1 occurrence in this chapter

Equation form expr-9763a163e7ff6591

w3w_3

Read as: world w subscript three

Means: world w subscript three

5 occurrences in this chapter

Equation form expr-9b6e0bc79908859e

M∣B⊩C[w]\mSat{M \mid !B}{!C}[w]

Read as: model M restricted by formula B satisfies formula C at world w

Means: model M restricted by formula B satisfies formula C at world w

1 occurrence in this chapter

Equation form expr-9dd4e4b646218a71

M⊩B[w′]\mSat{M}{!B}[w']

Read as: model M satisfies formula B at world w prime

Means: model M satisfies formula B at world w prime

2 occurrences in this chapter

Equation form expr-a4a51fbde8d39ce5

p2\Obj p_2

Read as: propositional variable p subscript two

Means: propositional variable p subscript two

2 occurrences in this chapter

Equation form expr-a7fafab80789aa07

M∣B=⟨W′,R′,V′⟩\mModel M \mid !B = \tuple{W', R', V'}

Read as: model M restricted by formula B equals the ordered triple remaining world set W prime, then accessibility relation R prime, then valuation V prime

Means: model M restricted by formula B equals the ordered triple remaining world set W prime, then accessibility relation R prime, then valuation V prime

1 occurrence in this chapter

Equation form expr-aa6eff998d60c259

∀wRww\forall w Rww

Read as: for every world w, w is accessible from itself under relation R

Means: for every world w, w is accessible from itself under relation R

1 occurrence in this chapter

Equation form expr-adde99a013d73284

K(p→q)→(Kp→Kq)\Knows (p \lif q) \lif (\Knows p \lif \Knows q)

Read as: if it is known that p implies q, then, if p is known, q is known

Means: if it is known that p implies q, then, if p is known, q is known

1 occurrence in this chapter

Equation form expr-ae304640a6834b61

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

Read as: model M satisfies every agent in the group containing agent a and agent b knows that not q at world w subscript three

Means: model M satisfies every agent in the group containing agent a and agent b knows that not q at world w subscript three

1 occurrence in this chapter

Equation form expr-b0f185182b60561e

M⊩[p]Kbp[w1]\mSat{M}{[p] \Knows_b p}[w_1]

Read as: model M satisfies after p is truthfully announced, agent b knows that p holds at world w subscript one

Means: model M satisfies after p is truthfully announced, agent b knows that p holds at world w subscript one

1 occurrence in this chapter

Equation form expr-b4c632b38392d176

G′⊆GG' \subseteq G

Read as: agent group G prime is a subset of agent set G

Means: agent group G prime is a subset of agent set G

2 occurrences in this chapter

Equation form expr-b59c0ca457682eca

M⊩p[w]\mSat{M}{p}[w]

Read as: model M satisfies p at world w

Means: model M satisfies p at world w

2 occurrences in this chapter

Equation form expr-b5b446abb4d0323b

M⊩A[w]\mSat{M}{!A}[w]

Read as: model M satisfies formula A at world w

Means: model M satisfies formula A at world w

2 occurrences in this chapter

Equation form expr-b99d2e5f37ae7e17

w′w'

Read as: world w prime

Means: world w prime

5 occurrences in this chapter

Equation form expr-ba358c923f2dc056

∀u∀v∀w((Ruv∧Rvw)→Ruw)\forall u \forall v \forall w ((Ruv \land Rvw) \lif Ruw)

Read as: for every u, v, and w, if v is accessible from u and w is accessible from v, then w is accessible from u

Means: for every u, v, and w, if v is accessible from u and w is accessible from v, then w is accessible from u

1 occurrence in this chapter

Equation form expr-bd92d26137da0ecb

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)}.

Read as: The source's indexed transitive-closure definition. R plus is the union of R to the n over natural numbers n. Here R to the zero equals R, and R to the n plus one is the set of ordered pairs x, z such that there exists a y for which R to the n relates x to y and R relates y to z.

Means: The source's indexed transitive-closure definition. R plus is the union of R to the n over natural numbers n. Here R to the zero equals R, and R to the n plus one is the set of ordered pairs x, z such that there exists a y for which R to the n relates x to y and R relates y to z.

1 occurrence in this chapter

Equation form expr-bdac1b066ea0952a

M⊩¬q[w1]\mSat{M}{\lnot q}[w_1]

Read as: model M satisfies not q at world w subscript one

Means: model M satisfies not q at world w subscript one

1 occurrence in this chapter

Equation form expr-c16b6b879881d7ba

KaB\Knows_a !B

Read as: agent a knows that formula B

Means: agent a knows that formula B

1 occurrence in this chapter

Equation form expr-c241b24098b230e9

¬Kp→K¬Kp\lnot \Knows p \lif \Knows \neg \Knows p

Read as: if p is not known, then it is known that p is not known

Means: if p is not known, then it is known that p is not known

1 occurrence in this chapter

Equation form expr-c250348f8183b663

M∣(p∧¬Kbp)\mModel M \mid (p \land \lnot \Knows_b p)

Read as: model M restricted by open scope, p and not agent b knows that p, close scope

Means: model M restricted by open scope, p and not agent b knows that p, close scope

1 occurrence in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not formula A

Means: not formula A

3 occurrences in this chapter

Equation form expr-ca978112ca1bbdca

aa

Read as: agent a

Means: agent a

15 occurrences in this chapter

Equation form expr-cc15fe8e6b938daf

Kp→KKp\Knows p \lif \Knows \Knows p

Read as: if p is known, then it is known that p is known

Means: if p is known, then it is known that p is known

1 occurrence in this chapter

Equation form expr-cdc2ed7d3b3d72c2

⊥\lfalse

Read as: falsity

Means: falsity

4 occurrences in this chapter

Equation form expr-cf26fe5bd7e6ea18

(A→B)(!A \lif !B)

Read as: open scope, formula A implies formula B, close scope

Means: open scope, formula A implies formula B, close scope

2 occurrences in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: the conditional connective

Means: the conditional connective

2 occurrences in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: formula B

Means: formula B

10 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

2 occurrences in this chapter

Equation form expr-d0c897fd435ba4d4

V′(p)={u∈W′:u∈V(p)}V'(p) = \Setabs{ u \in W'}{u \in V(p) }

Read as: valuation V prime of p equals the set of all world u in remaining world set W prime such that world u belongs to valuation V of p

Means: valuation V prime of p equals the set of all world u in remaining world set W prime such that world u belongs to valuation V of p

1 occurrence in this chapter

Equation form expr-d16b73ce79fc2dfd

M⊮B[w]\mSat/{M}{!B}[w]

Read as: model M does not satisfy formula B at world w

Means: model M does not satisfy formula B at world w

4 occurrences in this chapter

Equation form expr-d21058d45fb8b6fd

RG′ww′R_{G'} w w'

Read as: world w prime is accessible from world w under the group G prime accessibility relation

Means: world w prime is accessible from world w under the group G prime accessibility relation

1 occurrence in this chapter

Equation form expr-d417353d70f109cf

p,¬qp, \lnot q

Read as: p is true and q is false

Means: p is true and q is false

2 occurrences in this chapter

Equation form expr-d55259d136c3374c

p,qp,q

Read as: p is true and q is true

Means: p is true and q is true

1 occurrence in this chapter

Equation form expr-d6518d9bc2e9f8f0

R+R^+

Read as: transitive closure R plus

Means: transitive closure R plus

1 occurrence in this chapter

Equation form expr-daf3cd9a94aaa27d

M∣p\mModel M \mid p

Read as: model M restricted by p

Means: model M restricted by p

2 occurrences in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: valuation V

Means: valuation V

1 occurrence in this chapter

Equation form expr-df701b27f24bbe71

M1M_1

Read as: model M subscript one

Means: model M subscript one

1 occurrence in this chapter

Equation form expr-e0ce15852db94134

p∧¬Kbpp \land \lnot \Knows_b p

Read as: p and not agent b knows that p

Means: p and not agent b knows that p

1 occurrence in this chapter

Equation form expr-e27c7c3dbd7a0587

v1∈W1v_1 \in W_1

Read as: world v subscript one belongs to world set W subscript one

Means: world v subscript one belongs to world set W subscript one

2 occurrences in this chapter

Equation form expr-e632b7095b0bf32c

TT

Read as: axiom T

Means: axiom T

1 occurrence in this chapter

Equation form expr-e657646bf8534fcf

Kp→p\Knows p \lif p

Read as: if p is known, then p is true

Means: if p is known, then p is true

1 occurrence in this chapter

Equation form expr-e8f84252db99e5d9

⟨M1,w1⟩=↔⟨M2,w2⟩\tuple{M_1, w_1} \leftrightarroweq \tuple{M_2, w_2}

Read as: the ordered pair model M subscript one, then world w subscript one is bisimilar to the ordered pair model M subscript two, then world w subscript two

Means: the ordered pair model M subscript one, then world w subscript one is bisimilar to the ordered pair model M subscript two, then world w subscript two

2 occurrences in this chapter

Equation form expr-e945b5ddcecdc573

M2M_2

Read as: model M subscript two

Means: model M subscript two

1 occurrence in this chapter

Equation form expr-e95f0eb559dd6d09

p,qp, q

Read as: p is true and q is true

Means: p is true and q is true

1 occurrence in this chapter

Equation form expr-e9a636effb6eec07

Ka\Knows_a

Read as: the knowledge operator for agent a

Means: the knowledge operator for agent a

4 occurrences in this chapter

Equation form expr-e9cc42681343bdb8

w3′w'_3

Read as: world w prime subscript three

Means: world w prime subscript three

1 occurrence in this chapter

Equation form expr-e9fe8ee5ada9c8bf

W′W'

Read as: remaining world set W prime

Means: remaining world set W prime

1 occurrence in this chapter

Equation form expr-ea74679ed2e96b23

Ra{R}_a

Read as: agent a accessibility relation R

Means: agent a accessibility relation R

1 occurrence in this chapter

Equation form expr-f157f71e0163a897

□\Box

Read as: the necessity operator

Means: the necessity operator

3 occurrences in this chapter

Equation form expr-f50074d9022fd93f

M⊩CG′A[w]\mSat{M}{\CKnows_{G'} !A}[ w]

Read as: model M satisfies it is common knowledge among agent group G prime that formula A at world w

Means: model M satisfies it is common knowledge among agent group G prime that formula A at world w

1 occurrence in this chapter

Equation form expr-f7279042aa3a7c7c

M∣B\mModel M \mid !B

Read as: model M restricted by formula B

Means: model M restricted by formula B

1 occurrence in this chapter

Equation form expr-f8dcd48388f1ed21

w∈V(p)w \in V(p)

Read as: world w belongs to valuation V of p

Means: world w belongs to valuation V of p

3 occurrences in this chapter

Equation form expr-f9c6cbd6245f9917

M=⟨W,R,V⟩\mModel{M} = \tuple{W, R, V}

Read as: model M equals the ordered triple world set W, then accessibility relation R, then valuation V

Means: model M equals the ordered triple world set W, then accessibility relation R, then valuation V

1 occurrence in this chapter

Equation form expr-fa33c8f9a58085dc

K\Knows

Read as: the single-agent knowledge operator

Means: the single-agent knowledge operator

3 occurrences in this chapter

Equation form expr-fbdcb41ac2fae933

R\mathcal{R}

Read as: bisimulation relation script R

Means: bisimulation relation script R

1 occurrence in this chapter

Equation form expr-fcb5f40df9be6bae

WW

Read as: world set W

Means: world set W

2 occurrences in this chapter

Equation form expr-ff9ba27416d63e9a

(A∧B)(!A \land !B)

Read as: open scope, formula A and formula B, close scope

Means: open scope, formula A and formula B, close scope

2 occurrences in this chapter

Definition of the multi-agent epistemic language

The language has a set G of agent symbols, the selected propositional primitives and connectives, and for each agent a, a knowledge operator indexed by a.

Source

Inductive definition of epistemic formulas

The source gives the selected atomic and truth-functional clauses and adds that if A is a formula and a belongs to G, then agent a knows A is a formula.

Source

Definition of everybody knows

For a subgroup G prime, everybody knows A abbreviates the conjunction, over every b in G prime, that agent b knows A.

Source

Definition of a multi-agent epistemic model

A model contains a nonempty world set, one binary accessibility relation R subscript a for each agent a in G, and a valuation assigning worlds to propositional variables.

Source

Definition of truth at a world in an epistemic model

The selected propositional clauses are followed by the knowledge clause: agent a knows B at w exactly when B holds at every world accessible from w under agent a's relation.

Source

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

Simple three-world epistemic model graph

Worlds w one, w two, and w three carry six printed truth values. The graph prints agent a and b accessibility links and loops exactly as encoded in its structure record.

Source

Exercise evaluating six epistemic formulas

Determine which of six displayed satisfaction claims hold in the simple model. The exercise remains unsolved; no truth value or derivation is supplied.

Source

Indexed definition of transitive closure

The display calls R plus the union of R to the n, sets R to the zero equal to R, and defines R to the n plus one by relational composition. This source indexing is preserved exactly.

Source

Truth condition for common knowledge

Common knowledge of A among G prime holds at w exactly when A holds at every world reachable from w under the group relation R subscript G prime.

Source

Figure containing four epistemic correspondence principles

The outer table supplies the caption and label. Its inner tabular object gives one closure row and rows for reflexivity, transitivity, and euclideanness.

Source

Four epistemic correspondence rows

The source-ordered rows are Closure with a blank frame-condition cell, Veridicality for reflexivity, Positive Introspection for transitivity, and Negative Introspection for euclideanness.

Source

Definition of bisimulation

A relation between two models is a bisimulation when linked worlds agree on all propositional variables and satisfy the source's forth and back clauses for every agent. The source switches from agent set G to A in those clauses; that notation is retained.

Source

Theorem on invariance under bisimulation

Bisimilar pointed models satisfy exactly the same epistemic formulas.

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

Two bisimilar model graphs

The left graph has worlds w one through w three; the right has v one and v two. All accessibility arrows are for agent a. Dotted unlabelled links connect w one to v one and both w two and w three to v two. No valuation is printed.

Source

Definition of the language with public announcements

The epistemic language is extended by a public-announcement operator indexed by a formula B, alongside the selected propositional and agent-indexed knowledge operators.

Source

Inductive definition of public-announcement formulas

After the selected propositional and knowledge clauses, the source adds that after-A-announced B is a formula whenever A and B are formulas.

Source

Truth definition for public announcement logic

The announcement clause evaluates C in the model restricted to B-worlds whenever B is true. The source then explicitly restricts the world set, every agent relation, and the valuation.

Source

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

Public-announcement update graph

The left graph has worlds w one, w two, and w three. The right graph retains the p-worlds as w one prime and w three prime. Every printed agent relation and loop is recorded; the drawing marks no distinguished world.

Source

Cross-reference reference-001128

the knowledge clause in the definition of truth at a world

Source occurrence

Cross-reference reference-001129

the simple three-world epistemic model

Source occurrence

Cross-reference reference-001130

the section defining operations on relations

Source occurrence

Cross-reference reference-001131

the figure of two bisimilar models

Source occurrence

Cross-reference reference-001132

the before-and-after public-announcement model

Source occurrence

Cross-reference reference-001133

the before-and-after public-announcement model

Source occurrence

Source disclosures

Source-generated case expression tr058-source-macro-0001

A≡⊥!A \ident \lfalse

Read as: Case: A is falsity.

Read in context source

Source-generated case expression tr058-source-macro-0002

A≡¬B!A \ident \lnot !B

Read as: Case: A is the negation of B.

Read in context source

Source-generated case expression tr058-source-macro-0003

A≡(B∧C)!A \ident (!B \land !C)

Read as: Case: A is the conjunction of B and C.

Read in context source

Source-generated case expression tr058-source-macro-0004

A≡(B∨C)!A \ident (!B \lor !C)

Read as: Case: A is the disjunction of B and C.

Read in context source

Source-generated case expression tr058-source-macro-0005

A≡(B→C)!A \ident (!B \lif !C)

Read as: Case: A is the conditional from B to C.

Read in context source

Source-generated case expression tr058-source-macro-0006

A≡KaB!A \ident \Knows_a !B

Read as: Case: A says that agent a knows B.

Read in context source

Source-generated case expression tr058-source-macro-0014

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr058-source-macro-0015

¬q\mFalse{q}

Read as: q is false

Read in context source

Source-generated case expression tr058-source-macro-0016

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr058-source-macro-0017

q\mTrue{q}

Read as: q is true

Read in context source

Source-generated case expression tr058-source-macro-0018

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr058-source-macro-0019

¬q\mFalse{q}

Read as: q is false

Read in context source

Source-generated case expression tr058-source-macro-0007

A≡⊥!A \ident \lfalse

Read as: Case: A is falsity.

Read in context source

Source-generated case expression tr058-source-macro-0008

A≡¬B!A \ident \lnot !B

Read as: Case: A is the negation of B.

Read in context source

Source-generated case expression tr058-source-macro-0009

A≡(B∧C)!A \ident (!B \land !C)

Read as: Case: A is the conjunction of B and C.

Read in context source

Source-generated case expression tr058-source-macro-0010

A≡(B∨C)!A \ident (!B \lor !C)

Read as: Case: A is the disjunction of B and C.

Read in context source

Source-generated case expression tr058-source-macro-0011

A≡(B→C)!A \ident (!B \lif !C)

Read as: Case: A is the conditional from B to C.

Read in context source

Source-generated case expression tr058-source-macro-0012

A≡KaB!A \ident \Knows_a !B

Read as: Case: A says that agent a knows B.

Read in context source

Source-generated case expression tr058-source-macro-0013

A≡[B]C!A \ident [!B] !C

Read as: Case: A says that after B is truthfully announced, C holds.

Read in context source

Ordered structures

Simple three-world epistemic model graph

Structure: diagram tikz.

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.

Read the source-bound structure in context

Four epistemic correspondence rows

Structure: table.

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.

Read the source-bound structure in context

Two bisimilar model graphs

Structure: diagram tikz.

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.

Read the source-bound structure in context

Public-announcement update graph

Structure: diagram tikz.

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.

Read the source-bound structure in context