Normal Modal Logics

Completeness and Canonical Models

Equation form expr-022690f2601dfe04

p→□qp \lif \Box q

Read as: p implies necessarily q

Means: p implies necessarily q

1 occurrence in this chapter

Equation form expr-0261fbf4b36283f3

Ak∈Δ!A_k \in \Delta

Read as: formula A sub k belongs to Delta

Means: formula A sub k belongs to Delta

1 occurrence 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-04bd10699f6fe975

ni≤nn_i \le n

Read as: n sub i is less than or equal to n

Means: n sub i is less than or equal to n

1 occurrence in this chapter

Equation form expr-078c666a54de8798

RΣΔ′ΔR^\Sigma \Delta'\Delta

Read as: Delta is accessible from Delta prime under accessibility relation R superscript Sigma

Means: Delta is accessible from Delta prime under accessibility relation R superscript Sigma

1 occurrence in this chapter

Equation form expr-09ad6ae190e9283e

□B\Box !B

Read as: necessarily formula B

Means: necessarily formula B

1 occurrence in this chapter

Equation form expr-0ab83730c263f0b7

⊨A\Entails !A

Read as: formula A is valid

Means: formula A is valid

1 occurrence in this chapter

Equation form expr-0c78cf875e9976b0

◇A∈Δ\Diamond !A \in \Delta

Read as: possibly formula A belongs to Delta

Means: possibly formula A belongs to Delta

1 occurrence in this chapter

Equation form expr-0e83938a92c090ab

□−1Δ1⊆Δ2\Box^{-1}\Delta_1 \subseteq \Delta_2

Read as: inverse box of Delta sub one is a subset of Delta sub two

Means: inverse box of Delta sub one is a subset of Delta sub two

3 occurrences in this chapter

Equation form expr-0ebd4e398371827e

□A∉Γ\Box!A \notin \Gamma

Read as: necessarily formula A does not belong to Gamma

Means: necessarily formula A does not belong to Gamma

2 occurrences in this chapter

Equation form expr-104dd548cbae28fe

Bk∈Γ!B_k \in \Gamma

Read as: formula B sub k belongs to Gamma

Means: formula B sub k belongs to Gamma

1 occurrence in this chapter

Equation form expr-1088687be1308206

⊥∈Γ\lfalse \in \Gamma

Read as: falsity belongs to Gamma

Means: falsity belongs to Gamma

1 occurrence in this chapter

Equation form expr-109153a063e52825

¬□A\lnot\Box !A

Read as: not necessarily formula A

Means: not necessarily formula A

1 occurrence in this chapter

Equation form expr-10ce9e83b8f263de

Bm∈Δ2!B_m \in \Delta_2

Read as: formula B sub m belongs to Delta sub two

Means: formula B sub m belongs to Delta sub two

1 occurrence in this chapter

Equation form expr-139c7c04318de35e

n=0n = 0

Read as: n equals zero

Means: n equals zero

1 occurrence in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

1 occurrence in this chapter

Equation form expr-1526f7433abebc69

Δ3∈WΣ\Delta_3 \in W^\Sigma

Read as: Delta sub three belongs to world set W superscript Sigma

Means: Delta sub three belongs to world set W superscript Sigma

1 occurrence in this chapter

Equation form expr-178a55421d296783

□A∉Γ\Box!A \notin\Gamma

Read as: necessarily formula A does not belong to Gamma

Means: necessarily formula A does not belong to Gamma

1 occurrence in this chapter

Equation form expr-19682c95a2be8462

□B1\Box!B_1

Read as: necessarily formula B sub one

Means: necessarily formula B sub one

1 occurrence in this chapter

Equation form expr-1a8359b8cebcb5de

A∉Δ!A \notin \Delta

Read as: formula A does not belong to Delta

Means: formula A does not belong to Delta

5 occurrences in this chapter

Equation form expr-1af35c81144c00e6

Source-census fragment. Read the complete source formula tr053-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-1b16b1df538ba12d

nn

Read as: n

Means: n

6 occurrences in this chapter

Equation form expr-1b41af8a575ec8ec

MΣ⊩p[Δ]\mSat{M^\Sigma}{p}[\Delta]

Read as: p is true at Delta in canonical model M superscript Sigma

Means: p is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-1cd9646ce9f411d6

Δ′∈WΣ\Delta' \in W^\Sigma

Read as: Delta prime belongs to world set W superscript Sigma

Means: Delta prime belongs to world set W superscript Sigma

3 occurrences in this chapter

Equation form expr-1d5533d65d3ecd1f

□□−1Γ⊢□A\Box\Box^{-1}\Gamma \Proves \Box!A

Read as: box of inverse box of Gamma derives necessarily formula A

Means: box of inverse box of Gamma derives necessarily formula A

1 occurrence in this chapter

Equation form expr-1e1eed9c7b8f0d1c

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

Read as: necessarily formula A implies necessarily necessarily formula A

Means: necessarily formula A implies necessarily necessarily formula A

1 occurrence in this chapter

Equation form expr-1e7f7ac9413df1a1

Δ∈WΣ\Delta \in W^\Sigma

Read as: Delta belongs to world set W superscript Sigma

Means: Delta belongs to world set W superscript Sigma

3 occurrences in this chapter

Equation form expr-200dc7e459f1f468

Γ=□−1Δ1∪◇Δ2.\Gamma = \Box^{-1}\Delta_1 \cup \Diamond\Delta_2.

Read as: Gamma equals inverse box of Delta sub one union diamond of Delta sub two

Means: Gamma equals inverse box of Delta sub one union diamond of Delta sub two

1 occurrence in this chapter

Equation form expr-2172fa5e33fa695a

Δ2=Δ3\Delta_2=\Delta_3

Read as: Delta sub two equals Delta sub three

Means: Delta sub two equals Delta sub three

2 occurrences in this chapter

Equation form expr-2296dd8dc032180b

MK⊮A\mSat/{M^{\Log{K}}}{!A}

Read as: formula A is not true throughout model M superscript logic K

Means: formula A is not true throughout model M superscript logic K

1 occurrence in this chapter

Equation form expr-229e0feb70fefca0

◇Δ3⊆Δ1\Diamond\Delta_3 \subseteq \Delta_1

Read as: diamond of Delta sub three is a subset of Delta sub one

Means: diamond of Delta sub three is a subset of Delta sub one

1 occurrence in this chapter

Equation form expr-22dbfa974760388b

B∨C∈Δ!B \lor !C \in \Delta

Read as: formula B or formula C belongs to Delta

Means: formula B or formula C belongs to Delta

1 occurrence in this chapter

Equation form expr-230b1f1646879e67

B∈□−1Δ!B \in \Box^{-1} \Delta

Read as: formula B belongs to inverse box of Delta

Means: formula B belongs to inverse box of Delta

1 occurrence in this chapter

Equation form expr-23c012c2aea04feb

□B∈Δ2\Box!B \in \Delta_2

Read as: necessarily formula B belongs to Delta sub two

Means: necessarily formula B belongs to Delta sub two

1 occurrence in this chapter

Equation form expr-240beaec68ac54ef

MΣ⊩B[Δ]\mSat{M^\Sigma}{!B}[\Delta]

Read as: formula B is true at Delta in canonical model M superscript Sigma

Means: formula B is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-26840801c1f68169

¬B∈Γ\lnot !B \in \Gamma

Read as: not formula B belongs to Gamma

Means: not formula B belongs to Gamma

1 occurrence in this chapter

Equation form expr-2944081c20d9723d

□−1Δ⊆Δ\Box^{-1}\Delta \subseteq \Delta

Read as: inverse box of Delta is a subset of Delta

Means: inverse box of Delta is a subset of Delta

1 occurrence in this chapter

Equation form expr-2ae00d0a656160f6

Δ2⊆Δ3\Delta_2 \subseteq \Delta_3

Read as: Delta sub two is a subset of Delta sub three

Means: Delta sub two is a subset of Delta sub three

1 occurrence in this chapter

Equation form expr-2bb168c166c79f1d

Δ1\Delta_1

Read as: Delta sub one

Means: Delta sub one

2 occurrences in this chapter

Equation form expr-2bbb844fcec00c4b

C4\mClass{C}_\Ax{4}

Read as: class C subscript axiom four

Means: class C subscript axiom four

1 occurrence in this chapter

Equation form expr-2c7ebda8e773edb6

VΣ)V^\Sigma)

Read as: valuation V superscript Sigma, followed by the source closing parenthesis

Means: valuation V superscript Sigma, followed by the source closing parenthesis

1 occurrence in this chapter

Equation form expr-2d046fa0b80809f3

RΣΔ2Δ3R^\Sigma \Delta_2\Delta_3

Read as: Delta sub three is accessible from Delta sub two under accessibility relation R superscript Sigma

Means: Delta sub three is accessible from Delta sub two under accessibility relation R superscript Sigma

3 occurrences in this chapter

Equation form expr-2ebdae4d41d6240a

Σ⊢¬◇⊥\Sigma \Proves \lnot\Diamond \lfalse

Read as: Sigma derives not possibly falsity

Means: Sigma derives not possibly falsity

1 occurrence in this chapter

Equation form expr-2f38dcf87ebd3881

{A:□A∈Δ}⊆Δ′\Setabs{!A}{\Box!A \in \Delta} \subseteq \Delta'

Read as: the set of formula A such that necessarily formula A belongs to Delta is a subset of Delta prime

Means: the set of formula A such that necessarily formula A belongs to Delta is a subset of Delta prime

1 occurrence in this chapter

Equation form expr-303c445801500304

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

Read as: necessarily formula A implies formula A

Means: necessarily formula A implies formula A

1 occurrence in this chapter

Equation form expr-303d52c8d005ab48

B∈Γ!B \in \Gamma

Read as: formula B belongs to Gamma

Means: formula B belongs to Gamma

3 occurrences in this chapter

Equation form expr-30ad8c81c3d0e812

Δn⊆Δn+1\Delta_n \subseteq \Delta_{n+1}

Read as: Delta sub n is a subset of Delta sub n plus one

Means: Delta sub n is a subset of Delta sub n plus one

1 occurrence in this chapter

Equation form expr-30b69708b13eee56

⊢Σ¬A\Proves[\Sigma] \lnot !A

Read as: not formula A is derivable in system Sigma

Means: not formula A is derivable in system Sigma

1 occurrence in this chapter

Equation form expr-3133f12a1b0bb324

□q\Box q

Read as: necessarily q

Means: necessarily q

2 occurrences in this chapter

Equation form expr-32c2feddae9b174c

□−1Δ1⊆Δ3\Box^{-1}\Delta_1 \subseteq \Delta_3

Read as: inverse box of Delta sub one is a subset of Delta sub three

Means: inverse box of Delta sub one is a subset of Delta sub three

3 occurrences in this chapter

Equation form expr-35532100af10fc85

¬(A∨B)∈Γ\lnot(!A \lor !B) \in \Gamma

Read as: not open scope, formula A or formula B, close scope belongs to Gamma

Means: not open scope, formula A or formula B, close scope belongs to Gamma

1 occurrence in this chapter

Equation form expr-357f4478de0d91bc

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

Read as: not necessarily not formula A belongs to Gamma

Means: not necessarily not formula A belongs to Gamma

3 occurrences in this chapter

Equation form expr-35cc429e34e2cbef

□A∈Δ\Box!A \in \Delta

Read as: necessarily formula A belongs to Delta

Means: necessarily formula A belongs to Delta

2 occurrences in this chapter

Equation form expr-376d5037f2a5b8b0

p0\Obj p_0

Read as: object p sub zero

Means: object p sub zero

2 occurrences in this chapter

Equation form expr-37e02cba85f6fde3

¬A∉Δ\lnot!A \notin \Delta

Read as: not formula A does not belong to Delta

Means: not formula A does not belong to Delta

1 occurrence in this chapter

Equation form expr-3883a6dab66f5e38

MΣ⊩□A[Δ]\mSat{M^\Sigma}{\Box!A}[\Delta]

Read as: necessarily formula A is true at Delta in canonical model M superscript Sigma

Means: necessarily formula A is true at Delta in canonical model M superscript Sigma

2 occurrences in this chapter

Equation form expr-39327257b76f418e

□−1Γ⊆Δ\Box^{-1}\Gamma \subseteq \Delta

Read as: inverse box of Gamma is a subset of Delta

Means: inverse box of Gamma is a subset of Delta

6 occurrences in this chapter

Equation form expr-39c3d5a5ec4b06af

⊆\subseteq

Read as: the subset relation

Means: the subset relation

1 occurrence in this chapter

Equation form expr-3ad64bd7e45fcb6f

MΣ\mModel{M^\Sigma}

Read as: canonical model M superscript Sigma

Means: canonical model M superscript Sigma

3 occurrences in this chapter

Equation form expr-3b990430aacb7e3c

□−1Γ⊢ΣA\Box^{-1}\Gamma \Proves[\Sigma] !A

Read as: inverse box of Gamma derives formula A in system Sigma

Means: inverse box of Gamma derives formula A in system Sigma

1 occurrence in this chapter

Equation form expr-3bc4cba3253c3643

Δ=⋃nΔn\Delta = \bigcup_n \Delta_n

Read as: Delta equals the union over n of Delta sub n

Means: Delta equals the union over n of Delta sub n

1 occurrence in this chapter

Equation form expr-3bd68a6b64e3d4de

p∈Δp \in \Delta

Read as: p belongs to Delta

Means: p belongs to Delta

1 occurrence in this chapter

Equation form expr-3c5592ed3a6cb02b

Γ⊢Σ⊥\Gamma \Proves[\Sigma] \lfalse

Read as: Gamma derives falsity in system Sigma

Means: Gamma derives falsity in system Sigma

1 occurrence in this chapter

Equation form expr-3d9fe517b7dd1821

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

Read as: possibly not formula A belongs to Gamma

Means: possibly not formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-3dba35030b73ce9f

□Γ={□B:B∈Γ}◇Γ={◇B:B∈Γ}and□−1Γ={B:□B∈Γ}◇−1Γ={B:◇B∈Γ}\Box\Gamma & = \Setabs{\Box !B}{!B \in \Gamma}\\ \Diamond\Gamma & = \Setabs{\Diamond !B}{!B \in \Gamma}\\ \intertext{and} \Box^{-1}\Gamma & = \Setabs{!B}{\Box !B \in \Gamma}\\ \Diamond^{-1}\Gamma & = \Setabs{!B}{\Diamond !B \in \Gamma}\\

Read as: Four set operations. Box Gamma is the set of all necessarily B such that B belongs to Gamma. Diamond Gamma is the set of all possibly B such that B belongs to Gamma. Inverse box Gamma is the set of all B such that necessarily B belongs to Gamma. Inverse diamond Gamma is the set of all B such that possibly B belongs to Gamma. End definitions.

Means: Four set operations. Box Gamma is the set of all necessarily B such that B belongs to Gamma. Diamond Gamma is the set of all possibly B such that B belongs to Gamma. Inverse box Gamma is the set of all B such that necessarily B belongs to Gamma. Inverse diamond Gamma is the set of all B such that possibly B belongs to Gamma. End definitions.

1 occurrence in this chapter

Equation form expr-3f96bc573087aa57

A∈Σ!A \in \Sigma

Read as: A belongs to Sigma

Means: A belongs to Sigma

2 occurrences in this chapter

Equation form expr-40e3d0834c1f189a

pn\Obj p_n

Read as: object p sub n

Means: object p sub n

1 occurrence in this chapter

Equation form expr-41c93211f03c19a7

◇A∈Δ2\Diamond!A \in \Delta_2

Read as: possibly formula A belongs to Delta sub two

Means: possibly formula A belongs to Delta sub two

1 occurrence in this chapter

Equation form expr-41d7106ce385e41c

◇Δ⊆Δ′\Diamond\Delta \subseteq \Delta'

Read as: diamond of Delta is a subset of Delta prime

Means: diamond of Delta is a subset of Delta prime

1 occurrence in this chapter

Equation form expr-448b797d96dfcae7

Δ′⊇□−1Δ\Delta' \supseteq \Box^{-1}\Delta

Read as: Delta prime is a superset of inverse box of Delta

Means: Delta prime is a superset of inverse box of Delta

1 occurrence in this chapter

Equation form expr-4727a2caac11f055

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

Read as: necessarily not formula A belongs to Gamma

Means: necessarily not formula A belongs to Gamma

1 occurrence in this chapter

Equation form expr-48fb58a9bfb800b8

Source-census fragment. Read the complete source formula tr053-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-4b08cdf41a2a1cff

◇A∈Δ′\Diamond!A \in \Delta'

Read as: possibly formula A belongs to Delta prime

Means: possibly formula A belongs to Delta prime

1 occurrence in this chapter

Equation form expr-4de128c51d992b48

¬A→(¬B→¬(A∨B))\lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))

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

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

1 occurrence in this chapter

Equation form expr-4de8bc0fc0d5e945

Σ⊢B1→(B2→⋯(Bn→A)⋯)\Sigma \Proves !B_1 \lif (!B_2 \lif \cdots (!B_n \lif !A)\cdots)

Read as: Sigma derives the nested conditional from B sub one, through B sub n, to formula A

Means: Sigma derives the nested conditional from B sub one, through B sub n, to formula A

1 occurrence in this chapter

Equation form expr-4e212811e292e554

KD⊢A\Log{KD} \Proves !A

Read as: logic K D derives formula A

Means: logic K D derives formula A

1 occurrence in this chapter

Equation form expr-512291a98ab87ad8

MΣ⊩A\mSat{M^\Sigma}{!A}

Read as: formula A is true throughout canonical model M superscript Sigma

Means: formula A is true throughout canonical model M superscript Sigma

3 occurrences in this chapter

Equation form expr-52bb5adcf016a8a2

Γ⊬Σ⊥\Gamma \Proves/[\Sigma] \lfalse

Read as: Gamma does not derive falsity in system Sigma

Means: Gamma does not derive falsity in system Sigma

1 occurrence in this chapter

Equation form expr-52cba2e1bcfcb7e1

□−1Δ\Box^{-1}\Delta

Read as: inverse box of Delta

Means: inverse box of Delta

2 occurrences in this chapter

Equation form expr-5373e78c1dbea479

A,¬A⊢Σ⊥!A, \lnot !A \Proves[\Sigma] \lfalse

Read as: formula A, then not formula A derives falsity in system Sigma

Means: formula A, then not formula A derives falsity in system Sigma

1 occurrence in this chapter

Equation form expr-542de1299c1c558f

Δn\Delta_n

Read as: Delta sub n

Means: Delta sub n

9 occurrences in this chapter

Equation form expr-558ed8e1dbcc1ff9

¬B∈Δ\lnot !B \in \Delta

Read as: not formula B belongs to Delta

Means: not formula B belongs to Delta

1 occurrence in this chapter

Equation form expr-566393d2bb270223

VΣV^\Sigma

Read as: V superscript Sigma

Means: V superscript Sigma

3 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

33 occurrences in this chapter

Equation form expr-5a4e473ba66a5719

Δn∪{¬An}\Delta_n \cup \{\lnot!A_n\}

Read as: Delta sub n union the set containing not formula A sub n

Means: Delta sub n union the set containing not formula A sub n

2 occurrences in this chapter

Equation form expr-5a66b0f10043619c

¬A∉Δ\lnot !A \notin \Delta

Read as: not formula A does not belong to Delta

Means: not formula A does not belong to Delta

1 occurrence in this chapter

Equation form expr-5b6b43bf45a3e801

A∈Δ′!A \in \Delta'

Read as: formula A belongs to Delta prime

Means: formula A belongs to Delta prime

2 occurrences in this chapter

Equation form expr-5be57c59c7ae840c

Δ∈VΣ(p)\Delta \in V^\Sigma(p)

Read as: Delta belongs to valuation V superscript Sigma applied to p

Means: Delta belongs to valuation V superscript Sigma applied to p

2 occurrences in this chapter

Equation form expr-5d3c44d3ef3eaef1

MΣ⊮⊥[Δ]\mSat/{M^\Sigma}{\lfalse}[\Delta]

Read as: falsity is false at Delta in canonical model M superscript Sigma

Means: falsity is false at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-5e585fb8dfd9f7c9

Γ⊆Δ\Gamma \subseteq \Delta

Read as: Gamma is a subset of Delta

Means: Gamma is a subset of Delta

2 occurrences in this chapter

Equation form expr-5fd81597df9955a1

A∈Δ2!A \in \Delta_2

Read as: formula A belongs to Delta sub two

Means: formula A belongs to Delta sub two

1 occurrence in this chapter

Equation form expr-5febb4c83117b8cc

A∧B∈Γ!A \land !B \in \Gamma

Read as: formula A and formula B belongs to Gamma

Means: formula A and formula B belongs to Gamma

1 occurrence 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

1 occurrence in this chapter

Equation form expr-620ba2e83ca9d35d

□□−1Γ⊆Γ\Box\Box^{-1}\Gamma \subseteq \Gamma

Read as: box of inverse box of Gamma is a subset of Gamma

Means: box of inverse box of Gamma is a subset of Gamma

2 occurrences in this chapter

Equation form expr-62c7a709b84474b7

□−1Γ⊢ΣA\Box^{-1} \Gamma \Proves[\Sigma] !A

Read as: inverse box of Gamma derives formula A in system Sigma

Means: inverse box of Gamma derives formula A in system Sigma

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-65fb0d7eff50b8e8

Ai!A_i

Read as: formula A sub i

Means: formula A sub i

1 occurrence in this chapter

Equation form expr-676290a598449163

◇Δ⊆Γ\Diamond\Delta \subseteq \Gamma

Read as: diamond of Delta is a subset of Gamma

Means: diamond of Delta is a subset of Gamma

5 occurrences in this chapter

Equation form expr-68af1b29d5f49fb3

Σ⊢A\Sigma \Proves !A

Read as: Sigma derives formula A

Means: Sigma derives formula A

5 occurrences in this chapter

Equation form expr-6925ff9b79df9b04

RΣR^\Sigma

Read as: accessibility relation R superscript Sigma

Means: accessibility relation R superscript Sigma

7 occurrences in this chapter

Equation form expr-6b517f4943be1156

A1,…,An,◇B1,…,◇Bm⊢Σ⊥.!A_1, \dots, !A_n, \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse.

Read as: Formulas A sub one through A sub n, together with possibly B sub one through possibly B sub m, derive falsity in system Sigma.

Means: Formulas A sub one through A sub n, together with possibly B sub one through possibly B sub m, derive falsity in system Sigma.

1 occurrence in this chapter

Equation form expr-6c0afc00dfb2052c

KT⊢A\Log{KT} \Proves !A

Read as: logic K T derives formula A

Means: logic K T derives formula A

1 occurrence in this chapter

Equation form expr-6c0b4ab8dd399bba

Δ2\Delta_2

Read as: Delta sub two

Means: Delta sub two

2 occurrences in this chapter

Equation form expr-6c9be074f40bb058

□◇A∈Δ1\Box\Diamond!A \in \Delta_1

Read as: necessarily possibly formula A belongs to Delta sub one

Means: necessarily possibly formula A belongs to Delta sub one

1 occurrence in this chapter

Equation form expr-6d3a5561e6bca52b

KA1…An\Log{K}!A_1 \dots !A_n

Read as: logic K extended by schemas A sub one through A sub n

Means: logic K extended by schemas A sub one through A sub n

1 occurrence in this chapter

Equation form expr-6e345e1b8268b8d3

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

Read as: possibly formula A implies necessarily formula A

Means: possibly formula A implies necessarily formula A

1 occurrence in this chapter

Equation form expr-6e8fc099e44743b7

◇Δ3⊆Δ2\Diamond\Delta_3 \subseteq \Delta_2

Read as: diamond of Delta sub three is a subset of Delta sub two

Means: diamond of Delta sub three is a subset of Delta sub two

1 occurrence in this chapter

Equation form expr-6f8d58cb216b0769

□¬A∉Γ\Box\lnot!A \notin \Gamma

Read as: necessarily not formula A does not belong to Gamma

Means: necessarily not formula A does not belong to Gamma

2 occurrences in this chapter

Equation form expr-70d9153e6917b852

Δ=⋃n=0∞Δn\Delta = \bigcup_{n=0}^\infty \Delta_n

Read as: Delta equals the union of Delta sub n for n from zero to infinity

Means: Delta equals the union of Delta sub n for n from zero to infinity

2 occurrences in this chapter

Equation form expr-70fe91788a0dc965

Δ⊢Σ¬◇⊥\Delta \Proves[\Sigma] \lnot\Diamond \lfalse

Read as: Delta derives not possibly falsity in system Sigma

Means: Delta derives not possibly falsity in system Sigma

1 occurrence in this chapter

Equation form expr-713c4dda1279e009

□¬A∉Γ\Box\lnot !A \notin \Gamma

Read as: necessarily not formula A does not belong to Gamma

Means: necessarily not formula A does not belong to Gamma

2 occurrences in this chapter

Equation form expr-728beaa575a52447

□A∈Δ iff A∈Δ′ for all Δ′ with RΣΔΔ′\Box!A \in \Delta \text{ iff } !A \in \Delta' \text{ for all $\Delta'$ with } R^\Sigma\Delta\Delta'

Read as: Necessarily A belongs to Delta if and only if A belongs to every Delta prime accessible from Delta under relation R superscript Sigma.

Means: Necessarily A belongs to Delta if and only if A belongs to every Delta prime accessible from Delta under relation R superscript Sigma.

1 occurrence in this chapter

Equation form expr-73adaeb66edc4321

A→B∈Γ!A \lif !B \in \Gamma

Read as: formula A implies formula B belongs to Gamma

Means: formula A implies formula B belongs to Gamma

1 occurrence in this chapter

Equation form expr-753bc8d1d11a097f

Δ⊢Σ□⊥\Delta \Proves[\Sigma] \Box\lfalse

Read as: Delta derives necessarily falsity in system Sigma

Means: Delta derives necessarily falsity in system Sigma

1 occurrence in this chapter

Equation form expr-76460d6a72c5d8a9

A⊬Σ⊥!A \Proves/[\Sigma] \lfalse

Read as: formula A does not derive falsity in system Sigma

Means: formula A does not derive falsity in system Sigma

1 occurrence in this chapter

Equation form expr-77a747d2fe347770

Δ⊢Σ◇⊥\Delta \Proves[\Sigma] \Diamond\lfalse

Read as: Delta derives possibly falsity in system Sigma

Means: Delta derives possibly falsity in system Sigma

1 occurrence in this chapter

Equation form expr-77eda7eb9341aab6

□−1Δ⊆Δ′\Box^{-1}\Delta \subseteq \Delta'

Read as: inverse box of Delta is a subset of Delta prime

Means: inverse box of Delta is a subset of Delta prime

3 occurrences in this chapter

Equation form expr-7a251d077fd31d23

Γ∪{¬A}\Gamma \cup \{ \lnot!A\}

Read as: Gamma union the set containing not formula A

Means: Gamma union the set containing not formula A

1 occurrence in this chapter

Equation form expr-7a8ef5bfa4b7347d

A∉Γ!A \notin \Gamma

Read as: formula A does not belong to Gamma

Means: formula A does not belong to Gamma

6 occurrences in this chapter

Equation form expr-7b36863358791434

⊥∉Γ\lfalse \notin \Gamma

Read as: falsity does not belong to Gamma

Means: falsity does not belong to Gamma

1 occurrence in this chapter

Equation form expr-7bbacdf9cf42c651

Δ3⊆Δ2\Delta_3 \subseteq \Delta_2

Read as: Delta sub three is a subset of Delta sub two

Means: Delta sub three is a subset of Delta sub two

1 occurrence in this chapter

Equation form expr-7c0fc4915d9f04cb

n≥1n \ge 1

Read as: n is greater than or equal to one

Means: n is greater than or equal to one

1 occurrence in this chapter

Equation form expr-7c3db8ee830f2923

□−1Δ⊆Δ′\Box^{-1} \Delta \subseteq \Delta'

Read as: inverse box of Delta is a subset of Delta prime

Means: inverse box of Delta is a subset of Delta prime

1 occurrence in this chapter

Equation form expr-7ce66658ceef4b93

Δn+1\Delta_{n+1}

Read as: Delta sub n plus one

Means: Delta sub n plus one

4 occurrences in this chapter

Equation form expr-7dda9c60146c33f0

A∈□−1Γ⊆Δ!A \in \Box^{-1}\Gamma \subseteq \Delta

Read as: formula A belongs to inverse box Gamma, which is a subset of Delta

Means: formula A belongs to inverse box Gamma, which is a subset of Delta

1 occurrence in this chapter

Equation form expr-7e9aa09e150317ae

Γ⊬Σ□A\Gamma \Proves/[\Sigma] \Box !A

Read as: Gamma does not derive necessarily formula A in system Sigma

Means: Gamma does not derive necessarily formula A in system Sigma

1 occurrence in this chapter

Equation form expr-8039022c0b3fca47

Δn+1={Δn∪{An},if Δn∪{An} is Σ-consistent;Δn∪{¬An},otherwise.\Delta_{n+1} = \begin{cases} \Delta_n \cup \{!A_n\}, & \text{if $\Delta_n \cup \{ !A_n\}$ is $\Sigma$-consistent;} \\ \Delta_n \cup \{ \lnot !A_n\}, & \text{otherwise.} \end{cases}

Read as: Delta sub n plus one equals Delta sub n union the singleton containing formula A sub n, if that union is Sigma consistent; otherwise it equals Delta sub n union the singleton containing not A sub n. End cases.

Means: Delta sub n plus one equals Delta sub n union the singleton containing formula A sub n, if that union is Sigma consistent; otherwise it equals Delta sub n union the singleton containing not A sub n. End cases.

1 occurrence in this chapter

Equation form expr-80d983751d4ab89e

□−1Γ⊬ΣA\Box^{-1}\Gamma \Proves/[\Sigma] !A

Read as: inverse box of Gamma does not derive formula A in system Sigma

Means: inverse box of Gamma does not derive formula A in system Sigma

1 occurrence in this chapter

Equation form expr-81f3d4faf9b10085

□B∈Δ1\Box!B \in \Delta_1

Read as: necessarily formula B belongs to Delta sub one

Means: necessarily formula B belongs to Delta sub one

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: formula A

Means: formula A

30 occurrences in this chapter

Equation form expr-8342026c86fe60d2

◇A∈◇Δ\Diamond!A \in \Diamond\Delta

Read as: possibly formula A belongs to diamond of Delta

Means: possibly formula A belongs to diamond of Delta

1 occurrence in this chapter

Equation form expr-83e917e2ef07faf6

Γ⊢Σ□A\Gamma \Proves[\Sigma] \Box!A

Read as: Gamma derives necessarily formula A in system Sigma

Means: Gamma derives necessarily formula A in system Sigma

2 occurrences in this chapter

Equation form expr-84de8417fb7b0649

K⊬A\Log{K} \Proves/ !A

Read as: logic K does not derive formula A

Means: logic K does not derive formula A

1 occurrence in this chapter

Equation form expr-85c3ce29e3a4dc40

C\mClass{C}

Read as: class C

Means: class C

1 occurrence in this chapter

Equation form expr-86b6f340d70db4ad

MΣ⊮B[Δ]\mSat/{M^\Sigma}{!B}[\Delta]

Read as: formula B is false at Delta in canonical model M superscript Sigma

Means: formula B is false at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-88d87f02667745cc

B∈Δ′!B \in \Delta'

Read as: formula B belongs to Delta prime

Means: formula B belongs to Delta prime

3 occurrences in this chapter

Equation form expr-8b3ab3c6e27b1d3e

□Bk∈□Γ\Box!B_k \in \Box\Gamma

Read as: necessarily formula B sub k belongs to box of Gamma

Means: necessarily formula B sub k belongs to box of Gamma

1 occurrence in this chapter

Equation form expr-8b67dbfa2d13cc63

Σ⊆Γ\Sigma \subseteq \Gamma

Read as: Sigma is a subset of Gamma

Means: Sigma is a subset of Gamma

1 occurrence in this chapter

Equation form expr-8dffb88f67702d91

□Γ\Box\Gamma

Read as: box of Gamma

Means: box of Gamma

1 occurrence in this chapter

Equation form expr-8e35c2cd3bf6641b

qq

Read as: q

Means: q

1 occurrence in this chapter

Equation form expr-903d52c30476fc27

Γ⊬ΣA\Gamma \Proves/[\Sigma] !A

Read as: Gamma does not derive formula A in system Sigma

Means: Gamma does not derive formula A in system Sigma

1 occurrence in this chapter

Equation form expr-906d092b22f3802f

MΣ⊩¬B[Δ]\mSat{M^\Sigma}{\lnot !B}[\Delta]

Read as: not formula B is true at Delta in canonical model M superscript Sigma

Means: not formula B is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-90b7cf92cfed3ff9

RΣΔΔ′R^\Sigma \Delta\Delta'

Read as: Delta prime is accessible from Delta under accessibility relation R superscript Sigma

Means: Delta prime is accessible from Delta under accessibility relation R superscript Sigma

10 occurrences in this chapter

Equation form expr-913b3549cac3565b

RΣΔΔ′R^\Sigma\Delta\Delta'

Read as: Delta prime is accessible from Delta under accessibility relation R superscript Sigma

Means: Delta prime is accessible from Delta under accessibility relation R superscript Sigma

3 occurrences in this chapter

Equation form expr-913fa03cdeb2fcc1

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

Read as: necessarily necessarily formula A implies necessarily formula A

Means: necessarily necessarily formula A implies necessarily formula A

1 occurrence in this chapter

Equation form expr-91d76359805e41c4

RΣΔ3Δ2R^\Sigma \Delta_3\Delta_2

Read as: Delta sub two is accessible from Delta sub three under accessibility relation R superscript Sigma

Means: Delta sub two is accessible from Delta sub three under accessibility relation R superscript Sigma

2 occurrences in this chapter

Equation form expr-9213992d38bd529d

Γ=∅\Gamma = \emptyset

Read as: Gamma equals the empty set

Means: Gamma equals the empty set

2 occurrences in this chapter

Equation form expr-928897204ff28dd5

A0!A_0

Read as: formula A sub zero

Means: formula A sub zero

1 occurrence in this chapter

Equation form expr-928debc5fdadd664

◇Δ2⊆Δ3\Diamond\Delta_2 \subseteq \Delta_3

Read as: diamond of Delta sub two is a subset of Delta sub three

Means: diamond of Delta sub two is a subset of Delta sub three

1 occurrence in this chapter

Equation form expr-93cc589544d72405

B∈□−1Δ1!B \in \Box^{-1}\Delta_1

Read as: formula B belongs to inverse box of Delta sub one

Means: formula B belongs to inverse box of Delta sub 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-945331a2b90d4f05

□−1Γ⊆Δ\Box^{-1} \Gamma \subseteq \Delta

Read as: inverse box of Gamma is a subset of Delta

Means: inverse box of Gamma is a subset of Delta

1 occurrence in this chapter

Equation form expr-94cdffa86512c7ad

□An∈Δ1\Box!A_n \in \Delta_1

Read as: necessarily formula A sub n belongs to Delta sub one

Means: necessarily formula A sub n belongs to Delta sub one

1 occurrence in this chapter

Equation form expr-9590b9e353fb7eda

□−1Δ′⊆Δ\Box^{-1}\Delta' \subseteq \Delta

Read as: inverse box of Delta prime is a subset of Delta

Means: inverse box of Delta prime is a subset of Delta

1 occurrence in this chapter

Equation form expr-95ac943187f79bf8

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

Read as: necessarily necessarily formula A implies necessarily formula A

Means: necessarily necessarily formula A implies necessarily formula A

1 occurrence in this chapter

Equation form expr-97bca6203ba27774

Σ⊢□B1→(□B2→⋯(□Bn→□A)⋯)\Sigma \Proves \Box!B_1 \lif (\Box!B_2 \lif \cdots (\Box!B_n \lif \Box!A)\cdots)

Read as: Sigma derives the nested conditional from necessarily B sub one, through necessarily B sub n, to necessarily A

Means: Sigma derives the nested conditional from necessarily B sub one, through necessarily B sub n, to necessarily A

1 occurrence in this chapter

Equation form expr-992accb9917efeb5

C!C

Read as: formula C

Means: formula C

1 occurrence in this chapter

Equation form expr-998ec2fa4bd367ab

Δni⊆Δn\Delta_{n_i} \subseteq \Delta_n

Read as: Delta sub n sub i is a subset of Delta sub n

Means: Delta sub n sub i is a subset of Delta sub n

1 occurrence in this chapter

Equation form expr-9a44b9bb01db1eac

Δ⊢ΣA\Delta \Proves[\Sigma] !A

Read as: Delta derives formula A in system Sigma

Means: Delta derives formula A in system Sigma

1 occurrence in this chapter

Equation form expr-9a45de08a8324a70

B∈Δ3!B \in \Delta_3

Read as: formula B belongs to Delta sub three

Means: formula B belongs to Delta sub three

1 occurrence in this chapter

Equation form expr-9af20c45554404c8

¬A∈Γ\lnot !A \in \Gamma

Read as: not formula A belongs to Gamma

Means: not formula A belongs to Gamma

2 occurrences in this chapter

Equation form expr-9d39ba7a73f050ea

MΣ⊩A[Δ]\mSat{M^\Sigma}{!A}[\Delta]

Read as: formula A is true at Delta in canonical model M superscript Sigma

Means: formula A is true at Delta in canonical model M superscript Sigma

6 occurrences in this chapter

Equation form expr-a0199483db5ee219

MΣ⊩◇A[Δ]\mSat{M^\Sigma}{\Diamond !A}[\Delta]

Read as: possibly formula A is true at Delta in canonical model M superscript Sigma

Means: possibly formula A is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-a0cbb5b30ceb8f09

A∈Δ!A \in \Delta

Read as: formula A belongs to Delta

Means: formula A belongs to Delta

17 occurrences in this chapter

Equation form expr-a10d1e8bd329c89a

Γ∪{¬A}\Gamma \cup \{ \lnot!A \}

Read as: Gamma union the set containing not formula A

Means: Gamma union the set containing not formula A

1 occurrence in this chapter

Equation form expr-a11890c971449806

Ai∈Γ!A_i \in \Gamma

Read as: formula A sub i belongs to Gamma

Means: formula A sub i belongs to Gamma

1 occurrence in this chapter

Equation form expr-a158c8ba25884247

K⊢A\Log{K} \Proves !A

Read as: logic K derives formula A

Means: logic K derives formula A

2 occurrences in this chapter

Equation form expr-a1b8bafb53c619e2

A1→(A2→⋯(An→⊥)…)!A_1 \lif (!A_2 \lif \cdots (!A_n \lif \lfalse)\dots)

Read as: the nested conditional from A sub one, through A sub n, to falsity

Means: the nested conditional from A sub one, through A sub n, to falsity

1 occurrence 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

3 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

2 occurrences in this chapter

Equation form expr-a5ca9cc1e5d44325

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

Read as: possibly formula A implies necessarily formula A

Means: possibly formula A implies necessarily formula A

1 occurrence in this chapter

Equation form expr-a5effb8a9169bbe5

□−1Δ⊢Σ⊥\Box^{-1}\Delta \Proves[\Sigma] \lfalse

Read as: inverse box of Delta derives falsity in system Sigma

Means: inverse box of Delta derives falsity in system Sigma

1 occurrence in this chapter

Equation form expr-a7ca37f41ba5c76e

¬A∈Γ\lnot!A \in \Gamma

Read as: not formula A belongs to Gamma

Means: not formula A belongs to Gamma

4 occurrences in this chapter

Equation form expr-a84959a753d82ca7

M⊮A\mSat/{M}{!A}

Read as: formula A is not true throughout model M

Means: formula A is not true throughout model M

1 occurrence in this chapter

Equation form expr-ae4ee6e1b0bed029

A∈Δ3!A \in \Delta_3

Read as: formula A belongs to Delta sub three

Means: formula A belongs to Delta sub three

2 occurrences in this chapter

Equation form expr-ae50884201122a48

nin_i

Read as: n sub i

Means: n sub i

1 occurrence in this chapter

Equation form expr-af060e3443a37e5e

Δ0=Γ\Delta_0 = \Gamma

Read as: Delta sub zero equals Gamma

Means: Delta sub zero equals Gamma

3 occurrences in this chapter

Equation form expr-b0b1441f25249633

CT\mClass{C}_\Ax{T}

Read as: class C subscript axiom T

Means: class C subscript axiom T

1 occurrence in this chapter

Equation form expr-b41e1ea100e03325

□−1Γ∪{¬A}\Box^{-1}\Gamma \cup \{ \lnot!A \}

Read as: inverse box of Gamma union the set containing not formula A

Means: inverse box of Gamma union the set containing not formula A

1 occurrence in this chapter

Equation form expr-b543558e91ea2d61

S5=KT5=KTB4\Log{S5} = \Log{KT5} = \Log{KTB4}

Read as: logic S five equals logic K T five, which equals logic K T B four

Means: logic S five equals logic K T five, which equals logic K T B four

1 occurrence in this chapter

Equation form expr-b5dd791ec61bb16b

C∈Δ!C \in \Delta

Read as: formula C belongs to Delta

Means: formula C belongs to Delta

1 occurrence in this chapter

Equation form expr-b7fe41fa9485a352

Σ⊢A1→(A2→⋯(Ak→⊥)…)\Sigma \Proves !A_1 \lif (!A_2 \lif \cdots (!A_k \lif \lfalse)\dots)

Read as: Sigma derives the nested conditional from A sub one, through A sub k, to falsity

Means: Sigma derives the nested conditional from A sub one, through A sub k, to falsity

1 occurrence in this chapter

Equation form expr-bc9367794d2761fe

A∈Γ!A \in \Gamma

Read as: formula A belongs to Gamma

Means: formula A belongs to Gamma

7 occurrences in this chapter

Equation form expr-bd7a4ecf85446cc1

◇A∈Δ1\Diamond!A \in \Delta_1

Read as: possibly formula A belongs to Delta sub one

Means: possibly formula A belongs to Delta sub one

2 occurrences in this chapter

Equation form expr-bfb7070e82d9a0ad

Ai∈Δni!A_i \in \Delta_{n_i}

Read as: formula A sub i belongs to Delta sub n sub i

Means: formula A sub i belongs to Delta sub n sub i

1 occurrence in this chapter

Equation form expr-c0736f3100cb23f9

VΣ(p)={Δ:p∈Δ}V^\Sigma(p) = \Setabs{\Delta}{p \in \Delta}

Read as: valuation V superscript Sigma applied to p equals the set of Delta such that p belongs to Delta

Means: valuation V superscript Sigma applied to p equals the set of Delta such that p belongs to Delta

1 occurrence in this chapter

Equation form expr-c0d811ecf4e44efe

Σ⊬Σ¬A\Sigma \Proves/[\Sigma] \lnot !A

Read as: Sigma does not derive not formula A in system Sigma

Means: Sigma does not derive not formula A in system Sigma

1 occurrence in this chapter

Equation form expr-c14f3e62402337ae

MΣ⊩B[Δ′]\mSat{M^\Sigma}{!B}[\Delta']

Read as: formula B is true at Delta prime in canonical model M superscript Sigma

Means: formula B is true at Delta prime in canonical model M superscript Sigma

3 occurrences in this chapter

Equation form expr-c401325aafc4a85c

⊬¬A\Proves/ \lnot !A

Read as: not formula A is not derivable

Means: not formula A is not derivable

1 occurrence in this chapter

Equation form expr-c5195990e900aa5f

B∉Γ!B \notin \Gamma

Read as: formula B does not belong to Gamma

Means: formula B does not belong to Gamma

1 occurrence in this chapter

Equation form expr-c61e162bee4d9ef8

⊬A\Proves/ !A

Read as: formula A is not derivable

Means: formula A is not derivable

1 occurrence in this chapter

Equation form expr-c6293af8feb4b700

MΣ⊩C[Δ]\mSat{M^\Sigma}{!C}[\Delta]

Read as: formula C is true at Delta in canonical model M superscript Sigma

Means: formula C is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-c6acca37804b6eac

MΣ⊩B∨C[Δ]\mSat{M^\Sigma}{!B \lor !C}[\Delta]

Read as: formula B or formula C is true at Delta in canonical model M superscript Sigma

Means: formula B or formula C is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-c7d083471edaf049

⊢A\Proves !A

Read as: formula A is derivable

Means: formula A is derivable

1 occurrence in this chapter

Equation form expr-c86b5996e85dab89

Δn⊢Σ⊥\Delta_n \Proves[\Sigma] \lfalse

Read as: Delta sub n derives falsity in system Sigma

Means: Delta sub n derives falsity in system Sigma

1 occurrence in this chapter

Equation form expr-c92929a4021dba21

⊥∉Δ\lfalse \notin \Delta

Read as: falsity does not belong to Delta

Means: falsity does not belong to Delta

1 occurrence in this chapter

Equation form expr-c98ab9783dd0099b

□−1Γ\Box^{-1}\Gamma

Read as: inverse box of Gamma

Means: inverse box of Gamma

1 occurrence in this chapter

Equation form expr-c99941201027b5be

Γ⊢ΣA\Gamma \Proves[\Sigma] !A

Read as: Gamma derives formula A in system Sigma

Means: Gamma derives formula A in system Sigma

7 occurrences in this chapter

Equation form expr-cac764c57e861563

RΣΔΔR^\Sigma \Delta\Delta

Read as: Delta is accessible from Delta under accessibility relation R superscript Sigma

Means: Delta is accessible from Delta under accessibility relation R superscript Sigma

1 occurrence in this chapter

Equation form expr-caccbd5582611a49

□−1Γ∪{¬A}⊆Δ\Box^{-1}\Gamma \cup \{ \lnot!A \} \subseteq \Delta

Read as: inverse box of Gamma union the set containing not formula A is a subset of Delta

Means: inverse box of Gamma union the set containing not formula A is a subset of Delta

1 occurrence in this chapter

Equation form expr-cada9c4703ed290d

CD\mClass{C}_\Ax{D}

Read as: class C subscript axiom D

Means: class C subscript axiom D

1 occurrence in this chapter

Equation form expr-cca831e62fbffb72

□B∈Δ\Box !B \in \Delta

Read as: necessarily formula B belongs to Delta

Means: necessarily formula B belongs to Delta

3 occurrences in this chapter

Equation form expr-cf3db3ac2a0ea13f

RΣΔ1Δ3R^\Sigma \Delta_1\Delta_3

Read as: Delta sub three is accessible from Delta sub one under accessibility relation R superscript Sigma

Means: Delta sub three is accessible from Delta sub one under accessibility relation R superscript Sigma

8 occurrences in this chapter

Equation form expr-d027c6d7fe6f3a89

Δ3\Delta_3

Read as: Delta sub three

Means: Delta sub three

2 occurrences in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: formula B

Means: formula B

1 occurrence in this chapter

Equation form expr-d074674a87a1e992

Δn∪{An}\Delta_n \cup \{!A_n\}

Read as: Delta sub n union the set containing formula A sub n

Means: Delta sub n union the set containing formula A sub n

2 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

2 occurrences in this chapter

Equation form expr-d4080d70be336d28

◇¬A\Diamond\lnot!A

Read as: possibly not formula A

Means: possibly not formula A

1 occurrence in this chapter

Equation form expr-d654261bbde41149

MΣ⊩□B[Δ]\mSat{M^\Sigma}{\Box !B}[\Delta]

Read as: necessarily formula B is true at Delta in canonical model M superscript Sigma

Means: necessarily formula B is true at Delta in canonical model M superscript Sigma

2 occurrences in this chapter

Equation form expr-d65d75b1e6562713

Σ\Sigma

Read as: Sigma

Means: Sigma

112 occurrences in this chapter

Equation form expr-d7c89d8cc8001366

MΣ⊩□A[Δ]\mSat{M^\Sigma}{\Box !A}[\Delta]

Read as: necessarily formula A is true at Delta in canonical model M superscript Sigma

Means: necessarily formula A is true at Delta in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-d8ad952cd59fb203

RΣΔ1Δ2R^\Sigma \Delta_1\Delta_2

Read as: Delta sub two is accessible from Delta sub one under accessibility relation R superscript Sigma

Means: Delta sub two is accessible from Delta sub one under accessibility relation R superscript Sigma

5 occurrences in this chapter

Equation form expr-d99b498a81da6362

Δ′\Delta'

Read as: Delta prime

Means: Delta prime

7 occurrences in this chapter

Equation form expr-ddc61c8bc545f767

CB\mClass{C}_\Ax{B}

Read as: class C subscript axiom B

Means: class C subscript axiom B

1 occurrence in this chapter

Equation form expr-de194039b1a281e4

□◇A∈Δ\Box\Diamond!A \in \Delta

Read as: necessarily possibly formula A belongs to Delta

Means: necessarily possibly formula A belongs to Delta

1 occurrence in this chapter

Equation form expr-de64372991421159

An!A_n

Read as: formula A sub n

Means: formula A sub n

3 occurrences in this chapter

Equation form expr-dffa227108b65500

A1!A_1

Read as: formula A sub one

Means: formula A sub one

3 occurrences in this chapter

Equation form expr-e0cf3b4897f9cb5b

Δn⊆Δ\Delta_n \subseteq \Delta

Read as: Delta sub n is a subset of Delta

Means: Delta sub n is a subset of Delta

1 occurrence in this chapter

Equation form expr-e0e4140dca1f032f

Δ0⊆Δ\Delta_0 \subseteq \Delta

Read as: Delta sub zero is a subset of Delta

Means: Delta sub zero is a subset of Delta

1 occurrence in this chapter

Equation form expr-e110691703b850f5

A1,…,An,◇B1,…,◇Bm⊢Σ⊥A1,…,An⊢Σ(◇B1∧…∧◇Bm)→⊥by the deduction theoremthe proposition on derivability factsthe deduction-theorem clause of the derivability facts, and tautA1,…,An⊢Σ◇(B1∧…∧Bm)→⊥since Σ is normalA1,…,An⊢Σ¬◇(B1∧…∧Bm)by plA1,…,An⊢Σ□¬(B1∧…∧Bm)□¬ for ¬◇□A1,…,□An⊢Σ□□¬(B1∧…∧Bm)by the lemma lifting a derivation into boxed premises and conclusion□A1,…,□An⊢Σ□¬(B1∧…∧Bm)by schema □□A→□AΔ1⊢Σ□¬(B1∧…∧Bm)by monotonicity, the proposition on derivability factsthe monotonicity clause of the derivability facts□¬(B1∧…∧Bm)∈Δ1by deductive closure;¬(B1∧…∧Bm)∈Δ2since RΣΔ1Δ2.!A_1, \dots, !A_n, & \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse \\ !A_1, \dots,!A_n & \Proves[\Sigma] (\Diamond!B_1 \land \dots \land \Diamond!B_m) \lif \lfalse\\ & \qquad\text{by the deduction theorem}\\ & \qquad\text{\olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-deduction}, and \Taut} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Diamond(!B_1 \land \dots \land !B_m) \lif \lfalse\\ & \qquad \text{since $\Sigma$ is normal} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \lnot\Diamond (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \PL} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{$\Box\lnot$ for $\lnot\Diamond$} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\Box \lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \olref[mod]{lem:box1}} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by schema $\Box\Box!A \lif \Box!A$} \\ \Delta_1 & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by monotonicity, \olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-monotonicity}} \\ & \Box\lnot (!B_1 \land \dots \land !B_m) \in \Delta_1\\ &\qquad\text{by deductive closure}; \\ & \lnot (!B_1 \land \dots \land !B_m) \in \Delta_2\\ &\qquad \text{since } R^\Sigma \Delta_1\Delta_2.

Read as: Displayed derivation. Formulas A sub one through A sub n, together with possibly B sub one through possibly B sub m, derive falsity in Sigma. By the deduction theorem, the proposition on derivability facts, the deduction-theorem clause of the derivability facts, and tautology, the A formulas derive that the conjunction of possibly B sub one through possibly B sub m implies falsity. Normality converts this to the necessity of the negation of the conjunction of B sub one through B sub m. The lemma lifting a derivation into boxed premises and conclusion licenses the boxed step. Using the schema if necessarily necessarily A then necessarily A yields that Delta sub one derives that necessary negation. By monotonicity, the proposition on derivability facts and the monotonicity clause of the derivability facts preserve that derivation. Deductive closure puts the necessary negation in Delta sub one. Accessibility from Delta sub one to Delta sub two then puts the negation of the conjunction of B sub one through B sub m in Delta sub two. End displayed derivation.

Means: Displayed derivation. Formulas A sub one through A sub n, together with possibly B sub one through possibly B sub m, derive falsity in Sigma. By the deduction theorem, the proposition on derivability facts, the deduction-theorem clause of the derivability facts, and tautology, the A formulas derive that the conjunction of possibly B sub one through possibly B sub m implies falsity. Normality converts this to the necessity of the negation of the conjunction of B sub one through B sub m. The lemma lifting a derivation into boxed premises and conclusion licenses the boxed step. Using the schema if necessarily necessarily A then necessarily A yields that Delta sub one derives that necessary negation. By monotonicity, the proposition on derivability facts and the monotonicity clause of the derivability facts preserve that derivation. Deductive closure puts the necessary negation in Delta sub one. Accessibility from Delta sub one to Delta sub two then puts the negation of the conjunction of B sub one through B sub m in Delta sub two. End displayed derivation.

1 occurrence in this chapter

Equation form expr-e198acb55e2764a4

B∉Δ!B \notin \Delta

Read as: formula B does not belong to Delta

Means: formula B does not belong to Delta

1 occurrence in this chapter

Equation form expr-e2d470606de3d2ba

MΣ⊩A[Δ′]\mSat{M^\Sigma}{!A}[\Delta']

Read as: formula A is true at Delta prime in canonical model M superscript Sigma

Means: formula A is true at Delta prime in canonical model M superscript Sigma

1 occurrence in this chapter

Equation form expr-e300db42c973d40e

¬An\lnot !A_n

Read as: not formula A sub n

Means: not formula A sub n

1 occurrence in this chapter

Equation form expr-e43f050ae499c6a4

□Γ⊢Σ□A\Box\Gamma \Proves[\Sigma] \Box !A

Read as: box of Gamma derives necessarily formula A in system Sigma

Means: box of Gamma derives necessarily formula A in system Sigma

2 occurrences in this chapter

Equation form expr-e6f75a19dd339775

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

Read as: possibly formula A implies necessarily possibly formula A

Means: possibly formula A implies necessarily possibly formula A

1 occurrence in this chapter

Equation form expr-e78a1414699d2dfc

A∨B∈Γ!A \lor !B \in \Gamma

Read as: formula A or formula B belongs to Gamma

Means: formula A or formula B belongs to Gamma

2 occurrences in this chapter

Equation form expr-e845fe04f824da71

¬A∈Δ\lnot !A \in \Delta

Read as: not formula A belongs to Delta

Means: not formula A belongs to Delta

1 occurrence in this chapter

Equation form expr-e8cc70bcf82d09b2

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

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

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

1 occurrence in this chapter

Equation form expr-ead54b4f96a9f7ff

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

Read as: necessarily formula A implies possibly formula A

Means: necessarily formula A implies possibly formula A

1 occurrence in this chapter

Equation form expr-ebfa6451583bf3df

Δ⊢Σ¬A\Delta \Proves[\Sigma] \lnot!A

Read as: Delta derives not formula A in system Sigma

Means: Delta derives not formula A in system Sigma

1 occurrence in this chapter

Equation form expr-ec6bfcc198cb4d0e

□□−1Γ={□B:□B∈Γ}\Box\Box^{-1}\Gamma = \Setabs{\Box!B}{\Box!B \in \Gamma}

Read as: box of inverse box of Gamma equals the set of necessarily formula B such that necessarily formula B belongs to Gamma

Means: box of inverse box of Gamma equals the set of necessarily formula B such that necessarily formula B belongs to Gamma

1 occurrence in this chapter

Equation form expr-edc7024164795776

□A1\Box!A_1

Read as: necessarily formula A sub one

Means: necessarily formula A sub one

1 occurrence in this chapter

Equation form expr-efbc656af2a75a16

n≤mn \le m

Read as: n is less than or equal to m

Means: n is less than or equal to m

1 occurrence in this chapter

Equation form expr-f0907e96579213bd

□□B∈Δ1\Box\Box!B \in \Delta_1

Read as: necessarily necessarily formula B belongs to Delta sub one

Means: necessarily necessarily formula B belongs to Delta sub one

1 occurrence in this chapter

Equation form expr-f0b5e7c66d4e4e76

□A∈Δ\Box !A \in \Delta

Read as: necessarily formula A belongs to Delta

Means: necessarily formula A belongs to Delta

3 occurrences in this chapter

Equation form expr-f1173c7bdeda4beb

◇A∈◇Δ3\Diamond!A \in \Diamond\Delta_3

Read as: possibly formula A belongs to diamond of Delta sub three

Means: possibly formula A belongs to diamond of Delta sub three

1 occurrence in this chapter

Equation form expr-f14f346209a1c04b

B∈Δ!B \in \Delta

Read as: formula B belongs to Delta

Means: formula B belongs to Delta

1 occurrence in this chapter

Equation form expr-f157f71e0163a897

□\Box

Read as: the necessity operator

Means: the necessity operator

4 occurrences in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: Delta

31 occurrences in this chapter

Equation form expr-f1f7d078d07cf599

Δn⊆Δm\Delta_n \subseteq \Delta_{m}

Read as: Delta sub n is a subset of Delta sub m

Means: Delta sub n is a subset of Delta sub m

1 occurrence in this chapter

Equation form expr-f2c7da65211e0cb5

□−1Δ2⊆Δ3\Box^{-1}\Delta_2 \subseteq \Delta_3

Read as: inverse box of Delta sub two is a subset of Delta sub three

Means: inverse box of Delta sub two is a subset of Delta sub three

1 occurrence in this chapter

Equation form expr-f43dda61fd4d4ef2

Δ⊢Σ⊥\Delta \Proves[\Sigma] \lfalse

Read as: Delta derives falsity in system Sigma

Means: Delta derives falsity in system Sigma

1 occurrence in this chapter

Equation form expr-f4c8888445f7342f

◇(B1∧…∧Bm)→(◇B1∧…∧◇Bm)\Diamond (!B_1 \land \dots \land !B_m) \to (\Diamond!B_1 \land \dots \land \Diamond!B_m)

Read as: possibly the conjunction of B sub one through B sub m implies the conjunction of possibly B sub one through possibly B sub m

Means: possibly the conjunction of B sub one through B sub m implies the conjunction of possibly B sub one through possibly B sub m

1 occurrence in this chapter

Equation form expr-f54884f271847fe6

¬A∈Δ\lnot!A \in \Delta

Read as: not formula A belongs to Delta

Means: not formula A belongs to Delta

3 occurrences in this chapter

Equation form expr-f7165c2e70f742d8

⊬Σ¬A\Proves/[\Sigma] \lnot !A

Read as: not formula A is not derivable in system Sigma

Means: not formula A is not derivable in system Sigma

2 occurrences in this chapter

Equation form expr-f7295825c348ed02

C=CA1∩…∩CAn\mClass{C} = \mClass{C}_{!A_1} \cap \dots \cap \mClass{C}_{!A_n}

Read as: class C is the intersection of the model classes for schemas A sub one through A sub n

Means: class C is the intersection of the model classes for schemas A sub one through A sub n

1 occurrence in this chapter

Equation form expr-f87a549f62a7a792

□A\Box !A

Read as: necessarily formula A

Means: necessarily formula A

1 occurrence in this chapter

Equation form expr-f8d4a4f321d03e2a

◇C\Diamond !C

Read as: possibly formula C

Means: possibly formula C

1 occurrence in this chapter

Equation form expr-f9a633aede35511e

◇A↔□A\Diamond!A \liff \Box !A

Read as: possibly formula A if and only if necessarily formula A

Means: possibly formula A if and only if necessarily formula A

1 occurrence in this chapter

Equation form expr-f9e164b8f3f45044

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

Read as: formula A implies necessarily possibly formula A

Means: formula A implies necessarily possibly formula A

1 occurrence in this chapter

Equation form expr-fc6931d6862a7198

C5\mClass{C}_\Ax{5}

Read as: class C subscript axiom five

Means: class C subscript axiom five

1 occurrence in this chapter

Equation form expr-fe34fdf28585eda3

□A∈Δ1\Box!A \in \Delta_1

Read as: necessarily formula A belongs to Delta sub one

Means: necessarily formula A belongs to Delta sub one

1 occurrence in this chapter

Equation form expr-ff0ef5c23edbf7bf

B1!B_1

Read as: formula B sub one

Means: formula B sub one

2 occurrences in this chapter

Definition of a complete Sigma consistent set

A set Gamma is complete Sigma consistent exactly when it is Sigma consistent and, for every formula A, contains either A or not A.

Source

Properties of complete Sigma consistent sets

The source lists deductive closure, inclusion of Sigma, exclusion of falsity, inclusion of truth, and membership conditions for negation, conjunction, disjunction, the conditional, and the biconditional. Active source-profile clauses remain in source order.

Source

Exercise completing connective cases

Complete the source-selected missing cases in the proof of the proposition on complete Sigma consistent sets. The exercise remains unsolved.

Source

Lindenbaum Lemma

Every Sigma consistent set Gamma is extended by a complete Sigma consistent set Delta. The construction enumerates formulas and adds each formula or its negation while preserving consistency.

Source

Provability characterized by complete extensions

Gamma derives A in Sigma exactly when every complete Sigma consistent extension Delta of Gamma contains A. The empty-Gamma case characterizes the modal system itself.

Source

Box and diamond operations on sets of formulas

The display defines box Gamma, diamond Gamma, inverse box Gamma, and inverse diamond Gamma by adding or removing the corresponding modal operator from every member.

Source

Four modal set equations

Four source-ordered equations define the direct box and diamond images and their inverse images. Each set-builder condition retains which modal operator is present.

Source

Lifting a derivation under necessity

If Gamma derives A in Sigma, then box Gamma derives necessarily A in Sigma. The proof applies the normal modal rule to a finite curried conditional derivation.

Source

Derivation from inverse-box premises

If inverse box Gamma derives A in Sigma, then Gamma derives necessarily A in Sigma, using the preceding lifting lemma and inclusion of box inverse-box Gamma in Gamma.

Source

Complete-set characterization of necessity

For complete Sigma consistent Gamma, necessarily A belongs to Gamma exactly when A belongs to every complete Sigma consistent Delta extending inverse box Gamma.

Source

Equivalence of box and diamond accessibility conditions

For complete Sigma consistent Gamma and Delta, inverse box Gamma is a subset of Delta exactly when diamond Delta is a subset of Gamma.

Source

Complete-set characterization of possibility

Possibly A belongs to complete Sigma consistent Gamma exactly when some complete Sigma consistent Delta contains A and has diamond Delta included in Gamma.

Source

Exercise proving the alternate modal characterization

Prove the selected box-or-diamond characterization directly, without using the equivalence lemma. The exercise remains unsolved.

Source

Definition of the canonical model

Worlds are all complete Sigma consistent sets. Accessibility is defined by inverse-box inclusion, equivalently by the selected diamond condition. Valuation V superscript Sigma assigns p exactly to worlds Delta containing p.

Source

Truth Lemma

For every formula A, A is true at world Delta in the canonical model exactly when A belongs to Delta.

Source

Exercise completing Truth Lemma cases

Complete the source-selected missing induction cases in the Truth Lemma. The exercise remains unsolved.

Source

Definition of determination by a model

A model determines a normal modal logic Sigma exactly when it makes A true throughout if and only if Sigma derives A, for every formula A.

Source

Determination by the canonical model

The canonical model for Sigma makes A true throughout exactly when Sigma derives A.

Source

Completeness of basic modal logic K

If A is valid, then A is derivable in basic modal logic K. The proof uses the canonical-model determination theorem contrapositively.

Source

Canonical correspondence theorem

If Sigma contains one of axioms D, T, B, four, or five, its canonical model is respectively serial, reflexive, symmetric, transitive, or euclidean.

Source

Basic correspondence facts table

The outer table presents five source-ordered axiom schemas with the corresponding canonical-frame properties. Its inner tabular object carries the explicit row and column reading.

Source

Basic correspondence facts rows

Columns are the axiom schema contained in Sigma and the resulting canonical-model property. Rows D, T, B, four, and five map respectively to serial, reflexive, symmetric, transitive, and euclidean.

Source

Determination by intersected model classes

For any selected schemas among D, T, B, four, and five, the normal system formed by adding them to K is determined by the intersection of their corresponding model classes.

Source

Additional canonical-frame correspondences

The proposition associates the schema possibly A implies necessarily A with partial functionality, the biconditional version with functionality, and necessarily necessarily A implies necessarily A with weak density.

Source

Weak-density consistency derivation

The display derives a contradiction from an assumed inconsistent intermediate set. It preserves every source step from the premise formulas, through normality and necessitation, to a negated conjunction in Delta sub two.

Source

Cross-reference reference-001015

the deductive closure clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001016

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001017

the proposition on consistency facts

Source occurrence

Cross-reference reference-001018

the consistency alternative for a formula and its negation

Source occurrence

Cross-reference reference-001019

the lemma lifting a derivation into boxed premises and conclusion

Source occurrence

Cross-reference reference-001020

the lemma deriving a boxed conclusion from inverse-box premises

Source occurrence

Cross-reference reference-001021

the proposition on consistency facts

Source occurrence

Cross-reference reference-001022

the consistency fact for adding a negated formula

Source occurrence

Cross-reference reference-001023

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001024

the negation clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001025

the complete-consistent-set characterization of necessity

Source occurrence

Cross-reference reference-001026

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001027

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001028

the negation clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001029

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001030

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001031

the section on modalities and complete consistent sets

Source occurrence

Cross-reference reference-001032

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001033

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001034

the falsity clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001035

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001036

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001037

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001038

the negation clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001039

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001040

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001041

the disjunction clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001042

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001043

the complete-consistent-set characterization of necessity

Source occurrence

Cross-reference reference-001044

the definition of truth at a world in a modal model

Source occurrence

Cross-reference reference-001045

the Truth Lemma

Source occurrence

Cross-reference reference-001046

the complete-consistent-set characterization of provability

Source occurrence

Cross-reference reference-001047

the proposition listing properties of complete Sigma consistent sets

Source occurrence

Cross-reference reference-001048

the deductive closure clause for complete Sigma consistent sets

Source occurrence

Cross-reference reference-001049

the table of basic modal correspondence facts

Source occurrence

Cross-reference reference-001050

the lemma deriving a boxed conclusion from inverse-box premises

Source occurrence

Cross-reference reference-001051

the normal-modal theorem that falsity is not possible

Source occurrence

Cross-reference reference-001052

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001053

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001054

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001055

the table of additional frame correspondences

Source occurrence

Cross-reference reference-001056

the first additional canonical-frame property

Source occurrence

Cross-reference reference-001057

the canonical-frame correspondence theorem

Source occurrence

Cross-reference reference-001058

the equivalence between the inverse-box and diamond accessibility conditions

Source occurrence

Cross-reference reference-001059

the proposition on derivability facts

Source occurrence

Cross-reference reference-001060

the deduction-theorem clause of the derivability facts

Source occurrence

Cross-reference reference-001061

the lemma lifting a derivation into boxed premises and conclusion

Source occurrence

Cross-reference reference-001062

the proposition on derivability facts

Source occurrence

Cross-reference reference-001063

the monotonicity clause of the derivability facts

Source occurrence

Source disclosures

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

WΣ={Δ:Δ is complete Σ-consistent}W^\Sigma = \Setabs{ \Delta }{\Delta \text{ is complete $\Sigma$-consistent} }

Read as: World set W superscript Sigma is the set of all Delta such that Delta is complete Sigma consistent.

Read in context source

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

A≡⊥!A \ident \lfalse

Read as: Case: A is the falsity constant.

Read in context source

Source-generated case expression tr053-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 tr053-source-macro-0009

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

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

Read in context source

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

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 tr053-source-macro-0011

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 tr053-source-macro-0012

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 tr053-source-macro-0013

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

Read as: Case: A is necessarily B.

Read in context source

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

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

Read as: Case: A is possibly B.

Read in context source

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

D\Ax{D}

Read as: axiom D

Read in context source

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

T\Ax{T}

Read as: axiom T

Read in context source

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

B\Ax{B}

Read as: axiom B

Read in context source

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

4\Ax{4}

Read as: axiom four

Read in context source

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

5\Ax{5}

Read as: axiom five

Read in context source

Ordered structures

Basic correspondence facts rows

Structure: table.

Correspondence table. Column headers: if Sigma contains the axiom schema; the canonical model for Sigma has the stated property. Row one, axiom D, necessarily formula A implies possibly formula A; property serial. Row two, axiom T, necessarily formula A implies formula A; property reflexive. Row three, axiom B, formula A implies necessarily possibly formula A; property symmetric. Row four, axiom four, necessarily formula A implies necessarily necessarily formula A; property transitive. Row five, axiom five, possibly formula A implies necessarily possibly formula A; property euclidean. End table.

Read the source-bound structure in context