Normal Modal Logics

Filtrations and Decidability

Equation form expr-038966de9f6b9a90

[2][2]

Read as: the equivalence class of two

Means: the equivalence class of two

3 occurrences in this chapter

Equation form expr-03bad99383639db0

◇A∈Γ\Diamond !A \in \Gamma

Read as: possibly formula A belongs to Gamma

Means: possibly formula A belongs to Gamma

2 occurrences in this chapter

Equation form expr-03d04c9b1863399f

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

Read as: world u belongs to valuation V applied to p

Means: world u belongs to valuation V applied to p

2 occurrences in this chapter

Equation form expr-03fe3eb3642ed5a3

{p,□p,□p→p}\{p, \Box p, \Box p \lif p\}

Read as: the set containing p, necessarily p, and the conditional from necessarily p to p

Means: the set containing p, necessarily p, and the conditional from necessarily p to p

1 occurrence in this chapter

Equation form expr-055d5ee422435b80

R*R^*

Read as: accessibility relation R star

Means: accessibility relation R star

15 occurrences in this chapter

Equation form expr-0588ffe69d967fd7

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

Read as: necessarily formula B is true at world w in model M

Means: necessarily formula B is true at world w in model M

2 occurrences in this chapter

Equation form expr-066d8a7d36bb1f0b

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

Read as: formula C is true at the equivalence class of world w in model M star

Means: formula C is true at the equivalence class of world w in model M star

2 occurrences in this chapter

Equation form expr-0712b486b3e6cec7

C2C_2

Read as: condition C sub two

Means: condition C sub two

1 occurrence in this chapter

Equation form expr-080a9ed428559ef6

[1][1]

Read as: the equivalence class of one

Means: the equivalence class of one

3 occurrences in this chapter

Equation form expr-080d0f3a64123b59

u≡vu \equiv v

Read as: world u is equivalent to world v

Means: world u is equivalent to world v

3 occurrences in this chapter

Equation form expr-08eba634b321bf4d

C2(u,v)C_2(u, v)

Read as: condition C sub two of world u and world v

Means: condition C sub two of world u and world v

1 occurrence in this chapter

Equation form expr-09e32f43227dc6b2

□p\Box p

Read as: necessarily p

Means: necessarily p

6 occurrences in this chapter

Equation form expr-09e9a7ba3a516fc6

R*[w][v]R^*[w][v]

Read as: the equivalence class of world v is accessible from the equivalence class of world w under accessibility relation R star

Means: the equivalence class of world v is accessible from the equivalence class of world w under accessibility relation R star

2 occurrences in this chapter

Equation form expr-0ab54ed881cc46b0

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

Read as: formula A is true at the equivalence class of world w in model M star

Means: formula A is true at the equivalence class of world w in model M star

4 occurrences in this chapter

Equation form expr-0bfe935e70c321c7

uu

Read as: world u

Means: world u

15 occurrences in this chapter

Equation form expr-0e4e11f4c4e2b26e

◇◇A∈Γ\Diamond\Diamond!A \in \Gamma

Read as: possibly possibly formula A belongs to Gamma

Means: possibly possibly formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-13715f6c8b48ed1b

010010

Read as: zero one zero

Means: zero one zero

1 occurrence in this chapter

Equation form expr-139a01ed8789adde

C1(u,v)⇔C2(v,u)C_1(u,v) \Leftrightarrow C_2(v,u)

Read as: condition C sub one of world u and world v if and only if condition C sub two of world v and world u

Means: condition C sub one of world u and world v if and only if condition C sub two of world v and world u

1 occurrence in this chapter

Equation form expr-141a788a845573ec

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

Read as: the current induction-case formula is true at world w in model M

Means: the current induction-case formula is true at world w in model M

7 occurrences in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

8 occurrences in this chapter

Equation form expr-1568038f8354002c

[w5][w_5]

Read as: the equivalence class of world w sub five

Means: the equivalence class of world w sub five

1 occurrence in this chapter

Equation form expr-16380bff1169f800

u′≡uu' \equiv u

Read as: u prime is equivalent to world u

Means: u prime is equivalent to world u

1 occurrence in this chapter

Equation form expr-1a53000974926187

V(p)V(p)

Read as: valuation V applied to p

Means: valuation V applied to p

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

6 occurrences in this chapter

Equation form expr-1b6d2b1db965771b

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

Read as: formula A is true throughout model M star

Means: formula A is true throughout model M star

1 occurrence in this chapter

Equation form expr-1c045be285f46cfe

W×WW \times W

Read as: the Cartesian product of world set W with itself

Means: the Cartesian product of world set W with itself

1 occurrence in this chapter

Equation form expr-1c4164f7d3bd0bf7

{⟨[1],[2]⟩,⟨[2],[1]⟩} and {⟨[1],[2]⟩,⟨[2],[1]⟩,⟨[2],[2]⟩}.\{\tuple{[1],[2]}, \tuple{[2],[1]}\} \text{ and } \{\tuple{[1],[2]}, \tuple{[2],[1]}, \tuple{[2],[2]}\}.

Read as: Two accessibility relations. The first contains the ordered pair from class one to class two and the ordered pair from class two to class one. The second contains those two pairs and the loop from class two to itself. End relations.

Means: Two accessibility relations. The first contains the ordered pair from class one to class two and the ordered pair from class two to class one. The second contains those two pairs and the loop from class two to itself. End relations.

1 occurrence in this chapter

Equation form expr-207886cac1aa18fa

u≡wu \equiv w

Read as: world u is equivalent to world w

Means: world u is equivalent to world w

1 occurrence in this chapter

Equation form expr-2224dc04be4dd865

u∈[u]u \in [u]

Read as: world u belongs to the equivalence class of world u

Means: world u belongs to the equivalence class of world u

1 occurrence in this chapter

Equation form expr-23e451314400b450

w≡vw \equiv v

Read as: world w is equivalent to world v

Means: world w is equivalent to world v

3 occurrences in this chapter

Equation form expr-24fabe70838b1112

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

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

Means: possibly formula A is true at world v in model M

1 occurrence in this chapter

Equation form expr-258f31d0f70c1bec

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

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

Means: p is true at world u in model M

1 occurrence in this chapter

Equation form expr-27155c86d3e3fb44

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

Read as: formula B is false at the equivalence class of world w in model M star

Means: formula B is false at the equivalence class of world w in model M star

3 occurrences in this chapter

Equation form expr-280f25651d3820e4

V*(p)V^*(p)

Read as: valuation V star applied to p

Means: valuation V star applied to p

1 occurrence in this chapter

Equation form expr-29eef005e300fa48

u≡vif and only if ∀A∈Γ:M⊩A[u]⇔M⊩A[v].u \equiv v \quad \text{if and only if } \quad \forall !A \in \Gamma : \mSat{M}{!A}[u] \Leftrightarrow \mSat{M}{!A}[v].

Read as: World u is equivalent to world v if and only if, for every formula A in Gamma, A is true at u in model M exactly when A is true at v in model M.

Means: World u is equivalent to world v if and only if, for every formula A in Gamma, A is true at u in model M exactly when A is true at v in model M.

1 occurrence in this chapter

Equation form expr-2ac9a6746aca543a

000000

Read as: zero zero zero

Means: zero zero zero

1 occurrence in this chapter

Equation form expr-2bb2ce9e4af1fe32

p∈Γp \in \Gamma

Read as: p belongs to Gamma

Means: p belongs to Gamma

1 occurrence in this chapter

Equation form expr-2d17acc9ea4f6b0f

σ′=σ1\sigma' = \sigma 1

Read as: sigma prime equals the binary sequence sigma followed by one

Means: sigma prime equals the binary sequence sigma followed by one

1 occurrence in this chapter

Equation form expr-2ee48382c60ed8c9

V*(p)={[u]:u∈V(p)}V^*(p) = \Setabs{[u]}{u \in V(p)}

Read as: valuation V star assigns p to the equivalence classes of worlds u that valuation V assigns p

Means: valuation V star assigns p to the equivalence classes of worlds u that valuation V assigns p

1 occurrence in this chapter

Equation form expr-3106fac3e3c8f992

w2w_2

Read as: world w sub two

Means: world w sub two

3 occurrences in this chapter

Equation form expr-316470936f695f4f

C3(u,v)C_3(u,v)

Read as: condition C sub three of world u and world v

Means: condition C sub three of world u and world v

1 occurrence in this chapter

Equation form expr-31a145ebcc447caa

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

Read as: formula B is true at world v in model M

Means: formula B is true at world v in model M

2 occurrences in this chapter

Equation form expr-320b86ff9ed5a520

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

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

Means: necessarily formula A is true at world u in model M

1 occurrence in this chapter

Equation form expr-33c8f5d66fc898d7

W={0σ:σ∈B*}W = \Setabs{0\sigma}{\sigma \in \Bin^*}

Read as: W is the set of binary sequences zero sigma, where sigma is a finite binary sequence

Means: W is the set of binary sequences zero sigma, where sigma is a finite binary sequence

1 occurrence in this chapter

Equation form expr-347e4725a398d1df

C4(u,v)C_4(u,v)

Read as: condition C sub four of world u and world v

Means: condition C sub four of world u and world v

1 occurrence in this chapter

Equation form expr-34c4a8665075bdc1

RuvRuv

Read as: world v is accessible from world u under accessibility relation R

Means: world v is accessible from world u under accessibility relation R

11 occurrences in this chapter

Equation form expr-34e363f47cda9cba

2n22^{n^2}

Read as: two raised to the power n squared

Means: two raised to the power n squared

1 occurrence in this chapter

Equation form expr-354c64b64061143e

[v][v]

Read as: the equivalence class of world v

Means: the equivalence class of world v

2 occurrences in this chapter

Equation form expr-36b71994cff4b078

[u]=[v][u] = [v]

Read as: the equivalence class of world u equals the equivalence class of world v

Means: the equivalence class of world u equals the equivalence class of world v

1 occurrence in this chapter

Equation form expr-37950f59ecb0b6a8

V*(p)={[w]:M⊩p[w]}V^*(p) = \Setabs{[w]}{\mSat{M}{p}[w]}

Read as: valuation V star assigns p to the equivalence classes of worlds w at which p is true in model M

Means: valuation V star assigns p to the equivalence classes of worlds w at which p is true in model M

1 occurrence in this chapter

Equation form expr-3abc316ec8c5f671

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

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

Means: necessarily p is true at world one in model M

1 occurrence in this chapter

Equation form expr-3b524d8b1a1063d9

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

Read as: formula C is true at world w in model M

Means: formula C is true at world w in model M

2 occurrences in this chapter

Equation form expr-3c198ca66ccccccb

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

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

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

4 occurrences in this chapter

Equation form expr-3f2eed6a9c10a54b

W*={[1],[2]}W^* = \{ [1], [2] \}

Read as: world set W star is the set containing equivalence class one and equivalence class two

Means: world set W star is the set containing equivalence class one and equivalence class two

1 occurrence in this chapter

Equation form expr-3fdd6b00dce0bb38

Ci(u,v)C_i(u,v)

Read as: condition C sub i of world u and world v

Means: condition C sub i of world u and world v

1 occurrence in this chapter

Equation form expr-400fd61b54ebaaac

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

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

Means: possibly possibly formula A is true at world u in model M

1 occurrence in this chapter

Equation form expr-4096ab439decf39e

V(p)={σ0:σ∈B*}V(p) = \Setabs{\sigma 0}{\sigma \in \Bin^*}

Read as: valuation V assigns p to exactly the binary sequences sigma zero, where sigma is finite

Means: valuation V assigns p to exactly the binary sequences sigma zero, where sigma is finite

1 occurrence in this chapter

Equation form expr-438757f12dd8c3fc

w1w_1

Read as: world w sub one

Means: world w sub one

2 occurrences in this chapter

Equation form expr-45beba8ab41d3022

[w]∈V*[w] \in V^*

Read as: the equivalence class of world w belongs to valuation V star

Means: the equivalence class of world w belongs to valuation V star

1 occurrence in this chapter

Equation form expr-46bdd2669abea099

C1(u,v)C_1(u,v)

Read as: condition C sub one of world u and world v

Means: condition C sub one of world u and world v

11 occurrences in this chapter

Equation form expr-49d4940ec77cae94

℘(Γ)\Pow{\Gamma}

Read as: the power set of Gamma

Means: the power set of Gamma

1 occurrence in this chapter

Equation form expr-49ef8330b7c2fe32

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

Read as: model M is the ordered triple of world set W, accessibility relation R, and valuation V

Means: model M is the ordered triple of world set W, accessibility relation R, and valuation V

1 occurrence in this chapter

Equation form expr-4b227777d4dd1fc6

44

Read as: four

Means: four

1 occurrence in this chapter

Equation form expr-4b270ddb72d4b503

V*V^*

Read as: V star

Means: V star

4 occurrences in this chapter

Equation form expr-4c94485e0c21ae6c

vv

Read as: world v

Means: world v

22 occurrences in this chapter

Equation form expr-4e07408562bedb8b

33

Read as: three

Means: three

1 occurrence in this chapter

Equation form expr-4e7142ad42e2513e

v′v'

Read as: v prime

Means: v prime

1 occurrence in this chapter

Equation form expr-4f9a5d8ed864e09d

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

Read as: p is false at world one in model M

Means: p is false at world one in model M

1 occurrence in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: world w

Means: world w

14 occurrences in this chapter

Equation form expr-5348ee86c92f99c3

R*[u][v]if and only if∃u′∈[u]∃v′∈[v]:Ru′v′.R^*[u][v] \quad \text{if and only if} \quad \exists u'\in [u] \; \exists v' \in [v] : Ru'v'.

Read as: Class v is accessible from class u under R star if and only if there are representatives u prime in class u and v prime in class v such that v prime is accessible from u prime under R.

Means: Class v is accessible from class u under R star if and only if there are representatives u prime in class u and v prime in class v such that v prime is accessible from u prime under R.

1 occurrence in this chapter

Equation form expr-5773df195f6e6e6e

C2(u,v)C_2(u,v)

Read as: condition C sub two of world u and world v

Means: condition C sub two of world u and world v

3 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

52 occurrences in this chapter

Equation form expr-57e35902add95c7c

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

Read as: model M is the ordered triple of world set W, accessibility relation R, and valuation V

Means: model M is the ordered triple of world set W, accessibility relation R, and valuation V

1 occurrence in this chapter

Equation form expr-59f62e9e83f7cc60

[w4][w_4]

Read as: the equivalence class of world w sub four

Means: the equivalence class of world w sub four

2 occurrences in this chapter

Equation form expr-5a24681967d744de

[w]={v:v≡w}.[w] = \Setabs{v}{v \equiv w}.

Read as: the equivalence class of w is the set of all v equivalent to w

Means: the equivalence class of w is the set of all v equivalent to w

1 occurrence in this chapter

Equation form expr-5a80aefdedf617d0

v∈V(p)v \in V(p)

Read as: world v belongs to valuation V applied to p

Means: world v belongs to valuation V applied to p

1 occurrence in this chapter

Equation form expr-5af65f330196b4e6

U\mClass{U}

Read as: class U of universal models

Means: class U of universal models

2 occurrences in this chapter

Equation form expr-5c57d05d160fdce1

u∈[w]u \in [w]

Read as: world u belongs to the equivalence class of world w

Means: world u belongs to the equivalence class of world w

1 occurrence in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

3 occurrences in this chapter

Equation form expr-600b87b90b71c069

□A∈Γ\Box!A \in \Gamma

Read as: necessarily formula A belongs to Gamma

Means: necessarily formula A belongs to Gamma

8 occurrences in this chapter

Equation form expr-6061a5591edaa80a

5◇\Ax{5_\Diamond}

Read as: the diamond form of axiom five

Means: the diamond form of axiom five

1 occurrence in this chapter

Equation form expr-619c6509406bf4f8

⊮□p\mSat/{{}}{\Box p}

Read as: necessarily p is false at this displayed world

Means: necessarily p is false at this displayed world

4 occurrences in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: m

1 occurrence in this chapter

Equation form expr-63713d1f6d4dc4ed

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

Read as: formula A is true throughout model M

Means: formula A is true throughout model M

1 occurrence in this chapter

Equation form expr-63e9f67df251e4ad

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

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

Means: formula A is true at world w in model M star

1 occurrence in this chapter

Equation form expr-6492a053b86c0a8f

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

Read as: not formula B is true at world w in model M

Means: not formula B is true at world w in model M

1 occurrence in this chapter

Equation form expr-6645763562c410b5

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

Read as: model M star is the ordered triple of world set W star, accessibility relation R star, and valuation V star

Means: model M star is the ordered triple of world set W star, accessibility relation R star, and valuation V star

3 occurrences in this chapter

Equation form expr-66f3dc9d2f9a9955

□A∈Γ\Box!A \in\Gamma

Read as: necessarily formula A belongs to Gamma

Means: necessarily formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-67cbbf7fc57cc7f6

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

Read as: model M is the ordered triple of world set W, accessibility relation R, and valuation V

Means: model M is the ordered triple of world set W, accessibility relation R, and valuation V

2 occurrences in this chapter

Equation form expr-68ca3577d8206a28

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

Read as: formula A is true at v prime in model M

Means: formula A is true at v prime in model M

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: one

4 occurrences in this chapter

Equation form expr-6e41eea2e09f5fa7

V*(p)={[2]}V^*(p) = \{[2]\}

Read as: valuation V star applied to p equals the set containing the equivalence class of two

Means: valuation V star applied to p equals the set containing the equivalence class of two

1 occurrence in this chapter

Equation form expr-70133718bdd537a3

V(p)={2n:n∈ℕ}V(p) = \Setabs{2n}{n \in \Nat}

Read as: valuation V assigns p to the even natural numbers two times n

Means: valuation V assigns p to the even natural numbers two times n

1 occurrence in this chapter

Equation form expr-71cf265fa03b922a

M*⊩□B[[w]]\mSat{M^*}{\Box !B}[{[w]}]

Read as: necessarily formula B is true at the equivalence class of world w in model M star

Means: necessarily formula B is true at the equivalence class of world w in model M star

1 occurrence in this chapter

Equation form expr-71e94b6bb8727e01

R*[u][v]R^*[u][v]

Read as: the equivalence class of world v is accessible from the equivalence class of world u under accessibility relation R star

Means: the equivalence class of world v is accessible from the equivalence class of world u under accessibility relation R star

18 occurrences in this chapter

Equation form expr-7257e8eaa3fb3c6a

R*[2][3]R^*[2][3]

Read as: the equivalence class of three is accessible from the equivalence class of two under accessibility relation R star

Means: the equivalence class of three is accessible from the equivalence class of two under accessibility relation R star

1 occurrence in this chapter

Equation form expr-73640a868d09b401

[w2][w_2]

Read as: the equivalence class of world w sub two

Means: the equivalence class of world w sub two

2 occurrences in this chapter

Equation form expr-73ffecb5618fb3cc

W*W^*

Read as: world set W star

Means: world set W star

8 occurrences in this chapter

Equation form expr-744da9ee0a52f2e3

C1(u,v)∧C3(u,v)C_1(u, v) \land C_3(u,v)

Read as: condition C sub one of world u and world v and condition C sub three of world u and world v

Means: condition C sub one of world u and world v and condition C sub three of world u and world v

1 occurrence in this chapter

Equation form expr-75df5e48dc22d682

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

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

Means: necessarily formula A is true at world v in model M

5 occurrences in this chapter

Equation form expr-7905b07cde52d70f

V(q)={σ1:σ∈B*∖{1}}V(q) = \Setabs{\sigma 1}{\sigma \in \Bin^* \setminus \{1\}}

Read as: valuation V assigns q to exactly the binary sequences sigma one, where sigma is finite and is not the one-symbol sequence one

Means: valuation V assigns q to exactly the binary sequences sigma one, where sigma is finite and is not the one-symbol sequence one

1 occurrence in this chapter

Equation form expr-79a73397590ea1a9

u,v∈Wu,v \in W

Read as: worlds u and v belong to world set W

Means: worlds u and v belong to world set W

1 occurrence in this chapter

Equation form expr-79a9f9af64f1301e

v∈[v]v \in [v]

Read as: world v belongs to the equivalence class of world v

Means: world v belongs to the equivalence class of world v

1 occurrence in this chapter

Equation form expr-7a3e6b16cb75f48f

001001

Read as: zero zero one

Means: zero zero one

1 occurrence in this chapter

Equation form expr-7b5c6734ef37e127

C1(u,v)∧C2(u,v)∧C3(u,v)∧C4(u,v)C_1(u, v) \land C_2(u,v) \land C_3(u,v) \land C_4(u,v)

Read as: condition C sub one of world u and world v and condition C sub two of world u and world v and condition C sub three of world u and world v and condition C sub four of world u and world v

Means: condition C sub one of world u and world v and condition C sub two of world u and world v and condition C sub three of world u and world v and condition C sub four of world u and world v

1 occurrence in this chapter

Equation form expr-7b756202224c4f95

R*[1][2]R^*[1][2]

Read as: the equivalence class of two is accessible from the equivalence class of one under accessibility relation R star

Means: the equivalence class of two is accessible from the equivalence class of one under accessibility relation R star

1 occurrence in this chapter

Equation form expr-7cc21a3bda17828d

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

Read as: formula B is true at world w in model M

Means: formula B is true at world w in model M

2 occurrences in this chapter

Equation form expr-8058c94ee6e3cddc

|W*|≤2n\card{W^*} \le 2^n

Read as: the cardinality of world set W star is at most two to the power n

Means: the cardinality of world set W star is at most two to the power n

1 occurrence in this chapter

Equation form expr-807cecd7a0bc43cd

M⊩□B[v]\mSat{M}{\Box !B}[v]

Read as: necessarily formula B is true at world v in model M

Means: necessarily formula B is true at world v in model M

1 occurrence in this chapter

Equation form expr-822ecd5d047812a2

C1(u,w)C_1(u,w)

Read as: condition C sub one of world u and world w

Means: condition C sub one of world u and world w

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

41 occurrences in this chapter

Equation form expr-82b1041f1d1b78d1

[w][w]

Read as: the equivalence class of world w

Means: the equivalence class of world w

11 occurrences in this chapter

Equation form expr-83d4a511903443cd

Rσσ′R\sigma\sigma'

Read as: sigma prime is accessible from sigma under accessibility relation R

Means: sigma prime is accessible from sigma under accessibility relation R

1 occurrence in this chapter

Equation form expr-84552be6395d0730

RwvRwv

Read as: world v is accessible from world w under accessibility relation R

Means: world v is accessible from world w under accessibility relation R

1 occurrence in this chapter

Equation form expr-85c3ce29e3a4dc40

C\mClass{C}

Read as: class C of models

Means: class C of models

3 occurrences in this chapter

Equation form expr-8a080cea809d1b9d

011011

Read as: zero one one

Means: zero one one

1 occurrence in this chapter

Equation form expr-8da08ddf8b7deebe

W=Z+W = \PosInt

Read as: world set W equals the positive integers

Means: world set W equals the positive integers

1 occurrence in this chapter

Equation form expr-938db8c9f82c8cb5

0101

Read as: zero one

Means: zero one

1 occurrence in this chapter

Equation form expr-941df6a1d8d59002

∈Γ\in \Gamma

Read as: belongs to Gamma

Means: belongs to Gamma

1 occurrence in this chapter

Equation form expr-9681df6e51570eb3

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

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

Means: necessarily necessarily formula A is true at world u in model M

1 occurrence in this chapter

Equation form expr-9763a163e7ff6591

w3w_3

Read as: world w sub three

Means: world w sub three

2 occurrences in this chapter

Equation form expr-9772a17b113f48bc

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

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

Means: necessarily formula A is true at world u in model M

8 occurrences in this chapter

Equation form expr-97e96167297c5e84

R*[1][1]R^*[1][1]

Read as: the equivalence class of one is accessible from the equivalence class of one under accessibility relation R star

Means: the equivalence class of one is accessible from the equivalence class of one under accessibility relation R star

1 occurrence in this chapter

Equation form expr-997e84e88f9f6fa1

[u][u]

Read as: the equivalence class of world u

Means: the equivalence class of world u

2 occurrences in this chapter

Equation form expr-9cb2b1c49ab1fcbb

v′≡vv' \equiv v

Read as: v prime is equivalent to world v

Means: v prime is equivalent to world v

1 occurrence in this chapter

Equation form expr-9db1005d8d74f983

RnmRnm

Read as: m is accessible from n under accessibility relation R

Means: m is accessible from n under accessibility relation R

1 occurrence in this chapter

Equation form expr-9e8e1aa6a3325e99

1∉V(p)1 \notin V(p)

Read as: one does not belong to valuation V applied to p

Means: one does not belong to valuation V applied to p

1 occurrence in this chapter

Equation form expr-a046b66b410157f3

[w1]=[w3][w_1] = [w_3]

Read as: the equivalence class of world w sub one equals the equivalence class of world w sub three

Means: the equivalence class of world w sub one equals the equivalence class of world w sub three

1 occurrence in this chapter

Equation form expr-a39d2ca036172648

p1p_1

Read as: p sub one

Means: p sub one

2 occurrences in this chapter

Equation form expr-a5b3ddd5897cb462

◇A∈Γ\Diamond!A \in \Gamma

Read as: possibly formula A belongs to Gamma

Means: possibly formula A belongs to Gamma

7 occurrences in this chapter

Equation form expr-a5bee4b2a719e4b8

□A∈Γ\Box !A \in \Gamma

Read as: necessarily formula A belongs to Gamma

Means: necessarily formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-a6d391b0c97204da

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

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

Means: possibly formula A is true at world v in model M

4 occurrences in this chapter

Equation form expr-a8088dbfc859a14a

[1]={1,3,5,…}[1] = \{1, 3, 5, \dots\}

Read as: equivalence class one is the set containing the positive odd numbers one, three, five, and so on

Means: equivalence class one is the set containing the positive odd numbers one, three, five, and so on

1 occurrence in this chapter

Equation form expr-a87cc90f673e1f35

M*\mModel{M^*}

Read as: model M star

Means: model M star

24 occurrences in this chapter

Equation form expr-aab6120b6377f332

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

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

Means: possibly formula A is true at world u in model M

8 occurrences in this chapter

Equation form expr-ab898b876b097eeb

Γ(C)\Gamma(\mClass{C})

Read as: the class of Gamma filtrations of models in class C

Means: the class of Gamma filtrations of models in class C

2 occurrences in this chapter

Equation form expr-abf50f98fbcf7ba7

⟨[1],[2]⟩,⟨[2],[1]⟩\tuple{[1], [2]}, \tuple{[2],[1]}

Read as: the ordered pair from class one to class two, followed by the ordered pair from class two to class one

Means: the ordered pair from class one to class two, followed by the ordered pair from class two to class one

1 occurrence in this chapter

Equation form expr-ad733bdffdf2d93a

M*⊩B[[v]]\mSat{M^*}{!B}[{[v]}]

Read as: formula B is true at the equivalence class of world v in model M star

Means: formula B is true at the equivalence class of world v in model M star

2 occurrences in this chapter

Equation form expr-ae14dabe94d2bb95

M*⊩B[[u]]\mSat{M^*}{!B}[{[u]}]

Read as: formula B is true at the equivalence class of world u in model M star

Means: formula B is true at the equivalence class of world u in model M star

1 occurrence in this chapter

Equation form expr-af506e46ec00a0b8

2nm2^{nm}

Read as: two raised to the power n times m

Means: two raised to the power n times m

1 occurrence in this chapter

Equation form expr-af6cc0a9a5bf2859

M⊩□A[u′]\mSat{M}{\Box!A}[u']

Read as: necessarily formula A is true at u prime in model M

Means: necessarily formula A is true at u prime in model M

1 occurrence in this chapter

Equation form expr-b34e6b523ff3f823

M⊮□(p∨q)→(□p∨□q)[w]\mSat/{M}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[w]

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

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

1 occurrence in this chapter

Equation form expr-b4e105fdf9fe5031

[w]=[u][w] = [u]

Read as: the equivalence class of world w equals the equivalence class of world u

Means: the equivalence class of world w equals the equivalence class of world u

2 occurrences in this chapter

Equation form expr-b511bf3b406585a0

[1]∉V*(p)[1] \notin V^*(p)

Read as: the equivalence class of one does not belong to valuation V star applied to p

Means: the equivalence class of one does not belong to valuation V star applied to p

1 occurrence in this chapter

Equation form expr-b59c0ca457682eca

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

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

Means: p is true at world w in model M

2 occurrences in this chapter

Equation form expr-b5b446abb4d0323b

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

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

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

7 occurrences in this chapter

Equation form expr-b699745ed32fa62b

C1(u,v)∧C2(u,v)C_1(u, v) \land C_2(u,v)

Read as: condition C sub one of world u and world v and condition C sub two of world u and world v

Means: condition C sub one of world u and world v and condition C sub two of world u and world v

1 occurrence in this chapter

Equation form expr-b75a47bad776c420

w≡uw \equiv u

Read as: world w is equivalent to world u

Means: world w is equivalent to world u

2 occurrences in this chapter

Equation form expr-b7b96c57fe5a9d1c

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

Read as: formula B is true at world u in model M

Means: formula B is true at world u in model M

1 occurrence in this chapter

Equation form expr-b7c2f590e48639e6

R*[2][2]R^*[2][2]

Read as: the equivalence class of two is accessible from the equivalence class of two under accessibility relation R star

Means: the equivalence class of two is accessible from the equivalence class of two under accessibility relation R star

1 occurrence in this chapter

Equation form expr-baceba972d598f85

[3]=[1][3]=[1]

Read as: the equivalence class of three equals the equivalence class of one

Means: the equivalence class of three equals the equivalence class of one

1 occurrence in this chapter

Equation form expr-bb11d453542f6dc9

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

Read as: p is true at the equivalence class of world w in model M star

Means: p is true at the equivalence class of world w in model M star

2 occurrences in this chapter

Equation form expr-bc9367794d2761fe

A∈Γ!A \in \Gamma

Read as: formula A belongs to Gamma

Means: formula A belongs to Gamma

8 occurrences in this chapter

Equation form expr-bcdaff99987b8f0c

A≡p!A \equiv p

Read as: formula A is syntactically identical to p

Means: formula A is syntactically identical to p

1 occurrence in this chapter

Equation form expr-bf94c4cba0afb322

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

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

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

11 occurrences in this chapter

Equation form expr-c05e8f4dad4fd3f9

C2(u,v)⇔C1(v,u)C_2(u,v) \Leftrightarrow C_1(v,u)

Read as: condition C sub two of world u and world v if and only if condition C sub one of world v and world u

Means: condition C sub two of world u and world v if and only if condition C sub one of world v and world u

1 occurrence in this chapter

Equation form expr-c083ae2a42fd172a

[2]={2,4,6,…}[2] = \{2, 4, 6, \dots\}

Read as: equivalence class two is the set containing the positive even numbers two, four, six, and so on

Means: equivalence class two is the set containing the positive even numbers two, four, six, and so on

1 occurrence in this chapter

Equation form expr-c18d30ee7a50b333

⟨[1],[1]⟩\tuple{[1],[1]}

Read as: the ordered pair the equivalence class of one, then the equivalence class of one

Means: the ordered pair the equivalence class of one, then the equivalence class of one

1 occurrence in this chapter

Equation form expr-c1d77f70f7540cb5

□A,◇A∈Γ\Box!A, \Diamond!A \in \Gamma

Read as: necessarily A and possibly A both belong to Gamma

Means: necessarily A and possibly A both belong to Gamma

1 occurrence in this chapter

Equation form expr-c205c00dfeb99d0b

C1C_1

Read as: condition C sub one

Means: condition C sub one

1 occurrence in this chapter

Equation form expr-c312c51147893a62

C1(v,w)C_1(v,w)

Read as: condition C sub one of world v and world w

Means: condition C sub one of world v and world w

3 occurrences in this chapter

Equation form expr-c45688a66c30fc45

◇A∈Γ\Diamond!A \in\Gamma

Read as: possibly formula A belongs to Gamma

Means: possibly formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-c457dbcdd3b49987

w4w_4

Read as: world w sub four

Means: world w sub four

1 occurrence in this chapter

Equation form expr-c511ae3eaed0ae8a

[w]∈V*(p)[w] \in V^*(p)

Read as: the equivalence class of world w belongs to valuation V star applied to p

Means: the equivalence class of world w belongs to valuation V star applied to p

7 occurrences in this chapter

Equation form expr-c669a4a98fb064a3

σ′=σ0\sigma' = \sigma 0

Read as: sigma prime equals the binary sequence sigma followed by zero

Means: sigma prime equals the binary sequence sigma followed by zero

1 occurrence in this chapter

Equation form expr-c871c55770deaeb8

w≡ww \equiv w

Read as: world w is equivalent to world w

Means: world w is equivalent to world w

1 occurrence in this chapter

Equation form expr-c88159d3136f3ab2

R23R23

Read as: three is accessible from two under accessibility relation R

Means: three is accessible from two under accessibility relation R

1 occurrence in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

31 occurrences in this chapter

Equation form expr-d0a918b38a513fd7

w5w_5

Read as: world w sub five

Means: world w sub five

3 occurrences in this chapter

Equation form expr-d16b73ce79fc2dfd

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

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

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

3 occurrences in this chapter

Equation form expr-d2da161508eebc66

w∈Ww \in W

Read as: world w belongs to world set W

Means: world w belongs to world set W

2 occurrences in this chapter

Equation form expr-d4735e3a265e16ee

22

Read as: two

Means: two

3 occurrences in this chapter

Equation form expr-d479fbeb0a94485c

C1(u,v)∧C3(u,v)∧C4(u,v)C_1(u, v) \land C_3(u,v) \land C_4(u,v)

Read as: condition C sub one of world u and world v and condition C sub three of world u and world v and condition C sub four of world u and world v

Means: condition C sub one of world u and world v and condition C sub three of world u and world v and condition C sub four of world u and world v

1 occurrence in this chapter

Equation form expr-d51bf149d0325d24

W*={[w]:w∈W}W^* = \Setabs{[w]}{w \in W}

Read as: world set W star is the set of equivalence classes of worlds w in W

Means: world set W star is the set of equivalence classes of worlds w in W

1 occurrence in this chapter

Equation form expr-d65d75b1e6562713

Σ\Sigma

Read as: Sigma

Means: Sigma

3 occurrences in this chapter

Equation form expr-da18c1f3ce41853d

2∈V(p)2 \in V(p)

Read as: two belongs to valuation V applied to p

Means: two belongs to valuation V applied to p

1 occurrence in this chapter

Equation form expr-dc7ba1c49968c37c

pkp_k

Read as: p sub k

Means: p sub k

2 occurrences in this chapter

Equation form expr-dd02ac05c1e7763f

[w]=[v][w] = [v]

Read as: the equivalence class of world w equals the equivalence class of world v

Means: the equivalence class of world w equals the equivalence class of world v

1 occurrence in this chapter

Equation form expr-deb233fb25cbf75b

□(p∨q)→(□p∨□q)\Box(p \lor q) \lif (\Box p \lor \Box q)

Read as: if necessarily, open scope, p or q, close scope, then either necessarily p or necessarily q

Means: if necessarily, open scope, p or q, close scope, then either necessarily p or necessarily q

1 occurrence in this chapter

Equation form expr-decc37cfa250472b

|W|=n\card{W} = n

Read as: the cardinality of world set W equals n

Means: the cardinality of world set W equals n

1 occurrence in this chapter

Equation form expr-df66e334fbace274

4◇\Ax{4}_\Diamond

Read as: the diamond form of axiom four

Means: the diamond form of axiom four

1 occurrence in this chapter

Equation form expr-dfe37007fc21a987

Ru′v′Ru'v'

Read as: v prime is accessible from u prime under accessibility relation R

Means: v prime is accessible from u prime under accessibility relation R

1 occurrence in this chapter

Equation form expr-e17001035711d4f9

[w1][w_1]

Read as: the equivalence class of world w sub one

Means: the equivalence class of world w sub one

1 occurrence in this chapter

Equation form expr-e5bef91e6d1711d5

RvuRvu

Read as: world u is accessible from world v under accessibility relation R

Means: world u is accessible from world v under accessibility relation R

2 occurrences in this chapter

Equation form expr-e6bc30ec51dc31f9

M*⊩¬B[[w]]\mSat{M^*}{\lnot !B}[{[w]}]

Read as: not formula B is true at the equivalence class of world w in model M star

Means: not formula B is true at the equivalence class of world w in model M star

1 occurrence in this chapter

Equation form expr-e8a3fed33f2f1fe0

2n2^n

Read as: two raised to the power n

Means: two raised to the power n

2 occurrences in this chapter

Equation form expr-e8cbeba8b42e3b53

v∈Wv \in W

Read as: world v belongs to world set W

Means: world v belongs to world set W

1 occurrence in this chapter

Equation form expr-e9f8c51ef1abcf96

Γ={p,□p}\Gamma = \{p, \Box p \}

Read as: Gamma is the set containing p and necessarily p

Means: Gamma is the set containing p and necessarily p

1 occurrence in this chapter

Equation form expr-ea5cbfc3882fd921

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

Read as: formula B is true at the equivalence class of world w in model M star

Means: formula B is true at the equivalence class of world w in model M star

2 occurrences in this chapter

Equation form expr-ea7ef77bf7563068

≡\equiv

Read as: the filtration equivalence relation

Means: the filtration equivalence relation

6 occurrences in this chapter

Equation form expr-eb14c67f1aa72563

[w]≡[w]_\equiv

Read as: the equivalence class of world w under the filtration equivalence relation

Means: the equivalence class of world w under the filtration equivalence relation

1 occurrence in this chapter

Equation form expr-ec7d40a789aa2d83

u′u'

Read as: u prime

Means: u prime

1 occurrence in this chapter

Equation form expr-edb830d14cb5ddae

m=n+1m = n + 1

Read as: m equals n plus one

Means: m equals n plus one

1 occurrence in this chapter

Equation form expr-ee17c0bc612157fc

[w1]=[w3][w_1]=[w_3]

Read as: the equivalence class of world w sub one equals the equivalence class of world w sub three

Means: the equivalence class of world w sub one equals the equivalence class of world w sub three

1 occurrence in this chapter

Equation form expr-f0a6cd0884bfee98

R12R12

Read as: two is accessible from one under accessibility relation R

Means: two is accessible from one under accessibility relation R

1 occurrence in this chapter

Equation form expr-f1534392279bddbf

0000

Read as: zero zero

Means: zero zero

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-f23982583aa961f1

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

Read as: formula A is syntactically identical to not formula B

Means: formula A is syntactically identical to not formula B

1 occurrence in this chapter

Equation form expr-f28479ca0ee4db1f

⊩□p\mSat{{}}{\Box p}

Read as: necessarily p is true at this displayed world

Means: necessarily p is true at this displayed world

5 occurrences in this chapter

Equation form expr-f2c162140c5dcd8e

|W*|≤|℘(Γ)|\card{W^*} \le \card{\Pow{\Gamma}}

Read as: the cardinality of world set W star is at most the cardinality of the power set of Gamma

Means: the cardinality of world set W star is at most the cardinality of the power set of Gamma

1 occurrence in this chapter

Equation form expr-f2e77153d6d9c7f0

B◇\Ax{B_\Diamond}

Read as: the diamond form of axiom B

Means: the diamond form of axiom B

1 occurrence in this chapter

Equation form expr-f2f6a440e14b770c

[2]∈V*(p)[2] \in V^*(p)

Read as: the equivalence class of two belongs to valuation V star applied to p

Means: the equivalence class of two belongs to valuation V star applied to p

1 occurrence in this chapter

Equation form expr-f34a384a1b186833

UFin\mClass{U}_\mathrm{Fin}

Read as: the class of finite universal models

Means: the class of finite universal models

2 occurrences in this chapter

Equation form expr-f3c0109b6707f8e2

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

Read as: model M star is the ordered triple of world set W star, accessibility relation R star, and valuation V star

Means: model M star is the ordered triple of world set W star, accessibility relation R star, and valuation V star

3 occurrences in this chapter

Equation form expr-f497e48cb13e4d01

□□A∈Γ\Box\Box!A \in \Gamma

Read as: necessarily necessarily formula A belongs to Gamma

Means: necessarily necessarily formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-f4aec0fdd6c82c6d

u∈[v]u \in [v]

Read as: world u belongs to the equivalence class of world v

Means: world u belongs to the equivalence class of world v

1 occurrence in this chapter

Equation form expr-f6b9f8bdeb0b2c0d

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

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

Means: p is true at world v in model M

4 occurrences in this chapter

Equation form expr-f8dcd48388f1ed21

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

Read as: world w belongs to valuation V applied to p

Means: world w belongs to valuation V applied to p

3 occurrences in this chapter

Equation form expr-f9c6cbd6245f9917

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

Read as: model M is the ordered triple of world set W, accessibility relation R, and valuation V

Means: model M is the ordered triple of world set W, accessibility relation R, and valuation V

3 occurrences in this chapter

Equation form expr-f9e469296b427af3

□p→p\Box p \lif p

Read as: necessarily p implies p

Means: necessarily p implies p

6 occurrences in this chapter

Equation form expr-fcb5f40df9be6bae

WW

Read as: world set W

Means: world set W

6 occurrences in this chapter

Equation form expr-ff11c222c6de3e22

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

Read as: the current induction-case formula is true at the equivalence class of world w in model M star

Means: the current induction-case formula is true at the equivalence class of world w in model M star

8 occurrences in this chapter

Definition of subformula and modal closure

Gamma is closed under subformulas when it contains every subformula of each member. It is modally closed when it also contains necessarily A and possibly A whenever it contains A.

Source

Filtration equivalence relation

For model M and subformula-closed Gamma, worlds u and v are equivalent exactly when they agree on the truth of every formula A in Gamma. The class of w contains exactly the worlds equivalent to w.

Source

The filtration relation is an equivalence relation

The relation defined by agreement on all formulas in Gamma is reflexive, symmetric, and transitive.

Source

Definition of a filtration

A filtration through Gamma has equivalence classes as worlds and the induced valuation. Its accessibility relation inherits every original edge and satisfies the selected box and diamond preservation clauses.

Source

Filtration Theorem

For every A in Gamma and world w, A is true at w in the original model exactly when it is true at class w in any filtration through Gamma.

Source

Exercise completing the Filtration Theorem

Complete the source-selected missing induction cases in the Filtration Theorem. The exercise remains unsolved.

Source

Model truth and class validity under filtration

The Filtration Theorem extends from truth at worlds to truth throughout a model and to validity in a class and the class of its Gamma filtrations.

Source

Definition of the finest filtration

Class v is accessible from class u exactly when some representative u prime in class u accesses some representative v prime in class v in the original model.

Source

The finest construction is a filtration

The proposition verifies inheritance of original edges and the source-selected box and diamond preservation requirements.

Source

Exercise completing the finest-filtration proof

Complete the source-selected missing box or diamond preservation clauses for the finest filtration. The exercise remains unsolved.

Source

Definition of the coarsest filtration

The coarsest relation includes an edge exactly when all active box and diamond preservation conditions hold between the two source worlds.

Source

The coarsest construction is a filtration

The proof observes that the defining clauses already ensure modal preservation and checks that every original edge is inherited.

Source

Infinite alternating model and its filtrations

Positive integer n accesses n plus one, and p is true exactly at even worlds. Through the three subformulas of necessarily p implies p, odd and even worlds form two classes. Two possible filtered relations differ only by the loop at the even class.

Source

Figure of the alternating model and two filtrations

The outer figure contains one infinite-chain diagram and one diagram showing the finest and coarsest two-class filtrations. The two inner diagrams carry the complete node, valuation, edge, loop, and omission descriptions.

Source

Infinite alternating chain model

Worlds one through four are shown in successor order with p false, true, false, true. A dotted continuation after world four states that the chain continues; it is not recorded as a named accessibility edge to an actual world.

Source

Two two-class filtrations

The left two-class model has arrows in both directions between odd class one and even class two. The right model has the same two arrows and also a loop at even class two. No loop at class one is drawn.

Source

Exercise filtering an infinite binary tree

Compute the filtered worlds, valuation, finest relation, and coarsest relation for the displayed binary tree and the subformulas of the stated modal conditional. The source states that the conditional is false at every world. The exercise remains unsolved.

Source

Infinite binary tree model

The shown prefix worlds branch from zero to zero-zero and zero-one and then to four length-three worlds. Each world has the printed p and q valuation. Dotted child stubs explicitly indicate omitted continuation beyond the drawn depth.

Source

Finite size of a filtration

If Gamma is finite, every filtration through Gamma is finite. Distinct equivalence classes inject into the power set of Gamma, so n formulas yield at most two to the n worlds.

Source

Definition of the finite model property

A modal system has the finite model property when every formula true at a world in one of its models is also true at a world in a finite model of that system.

Source

Finite model property for K

Filtering a K model through the finite set of subformulas preserves the target formula and yields at most two to the n worlds. K imposes no further frame restriction.

Source

Universal validity reduced to finite universal models

A formula is valid in all universal models exactly when it is valid in all finite universal models. A filtration of a universal model remains universal because every original pair is accessible.

Source

Finite model property for S five

The source combines the universal-model characterization with finite universal filtrations to obtain a finite reflexive euclidean model.

Source

Exercise on serial and reflexive filtrations

Show that every filtration of a serial model is serial and every filtration of a reflexive model is reflexive. The exercise remains unsolved.

Source

Exercise finding property-losing filtrations

Find filtrations that lose symmetry, transitivity, or euclideanness from models having the corresponding property. The exercise remains unsolved.

Source

Decidability of S five

The source proposes parallel proof enumeration and finite-model search. A source note records that the written search says all models rather than restricting the countermodel lane to the relevant universal models.

Source

Conditions for accessibility-preserving filtrations

The outer table presents four conditions C one through C four between worlds u and v. Its nested tabular object supplies the explicit ordered formula reading.

Source

Rows C one through C four

Each row gives its box clause followed by its diamond clause. C one preserves truth from u toward v, C two reverses the worlds, C three preserves the modalized truth in the forward comparison, and C four reverses that comparison.

Source

Filtrations with selected accessibility properties

Combinations of C one through C four define symmetric, transitive, symmetric-and-transitive, or transitive-and-euclidean filtrations when the original model has the corresponding property.

Source

Exercise completing the accessibility proof

Complete the remaining three cases of the theorem on filtrations preserving accessibility properties. The exercise remains unsolved.

Source

Figure called a serial and euclidean model

The outer figure contains the first five-world source graph. Its inner diagram lists all five worlds, truth labels, directed edges, and loops. The source calls the graph serial, although no outgoing edge from w sub two is drawn; no loop or edge is invented.

Source

Five-world euclidean source graph

World w one accesses w two. World w three accesses w four. Worlds w four and w five access each other and each has a loop. The printed p and necessity-of-p statuses are retained. No outgoing edge from w two is shown.

Source

Figure of the filtered euclidean example

The outer figure contains the four-class filtration graph. The inner diagram records the merged class of w one and w three, every printed valuation and modal status, all arrows, and both loops.

Source

Four-class filtration source graph

Merged class w one equals class w three accesses class w two and class w four. Class w four and class w five access each other and each has a loop. The printed p and necessity-of-p statuses are retained without adding the absent arrows discussed in the prose.

Source

Coarsest filtrations through modally closed sets

The theorem states preservation of symmetry, transitivity, and euclideanness by the coarsest filtration through modally closed Gamma. The following proof-item order is inconsistent with the statement and is separately disclosed.

Source

Exercise completing modally closed filtration cases

Complete the source proof using the stated diamond forms of axioms five and B. The exercise remains unsolved; the mismatched statement and proof item order is not silently repaired.

Source

Cross-reference reference-001064

the definition of a filtration

Source occurrence

Cross-reference reference-001065

the necessity-preservation condition for a filtration

Source occurrence

Cross-reference reference-001066

the definition of a filtration

Source occurrence

Cross-reference reference-001067

the inherited-edge condition for a filtration

Source occurrence

Cross-reference reference-001068

the Filtration Theorem preserving truth of formulas in Gamma

Source occurrence

Cross-reference reference-001069

the definition of a filtration

Source occurrence

Cross-reference reference-001070

the definition of a filtration

Source occurrence

Cross-reference reference-001071

the accessibility conditions in the definition of a filtration

Source occurrence

Cross-reference reference-001072

the inherited-edge condition for a filtration

Source occurrence

Cross-reference reference-001073

the necessity-preservation condition for a filtration

Source occurrence

Cross-reference reference-001074

the possibility-preservation condition for a filtration

Source occurrence

Cross-reference reference-001075

the proposition that the finest construction is a filtration

Source occurrence

Cross-reference reference-001076

the box clause in the definition of the coarsest filtration

Source occurrence

Cross-reference reference-001077

the diamond clause in the definition of the coarsest filtration

Source occurrence

Cross-reference reference-001078

the figure showing the infinite alternating model and its two filtrations

Source occurrence

Cross-reference reference-001079

the definition of a filtration

Source occurrence

Cross-reference reference-001080

the inherited-edge condition for a filtration

Source occurrence

Cross-reference reference-001081

the necessity-preservation condition for a filtration

Source occurrence

Cross-reference reference-001082

the Filtration Theorem preserving truth of formulas in Gamma

Source occurrence

Cross-reference reference-001083

the proposition bounding the size of a filtration

Source occurrence

Cross-reference reference-001084

the equivalence between S five models and universal models used here

Source occurrence

Cross-reference reference-001085

the proposition bounding the size of a filtration

Source occurrence

Cross-reference reference-001086

the Filtration Theorem preserving truth of formulas in Gamma

Source occurrence

Cross-reference reference-001087

the definition of a filtration

Source occurrence

Cross-reference reference-001088

the accessibility conditions in the definition of a filtration

Source occurrence

Cross-reference reference-001089

the equivalence between S five models and universal models used here

Source occurrence

Cross-reference reference-001090

the proposition reducing universal-model validity to finite universal models

Source occurrence

Cross-reference reference-001091

the general canonical-model determination theorem

Source occurrence

Cross-reference reference-001092

the finite model property corollary for S five

Source occurrence

Cross-reference reference-001093

the table of conditions C one through C four

Source occurrence

Cross-reference reference-001094

the definition of a filtration

Source occurrence

Cross-reference reference-001095

the necessity-preservation condition for a filtration

Source occurrence

Cross-reference reference-001096

the possibility-preservation condition for a filtration

Source occurrence

Cross-reference reference-001097

the definition of a filtration

Source occurrence

Cross-reference reference-001098

the definition of a filtration

Source occurrence

Cross-reference reference-001099

the inherited-edge condition for a filtration

Source occurrence

Cross-reference reference-001100

the theorem constructing filtrations with selected accessibility properties

Source occurrence

Cross-reference reference-001101

the section on filtrations and accessibility properties

Source occurrence

Cross-reference reference-001102

the displayed source model described as serial and euclidean

Source occurrence

Cross-reference reference-001103

the displayed filtration of that model

Source occurrence

Cross-reference reference-001104

the displayed source model described as serial and euclidean

Source occurrence

Cross-reference reference-001105

the definition of a modally closed set of formulas

Source occurrence

Cross-reference reference-001106

the theorem on coarsest filtrations through modally closed sets

Source occurrence

Source disclosures

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

A≡⊥!A \ident \lfalse

Read as: Case: A is the falsity constant.

Read in context source

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

A≡p!A \ident p

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

Read in context source

Source-generated case expression tr054-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 tr054-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 tr054-source-macro-0005

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

Read as: Case: A is necessarily B.

Read in context source

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

¬p\mFalse{p}

Read as: p is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬p\mFalse{p}

Read as: p is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬p\mFalse{p}

Read as: p is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬p\mFalse{p}

Read as: p is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬q\mFalse{q}

Read as: q is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬q\mFalse{q}

Read as: q is false

Read in context source

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

p\mTrue{p}

Read as: p is true

Read in context source

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

¬q\mFalse{q}

Read as: q is false

Read in context source

Source-generated case expression tr054-source-macro-0020

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0021

q\mTrue{q}

Read as: q is true

Read in context source

Source-generated case expression tr054-source-macro-0022

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0023

q\mTrue{q}

Read as: q is true

Read in context source

Source-generated case expression tr054-source-macro-0024

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr054-source-macro-0025

¬q\mFalse{q}

Read as: q is false

Read in context source

Source-generated case expression tr054-source-macro-0026

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0027

q\mTrue{q}

Read as: q is true

Read in context source

Source-generated case expression tr054-source-macro-0028

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0029

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr054-source-macro-0030

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0031

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr054-source-macro-0032

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0033

¬p\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr054-source-macro-0034

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr054-source-macro-0035

p\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr054-source-macro-0036

¬p\mFalse{p}

Read as: p is false

Read in context source

Ordered structures

Infinite alternating chain model

Structure: diagram tikz.

Infinite alternating successor-chain model. Nodes in source order. Source world node world one. Valuation label p is false. Printed node label one. Source world node world two. Valuation label p is true. Printed node label two. Source world node world three. Valuation label p is false. Printed node label three. Source world node world four. Valuation label p is true. Printed node label four. Source phantom node phantom marker five is an unlabeled layout marker and is not an actual world. Directed edges in source order. Directed accessibility edge from world one to world two. Directed accessibility edge from world two to world three. Directed accessibility edge from world three to world four. Omissions and continuation marks. A dotted, non-arrow line from world four to phantom marker five indicates that the successor chain continues; it is not recorded as a directed accessibility edge to a named world. Only the three solid directed arrows are accessibility edges. The dotted line has no arrowhead and records continuation without naming another actual world. End diagram.

Read the source-bound structure in context

Two two-class filtrations

Structure: diagram tikz.

Two separate two-class filtrations printed in one TikZ picture. Nodes in source order. In the first two-class filtration, Source world node first-model odd-class node. Valuation label p is false. Printed node label the equivalence class of one. In the first two-class filtration, Source world node first-model even-class node. Valuation label p is true. Printed node label the equivalence class of two. In the second two-class filtration, Source world node second-model odd-class node. Valuation label p is false. Printed node label the equivalence class of one. In the second two-class filtration, Source world node second-model even-class node. Valuation label p is true. Printed node label the equivalence class of two. Directed edges in source order. Directed accessibility edge from first-model odd-class node to first-model even-class node. Directed accessibility edge from first-model even-class node to first-model odd-class node. Directed accessibility edge from second-model odd-class node to second-model even-class node. Directed accessibility edge from second-model even-class node to second-model odd-class node. Directed accessibility loop at second-model even-class node. Omissions and continuation marks. There are no edges between the first and second displayed components. The second component alone has the printed loop at its even class; no other loop is inferred. End diagram.

Read the source-bound structure in context

Infinite binary tree model

Structure: diagram tikz.

Displayed finite prefix of an infinite binary-tree model. Nodes in source order. Source world node world zero. Valuation label p is true. Valuation label q is false. Printed node label zero. Source world node world zero zero. Valuation label p is true. Valuation label q is false. Printed node label zero zero. Source world node world zero zero zero. Valuation label p is true. Valuation label q is false. Printed node label zero zero zero. Source phantom node phantom marker zero zero zero zero is an unlabeled layout marker and is not an actual world. Source phantom node phantom marker zero zero zero one is an unlabeled layout marker and is not an actual world. Source world node world zero zero one. Valuation label p is false. Valuation label q is true. Printed node label zero zero one. Source phantom node phantom marker zero zero one zero is an unlabeled layout marker and is not an actual world. Source phantom node phantom marker zero zero one one is an unlabeled layout marker and is not an actual world. Source world node world zero one. Valuation label p is false. Valuation label q is true. Printed node label zero one. Source world node world zero one zero. Valuation label p is true. Valuation label q is false. Printed node label zero one zero. Source phantom node phantom marker zero one zero zero is an unlabeled layout marker and is not an actual world. Source phantom node phantom marker zero one zero one is an unlabeled layout marker and is not an actual world. Source world node world zero one one. Valuation label p is false. Valuation label q is true. Printed node label zero one one. Source phantom node phantom marker zero one one zero is an unlabeled layout marker and is not an actual world. Source phantom node phantom marker zero one one one is an unlabeled layout marker and is not an actual world. Directed edges in source order. Directed accessibility edge from world zero to world zero zero. Directed accessibility edge from world zero to world zero one. Directed accessibility edge from world zero zero to world zero zero zero. Directed accessibility edge from world zero zero to world zero zero one. Directed accessibility edge from world zero one to world zero one zero. Directed accessibility edge from world zero one to world zero one one. Omissions and continuation marks. A dotted, non-arrow child stub from world zero zero zero to phantom marker zero zero zero zero indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero zero zero to phantom marker zero zero zero one indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero zero one to phantom marker zero zero one zero indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero zero one to phantom marker zero zero one one indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero one zero to phantom marker zero one zero zero indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero one zero to phantom marker zero one zero one indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero one one to phantom marker zero one one zero indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. A dotted, non-arrow child stub from world zero one one to phantom marker zero one one one indicates omitted continuation of the binary tree; it is not recorded as a directed accessibility edge. Only the six solid directed arrows are recorded as accessibility edges. Each dotted child stub is an explicit continuation marker, not a solid directed edge to an actual named world. End diagram.

Read the source-bound structure in context

Rows C one through C four

Structure: table.

Table of four conditions on possible worlds for defining filtrations. The source has no printed header row; the accessible column roles are condition label and condition clause. Source row one, label condition C sub one of world u and world v, box clause: if necessarily formula A belongs to Gamma and necessarily formula A is true at world u in model M, then formula A is true at world v in model M. Source row two, condition C one continued, diamond clause: if possibly formula A belongs to Gamma and formula A is true at world v in model M, then possibly formula A is true at world u in model M. Source row three, label condition C sub two of world u and world v, box clause: if necessarily formula A belongs to Gamma and necessarily formula A is true at world v in model M, then formula A is true at world u in model M. Source row four, condition C two continued, diamond clause: if possibly formula A belongs to Gamma and formula A is true at world u in model M, then possibly formula A is true at world v in model M. Source row five, label condition C sub three of world u and world v, box clause: if necessarily formula A belongs to Gamma and necessarily formula A is true at world u in model M, then necessarily formula A is true at world v in model M. Source row six, condition C three continued, diamond clause: if possibly formula A belongs to Gamma and possibly formula A is true at world v in model M, then possibly formula A is true at world u in model M. Source row seven, label condition C sub four of world u and world v, box clause: if necessarily formula A belongs to Gamma and necessarily formula A is true at world v in model M, then necessarily formula A is true at world u in model M. Source row eight, condition C four continued, diamond clause: if possibly formula A belongs to Gamma and possibly formula A is true at world u in model M, then possibly formula A is true at world v in model M. End table.

Read the source-bound structure in context

Five-world euclidean source graph

Structure: diagram tikz.

Five-world graph captioned by the source as a serial and euclidean model. Nodes in source order. Source world node world w sub one. Valuation label p is false. Modal-status label necessarily p is true at this displayed world. Printed node label world w sub one. Source world node world w sub two. Valuation label p is true. Modal-status label necessarily p is true at this displayed world. Printed node label world w sub two. Source world node world w sub three. Valuation label p is false. Modal-status label necessarily p is true at this displayed world. Printed node label world w sub three. Source world node world w sub four. Valuation label p is true. Modal-status label necessarily p is false at this displayed world. Printed node label world w sub four. Source world node world w sub five. Valuation label p is false. Modal-status label necessarily p is false at this displayed world. Printed node label world w sub five. Directed edges in source order. Directed accessibility edge from world w sub one to world w sub two. Directed accessibility edge from world w sub three to world w sub four. Directed accessibility loop at world w sub four. Directed accessibility edge from world w sub four to world w sub five. Directed accessibility edge from world w sub five to world w sub four. Directed accessibility loop at world w sub five. Omissions and continuation marks. The edge list is exactly the printed graph. In particular, no outgoing edge or loop is drawn from world w sub two, so none is added despite the source caption calling the model serial. End diagram.

Read the source-bound structure in context

Four-class filtration source graph

Structure: diagram tikz.

Four-node filtration graph with the first and third source worlds merged. Nodes in source order. Source world node merged class w sub one and w sub three. Valuation label p is false. Printed node annotation the equivalence class of world w sub one equals the equivalence class of world w sub three. Modal-status label necessarily p is true at this displayed world. Printed node label the equivalence class of world w sub one. Source world node class w sub two. Valuation label p is true. Modal-status label necessarily p is true at this displayed world. Printed node label the equivalence class of world w sub two. Source world node class w sub four. Valuation label p is true. Modal-status label necessarily p is false at this displayed world. Printed node label the equivalence class of world w sub four. Source world node class w sub five. Valuation label p is false. Modal-status label necessarily p is false at this displayed world. Printed node label the equivalence class of world w sub five. Directed edges in source order. Directed accessibility edge from merged class w sub one and w sub three to class w sub two. Directed accessibility edge from merged class w sub one and w sub three to class w sub four. Directed accessibility loop at class w sub four. Directed accessibility edge from class w sub four to class w sub five. Directed accessibility edge from class w sub five to class w sub four. Directed accessibility loop at class w sub five. Omissions and continuation marks. The edge list is exactly the printed filtration. No unprinted double arrows or other euclidean repair edges from the surrounding prose are added. End diagram.

Read the source-bound structure in context