Normal Modal Logics

Frame Definability

Equation form expr-01cadf2075e66b6d

Ak!A_k

Read as: A subscript k

Means: A subscript k

1 occurrence in this chapter

Equation form expr-02e18552519285db

Source-census fragment. Read the complete source formula tr051-reader-composite-math-0001. The original fragment is preserved as forensic source evidence, not as a complete reader equation.

1 occurrence in this chapter

Equation form expr-030f743a5c241eef

M⊨∀X∀x(∀y(Q(x,y)→X(y))→X(x))\Sat{M}{\lforall[X][\lforall[x][(\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})] \lif \Atom{X}{x})]]}

Read as: structure M satisfies: for every set X, for every x, if for every y, Q relates x to y only if X holds of y, then X holds of x

Means: structure M satisfies: for every set X, for every x, if for every y, Q relates x to y only if X holds of y, then X holds of x

1 occurrence in this chapter

Equation form expr-034a69bf5d96f8a8

i=1i = 1

Read as: i equals one

Means: i equals one

1 occurrence in this chapter

Equation form expr-03d04c9b1863399f

u∈V(p)u \in V(p)

Read as: u belongs to V of p

Means: u belongs to V of p

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: s

4 occurrences in this chapter

Equation form expr-05ae1fcf8064cc29

M⊨∀xQ(x,x)\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}

Read as: structure M satisfies that for every x, Q relates x to itself

Means: structure M satisfies that for every x, Q relates x to itself

3 occurrences in this chapter

Equation form expr-063bdaf14dd716fa

Rw2w3Rw_2w_3

Read as: R relates w subscript two to w subscript three

Means: R relates w subscript two to w subscript three

1 occurrence in this chapter

Equation form expr-06bf026a7f4cf24c

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

Read as: B is false in modal model M prime at world w

Means: B is false in modal model M prime at world w

1 occurrence in this chapter

Equation form expr-071eb4ebfd95772d

M⊩A[w] iff M′,s⊨STx(A)\mSat{M}{!A}[w] \text{ iff } \Sat{M'}{\ST_x(!A)}[s]

Read as: A is true in modal model M at world w if and only if structure M prime satisfies the standard translation at x of A under assignment s

Means: A is true in modal model M at world w if and only if structure M prime satisfies the standard translation at x of A under assignment s

1 occurrence in this chapter

Equation form expr-0ad4e4e6f349e224

M⊨∀y(Q(x,y)→X(y))→X(x)\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})] \lif \Atom{X}{x}}

Read as: structure M satisfies: if, for every y, Q relates x to y only if X holds of y, then X holds of x

Means: structure M satisfies: if, for every y, Q relates x to y only if X holds of y, then X holds of x

1 occurrence in this chapter

Equation form expr-0bfe935e70c321c7

uu

Read as: u

Means: u

13 occurrences in this chapter

Equation form expr-0da73571098ef11f

a2M\Assign{a_2}{M}

Read as: the interpretation of a subscript two in structure M

Means: the interpretation of a subscript two in structure M

1 occurrence in this chapter

Equation form expr-0e21ee98c84daaad

□A→A\Box !A \lif !A

Read as: if necessarily A, then A

Means: if necessarily A, then A

2 occurrences in this chapter

Equation form expr-13f75e1a99fec552

M′\mModel{M'}

Read as: M prime

Means: M prime

1 occurrence in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

7 occurrences in this chapter

Equation form expr-172a6d6592e8e4f4

C⊨A\mClass{C} \Entails !A

Read as: A is valid in the class of models C

Means: A is valid in the class of models C

1 occurrence in this chapter

Equation form expr-1a53000974926187

V(p)V(p)

Read as: V of p

Means: V of p

1 occurrence in this chapter

Equation form expr-1acc772fea2bf354

F⊭◇p→□◇p\mModel{F} \Entails/ \Diamond p \lif \Box\Diamond p

Read as: the conditional from possibly p to necessarily possibly p is not valid in frame F

Means: the conditional from possibly p to necessarily possibly p is not valid in frame F

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

1 occurrence in this chapter

Equation form expr-1b38809e40d7d75f

QM\Assign{Q}{M}

Read as: the interpretation of Q in structure M

Means: the interpretation of Q in structure M

1 occurrence in this chapter

Equation form expr-1caa49930400d88d

aiMk=i\Assign{a_i}{M_k} = i

Read as: the interpretation of a subscript i in structure M subscript k equals i

Means: the interpretation of a subscript i in structure M subscript k equals i

1 occurrence in this chapter

Equation form expr-1d4410026fb2d41e

F⊨□p→◇p\mModel{F} \Entails \Box p \lif \Diamond p

Read as: the conditional from necessarily p to possibly p is valid in frame F

Means: the conditional from necessarily p to possibly p is valid in frame F

2 occurrences in this chapter

Equation form expr-1e1c96a427cf151d

M⊮□◇p[u]\mSat/{M}{\Box\Diamond p}[u]

Read as: necessarily possibly p is false in modal model M at world u

Means: necessarily possibly p is false in modal model M at world u

1 occurrence in this chapter

Equation form expr-1f89a8bab0a2d67e

M⊨F\Sat{M}{!F}

Read as: structure M satisfies F

Means: structure M satisfies F

2 occurrences in this chapter

Equation form expr-20062f7e457d1946

[w]={w′∈W:Rww′}[w] = \{w'\in W : Rww'\}

Read as: the equivalence class of w equals the set of worlds w prime in W such that R relates w to w prime

Means: the equivalence class of w equals the set of worlds w prime in W such that R relates w to w prime

1 occurrence in this chapter

Equation form expr-22de243917a2bb24

M⊮□p→◇p[w]\mSat/{M}{\Box p \lif \Diamond p}[w]

Read as: the conditional from necessarily p to possibly p is false in modal model M at world w

Means: the conditional from necessarily p to possibly p is false in modal model M at world w

1 occurrence in this chapter

Equation form expr-23fac266c08cc34b

pi\Obj p_i

Read as: p subscript i

Means: p subscript i

1 occurrence in this chapter

Equation form expr-255c3d3e7ffa6e47

M⊮◇p[u]\mSat/{M}{\Diamond p}[u]

Read as: possibly p is false in modal model M at world u

Means: possibly p is false in modal model M at world u

1 occurrence in this chapter

Equation form expr-258f31d0f70c1bec

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

Read as: p is true in modal model M at world u

Means: p is true in modal model M at world u

2 occurrences in this chapter

Equation form expr-28e26518e42f4d7c

□¬p→¬p\Box \lnot p \lif \lnot p

Read as: if necessarily not p, then not p

Means: if necessarily not p, then not p

1 occurrence in this chapter

Equation form expr-28f5470053807ed9

RuzRuz

Read as: R relates u to z

Means: R relates u to z

3 occurrences in this chapter

Equation form expr-298035719d684b30

M⊮p→□◇p[u]\mSat/{M}{p \lif \Box\Diamond p}[u]

Read as: the conditional from p to necessarily possibly p is false in modal model M at world u

Means: the conditional from p to necessarily possibly p is false in modal model M at world u

1 occurrence in this chapter

Equation form expr-2a54e65b077d8815

M′,s⊨STx(A)\Sat{M'}{\ST_x(!A)}[s]

Read as: structure M prime satisfies the standard translation at x of A under assignment s

Means: structure M prime satisfies the standard translation at x of A under assignment s

1 occurrence in this chapter

Equation form expr-2a918e6d283c930a

z∈V(p)z \in V(p)

Read as: z belongs to V of p

Means: z belongs to V of p

2 occurrences 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 R relates w to u and R relates w to v, then R relates u to v

Means: for every w, u, and v, if R relates w to u and R relates w to v, then R relates u to v

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

1 occurrence in this chapter

Equation form expr-3030b1c1f49f45a7

QM′=R\Assign{Q}{M'} = R

Read as: the interpretation of Q in structure M prime equals R

Means: the interpretation of Q in structure M prime equals R

1 occurrence in this chapter

Equation form expr-30a4b27320f21c4b

⊩◇A\mSat{{}}{\Diamond \formula{A}}

Read as: possibly A is true at this world

Means: possibly A is true at this world

1 occurrence in this chapter

Equation form expr-30cd910ecf656b71

M⊮◇p[v]\mSat/{M}{\Diamond p}[v]

Read as: possibly p is false in modal model M at world v

Means: possibly p is false in modal model M at world v

1 occurrence in this chapter

Equation form expr-3106fac3e3c8f992

w2w_2

Read as: w subscript two

Means: w subscript two

2 occurrences in this chapter

Equation form expr-313b1a695b7f40bf

s′(y)=s(x)s'(y) = s(x)

Read as: s prime of y equals s of x

Means: s prime of y equals s of x

1 occurrence in this chapter

Equation form expr-3209b39334421779

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

Read as: modal model M prime equals the ordered triple W prime, R prime, V prime

Means: modal model M prime equals the ordered triple W prime, R prime, V prime

1 occurrence in this chapter

Equation form expr-340ca67836dd97ea

RwuRwu

Read as: R relates w to u

Means: R relates w to u

4 occurrences in this chapter

Equation form expr-34c4a8665075bdc1

RuvRuv

Read as: R relates u to v

Means: R relates u to v

9 occurrences in this chapter

Equation form expr-354c64b64061143e

[v][v]

Read as: the equivalence class of v

Means: the equivalence class of v

1 occurrence in this chapter

Equation form expr-399c3876c2d85777

F⊨A iff F′⊨A′\mModel{F} \Entails !A \text{ iff } \Sat{F'}{!A'}

Read as: A is valid in frame F if and only if structure F prime satisfies A prime

Means: A is valid in frame F if and only if structure F prime satisfies A prime

1 occurrence in this chapter

Equation form expr-3a856f816d796fcd

Mk⊨F\Sat{M_k}{!F}

Read as: structure M subscript k satisfies F

Means: structure M subscript k satisfies F

1 occurrence in this chapter

Equation form expr-3ae05107aa9fd677

Rw2w1Rw_2w_1

Read as: R relates w subscript two to w subscript one

Means: R relates w subscript two to w subscript one

1 occurrence in this chapter

Equation form expr-3bbc93510b43d2ef

M,s⊨X(x)\Sat{M}{\Atom{X}{x}}[s]

Read as: structure M satisfies X of x under assignment s

Means: structure M satisfies X of x under assignment s

1 occurrence in this chapter

Equation form expr-3c198ca66ccccccb

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

Read as: A is true in modal model M at world u

Means: A is true in modal model M at world u

1 occurrence in this chapter

Equation form expr-3f4ac1c344779933

F=⟨W,R⟩\mModel{F}= \tuple{W, R}

Read as: frame F equals the ordered pair W, R

Means: frame F equals the ordered pair W, R

1 occurrence in this chapter

Equation form expr-4065cb3d8fa520d1

M⊩T[w]\mSat{M}{\Ax{T}}[w]

Read as: axiom T is true in modal model M at world w

Means: axiom T is true in modal model M at world w

1 occurrence in this chapter

Equation form expr-40cf1002ea30f263

F⊨□p→□□p\mModel{F} \Entails \Box p \lif \Box\Box p

Read as: the conditional from necessarily p to necessarily necessarily p is valid in frame F

Means: the conditional from necessarily p to necessarily necessarily p is valid in frame F

1 occurrence in this chapter

Equation form expr-4284ca25200dbeb1

|Mk|={1,…,k}\Domain{M_k} = \{1, \dots, k\}

Read as: the domain of structure M subscript k equals the set of integers from one through k

Means: the domain of structure M subscript k equals the set of integers from one through k

1 occurrence in this chapter

Equation form expr-429e7f1087bafa6e

PiP_i

Read as: P subscript i

Means: P subscript i

3 occurrences in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: M

Means: M

5 occurrences in this chapter

Equation form expr-438757f12dd8c3fc

w1w_1

Read as: w subscript one

Means: w subscript one

2 occurrences in this chapter

Equation form expr-45ef2afb7c8b6bb1

V′(p)=V(p)∩W′V'(p) = V(p) \cap W'

Read as: V prime of p equals the intersection of V of p with W prime

Means: V prime of p equals the intersection of V of p with W prime

1 occurrence in this chapter

Equation form expr-4ab5585274f8cba1

RvwRvw

Read as: R relates v to w

Means: R relates v to w

6 occurrences in this chapter

Equation form expr-4ae81572f06e1b88

QQ

Read as: Q

Means: Q

4 occurrences in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: X

Means: X

1 occurrence in this chapter

Equation form expr-4c94485e0c21ae6c

vv

Read as: v

Means: v

11 occurrences in this chapter

Equation form expr-4e6f1aff004845a2

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

Read as: possibly A is true in modal model M at world w prime

Means: possibly A is true in modal model M at world w prime

1 occurrence in this chapter

Equation form expr-50789075178de4bd

F=⟨W,R⟩\mModel{F} = \tuple{W,R}

Read as: frame F equals the ordered pair W, R

Means: frame F equals the ordered pair W, R

3 occurrences in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: w

Means: w

26 occurrences in this chapter

Equation form expr-5136fc4246e7d497

◇\Diamond

Read as: the possibility operator

Means: the possibility operator

1 occurrence in this chapter

Equation form expr-534752748f7021e0

F=⟨W,R⟩\mModel{F} =\tuple{W,R}

Read as: frame F equals the ordered pair W, R

Means: frame F equals the ordered pair W, R

2 occurrences in this chapter

Equation form expr-5393b99b487343b8

◇p↔□p\Diamond p \liff \Box p

Read as: possibly p if and only if necessarily p

Means: possibly p if and only if necessarily p

1 occurrence in this chapter

Equation form expr-54f7441936e33e75

M⊮p[w]\mSat/{M}{p}[w]

Read as: p is false in modal model M at world w

Means: p is false in modal model M at world w

1 occurrence in this chapter

Equation form expr-555ae909a5687237

A→□◇A!A \lif \Box\Diamond !A

Read as: if A, then necessarily possibly A

Means: if A, then necessarily possibly A

1 occurrence in this chapter

Equation form expr-56a481714be784c1

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

Read as: p is true in modal model M at world z

Means: p is true in modal model M at world z

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

2 occurrences in this chapter

Equation form expr-5788fffe7e0d5fac

W′⊆WW' \subseteq W

Read as: W prime is a subset of W

Means: W prime is a subset of W

1 occurrence in this chapter

Equation form expr-594e519ae499312b

zz

Read as: z

Means: z

2 occurrences in this chapter

Equation form expr-59e881250d16c35d

s(X)={z:Rxz}s(X) = \Setabs{z}{Rxz}

Read as: s of X equals the set of z such that R relates x to z

Means: s of X equals the set of z such that R relates x to z

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

1 occurrence in this chapter

Equation form expr-5c82e14a4ff9612e

RuyRuy

Read as: R relates u to y

Means: R relates u to y

1 occurrence in this chapter

Equation form expr-5e769b89788d547a

s′s'

Read as: s prime

Means: s prime

1 occurrence in this chapter

Equation form expr-607e495a98cb5559

ℤ\Int

Read as: the integers

Means: the integers

1 occurrence in this chapter

Equation form expr-612f0c2929c3d913

M⊩D\mSat{M}{\Ax{D}}

Read as: axiom D is true in modal model M

Means: axiom D is true in modal model M

1 occurrence in this chapter

Equation form expr-62019e757a9cfb48

M⊮◇A[w]\mSat/{M}{\Diamond !A}[w]

Read as: possibly A is false in modal model M at world w

Means: possibly A is false in modal model M at world w

1 occurrence in this chapter

Equation form expr-63713d1f6d4dc4ed

M⊩A\mSat{M}{!A}

Read as: A is true in modal model M

Means: A is true in modal model M

2 occurrences in this chapter

Equation form expr-66d6ef256f74e223

∀x∀y(Q(x,y)→Q(y,x))\lforall[x][\lforall[y][(\Atom{Q}{x,y} \lif \Atom{Q}{y, x})]]

Read as: for every x and every y, if Q relates x to y, then Q relates y to x

Means: for every x and every y, if Q relates x to y, then Q relates y to x

1 occurrence in this chapter

Equation form expr-67cbbf7fc57cc7f6

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

Read as: modal model M equals the ordered triple W, R, V

Means: modal model M equals the ordered triple W, R, V

3 occurrences in this chapter

Equation form expr-67f413e7a3fdc858

X⊆WX \subseteq W

Read as: X is a subset of W

Means: X is a subset of W

1 occurrence in this chapter

Equation form expr-69622ca4d72983a3

QF′=R\Assign{Q}{F'} = R

Read as: the interpretation of Q in structure F prime equals R

Means: the interpretation of Q in structure F prime equals R

1 occurrence in this chapter

Equation form expr-69ef9ee2c45eb3b7

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

Read as: A is true in modal model M at world w prime

Means: A is true in modal model M at world w prime

1 occurrence in this chapter

Equation form expr-6a020b42f6471d12

◇□p→□◇p\Diamond\Box p \lif \Box\Diamond p

Read as: if possibly necessarily p, then necessarily possibly p

Means: if possibly necessarily p, then necessarily possibly p

1 occurrence in this chapter

Equation form expr-6c22e22b0fbbf854

M⊮□◇p[w]\mSat/{M}{\Box\Diamond p}[w]

Read as: necessarily possibly p is false in modal model M at world w

Means: necessarily possibly p is false in modal model M at world w

1 occurrence in this chapter

Equation form expr-6cfa4554888e09ea

Rw1w2Rw_1w_2

Read as: R relates w subscript one to w subscript two

Means: R relates w subscript one to w subscript two

1 occurrence in this chapter

Equation form expr-6db8da226ec54d03

V(pi)V(\Obj p_i)

Read as: V of p subscript i

Means: V of p subscript i

1 occurrence in this chapter

Equation form expr-6ef14c45df800067

∀X1…∀Xn∀xSTx(A)[X1/P1,…,Xn/Pn],\lforall[X_1][\dots\lforall[X_n][\lforall[x][ \SSubst{\ST_x(!A)}{\subst{X_1}{P_1}, \dots, \subst{X_n}{P_n}}]]],

Read as: for every X subscript one through X subscript n, and every x, the result of simultaneously substituting X subscript one through X subscript n for P subscript one through P subscript n in the standard translation at x of A

Means: for every X subscript one through X subscript n, and every x, the result of simultaneously substituting X subscript one through X subscript n for P subscript one through P subscript n in the standard translation at x of A

1 occurrence in this chapter

Equation form expr-6f76ca43c33130e7

W′=[w]W' = [w]

Read as: W prime equals the equivalence class of w

Means: W prime equals the equivalence class of w

1 occurrence in this chapter

Equation form expr-7023b10755c9b26e

p→□◇pp \lif \Box\Diamond p

Read as: if p, then necessarily possibly p

Means: if p, then necessarily possibly p

3 occurrences in this chapter

Equation form expr-710bbcd2514e5ebd

STx(A)\ST_x(!A)

Read as: the standard translation at x of A

Means: the standard translation at x of A

4 occurrences in this chapter

Equation form expr-71814e536cd352ba

PM=R\Assign{P}{M} = R

Read as: the interpretation of P in structure M equals R

Means: the interpretation of P in structure M equals R

1 occurrence in this chapter

Equation form expr-76b7670fac05addd

PnP_n

Read as: P subscript n

Means: P subscript n

1 occurrence in this chapter

Equation form expr-77f38de71e5cae32

STx(A)=(STx(B)∧STx(C))\ST_x(\indfrm) = (\ST_x(!B) \land \ST_x(!C))

Read as: the standard translation at x of the current formula equals the conjunction of the standard translation at x of B and the standard translation at x of C

Means: the standard translation at x of the current formula equals the conjunction of the standard translation at x of B and the standard translation at x of C

1 occurrence in this chapter

Equation form expr-786aa0b01b2874ad

Rww′Rww'

Read as: R relates w to w prime

Means: R relates w to w prime

2 occurrences in this chapter

Equation form expr-7896a107ff051a92

□◇A\Box \Diamond !A

Read as: necessarily possibly A

Means: necessarily possibly A

1 occurrence in this chapter

Equation form expr-79a73397590ea1a9

u,v∈Wu,v \in W

Read as: u and v belong to W

Means: u and v belong to W

1 occurrence in this chapter

Equation form expr-79d4c7f9c8579543

ℕ\Nat

Read as: the natural numbers

Means: the natural numbers

1 occurrence in this chapter

Equation form expr-7b3029693916bc22

QMk=<\Assign{Q}{M_k} = <

Read as: the interpretation of Q in structure M subscript k equals the less than relation

Means: the interpretation of Q in structure M subscript k equals the less than relation

1 occurrence in this chapter

Equation form expr-7b422f4adc28e797

W={u,v}W = \{u, v \}

Read as: W equals the set containing u and v

Means: W equals the set containing u and v

1 occurrence in this chapter

Equation form expr-7b44178dea34664e

s(x)=ws(x) = w

Read as: s of x equals w

Means: s of x equals w

1 occurrence in this chapter

Equation form expr-7d5e823693d6fbee

M,s′⊨Q(x,y)→X(y)\Sat{M}{\Atom{Q}{x,y} \lif \Atom{X}{y}}[s']

Read as: structure M satisfies the conditional from Q relating x to y to X holding of y, under assignment s prime

Means: structure M satisfies the conditional from Q relating x to y to X holding of y, under assignment s prime

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

22 occurrences in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

1 occurrence in this chapter

Equation form expr-82b1041f1d1b78d1

[w][w]

Read as: open bracket w close bracket

Means: open bracket w close bracket

2 occurrences in this chapter

Equation form expr-82b25b3e734d5b2c

QM=R\Assign{Q}{M} = R

Read as: the interpretation of Q in structure M equals R

Means: the interpretation of Q in structure M equals R

2 occurrences in this chapter

Equation form expr-830c714933e2096e

F\mModel{F}

Read as: F

Means: F

21 occurrences in this chapter

Equation form expr-84552be6395d0730

RwvRwv

Read as: R relates w to v

Means: R relates w to v

3 occurrences in this chapter

Equation form expr-84db8bf2fc43471a

∀u∃vRuv\forall u \exists v Ruv

Read as: for every u there exists a v such that R relates u to v

Means: for every u there exists a v such that R relates u to v

1 occurrence in this chapter

Equation form expr-84dd6ba0577ab84b

Source-census fragment. Read the complete source formula tr051-reader-composite-math-0002. The original fragment is preserved as forensic source evidence, not as a complete reader equation.

1 occurrence in this chapter

Equation form expr-85c3ce29e3a4dc40

C\mClass{C}

Read as: C

Means: C

1 occurrence in this chapter

Equation form expr-87e6369aa2e00a65

a1M\Assign{a_1}{M}

Read as: the interpretation of a subscript one in structure M

Means: the interpretation of a subscript one in structure M

1 occurrence in this chapter

Equation form expr-88431f9c7d8d3ed0

F⊨□p→p\mModel{F} \Entails \Box p \lif p

Read as: the conditional from necessarily p to p is valid in frame F

Means: the conditional from necessarily p to p is valid in frame F

2 occurrences in this chapter

Equation form expr-887d873a56a18172

STx(□p→p)\ST_x(\Box p \lif p)

Read as: the standard translation at x of the conditional from necessarily p to p

Means: the standard translation at x of the conditional from necessarily p to p

1 occurrence in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

41 occurrences in this chapter

Equation form expr-8e35c2cd3bf6641b

qq

Read as: q

Means: q

1 occurrence in this chapter

Equation form expr-900aeb8b11807edf

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

Read as: possibly p is true in modal model M at world w

Means: possibly p is true in modal model M at world w

1 occurrence in this chapter

Equation form expr-909c5f872f90ea72

F∈F\mModel{F} \in \mClass{F}

Read as: frame F belongs to the class of frames F

Means: frame F belongs to the class of frames F

2 occurrences in this chapter

Equation form expr-93b250c2764b3c69

∀y(Q(x,y)→P(y))→P(x)\lforall[y][(\Atom{Q}{x,y} \lif \Atom{P}{y})] \lif \Atom{P}{x}

Read as: if, for every y, Q relates x to y only if P holds of y, then P holds of x

Means: if, for every y, Q relates x to y only if P holds of y, then P holds of x

1 occurrence in this chapter

Equation form expr-94dfe5eb5dff488b

∀u∀v(Ruv→Rvu)\forall u\forall v(Ruv \lif Rvu)

Read as: for every u and v, if R relates u to v, then R relates v to u

Means: for every u and v, if R relates u to v, then R relates v to u

1 occurrence in this chapter

Equation form expr-951df9d014962a47

u∈V(p)⇔v∈V(p)u \in V(p) \Leftrightarrow v \in V(p)

Read as: u belongs to V of p if and only if v belongs to V of p

Means: u belongs to V of p if and only if v belongs to V of p

1 occurrence in this chapter

Equation form expr-95c477cdfc49fba6

PiM′=V(pi)\Assign{P_i}{M'} = V(\Obj p_i)

Read as: the interpretation of P subscript i in structure M prime equals V of p subscript i

Means: the interpretation of P subscript i in structure M prime equals V of p subscript i

1 occurrence in this chapter

Equation form expr-98a38529b6784639

M⊩□◇A[w]\mSat{M}{\Box\Diamond!A}[w]

Read as: necessarily possibly A is true in modal model M at world w

Means: necessarily possibly A is true in modal model M at world w

1 occurrence in this chapter

Equation form expr-98efbabc0f4021a6

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

Read as: necessarily p is true in modal model M at world w

Means: necessarily p is true in modal model M at world w

2 occurrences in this chapter

Equation form expr-9923df073da51869

F′\Struct{F'}

Read as: F prime

Means: F prime

1 occurrence in this chapter

Equation form expr-997e84e88f9f6fa1

[u][u]

Read as: the equivalence class of u

Means: the equivalence class of u

1 occurrence in this chapter

Equation form expr-9a219d06e553d629

F′⊨A′\Sat{F'}{!A'}

Read as: structure F prime satisfies A prime

Means: structure F prime satisfies A prime

1 occurrence in this chapter

Equation form expr-9ae0b14a28573926

M′\mModel{M}'

Read as: M prime

Means: M prime

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: y

2 occurrences in this chapter

Equation form expr-a29ea63167d68f64

M,s⊨Q(x,x)→X(x)\Sat{M}{\Atom{Q}{x,x} \lif \Atom{X}{x}}[s]

Read as: structure M satisfies the conditional from Q relating x to itself to X holding of x, under assignment s

Means: structure M satisfies the conditional from Q relating x to itself to X holding of x, under assignment s

1 occurrence in this chapter

Equation form expr-a365abdce444ccef

Rw3w2Rw_3w_2

Read as: R relates w subscript three to w subscript two

Means: R relates w subscript three to w subscript two

1 occurrence in this chapter

Equation form expr-a38008f15819d3c5

Rw′wRw'w

Read as: R relates w prime to w

Means: R relates w prime to w

1 occurrence in this chapter

Equation form expr-a41871adf38c58cc

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

Read as: p is true in modal model M at world y

Means: p is true in modal model M at world y

1 occurrence in this chapter

Equation form expr-a42da9cbc2de8bee

STx(A)=(STx(B)∨STx(C))\ST_x(\indfrm) = (\ST_x(!B) \lor \ST_x(!C))

Read as: the standard translation at x of the current formula equals the disjunction of the standard translation at x of B and the standard translation at x of C

Means: the standard translation at x of the current formula equals the disjunction of the standard translation at x of B and the standard translation at x of C

1 occurrence in this chapter

Equation form expr-a5ec5fb481a7b768

M⊩□A\mSat{M}{\Box !A}

Read as: necessarily A is true in modal model M

Means: necessarily A is true in modal model M

1 occurrence in this chapter

Equation form expr-a690db8f92d5b67d

V(p)=W∖{w}V(p) = W \setminus \{w\}

Read as: V of p equals W with w removed

Means: V of p equals W with w removed

1 occurrence in this chapter

Equation form expr-a6ab33e2cc3ae09c

Mk⊨Ai\Sat{M_k}{!A_i}

Read as: structure M subscript k satisfies A subscript i

Means: structure M subscript k satisfies A subscript i

1 occurrence in this chapter

Equation form expr-a76b1dd794f8c01c

R=QMR = \Assign{Q}{M}

Read as: R equals the interpretation of Q in structure M

Means: R equals the interpretation of Q in structure M

2 occurrences in this chapter

Equation form expr-a8081325b277f9ef

i≤ki \le k

Read as: i is less than or equal to k

Means: i is less than or equal to k

1 occurrence in this chapter

Equation form expr-a906f986debfac0c

M⊩□p[u]\mSat{M}{\Box p}[u]

Read as: necessarily p is true in modal model M at world u

Means: necessarily p is true in modal model M at world u

1 occurrence in this chapter

Equation form expr-a9b75fc74e37ab87

⟨W,R⟩\tuple{W,R}

Read as: the ordered pair W, R

Means: the ordered pair W, R

1 occurrence in this chapter

Equation form expr-aa6eff998d60c259

∀wRww\forall w Rww

Read as: for every w, R relates w to itself

Means: for every w, R relates w to itself

1 occurrence in this chapter

Equation form expr-aabc6d88cbd006dc

R′R'

Read as: R prime

Means: R prime

2 occurrences in this chapter

Equation form expr-ab06abe3932feaeb

Source-census fragment. Read the complete source formula tr051-reader-composite-math-0001, complete source formula tr051-reader-composite-math-0002. The original fragment is preserved as forensic source evidence, not as a complete reader equation.

2 occurrences in this chapter

Equation form expr-acda45202077c4ee

STx(A)=∀y(Q(x,y)→STy(B))\ST_x(\indfrm) = \lforall[y][(\Atom{Q}{x,y} \lif \ST_y(!B))]

Read as: the standard translation at x of the current formula equals: for every y, if Q relates x to y, then the standard translation at y of B

Means: the standard translation at x of the current formula equals: for every y, if Q relates x to y, then the standard translation at y of B

1 occurrence in this chapter

Equation form expr-b0a0770ba61541fb

STx(A)=¬STx(B)\ST_x(\indfrm) = \lnot \ST_x(!B)

Read as: the standard translation at x of the current formula equals the negation of the standard translation at x of B

Means: the standard translation at x of the current formula equals the negation of the standard translation at x of B

1 occurrence in this chapter

Equation form expr-b0f11570ad8699fd

∀w∃v∀u(Rwu↔u=v)\forall w \exists v \forall u(Rwu \liff \eq[u][v])

Read as: for every w there exists a v such that, for every u, R relates w to u if and only if u equals v

Means: for every w there exists a v such that, for every u, R relates w to u if and only if u equals v

1 occurrence in this chapter

Equation form expr-b15ce62a6c2b00a9

s(x)∈Ws(x) \in W

Read as: s of x belongs to W

Means: s of x belongs to W

2 occurrences in this chapter

Equation form expr-b19b7ef0f6861145

F=⟨W,R⟩\mModel{F} = \tuple{W, R}

Read as: frame F equals the ordered pair W, R

Means: frame F equals the ordered pair W, R

3 occurrences in this chapter

Equation form expr-b19df5c5b1b7d183

M⊩□□p[u]\mSat{M}{\Box \Box p}[u]

Read as: necessarily necessarily p is true in modal model M at world u

Means: necessarily necessarily p is true in modal model M at world u

1 occurrence in this chapter

Equation form expr-b2201d20b09d086f

RuwRuw

Read as: R relates u to w

Means: R relates u to w

2 occurrences in this chapter

Equation form expr-b59c0ca457682eca

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

Read as: p is true in modal model M at world w

Means: p is true in modal model M at world w

4 occurrences in this chapter

Equation form expr-b5b446abb4d0323b

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

Read as: A is true in modal model M at world w

Means: A is true in modal model M at world w

2 occurrences in this chapter

Equation form expr-b99d2e5f37ae7e17

w′w'

Read as: w prime

Means: w prime

4 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 R relates u to v and R relates v to w, then R relates u to w

Means: for every u, v, and w, if R relates u to v and R relates v to w, then R relates u to w

1 occurrence in this chapter

Equation form expr-baacfd9d189243cd

◇A\Diamond !A

Read as: possibly A

Means: possibly A

2 occurrences in this chapter

Equation form expr-bcc649a3fbfdb624

V(q)V(q)

Read as: V of q

Means: V of q

1 occurrence in this chapter

Equation form expr-be2b045bd4f8ebc3

F⊨A\mClass{F} \Entails !A

Read as: A is valid in the class of frames F

Means: A is valid in the class of frames F

2 occurrences in this chapter

Equation form expr-bf94c4cba0afb322

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

Read as: A is true in modal model M at world v

Means: A is true in modal model M at world v

1 occurrence in this chapter

Equation form expr-c1cea27e65d876e1

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

Read as: for every w, u, and v, if R relates w to u and R relates w to v, then u equals v

Means: for every w, u, and v, if R relates w to u and R relates w to v, then u equals v

1 occurrence in this chapter

Equation form expr-c229d8c18cd80a5c

W={w}W = \{w\}

Read as: W is the singleton set containing w

Means: W is the singleton set containing w

1 occurrence in this chapter

Equation form expr-c34f8eb798f704d2

□□p→□p\Box \Box p \lif \Box p

Read as: if necessarily necessarily p, then necessarily p

Means: if necessarily necessarily p, then necessarily p

1 occurrence in this chapter

Equation form expr-c40e112d9ad379d0

RwwRww

Read as: R relates w to itself

Means: R relates w to itself

4 occurrences in this chapter

Equation form expr-c70fd563ab6ac56d

s(x)s(x)

Read as: s of x

Means: s of x

1 occurrence in this chapter

Equation form expr-ca6c5f671cdc3f3a

s(X)s(X)

Read as: s of X

Means: s of X

1 occurrence in this chapter

Equation form expr-cc9a65ac16e76480

w′∈W′w' \in W'

Read as: w prime belongs to W prime

Means: w prime belongs to W prime

1 occurrence in this chapter

Equation form expr-ce69b27f116c06c9

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

Read as: A is true in modal model M prime at world w prime

Means: A is true in modal model M prime at world w prime

1 occurrence in this chapter

Equation form expr-cea711ada9c63af0

⟨W,R⟩\tuple{W, R}

Read as: the ordered pair W, R

Means: the ordered pair W, R

2 occurrences in this chapter

Equation form expr-cef3e6639fe132be

M′\Struct{M'}

Read as: M prime

Means: M prime

1 occurrence in this chapter

Equation form expr-d0084cee1188f92f

M,s⊨∀y(Q(x,y)→Q(x,y))→Q(x,x)\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{Q}{x,y})] \lif \Atom{Q}{x,x}}[s]

Read as: structure M satisfies: if for every y, Q relating x to y implies itself, then Q relates x to itself, under assignment s

Means: structure M satisfies: if for every y, Q relating x to y implies itself, then Q relates x to itself, under assignment s

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: B

Means: B

2 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: M

Means: M

19 occurrences in this chapter

Equation form expr-d1641bdc80ea783c

P1P_1

Read as: P subscript one

Means: P subscript one

1 occurrence in this chapter

Equation form expr-d16b73ce79fc2dfd

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

Read as: B is false in modal model M at world w

Means: B is false in modal model M at world w

1 occurrence in this chapter

Equation form expr-d2da161508eebc66

w∈Ww \in W

Read as: w belongs to W

Means: w belongs to W

8 occurrences in this chapter

Equation form expr-d31acf4a1b7e99f1

STx(A)=Pi(x)\ST_x(\indfrm) = \Atom{P_i}{x}

Read as: the standard translation at x of the current formula equals P subscript i of x

Means: the standard translation at x of the current formula equals P subscript i of x

1 occurrence in this chapter

Equation form expr-d3531780ea511e66

STx(A)=⊥\ST_x(\indfrm) = \lfalse

Read as: the standard translation at x of the current formula equals falsity

Means: the standard translation at x of the current formula equals falsity

1 occurrence in this chapter

Equation form expr-da3c528d15439d91

⟨W,R,V⟩\tuple{W, R, V}

Read as: the ordered triple W, R, V

Means: the ordered triple W, R, V

1 occurrence in this chapter

Equation form expr-da533fcbb7e64233

(Q(a1,a2)∧…∧Q(an−1,an))(\Atom{Q}{a_1,a_2} \land \dots \land \Atom{Q}{a_{n-1},a_{n}})

Read as: the conjunction of Q relating a subscript one to a subscript two, continuing through Q relating a subscript n minus one to a subscript n

Means: the conjunction of Q relating a subscript one to a subscript two, continuing through Q relating a subscript n minus one to a subscript n

1 occurrence in this chapter

Equation form expr-da6dc51fb3f3728c

B\Ax{B}

Read as: axiom B

Means: axiom B

1 occurrence in this chapter

Equation form expr-dabd3aff769f07eb

<<

Read as: the less than relation

Means: the less than relation

3 occurrences in this chapter

Equation form expr-dd7d690b005e955c

M⊨A\Sat{M}{!A}

Read as: structure M satisfies A

Means: structure M satisfies A

2 occurrences in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: V

Means: V

13 occurrences in this chapter

Equation form expr-de64372991421159

An!A_n

Read as: A subscript n

Means: A subscript n

1 occurrence in this chapter

Equation form expr-def094c3b6d5160a

V(q)=∅)V(q) = \emptyset)

Read as: V of q equals the empty set, followed by a closing parenthesis

Means: V of q equals the empty set, followed by a closing parenthesis

1 occurrence in this chapter

Equation form expr-df1591cb2711b1d1

F\mClass{F}

Read as: F

Means: F

8 occurrences in this chapter

Equation form expr-df70b62ace0c6812

□p→□□p\Box p \lif \Box \Box p

Read as: if necessarily p, then necessarily necessarily p

Means: if necessarily p, then necessarily necessarily p

2 occurrences in this chapter

Equation form expr-e0fda14f6a4cfc37

w∈[w]w \in [w]

Read as: w belongs to its equivalence class

Means: w belongs to its equivalence class

1 occurrence in this chapter

Equation form expr-e1b4ffef22fc02b0

M,s⊨∀y(Q(x,y)→X(y))\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})]}[s]

Read as: structure M satisfies that, for every y, if Q relates x to y then X holds of y, under assignment s

Means: structure M satisfies that, for every y, if Q relates x to y then X holds of y, under assignment s

1 occurrence in this chapter

Equation form expr-e2e55dcffa8e0481

∀u∀v(Ruv→∃w(Ruw∧Rwv))\forall u\forall v(Ruv \lif \exists w(Ruw \land Rwv))

Read as: for every u and v, if R relates u to v, then there exists a w such that R relates u to w and R relates w to v

Means: for every u and v, if R relates u to v, then there exists a w such that R relates u to w and R relates w to v

1 occurrence in this chapter

Equation form expr-e3b98a4da31a127d

tt

Read as: t

Means: t

1 occurrence in this chapter

Equation form expr-e42dfadf224f0ff1

{1,…,k}\{1, \dots, k\}

Read as: the set of integers from one through k

Means: the set of integers from one through k

1 occurrence in this chapter

Equation form expr-e54a55ac46202cd8

x∈Wx \in W

Read as: x belongs to W

Means: x belongs to W

1 occurrence in this chapter

Equation form expr-e5bef91e6d1711d5

RvuRvu

Read as: R relates v to u

Means: R relates v to u

3 occurrences in this chapter

Equation form expr-e63589055e7e0cfa

|M′|=W\Domain{M'} = W

Read as: the domain of structure M prime equals W

Means: the domain of structure M prime equals W

1 occurrence in this chapter

Equation form expr-e70e4fb12cb73cf9

⊩A\mSat{{}}{\formula{A}}

Read as: A is true at this world

Means: A is true at this world

1 occurrence in this chapter

Equation form expr-e7eeddc9c332c390

A′!A'

Read as: A prime

Means: A prime

3 occurrences in this chapter

Equation form expr-e83f0b9667e07fd7

PiM′⊆W\Assign{P_i}{M'} \subseteq W

Read as: the interpretation of P subscript i in structure M prime is a subset of W

Means: the interpretation of P subscript i in structure M prime is a subset of W

1 occurrence in this chapter

Equation form expr-e8cbeba8b42e3b53

v∈Wv \in W

Read as: v belongs to W

Means: v belongs to W

1 occurrence in this chapter

Equation form expr-e9fe8ee5ada9c8bf

W′W'

Read as: W prime

Means: W prime

3 occurrences in this chapter

Equation form expr-ebd9d8f61917c1ea

□(□p→p)→□p.row label W\Box(\Box p \lif p) \lif \Box p. \tag{\Ax{W}}

Read as: axiom W, the Loeb formula: if it is necessary that necessarily p implies p, then necessarily p

Means: axiom W, the Loeb formula: if it is necessary that necessarily p implies p, then necessarily p

1 occurrence in this chapter

Equation form expr-ec8f4ca04e3ea525

∀X∀x(∀y(Q(x,y)→X(y))→X(x)).\lforall[X][\lforall[x][(\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})] \lif \Atom{X}{x})]].

Read as: for every set X and every x, if for every y, Q relates x to y only if X holds of y, then X holds of x

Means: for every set X and every x, if for every y, Q relates x to y only if X holds of y, then X holds of x

1 occurrence in this chapter

Equation form expr-ed0aea9b0d314e9a

∀x∀yQ(x,y)\lforall[x][\lforall[y][\Atom{Q}{x,y}]]

Read as: for every x and every y, Q relates x to y

Means: for every x and every y, Q relates x to y

1 occurrence in this chapter

Equation form expr-ed4dc337df9c3390

STx(A)=(STx(B)→STx(C))\ST_x(\indfrm) = (\ST_x(!B) \lif \ST_x(!C))

Read as: the standard translation at x of the current formula equals the conditional from the standard translation at x of B to the standard translation at x of C

Means: the standard translation at x of the current formula equals the conditional from the standard translation at x of B to the standard translation at x of C

1 occurrence in this chapter

Equation form expr-edaa6cae1201c9a9

◇p→□◇p\Diamond p \lif \Box\Diamond p

Read as: if possibly p, then necessarily possibly p

Means: if possibly p, then necessarily possibly p

2 occurrences in this chapter

Equation form expr-ee690c4fd75c8d3a

∀xQ(x,x)\lforall[x][\Atom{Q}{x,x}]

Read as: for every x, Q relates x to itself

Means: for every x, Q relates x to itself

1 occurrence in this chapter

Equation form expr-efeb43a2f191e913

□p→◇p\Box p \lif \Diamond p

Read as: if necessarily p, then possibly p

Means: if necessarily p, then possibly p

1 occurrence in this chapter

Equation form expr-effc6992952633c8

{z:Rxz}\Setabs{z}{Rxz}

Read as: the set of z such that R relates x to z

Means: the set of z such that R relates x to z

1 occurrence in this chapter

Equation form expr-f157f71e0163a897

□\Box

Read as: the necessity operator

Means: the necessity operator

1 occurrence in this chapter

Equation form expr-f1c31a484cb01acc

F=⟨W,R⟩∈F\mModel{F} = \tuple{W, R} \in \mClass{F}

Read as: frame F, equal to the ordered pair W, R, belongs to the class of frames F

Means: frame F, equal to the ordered pair W, R, belongs to the class of frames F

2 occurrences in this chapter

Equation form expr-f20de03e055153df

Q(x,x)\Atom{Q}{x,x}

Read as: Q relates x to itself

Means: Q relates x to itself

1 occurrence in this chapter

Equation form expr-f32ef8758b415fe0

STx(A)=∃y(Q(x,y)∧STy(B))\ST_x(\indfrm) = \lexists[y][(\Atom{Q}{x,y} \land \ST_y(!B))]

Read as: the standard translation at x of the current formula equals: there exists a y such that Q relates x to y and the standard translation at y of B

Means: the standard translation at x of the current formula equals: there exists a y such that Q relates x to y and the standard translation at y of B

1 occurrence in this chapter

Equation form expr-f3f3df2cfbe6a33d

V(p)=∅V(p) = \emptyset

Read as: V of p equals the empty set

Means: V of p equals the empty set

1 occurrence in this chapter

Equation form expr-f484ef27a61988eb

⊩□◇A\mSat{{}}{\Box\Diamond \formula{A}}

Read as: necessarily possibly A is true at this world

Means: necessarily possibly A is true at this world

1 occurrence in this chapter

Equation form expr-f48cc60070f00c24

[z][z]

Read as: the equivalence class of z

Means: the equivalence class of z

1 occurrence in this chapter

Equation form expr-f4dec0cece1e3f6b

◇p→□p\Diamond p \lif \Box p

Read as: if possibly p, then necessarily p

Means: if possibly p, then necessarily p

1 occurrence in this chapter

Equation form expr-f59e5a7770c3fae8

M⊩D[w]\mSat{M}{\Ax{D}}[w]

Read as: axiom D is true in modal model M at world w

Means: axiom D is true in modal model M at world w

1 occurrence in this chapter

Equation form expr-f608299e383a7f01

|F′|=W\Domain{F'} = W

Read as: the domain of structure F prime equals W

Means: the domain of structure F prime equals W

1 occurrence in this chapter

Equation form expr-f622b1978ee95aca

Γ={F,A1,A2,…}.\Gamma = \{!F, !A_1, !A_2, \dots\}.

Read as: Gamma equals the set containing F and A subscript one, A subscript two, and so on

Means: Gamma equals the set containing F and A subscript one, A subscript two, and so on

1 occurrence in this chapter

Equation form expr-f6506acbcb854110

|M|=W\Domain{M} = W

Read as: the domain of structure M equals W

Means: the domain of structure M equals W

3 occurrences in this chapter

Equation form expr-f6b9f8bdeb0b2c0d

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

Read as: p is true in modal model M at world v

Means: p is true in modal model M at world v

1 occurrence in this chapter

Equation form expr-f87365f9f2969ebc

□((p∧□p)→q)∨□((q∧□q)→p)\begin{array}{@{}l@{}} \Box ((p \land \Box p) \lif q) \lor {} \\ \qquad \Box ((q \land \Box q) \lif p) \end{array}

Read as: either it is necessary that, if p and necessarily p, then q; or it is necessary that, if q and necessarily q, then p

Means: either it is necessary that, if p and necessarily p, then q; or it is necessary that, if q and necessarily q, then p

1 occurrence in this chapter

Equation form expr-f87a549f62a7a792

□A\Box !A

Read as: necessarily A

Means: necessarily A

2 occurrences in this chapter

Equation form expr-f8dcd48388f1ed21

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

Read as: w belongs to V of p

Means: w belongs to V of p

2 occurrences in this chapter

Equation form expr-f9c6cbd6245f9917

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

Read as: modal model M equals the ordered triple W, R, V

Means: modal model M equals the ordered triple W, R, V

8 occurrences in this chapter

Equation form expr-f9e469296b427af3

□p→p\Box p \lif p

Read as: if necessarily p, then p

Means: if necessarily p, then p

8 occurrences in this chapter

Equation form expr-fcb5f40df9be6bae

WW

Read as: W

Means: W

9 occurrences in this chapter

Equation form expr-fda3b7f4363919dd

F⊨A\mModel{F} \Entails !A

Read as: A is valid in frame F

Means: A is valid in frame F

5 occurrences in this chapter

Equation form expr-fda578f0ffa059b0

w∉V(p)w \notin V(p)

Read as: w does not belong to V of p

Means: w does not belong to V of p

1 occurrence in this chapter

Five sound modal correspondence schemas

If a model accessibility relation has the property in the first correspondence table, then every substitution instance of the modal schema in the corresponding row is true in that model.

Source

Outer table of five classical correspondence facts

The outer table contains the source caption and an inner row-and-column table. The inner table is the sole listener structure authority, avoiding duplicate readings of the same twelve formulas.

Source

Five classical correspondence facts

Five source-ordered rows pair seriality, reflexivity, symmetry, transitivity, and euclideanness with their defining relation conditions and the modal schemas labelled D, T, B, four, and five.

Source

Exercise completing the five soundness cases

Complete the proof of the theorem on five sound correspondence schemas. The source proves only the symmetry case; this edition does not add the omitted proofs.

Source

Figure containing the symmetry argument graph

The outer figure contains the caption and an enclosed two-world accessibility diagram. Its inner diagram is the sole structural listener authority.

Source

Two-world graph for the symmetry argument

World w is labelled with A and necessarily possibly A true. World w prime is labelled with possibly A true. One accessibility arrow goes from w to w prime and a second returns from w prime to w; no loops or other edges are printed.

Source

Two-world model with every T instance true

The proposition assumes two worlds connected in both directions and identical propositional valuations. It claims every formula has the same truth value at the two worlds and hence every T instance is true. Its subsequent claim that the model is irreflexive needs the separately preserved source caveat because the stated hypotheses do not exclude loops.

Source

Exercise proving the two-world model claims

Prove the two claims in the preceding proposition, including the induction on formulas. No proof is supplied.

Source

Outer table of five additional correspondence facts

The outer table contains the source caption and an inner row-and-column table. The inner table is the sole listener structure authority, avoiding duplicate readings of the same fourteen formulas.

Source

Five additional correspondence facts

Five source-ordered rows pair partial functionality, functionality, weak density, weak connectedness, and weak directedness with their relation conditions and corresponding modal formulas. The split weak-connected and weak-directed conditions remain joined in their row descriptions.

Source

Exercise proving the five additional soundness facts

Show that each relation property in the second table makes every instance of its corresponding modal formula true in the model. No solution is supplied.

Source

Definition of a modal frame and based model

A frame is an ordered pair of a nonempty set of worlds and a binary accessibility relation. A model is based on that frame exactly when it adds a valuation to the same worlds and relation.

Source

Validity in a frame and in a class of frames

A formula is valid in a frame when it is true in every model based on that frame. It is valid in a class of frames when it is valid in every member frame.

Source

Definition of modal frame definability

A modal formula defines a class of frames exactly when it is valid in all and only the frames belonging to that class.

Source

Full correspondence theorem for D, T, B, four, and five

If one of the five modal schemas in the first table is valid in a frame, the accessibility relation has the corresponding property. The proof treats seriality, reflexivity, symmetry, transitivity, and euclideanness in source order.

Source

Axiom D implies seriality even at model level

Any model in which axiom D is true is serial; unlike the other displayed correspondence results, this statement does not require quantification over all valuations on a frame.

Source

Five modal formulas define their frame classes

Each modal schema in the first table defines exactly the class of frames having the paired accessibility property, by combining the soundness theorem with the full correspondence theorem.

Source

Exercise proving converse correspondence for the second table

For each additional relation property, start with a frame lacking it and choose a valuation making the paired modal formula false somewhere. The exercise remains unsolved.

Source

Five implications among accessibility properties

The proposition records reflexive implies serial; under symmetry, transitive is equivalent to euclidean; symmetric or euclidean implies weakly directed; euclidean implies weakly connected; and functional implies serial.

Source

Exercise proving the five relation facts

Prove the preceding proposition about implications among accessibility properties. No proof is supplied.

Source

Definition of a first-order definable frame class

A frame class is first-order definable when a sentence with one binary predicate Q holds in the corresponding structure exactly for the frames in the class, with the structure domain as worlds and Q interpreted as accessibility.

Source

Loeb formula, axiom W

The displayed formula is the conditional from necessarily, if necessarily p then p, to necessarily p. The source states that it defines transitive converse well-founded frames.

Source

Definitions of equivalence and universal relations

An equivalence relation is reflexive, symmetric, and transitive. A universal relation relates every ordered pair of worlds.

Source

Four equivalent characterizations of equivalence relations

The proposition lists equivalence; reflexive plus euclidean; serial plus symmetric plus euclidean; and serial plus symmetric plus transitive. Its source proof is only the word Exercise and is not expanded here.

Source

Exercise proving the equivalence-relation characterizations

Prove five stated implications among symmetry, transitivity, euclideanness, reflexivity, and seriality, then explain why they establish equivalence. No solution is supplied.

Source

Equivalence classes partition the world set

For an equivalence relation, each world belongs to its own class, the relation is universal within each class, and all equivalence classes form mutually exclusive and jointly exhaustive subsets of W.

Source

Universal and equivalence frames have the same modal logic

A modal formula is valid on all equivalence frames exactly when it is valid on all universal frames. The proof restricts a countermodel to the equivalence class of the world where the formula fails.

Source

Figure of a partition into equivalence classes

The outer figure contains the caption and an enclosed partition diagram. The shaded area represents W prime, the equivalence class of w; the inner diagram is the sole structural listener authority.

Source

Partition diagram with four equivalence classes

An outer rounded rectangle represents W. Two curved boundaries divide it into regions labelled the equivalence classes of w, u, v, and z. The shaded region represents W prime, equal to the class of w. This is not an accessibility graph and prints no arrows or valuations.

Source

Inductive definition of the standard translation

The selected source clauses translate falsity, a propositional variable, negation, conjunction, disjunction, conditional, necessity, and possibility. Necessity becomes a universal Q condition and possibility becomes an existential Q condition. Profile-excluded clauses are not invented.

Source

Truth preservation by the standard translation

For corresponding modal model M, first-order structure M prime, world w, and assignment s sending x to w, modal A is true at w exactly when M prime satisfies its standard translation under s. The source proof is induction on A.

Source

Monadic second-order sentence for modal frame validity

Universally quantify one set variable for every propositional predicate in the standard translation and every world variable x, then substitute those set variables for the predicates. A modal formula is valid in the frame exactly when the corresponding first-order frame structure satisfies this second-order sentence.

Source

Definition of a monadic second-order definable frame class

A frame class is second-order definable when a sentence with one binary accessibility predicate and only monadic set quantifiers holds in the corresponding structure exactly for the frames in the class.

Source

Modal definability implies monadic second-order definability

Every class of frames defined by a modal formula has a corresponding class of accessibility relations defined by the monadic second-order sentence constructed in the preceding proposition.

Source

Cross-reference reference-000950

the table of five classical correspondence facts

Source occurrence

Cross-reference reference-000951

the two-world figure illustrating the symmetry argument

Source occurrence

Cross-reference reference-000952

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000953

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000954

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000955

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000956

the proposition about the two-world model in which every T instance is true

Source occurrence

Cross-reference reference-000957

the table of five additional correspondence facts

Source occurrence

Cross-reference reference-000958

the table of five additional correspondence facts

Source occurrence

Cross-reference reference-000959

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000960

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000961

the table of five classical correspondence facts

Source occurrence

Cross-reference reference-000962

the table of five classical correspondence facts

Source occurrence

Cross-reference reference-000963

the theorem that five accessibility properties guarantee their corresponding modal schemas

Source occurrence

Cross-reference reference-000964

the full correspondence theorem for D, T, B, four, and five

Source occurrence

Cross-reference reference-000965

the table of five additional correspondence facts

Source occurrence

Cross-reference reference-000966

the full correspondence theorem for D, T, B, four, and five

Source occurrence

Cross-reference reference-000967

the proposition on five implications among accessibility properties

Source occurrence

Cross-reference reference-000968

the proposition giving four equivalent characterizations of equivalence relations

Source occurrence

Cross-reference reference-000969

the proposition giving four equivalent characterizations of equivalence relations

Source occurrence

Cross-reference reference-000970

the later proposition listing four equivalent axiomatizations of S five

Source occurrence

Cross-reference reference-000971

the figure partitioning W into equivalence classes

Source occurrence

Cross-reference reference-000972

the proposition that the standard translation preserves truth at a world

Source occurrence

Source disclosures

Complete source formula tr051-reader-composite-math-0001

∀w∀u∀v((Rwu∧Rwv)→(Ruv∨u=v∨Rvu))\forall w \forall u \forall v ((Rwu \land Rwv) \lif (Ruv \lor u=v \lor Rvu))

Read as: For every w, u, and v, if R relates w to u and R relates w to v, then either R relates u to v, u equals v, or R relates v to u.

Read in context source

Complete source formula tr051-reader-composite-math-0002

∀w∀u∀v((Rwu∧Rwv)→∃t(Rut∧Rvt))\forall w \forall u \forall v ((Rwu \land Rwv) \lif \exists t (Rut \land Rvt))

Read as: For every w, u, and v, if R relates w to u and R relates w to v, then there exists t such that R relates u to t and R relates v to t.

Read in context source

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

D\Ax{D}

Read as: axiom D

Read in context source

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

T\Ax{T}

Read as: axiom T

Read in context source

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

B\Ax{B}

Read as: axiom B

Read in context source

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

4\Ax{4}

Read as: axiom four

Read in context source

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

5\Ax{5}

Read as: axiom five

Read in context source

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

L\Ax{L}

Read as: axiom L

Read in context source

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

G\Ax{G}

Read as: axiom G

Read in context source

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

A≡⊥!A \ident \lfalse

Read as: Case: A is the falsity constant.

Read in context source

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

A≡pi!A \ident \Obj p_i

Read as: Case: A is the propositional variable p subscript i.

Read in context source

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

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

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

Read in context source

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

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 tr051-source-macro-0005

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 tr051-source-macro-0006

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 tr051-source-macro-0007

A≡□B!A \ident \Box !B

Read as: Case: A is necessarily B.

Read in context source

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

A≡◇B!A \ident \Diamond !B

Read as: Case: A is possibly B.

Read in context source

Ordered structures

Five classical correspondence facts

Structure: table.

Five classical correspondence facts. Header: if R has the named property, then the paired formula is true in M. Serial row. Relation condition: for every u there exists a v such that R relates u to v. Modal schema: if necessarily p, then possibly p, labelled axiom D. Reflexive row. Relation condition: for every w, R relates w to itself. Modal schema: if necessarily p, then p, labelled axiom T. Symmetric row. The source first prints the modal schema if p, then necessarily possibly p, labelled axiom B, then on the following line its relation condition for every u and v, if R relates u to v, then R relates v to u. Transitive row. The source first prints the modal schema if necessarily p, then necessarily necessarily p, labelled axiom four, then its relation condition for every u, v, and w, if R relates u to v and R relates v to w, then R relates u to w. Euclidean row. The source first prints the modal schema if possibly p, then necessarily possibly p, labelled axiom five, then its relation condition for every w, u, and v, if R relates w to u and R relates w to v, then R relates u to v. End table.

Read the source-bound structure in context

Two-world graph for the symmetry argument

Structure: diagram tikz.

Two-world accessibility graph for symmetry. The first node annotations, in source order, are A is true at this world and necessarily possibly A is true at this world. That node is world w. The second node annotation is possibly A is true at this world. That node is world w prime. The first directed arrow goes from w to w prime. The second directed arrow goes from w prime back to w. No loops, additional worlds, additional valuations, or other accessibility arrows are printed. End diagram.

Read the source-bound structure in context

Five additional correspondence facts

Structure: table.

Five additional correspondence facts. Header: if R has the named property, then the paired formula is true in M. Partially functional row. Modal schema: if possibly p, then necessarily p. Relation condition: for every w, u, and v, if R relates w to u and R relates w to v, then u equals v. Functional row. Relation condition: for every w there exists a v such that, for every u, R relates w to u if and only if u equals v. Modal schema: possibly p if and only if necessarily p. Weakly dense row. Modal schema: if necessarily necessarily p, then necessarily p. Relation condition: for every u and v, if R relates u to v, then there exists a w such that R relates u to w and R relates w to v. Weakly connected row. Modal schema: either it is necessary that, if p and necessarily p, then q; or it is necessary that, if q and necessarily q, then p, labelled axiom L. Relation condition: For every w, u, and v, if R relates w to u and R relates w to v, then either R relates u to v, u equals v, or R relates v to u.. Weakly directed row. Modal schema: if possibly necessarily p, then necessarily possibly p, labelled axiom G. Relation condition: For every w, u, and v, if R relates w to u and R relates w to v, then there exists t such that R relates u to t and R relates v to t.. End table.

Read the source-bound structure in context

Partition diagram with four equivalence classes

Structure: diagram tikz.

Equivalence-class partition diagram. Four region labels appear in source order: the equivalence class of w, the equivalence class of u, the equivalence class of v, and the equivalence class of z. An outer rounded rectangle represents W. Two curved boundaries divide it into the four labelled regions. The gray shaded region represents W prime, equal to the equivalence class of w, as stated immediately before the figure. This is a partition picture, not a Kripke accessibility graph: it prints no directed edges, relation labels, worlds inside the classes, or valuations. End diagram.

Read the source-bound structure in context