Modal Tableaux — Explore

Equation form expr-007dac77de886d9f

\sFmla{\False}{!A}[\sigma]

Read as: false formula A at prefix sigma

Means: false formula A at prefix sigma

2 occurrences in this chapter

Equation form expr-03d34828b4a3e906

\sFmla{\False}{!B}[\sigma.n] \in \Delta

Read as: false formula B at prefix sigma dot n belongs to Delta

Means: false formula B at prefix sigma dot n belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027851

Equation form expr-04bdf66ee83c43d2

\mSat{M(\Delta)}{\Gamma}

Read as: Gamma is satisfied in model M of Delta

Means: Gamma is satisfied in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027858

Equation form expr-07ea89381935676e

\Log{S4} = \Log{KT4}

Read as: logic S four equals logic K T four

Means: logic S four equals logic K T four

1 occurrence in this chapter

Occurrence projected-formula-0027652

Equation form expr-092317f4ffe738ba

\Log{KT5} \Proves \Ax{B}

Read as: logic K T five derives axiom B

Means: logic K T five derives axiom B

1 occurrence in this chapter

Occurrence projected-formula-0027667

Equation form expr-0ab83730c263f0b7

\Entails !A

Read as: formula A is semantically valid

Means: formula A is semantically valid

1 occurrence in this chapter

Occurrence projected-formula-0027863

Equation form expr-0adcf3b28e16c022

\Log{D} = \Log{KD}

Read as: logic D equals logic K D

Means: logic D equals logic K D

1 occurrence in this chapter

Occurrence projected-formula-0027641

Equation form expr-0bfe935e70c321c7

u

Read as: world u

Means: world u

1 occurrence in this chapter

Occurrence projected-formula-0027767

Equation form expr-0c9d36851e5eca4a

\sigma.n \notin P(\Gamma)

Read as: prefix sigma dot n does not belong to the prefix set of Gamma

Means: prefix sigma dot n does not belong to the prefix set of Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027558

Equation form expr-0e700f776b9caff0

\sFmla{\True}{p}[\sigma]

Read as: true p at prefix sigma

Means: true p at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027781

Equation form expr-0f06b9b9134a242f

\Gamma \cup \{\sFmla{\False}{!B}[\sigma]\}

Read as: Gamma union the set containing false formula B at prefix sigma

Means: Gamma union the set containing false formula B at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027506

Equation form expr-1095616c168d2d37

\Diamond \formula{A} \Entails/ \Box \formula{A}

Read as: possibly formula A does not semantically entail necessarily formula A

Means: possibly formula A does not semantically entail necessarily formula A

1 occurrence in this chapter

Occurrence projected-formula-0027436

Equation form expr-12e936f43d808efc

\sigma' \in P(\Delta)

Read as: prefix sigma prime belongs to the prefix set of Delta

Means: prefix sigma prime belongs to the prefix set of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027843

Equation form expr-13068b6c2dfe8ad1

\sFmla{\False}{!B \lor !C} \in \Gamma

Read as: false the disjunction of formula B and formula C belongs to Gamma

Means: false the disjunction of formula B and formula C belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027528

Equation form expr-148de9c5a7a44d19

p

Read as: p

Means: p

1 occurrence in this chapter

Occurrence projected-formula-0027779

Equation form expr-165a2676a255cdfb

\Log{KT} \Proves \Ax{D}

Read as: logic K T derives axiom D

Means: logic K T derives axiom D

1 occurrence in this chapter

Occurrence projected-formula-0027672

Equation form expr-1705de07fe24b5b5

\sigma \in V(p)

Read as: prefix sigma belongs to valuation V of p

Means: prefix sigma belongs to valuation V of p

1 occurrence in this chapter

Occurrence projected-formula-0027813

Equation form expr-176ac74c18155191

1.2.1.3

Read as: prefix one point two point one point three

Means: prefix one point two point one point three

1 occurrence in this chapter

Occurrence projected-formula-0027391

Equation form expr-18069020c5e029eb

\TRule{\False}{\lor}

Read as: false disjunction rule

Means: false disjunction rule

1 occurrence in this chapter

Occurrence projected-formula-0027527

Equation form expr-19086e05fd052ff5

\sFmla{S}{!A}[\sigma] \in \Gamma

Read as: with sign S formula A at prefix sigma belongs to Gamma

Means: with sign S formula A at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027502

Equation form expr-1aad0f88149a6284

\sFmla{\True}{\Box}[\sigma]

Read as: true the necessity operator with no printed operand at prefix sigma

Means: true the necessity operator with no printed operand at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027792

Equation form expr-1b16b1df538ba12d

n

Read as: n

Means: n

5 occurrences in this chapter

Equation form expr-1e095d3ffc5363ea

\Log{KB5} \Proves \Ax{4}

Read as: logic K B five derives axiom four

Means: logic K B five derives axiom four

1 occurrence in this chapter

Occurrence projected-formula-0027671

Equation form expr-1fcb2a117f1a4fa5

\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma

Read as: Gamma sub zero is the set of formulas B sub one through B sub n, and is a subset of Gamma

Means: Gamma sub zero is the set of formulas B sub one through B sub n, and is a subset of Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027375

Equation form expr-2009e354f61d919f

\def\arraystretch{3}\begin{array}{|c|c|} \hline \AxiomC{\sFmla{\True}{\lnot !A}[\sigma]} \RightLabel{\TRule{\True}{\lnot}} \UnaryInfC{\sFmla{\False}{!A}[\sigma]} \DisplayProof & \AxiomC{\sFmla{\False}{\lnot !A}[\sigma]} \RightLabel{\TRule{\False}{\lnot}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \DisplayProof \\[1ex] \hline \AxiomC{\sFmla{\True}{!A \land !B}[\sigma]} \RightLabel{\TRule{\True}{\land}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\True}{!B}[\sigma]} \DisplayProof & \AxiomC{\sFmla{\False}{!A \land !B}[\sigma]} \RightLabel{\TRule{\False}{\land}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad \sFmla{\False}{!B}[\sigma]$} \DisplayProof \\[2ex] \hline \AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\True}{\lor}} \UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad \sFmla{\True}{!B}[\sigma]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\False}{\lor}} \UnaryInfC{\sFmla{\False}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma]} \DisplayProof \\[2ex] \hline \AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\True}{\lif}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad \sFmla{\True}{!B}[\sigma]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\False}{\lif}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma]} \DisplayProof \\[2ex] \hline \end{array}

Read as: Propositional prefixed tableau rules. Row one, true negation: from true not A at prefix sigma, infer false A at prefix sigma. False negation: from false not A at prefix sigma, infer true A at prefix sigma. Row two, true conjunction: from true A and B at prefix sigma, stack true A and true B at that prefix. False conjunction: from false A and B at prefix sigma, branch to false A or false B at that prefix. Row three, true disjunction: from true A or B at prefix sigma, branch to true A or true B at that prefix. False disjunction: from false A or B at prefix sigma, stack false A and false B at that prefix. Row four, true conditional: from true if A then B at prefix sigma, branch to false A or true B at that prefix. False conditional: from false if A then B at prefix sigma, stack true A and false B at that prefix. End propositional rule table.

Means: Propositional prefixed tableau rules. Row one, true negation: from true not A at prefix sigma, infer false A at prefix sigma. False negation: from false not A at prefix sigma, infer true A at prefix sigma. Row two, true conjunction: from true A and B at prefix sigma, stack true A and true B at that prefix. False conjunction: from false A and B at prefix sigma, branch to false A or false B at that prefix. Row three, true disjunction: from true A or B at prefix sigma, branch to true A or true B at that prefix. False disjunction: from false A or B at prefix sigma, stack false A and false B at that prefix. Row four, true conditional: from true if A then B at prefix sigma, branch to false A or true B at that prefix. False conditional: from false if A then B at prefix sigma, stack true A and false B at that prefix. End propositional rule table.

1 occurrence in this chapter

Occurrence projected-formula-0027403

Equation form expr-20732e65a0b29eb1

!B_1, \dots, !B_n \Entails !A

Read as: formulas B sub one through B sub n semantically entails formula A

Means: formulas B sub one through B sub n semantically entails formula A

1 occurrence in this chapter

Occurrence projected-formula-0027445

Equation form expr-213b22437e14fef7

\TRule{\False}{\land}

Read as: false conjunction rule

Means: false conjunction rule

1 occurrence in this chapter

Occurrence projected-formula-0027585

Equation form expr-21d031b0dacd8cc7

\Log{K}

Read as: logic K

Means: logic K

3 occurrences in this chapter

Equation form expr-22b2c187a0e73a7c

\Gamma \cup \{\sFmla{\False}{!B}[\sigma.n]\}

Read as: Gamma union the set containing false formula B at prefix sigma dot n

Means: Gamma union the set containing false formula B at prefix sigma dot n

2 occurrences in this chapter

Equation form expr-23787e9916d65124

!B_1, \dots, !B_n \Proves !A

Read as: formulas B sub one through B sub n derives formula A

Means: formulas B sub one through B sub n derives formula A

1 occurrence in this chapter

Occurrence projected-formula-0027408

Equation form expr-252f10c83610ebca

f

Read as: interpretation f

Means: interpretation f

15 occurrences in this chapter

Equation form expr-26a9c61e7b9d13d4

\sFmla{\True}{\Box !A \lif !A}[1.2]

Read as: true the conditional from necessarily formula A to formula A at prefix one point two

Means: true the conditional from necessarily formula A to formula A at prefix one point two

1 occurrence in this chapter

Occurrence projected-formula-0027392

Equation form expr-27d5651e66d95235

\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.

Read as: true A or false A

Means: true A or false A

1 occurrence in this chapter

Occurrence projected-formula-0027370

Equation form expr-2a7770d0b738c63c

\sFmla{\True}{\Box!B}[\sigma.n]

Read as: true necessarily formula B at prefix sigma dot n

Means: true necessarily formula B at prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027725

Equation form expr-2d9c017ce04cb9be

Rf(\sigma)f(\sigma.n)

Read as: accessibility relation R holds from interpretation f of prefix sigma to interpretation f of prefix sigma dot n

Means: accessibility relation R holds from interpretation f of prefix sigma to interpretation f of prefix sigma dot n

5 occurrences in this chapter

Equation form expr-2f4583c8b7c73ba0

f'

Read as: interpretation f prime

Means: interpretation f prime

2 occurrences in this chapter

Equation form expr-308e7581edc27c37

\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)

Read as: the conditional from the conjunction of necessarily formula A and necessarily formula B to necessarily the conjunction of formula A and formula B is derivable

Means: the conditional from the conjunction of necessarily formula A and necessarily formula B to necessarily the conjunction of formula A and formula B is derivable

1 occurrence in this chapter

Occurrence projected-formula-0027437

Equation form expr-319b49b17c38d247

!B_n \in \Gamma

Read as: formula B sub n belongs to Gamma

Means: formula B sub n belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027605

Equation form expr-3244cb9195abf172

\mSat/{M(\Delta)}{!A}[\sigma]

Read as: formula A is false at prefix sigma in model M of Delta

Means: formula A is false at prefix sigma in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027811

Equation form expr-333bf014c1cf8aa6

\sFmla{\False}{!C}[\sigma]

Read as: false formula C at prefix sigma

Means: false formula C at prefix sigma

4 occurrences in this chapter

Equation form expr-3442bfb297a43539

\sFmla{\False}{\Box}[\sigma.n]

Read as: false the necessity operator with no printed operand at prefix sigma dot n

Means: false the necessity operator with no printed operand at prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027790

Equation form expr-34ecf55785be57ae

\sFmla{\False}{\Box}[\sigma]

Read as: false the necessity operator with no printed operand at prefix sigma

Means: false the necessity operator with no printed operand at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027789

Equation form expr-350c15688d837138

\TRule{\False}{\Diamond}

Read as: false possibility rule

Means: false possibility rule

2 occurrences in this chapter

Equation form expr-3762bf925b6f0e5b

i=1

Read as: i equals one

Means: i equals one

2 occurrences in this chapter

Equation form expr-3ab205095a2faa4e

\mSat{M}{!B_i}[w]

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

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

2 occurrences in this chapter

Equation form expr-3b9b79000d3b0004

\Log{S5} \Proves \Ax{5}

Read as: logic S five derives axiom five

Means: logic S five derives axiom five

2 occurrences in this chapter

Equation form expr-3bbeed026b312599

\TRule{\True}{\lif}

Read as: true conditional rule

Means: true conditional rule

1 occurrence in this chapter

Occurrence projected-formula-0027599

Equation form expr-3cad68311bf136e9

\mSat{M(\Delta)}{!B}[\sigma]

Read as: formula B is true at prefix sigma in model M of Delta

Means: formula B is true at prefix sigma in model M of Delta

2 occurrences in this chapter

Equation form expr-3e5b27e999bd94b2

\mSat{M}{!B}[f(\sigma)]

Read as: formula B is true at interpretation f of prefix sigma in model M

Means: formula B is true at interpretation f of prefix sigma in model M

4 occurrences in this chapter

Equation form expr-3f74b0ddf84e7a8c

\sFmla{\True}{\Box(p \lor q)}[1]

Read as: true necessarily the disjunction of p and q at prefix one

Means: true necessarily the disjunction of p and q at prefix one

1 occurrence in this chapter

Occurrence projected-formula-0027879

Equation form expr-415e084f6ce09ce4

W = \{1, 1.1, 1.2\}

Read as: world set W is the set containing one, one point one, and one point two

Means: world set W is the set containing one, one point one, and one point two

1 occurrence in this chapter

Occurrence projected-formula-0027885

Equation form expr-42764fdacbaee1ca

\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma]

Read as: true A at prefix sigma and false A at prefix sigma

Means: true A at prefix sigma and false A at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027404

Equation form expr-42b8f19ae63d24a4

\Struct{M}

Read as: structure M

Means: structure M

1 occurrence in this chapter

Occurrence projected-formula-0027560

Equation form expr-4336f7aef0d4db7f

\mSat{M}{\Box !B}[f(\sigma.n)]

Read as: necessarily formula B is true at interpretation f of prefix sigma dot n in model M

Means: necessarily formula B is true at interpretation f of prefix sigma dot n in model M

4 occurrences in this chapter

Equation form expr-4363d711b46caeda

\sFmla{\False}{!B \lif !C}[\sigma] \in \Gamma

Read as: false the conditional from formula B to formula C at prefix sigma belongs to Gamma

Means: false the conditional from formula B to formula C at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027530

Equation form expr-4414cf0c52ecc4b0

\sFmla{\True}{!B \lor !C}[\sigma] \in \Gamma

Read as: true the disjunction of formula B and formula C at prefix sigma belongs to Gamma

Means: true the disjunction of formula B and formula C at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027598

Equation form expr-44b81c75951f896f

\sFmla{\True}{\Box}[\sigma.n]

Read as: true the necessity operator with no printed operand at prefix sigma dot n

Means: true the necessity operator with no printed operand at prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027793

Equation form expr-4579bd19edd91c98

\mSat/{M}{!A}[f(\sigma)]

Read as: formula A is false at interpretation f of prefix sigma in model M

Means: formula A is false at interpretation f of prefix sigma in model M

2 occurrences in this chapter

Equation form expr-457d4e8341a8e696

\Gamma \Entails/ !A

Read as: Gamma does not semantically entail formula A

Means: Gamma does not semantically entail formula A

2 occurrences in this chapter

Equation form expr-45daa3f5376260f6

Rf(\sigma.n)w

Read as: accessibility relation R holds from interpretation f of prefix sigma dot n to world w

Means: accessibility relation R holds from interpretation f of prefix sigma dot n to world w

2 occurrences in this chapter

Equation form expr-464c4d3f1a97e359

V(q) = \{1.1\}

Read as: valuation V of q is the singleton containing one point one

Means: valuation V of q is the singleton containing one point one

1 occurrence in this chapter

Occurrence projected-formula-0027889

Equation form expr-475c3956abc8bb4e

\sFmla{\True}{q}[1.1]

Read as: true q at prefix one point one

Means: true q at prefix one point one

1 occurrence in this chapter

Occurrence projected-formula-0027890

Equation form expr-4877305150ddd9db

\TRule{\True}{\lor}

Read as: true disjunction rule

Means: true disjunction rule

2 occurrences in this chapter

Equation form expr-48b7b8587503e897

\Log{B} = \Log{KTB}

Read as: logic B equals logic K T B

Means: logic B equals logic K T B

1 occurrence in this chapter

Occurrence projected-formula-0027647

Equation form expr-49e7273bd7309be4

\TRule{\False}{\lnot}

Read as: false negation rule

Means: false negation rule

1 occurrence in this chapter

Occurrence projected-formula-0027513

Equation form expr-4ee59b68125f5f6c

(\Box p \lor \Box q) \lif \Box(p \lor q)

Read as: the conditional from the disjunction of necessarily p and necessarily q to necessarily the disjunction of p and q

Means: the conditional from the disjunction of necessarily p and necessarily q to necessarily the disjunction of p and q

1 occurrence in this chapter

Occurrence projected-formula-0027441

Equation form expr-4fca26ac13b7e1f9

\sFmla{\False}{!A}[\sigma.n]

Read as: false formula A at prefix sigma dot n

Means: false formula A at prefix sigma dot n

3 occurrences in this chapter

Equation form expr-50e721e49c013f00

w

Read as: world w

Means: world w

6 occurrences in this chapter

Equation form expr-5136fc4246e7d497

\Diamond

Read as: the possibility operator

Means: the possibility operator

28 occurrences in this chapter

Equation form expr-513e83da52aa90cf

\mModel{M}, f'

Read as: model M and interpretation f prime

Means: model M and interpretation f prime

1 occurrence in this chapter

Occurrence projected-formula-0027583

Equation form expr-51654729f4e4c6fb

\sFmla{\True}{\Diamond !B}[\sigma]

Read as: true possibly formula B at prefix sigma

Means: true possibly formula B at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027691

Equation form expr-51abc71a5b4fda2d

\Proves \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond !B)

Read as: the conditional from possibly the disjunction of formula A and formula B to the disjunction of possibly formula A and possibly formula B is derivable

Means: the conditional from possibly the disjunction of formula A and formula B to the disjunction of possibly formula A and possibly formula B is derivable

1 occurrence in this chapter

Occurrence projected-formula-0027438

Equation form expr-52a1eb2402f22a50

P(\Gamma)

Read as: the prefix set of Gamma

Means: the prefix set of Gamma

5 occurrences in this chapter

Equation form expr-52baf5b113b97063

\Log{KDB4} \Proves \Ax{T}

Read as: logic K D B four derives axiom T

Means: logic K D B four derives axiom T

1 occurrence in this chapter

Occurrence projected-formula-0027669

Equation form expr-52bbd4e510cb9433

\Entails/ A

Read as: the source expression A, without a formula marker, is not semantically valid

Means: the source expression A, without a formula marker, is not semantically valid

1 occurrence in this chapter

Occurrence projected-formula-0027866

Equation form expr-52c55664649cce9d

\TRule{\False}{\Box}

Read as: false necessity rule

Means: false necessity rule

3 occurrences in this chapter

Equation form expr-551658344ba88180

\mSat{M}{\Diamond !B}[f(\sigma)]

Read as: possibly formula B is true at interpretation f of prefix sigma in model M

Means: possibly formula B is true at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027698

Equation form expr-5536631e7f4faee8

\mSat/{M(\Delta)}{!B}[\sigma.n]

Read as: formula B is false at prefix sigma dot n in model M of Delta

Means: formula B is false at prefix sigma dot n in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027852

Equation form expr-5682d419e4379901

\mSat/{M}{!B}[f'(\sigma.n)]

Read as: formula B is false at interpretation f prime of prefix sigma dot n in model M

Means: formula B is false at interpretation f prime of prefix sigma dot n in model M

1 occurrence in this chapter

Occurrence projected-formula-0027579

Equation form expr-57885e4c75965b23

\Gamma

Read as: Gamma

Means: Gamma

18 occurrences in this chapter

Equation form expr-57a641fd810b5a91

\Proves

Read as: the derivability symbol

Means: the derivability symbol

1 occurrence in this chapter

Occurrence projected-formula-0027373

Equation form expr-57f9c709d0eb3346

\mSat{M}{\Box !B}[f(\sigma).n]

Read as: necessarily formula B is true at the source location f of sigma, followed outside the function argument by dot n, in model M

Means: necessarily formula B is true at the source location f of sigma, followed outside the function argument by dot n, in model M

1 occurrence in this chapter

Occurrence projected-formula-0027757

Equation form expr-5810793836dd180c

\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1].

Read as: true B sub one through true B sub n at prefix one, followed by false A at prefix one

Means: true B sub one through true B sub n at prefix one, followed by false A at prefix one

1 occurrence in this chapter

Occurrence projected-formula-0027409

Equation form expr-5957b44ec81446ba

\Log{S5} = \Log{KT4B}

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

Means: logic S five equals logic K T four B

1 occurrence in this chapter

Occurrence projected-formula-0027657

Equation form expr-59cf7cd4fdb9ff5b

\True

Read as: true sign

Means: true sign

3 occurrences in this chapter

Equation form expr-5c62e091b8c0565f

P

Read as: prefix set P

Means: prefix set P

4 occurrences in this chapter

Equation form expr-5ce29c3c24488728

\TRule{\False}{\lif}

Read as: false conditional rule

Means: false conditional rule

1 occurrence in this chapter

Occurrence projected-formula-0027529

Equation form expr-5d278b3fd61080be

\sFmla{\True}{\Diamond!B}[\sigma]

Read as: true possibly formula B at prefix sigma

Means: true possibly formula B at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027700

Equation form expr-5e286c07a123d9f7

\mSat{M}{!B}[f(\sigma.n)]

Read as: formula B is true at interpretation f of prefix sigma dot n in model M

Means: formula B is true at interpretation f of prefix sigma dot n in model M

1 occurrence in this chapter

Occurrence projected-formula-0027551

Equation form expr-5e585fb8dfd9f7c9

\Gamma \subseteq \Delta

Read as: Gamma is a subset of Delta

Means: Gamma is a subset of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027857

Equation form expr-5f5e6fc357a6dae4

\sFmla{S}{!A}[\sigma]

Read as: with sign S formula A at prefix sigma

Means: with sign S formula A at prefix sigma

3 occurrences in this chapter

Equation form expr-61767df7eeab65d5

\sFmla{\True}{\Box!B}[\sigma]

Read as: true necessarily formula B at prefix sigma

Means: true necessarily formula B at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027747

Equation form expr-62a7581d7620bb78

\Log{K4}

Read as: logic K four

Means: logic K four

1 occurrence in this chapter

Occurrence projected-formula-0027644

Equation form expr-62c66a7a5dd70c31

m

Read as: prefix m

Means: prefix m

4 occurrences in this chapter

Equation form expr-641c595f15367409

Rf(\sigma.n)f(\sigma)

Read as: accessibility relation R holds from interpretation f of prefix sigma dot n to interpretation f of prefix sigma

Means: accessibility relation R holds from interpretation f of prefix sigma dot n to interpretation f of prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027714

Equation form expr-66000281e78ba63e

\sFmla{\True}{\indfrm}[\sigma] \in \Delta

Read as: true the induction formula at prefix sigma belongs to Delta

Means: true the induction formula at prefix sigma belongs to Delta

4 occurrences in this chapter

Equation form expr-66d37b60c4ba042d

R\sigma\sigma' \quad \text{iff} \quad \sigma'=\sigma.n \quad \text{for some~$n$}

Read as: prefix sigma is accessible to prefix sigma prime if and only if sigma prime equals sigma dot n for some n

Means: prefix sigma is accessible to prefix sigma prime if and only if sigma prime equals sigma dot n for some n

1 occurrence in this chapter

Occurrence projected-formula-0027805

Equation form expr-67e222a2ea549cec

\sigma.n \in P(\Gamma)

Read as: prefix sigma dot n belongs to the prefix set of Gamma

Means: prefix sigma dot n belongs to the prefix set of Gamma

2 occurrences in this chapter

Equation form expr-6b86b273ff34fce1

1

Read as: prefix one

Means: prefix one

2 occurrences in this chapter

Equation form expr-70d99b2f4841350f

\mModel{M(\Delta)} = \tuple{P(\Delta), R, V}

Read as: model M of Delta is the ordered triple consisting of the prefix set P of Delta, accessibility relation R, and valuation V

Means: model M of Delta is the ordered triple consisting of the prefix set P of Delta, accessibility relation R, and valuation V

1 occurrence in this chapter

Occurrence projected-formula-0027803

Equation form expr-7120f8695fd9aa83

\Log{KB4} \Proves \Ax{5}

Read as: logic K B four derives axiom five

Means: logic K B four derives axiom five

1 occurrence in this chapter

Occurrence projected-formula-0027670

Equation form expr-7338612386109e58

Rf(\sigma)f(\sigma)

Read as: accessibility relation R holds from interpretation f of prefix sigma to interpretation f of prefix sigma

Means: accessibility relation R holds from interpretation f of prefix sigma to interpretation f of prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027681

Equation form expr-751379acac529582

\Diamond p \lif \Diamond(p \lor q)

Read as: if possibly p, then possibly the disjunction of p and q

Means: if possibly p, then possibly the disjunction of p and q

1 occurrence in this chapter

Occurrence projected-formula-0027442

Equation form expr-77ac319bfe1979e2

1.2

Read as: prefix one point two

Means: prefix one point two

2 occurrences in this chapter

Equation form expr-78046105f9332890

f'(\sigma) = f(\sigma)

Read as: interpretation f prime of prefix sigma equals interpretation f of prefix sigma

Means: interpretation f prime of prefix sigma equals interpretation f of prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027574

Equation form expr-781d31b47435539d

\Box \formula{A} \Entails/ \Diamond \formula{A}

Read as: necessarily formula A does not semantically entail possibly formula A

Means: necessarily formula A does not semantically entail possibly formula A

1 occurrence in this chapter

Occurrence projected-formula-0027435

Equation form expr-7aac21b858f44550

\mSat{M}{\Gamma}[f]

Read as: Gamma is satisfied with respect to interpretation f in model M

Means: Gamma is satisfied with respect to interpretation f in model M

12 occurrences in this chapter

Equation form expr-7ac880016e9f5b71

P(\Delta)

Read as: the prefix set of Delta

Means: the prefix set of Delta

2 occurrences in this chapter

Equation form expr-7cc21a3bda17828d

\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

3 occurrences in this chapter

Equation form expr-7ce2af3bdcb335f5

\sFmla{\False}{!B}[\sigma] \in \Delta

Read as: false formula B at prefix sigma belongs to Delta

Means: false formula B at prefix sigma belongs to Delta

2 occurrences in this chapter

Equation form expr-7d9f8feedfb757f6

\sFmla{\True}{\lnot !B}[\sigma] \in \Gamma

Read as: true not formula B at prefix sigma belongs to Gamma

Means: true not formula B at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027505

Equation form expr-7e7326e740b2b753

\sFmla{\True}{!B \land !C}

Read as: true the conjunction of formula B and formula C

Means: true the conjunction of formula B and formula C

1 occurrence in this chapter

Occurrence projected-formula-0027785

Equation form expr-7f4f9d134acea642

\sFmla{\False}{\Box !A}[\sigma]

Read as: false necessarily formula A at prefix sigma

Means: false necessarily formula A at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027425

Equation form expr-801c80c1290aba05

R = \{\tuple{1, 1.1}, \tuple{1, 1.2}\}

Read as: accessibility relation R contains the ordered pair one to one point one and the ordered pair one to one point two

Means: accessibility relation R contains the ordered pair one to one point one and the ordered pair one to one point two

1 occurrence in this chapter

Occurrence projected-formula-0027886

Equation form expr-8121180d21842190

\Proves/ \Box(p \lor q) \lif (\Box p \lor \Box q)

Read as: the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q is not derivable

Means: the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q is not derivable

1 occurrence in this chapter

Occurrence projected-formula-0027878

Equation form expr-8238c028f61fc0f7

!A

Read as: formula A

Means: formula A

7 occurrences in this chapter

Equation form expr-83295d4be08231b6

\sFmla{\False}{\Diamond !A}[\sigma]

Read as: false possibly formula A at prefix sigma

Means: false possibly formula A at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027421

Equation form expr-8353b5c6cd768adf

\sFmla{\True}{!C}[\sigma]

Read as: true formula C at prefix sigma

Means: true formula C at prefix sigma

4 occurrences in this chapter

Equation form expr-83d4a511903443cd

R\sigma\sigma'

Read as: accessibility relation R holds from prefix sigma to prefix sigma prime

Means: accessibility relation R holds from prefix sigma to prefix sigma prime

2 occurrences in this chapter

Equation form expr-83e2071a842d5098

\TRule{\True}{\lnot}

Read as: true negation rule

Means: true negation rule

1 occurrence in this chapter

Occurrence projected-formula-0027504

Equation form expr-8652eb93f02381c9

\mSat/{M}{\Box !B}[f(\sigma)]

Read as: necessarily formula B is false at interpretation f of prefix sigma in model M

Means: necessarily formula B is false at interpretation f of prefix sigma in model M

2 occurrences in this chapter

Equation form expr-88855060a722f93c

\Diamond!A \lif \Box\Diamond!A

Read as: if possibly formula A, then necessarily possibly formula A

Means: if possibly formula A, then necessarily possibly formula A

1 occurrence in this chapter

Occurrence projected-formula-0027776

Equation form expr-89383b4fbde3a8bf

f'(\sigma.n) = w

Read as: interpretation f prime of prefix sigma dot n equals world w

Means: interpretation f prime of prefix sigma dot n equals world w

1 occurrence in this chapter

Occurrence projected-formula-0027573

Equation form expr-8986c9fb12676f69

Rf'(\sigma)f'(\sigma.n)

Read as: accessibility relation R holds from interpretation f prime of prefix sigma to interpretation f prime of prefix sigma dot n

Means: accessibility relation R holds from interpretation f prime of prefix sigma to interpretation f prime of prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027576

Equation form expr-89937f947333635b

\sFmla{\False}{\lnot !B}[\sigma] \in \Gamma

Read as: false not formula B at prefix sigma belongs to Gamma

Means: false not formula B at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027514

Equation form expr-8a5886ea8729e9d1

\sigma = 1.2.1

Read as: prefix sigma equals prefix one point two point one

Means: prefix sigma equals prefix one point two point one

1 occurrence in this chapter

Occurrence projected-formula-0027389

Equation form expr-8b73294bb700d439

\mSat{M}{!A}[f(\sigma)]

Read as: formula A is true at interpretation f of prefix sigma in model M

Means: formula A is true at interpretation f of prefix sigma in model M

2 occurrences in this chapter

Equation form expr-8c2574892063f995

R

Read as: accessibility relation R

Means: accessibility relation R

6 occurrences in this chapter

Equation form expr-8c2ec4ac07ee1593

\Log{T} = \Log{KT}

Read as: logic T equals logic K T

Means: logic T equals logic K T

1 occurrence in this chapter

Occurrence projected-formula-0027638

Equation form expr-8c3b80aa9ba71711

\TRule{\True}{\Box}

Read as: true necessity rule

Means: true necessity rule

4 occurrences in this chapter

Equation form expr-8cd273e85fd60c89

f\colon P \to W

Read as: interpretation f is a function from prefix set P to world set W

Means: interpretation f is a function from prefix set P to world set W

1 occurrence in this chapter

Occurrence projected-formula-0027455

Equation form expr-8dc500341e756846

\sFmla{\True}{!A}[\sigma.n]

Read as: true formula A at prefix sigma dot n

Means: true formula A at prefix sigma dot n

2 occurrences in this chapter

Equation form expr-8f9aaf394ef17b96

\mSat{M}{!C}[f(\sigma)]

Read as: formula C is true at interpretation f of prefix sigma in model M

Means: formula C is true at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027522

Equation form expr-914737c3382d34c2

\sFmla{\False}{!A}[\sigma] \in \Delta

Read as: false formula A at prefix sigma belongs to Delta

Means: false formula A at prefix sigma belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027810

Equation form expr-9838b89d557550b4

\sFmla{\False}{!B}[\sigma]

Read as: false formula B at prefix sigma

Means: false formula B at prefix sigma

4 occurrences in this chapter

Equation form expr-99f464bb674e1e2f

\mSat/{M(\Delta)}{!B}[\sigma]

Read as: formula B is false at prefix sigma in model M of Delta

Means: formula B is false at prefix sigma in model M of Delta

3 occurrences in this chapter

Equation form expr-9a1aa907db88fe1f

\mSat{M(\Delta)}{!C}[\sigma]

Read as: formula C is true at prefix sigma in model M of Delta

Means: formula C is true at prefix sigma in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027832

Equation form expr-9c3245dfb4ac54c1

\sigma

Read as: prefix sigma

Means: prefix sigma

14 occurrences in this chapter

Equation form expr-9cc49755e722fb91

\sFmla{\True}{!A}[\sigma]

Read as: true formula A at prefix sigma

Means: true formula A at prefix sigma

2 occurrences in this chapter

Equation form expr-9db90411d96a9f72

\mSat/{M}{!B \lif !C}[f(\sigma)]

Read as: the conditional from formula B to formula C is false at interpretation f of prefix sigma in model M

Means: the conditional from formula B to formula C is false at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027534

Equation form expr-9ebc11c6465146d3

\sFmla{\True}{!B}[\sigma] \in \Delta

Read as: true formula B at prefix sigma belongs to Delta

Means: true formula B at prefix sigma belongs to Delta

2 occurrences in this chapter

Equation form expr-9ed185d202e0b9ca

\tuple{\ }

Read as: the empty sequence

Means: the empty sequence

1 occurrence in this chapter

Occurrence projected-formula-0027383

Equation form expr-a14ec3f38238b4d6

R\sigma(\sigma.n)

Read as: accessibility relation R holds from prefix sigma to prefix sigma dot n

Means: accessibility relation R holds from prefix sigma to prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027853

Equation form expr-a208e49539ec16d3

\sFmla{\True}{\Box !B}[\sigma] \in \Gamma

Read as: true necessarily formula B at prefix sigma belongs to Gamma

Means: true necessarily formula B at prefix sigma belongs to Gamma

4 occurrences in this chapter

Equation form expr-a301f6852f7cb93f

\sFmla{\True}{\Box !B}[\sigma.n]

Read as: true necessarily formula B at prefix sigma dot n

Means: true necessarily formula B at prefix sigma dot n

1 occurrence in this chapter

Occurrence projected-formula-0027740

Equation form expr-a374f128563b6def

\mSat{M(\Delta)}{!A}[\sigma]

Read as: formula A is true at prefix sigma in model M of Delta

Means: formula A is true at prefix sigma in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027809

Equation form expr-a416961eb56761c3

\sFmla{\False}{!C}[\sigma] \in \Delta

Read as: false formula C at prefix sigma belongs to Delta

Means: false formula C at prefix sigma belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027836

Equation form expr-a53a25ad7fa765d7

\sigma \concat \tuple{n}

Read as: prefix sigma concatenated with the one-element sequence n

Means: prefix sigma concatenated with the one-element sequence n

1 occurrence in this chapter

Occurrence projected-formula-0027388

Equation form expr-a5bf061e48c501d7

\sigma.3

Read as: prefix sigma dot three

Means: prefix sigma dot three

1 occurrence in this chapter

Occurrence projected-formula-0027390

Equation form expr-a97850b19ac36f58

\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1]

Read as: true B sub one through true B sub n at prefix one, followed by false A at prefix one

Means: true B sub one through true B sub n at prefix one, followed by false A at prefix one

1 occurrence in this chapter

Occurrence projected-formula-0027444

Equation form expr-aa8f4af5c142c59a

f(1) = w

Read as: interpretation f of prefix one equals world w

Means: interpretation f of prefix one equals world w

1 occurrence in this chapter

Occurrence projected-formula-0027614

Equation form expr-ab733e02bed54e75

\Gamma \Entails !A

Read as: Gamma semantically entails formula A

Means: Gamma semantically entails formula A

4 occurrences in this chapter

Equation form expr-ae839bfc37daea0a

\mSat/{M}{!B}[f(\sigma)]

Read as: formula B is false at interpretation f of prefix sigma in model M

Means: formula B is false at interpretation f of prefix sigma in model M

2 occurrences in this chapter

Equation form expr-b05e244762b1e472

1.1

Read as: prefix one point one

Means: prefix one point one

2 occurrences in this chapter

Equation form expr-b0c0b42f7e1a7499

\mSat{M}{\lnot !B}[f(\sigma)]

Read as: not formula B is true at interpretation f of prefix sigma in model M

Means: not formula B is true at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027508

Equation form expr-b303a371d23e11c8

\mSat{M}{\Box !B}[f(\sigma)]

Read as: necessarily formula B is true at interpretation f of prefix sigma in model M

Means: necessarily formula B is true at interpretation f of prefix sigma in model M

6 occurrences in this chapter

Equation form expr-b421307b9fc485b8

\sFmla{\False}{\Diamond !B}[\sigma] \in \Gamma

Read as: false possibly formula B at prefix sigma belongs to Gamma

Means: false possibly formula B at prefix sigma belongs to Gamma

3 occurrences in this chapter

Equation form expr-b4236f414ba063d4

\sFmla{\False}{!B \land !C}[\sigma] \in \Gamma

Read as: false the conjunction of formula B and formula C at prefix sigma belongs to Gamma

Means: false the conjunction of formula B and formula C at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027586

Equation form expr-b5b446abb4d0323b

\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

2 occurrences in this chapter

Equation form expr-b73878aa3d9c90ca

\sFmla{\True}{!A}[\sigma] \in \Delta

Read as: true formula A at prefix sigma belongs to Delta

Means: true formula A at prefix sigma belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027808

Equation form expr-b8a1bf1bab77ec11

\sigma'

Read as: prefix sigma prime

Means: prefix sigma prime

2 occurrences in this chapter

Equation form expr-bb67dd931d26c8e1

\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.

Read as: the set containing false A and true B sub one through true B sub n

Means: the set containing false A and true B sub one through true B sub n

1 occurrence in this chapter

Occurrence projected-formula-0027376

Equation form expr-bcdbfaccac910427

\mModel{M}, f

Read as: model M and interpretation f

Means: model M and interpretation f

9 occurrences in this chapter

Equation form expr-bcdf84e107e25cdc

\Sat{M}{\Gamma}[f]

Read as: Gamma is satisfied with respect to interpretation f in model M

Means: Gamma is satisfied with respect to interpretation f in model M

1 occurrence in this chapter

Occurrence projected-formula-0027563

Equation form expr-bdce57211b2c7626

\sFmla{\True}{\Box !B}[\sigma.n] \in \Gamma

Read as: true necessarily formula B at prefix sigma dot n belongs to Gamma

Means: true necessarily formula B at prefix sigma dot n belongs to Gamma

2 occurrences in this chapter

Equation form expr-bf13f30556ae5738

Rf(\sigma)w

Read as: accessibility relation R holds from interpretation f of prefix sigma to world w

Means: accessibility relation R holds from interpretation f of prefix sigma to world w

5 occurrences in this chapter

Equation form expr-bf1df883a744abb3

!A \land !B

Read as: the conjunction of formula A and formula B

Means: the conjunction of formula A and formula B

1 occurrence in this chapter

Occurrence projected-formula-0027398

Equation form expr-c280d69165733b4d

\sFmla{\True}{!B}[\sigma.n] \in \Delta

Read as: true formula B at prefix sigma dot n belongs to Delta

Means: true formula B at prefix sigma dot n belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027841

Equation form expr-c372d99f1f0b2736

\sFmla{\True}{!B}[\sigma.n]

Read as: true formula B at prefix sigma dot n

Means: true formula B at prefix sigma dot n

2 occurrences in this chapter

Equation form expr-c4e49a40ff2bb1f0

P \subseteq (\PosInt)^* \setminus \{\emptyseq\}

Read as: prefix set P is a subset of the set of nonempty finite sequences of positive integers

Means: prefix set P is a subset of the set of nonempty finite sequences of positive integers

1 occurrence in this chapter

Occurrence projected-formula-0027453

Equation form expr-c52df62ba446cfcb

\TRule{\True}{\Diamond}

Read as: true possibility rule

Means: true possibility rule

2 occurrences in this chapter

Equation form expr-c5ada008cc655003

\sFmla{\False}{!A}

Read as: false formula A

Means: false formula A

1 occurrence in this chapter

Occurrence projected-formula-0027372

Equation form expr-c7d083471edaf049

\Proves !A

Read as: formula A is derivable

Means: formula A is derivable

3 occurrences in this chapter

Equation form expr-c8db78df5316b38e

\sFmla{\True}{\Box !A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Means: true necessarily formula A at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027418

Equation form expr-cad706b77aef949a

\sFmla{\True}{!B \land !C}[\sigma] \in \Gamma

Read as: true the conjunction of formula B and formula C at prefix sigma belongs to Gamma

Means: true the conjunction of formula B and formula C at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027516

Equation form expr-cb25c8c90684f59b

V(p) = \{1.2\}

Read as: valuation V of p is the singleton containing one point two

Means: valuation V of p is the singleton containing one point two

1 occurrence in this chapter

Occurrence projected-formula-0027887

Equation form expr-cb8b58c892b5e758

\mSat/{M}{!C}[f(\sigma)]

Read as: formula C is false at interpretation f of prefix sigma in model M

Means: formula C is false at interpretation f of prefix sigma in model M

2 occurrences in this chapter

Equation form expr-cbbba670a3f47b53

\Gamma \Proves !A

Read as: Gamma derives formula A

Means: Gamma derives formula A

7 occurrences in this chapter

Equation form expr-ccd794a5a1928851

\sFmla{\True}{p}[1.2]

Read as: true p at prefix one point two

Means: true p at prefix one point two

1 occurrence in this chapter

Occurrence projected-formula-0027888

Equation form expr-cdb4ee2aea69cc6a

.

Read as: source period

Means: source period

1 occurrence in this chapter

Occurrence projected-formula-0027384

Equation form expr-d01fe6b0ab557c74

\mSat/{M}{!B \land !C}[f(\sigma)]

Read as: the conjunction of formula B and formula C is false at interpretation f of prefix sigma in model M

Means: the conjunction of formula B and formula C is false at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027590

Equation form expr-d03502c43d74a30b

,

Read as: source comma

Means: source comma

1 occurrence in this chapter

Occurrence projected-formula-0027385

Equation form expr-d055ee4dbcdd0c8b

!B

Read as: formula B

Means: formula B

1 occurrence in this chapter

Occurrence projected-formula-0027401

Equation form expr-d072c965a150a2e4

\sigma \notin V(p)

Read as: prefix sigma does not belong to valuation V of p

Means: prefix sigma does not belong to valuation V of p

1 occurrence in this chapter

Occurrence projected-formula-0027818

Equation form expr-d0a2b90b3d18abd7

\mModel{M}

Read as: model M

Means: model M

18 occurrences in this chapter

Equation form expr-d148fb86b1972296

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

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

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

1 occurrence in this chapter

Occurrence projected-formula-0027613

Equation form expr-d16b73ce79fc2dfd

\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

1 occurrence in this chapter

Occurrence projected-formula-0027570

Equation form expr-d2da161508eebc66

w \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-d315d7e4b5fa6640

\sFmla{\False}{\Box !B}[\sigma] \in \Gamma

Read as: false necessarily formula B at prefix sigma belongs to Gamma

Means: false necessarily formula B at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027555

Equation form expr-d44e11b041ae1e79

\mSat{M(\Delta)}{\indfrm}[\sigma]

Read as: the induction formula is true at prefix sigma in model M of Delta

Means: the induction formula is true at prefix sigma in model M of Delta

4 occurrences in this chapter

Equation form expr-d4657b8da2e75a37

\sFmla{\True}{!A}

Read as: true formula A

Means: true formula A

1 occurrence in this chapter

Occurrence projected-formula-0027371

Equation form expr-d4735e3a265e16ee

2

Read as: prefix two

Means: prefix two

1 occurrence in this chapter

Occurrence projected-formula-0027880

Equation form expr-d5db1613bac7d39c

\sFmla{\True}{!C}[\sigma] \in \Delta

Read as: true formula C at prefix sigma belongs to Delta

Means: true formula C at prefix sigma belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027830

Equation form expr-d629deeb0e872c5e

\mSat/{M(\Delta)}{!B}[\sigma']

Read as: formula B is false at prefix sigma prime in model M of Delta

Means: formula B is false at prefix sigma prime in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027855

Equation form expr-d9514a6468bb2595

\Box!A \lif \Box\Diamond!A

Read as: if necessarily formula A, then necessarily possibly formula A

Means: if necessarily formula A, then necessarily possibly formula A

1 occurrence in this chapter

Occurrence projected-formula-0027665

Equation form expr-d9ebbad91f38ff2f

\sFmla{\False}{\Diamond !B}[\sigma.n] \in \Gamma

Read as: false possibly formula B at prefix sigma dot n belongs to Gamma

Means: false possibly formula B at prefix sigma dot n belongs to Gamma

2 occurrences in this chapter

Equation form expr-da528f74f8845ade

\sigma.n

Read as: prefix sigma dot n

Means: prefix sigma dot n

19 occurrences in this chapter

Equation form expr-db8757ba1b5fc53f

\sigma' \in P(\Gamma)

Read as: prefix sigma prime belongs to the prefix set of Gamma

Means: prefix sigma prime belongs to the prefix set of Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027581

Equation form expr-dbcb6ec19cfc80e5

\Delta = \{\sFmla{\False}{!A}[1], \sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1]\}

Read as: Delta is the set containing false A at prefix one and true B sub one through true B sub n at prefix one

Means: Delta is the set containing false A at prefix one and true B sub one through true B sub n at prefix one

1 occurrence in this chapter

Occurrence projected-formula-0027606

Equation form expr-dc85a64738a53d1e

\sFmla{\True}{\indfrm}[\sigma] \notin \Delta

Read as: true the induction formula at prefix sigma does not belong to Delta

Means: true the induction formula at prefix sigma does not belong to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027817

Equation form expr-dd5ced94250ee670

\mSat{M}{\Gamma}[f']

Read as: Gamma is satisfied with respect to interpretation f prime in model M

Means: Gamma is satisfied with respect to interpretation f prime in model M

1 occurrence in this chapter

Occurrence projected-formula-0027582

Equation form expr-de5a6f78116eca62

V

Read as: V

Means: V

2 occurrences in this chapter

Equation form expr-deb233fb25cbf75b

\Box(p \lor q) \lif (\Box p \lor \Box q)

Read as: if necessarily the disjunction of p and q, then the disjunction of necessarily p and necessarily q

Means: if necessarily the disjunction of p and q, then the disjunction of necessarily p and necessarily q

2 occurrences in this chapter

Equation form expr-e13fe245d940f68a

\sFmla{\False}{\indfrm}[\sigma] \in \Delta

Read as: false the induction formula at prefix sigma belongs to Delta

Means: false the induction formula at prefix sigma belongs to Delta

4 occurrences in this chapter

Equation form expr-e141e0e5ae67e868

\sFmla{\True}{!B \lor !C}[\sigma]

Read as: true the disjunction of formula B and formula C at prefix sigma

Means: true the disjunction of formula B and formula C at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027786

Equation form expr-e42afbd86060e191

\mSat{M(\Delta)}{!B}[\sigma']

Read as: formula B is true at prefix sigma prime in model M of Delta

Means: formula B is true at prefix sigma prime in model M of Delta

1 occurrence in this chapter

Occurrence projected-formula-0027845

Equation form expr-e4692cb2e04e41ec

f(\sigma') = f'(\sigma')

Read as: interpretation f of prefix sigma prime equals interpretation f prime of prefix sigma prime

Means: interpretation f of prefix sigma prime equals interpretation f prime of prefix sigma prime

1 occurrence in this chapter

Occurrence projected-formula-0027580

Equation form expr-e8acd579b14893cc

\sigma \in (\PosInt)^* \setminus \{\emptyseq\}

Read as: prefix sigma belongs to the set of nonempty finite sequences of positive integers

Means: prefix sigma belongs to the set of nonempty finite sequences of positive integers

1 occurrence in this chapter

Occurrence projected-formula-0027382

Equation form expr-ea6ad66fc089660a

\sFmla{\True}{\Box !B}[\sigma]

Read as: true necessarily formula B at prefix sigma

Means: true necessarily formula B at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027761

Equation form expr-eb45097515077452

\mSat/{M(\Delta)}{\indfrm}[\sigma]

Read as: the induction formula is false at prefix sigma in model M of Delta

Means: the induction formula is false at prefix sigma in model M of Delta

4 occurrences in this chapter

Equation form expr-ef2e8f6fac20e974

\sFmla{\True}{!B}[\sigma]

Read as: true formula B at prefix sigma

Means: true formula B at prefix sigma

9 occurrences in this chapter

Equation form expr-f157f71e0163a897

\Box

Read as: the necessity operator

Means: the necessity operator

27 occurrences in this chapter

Equation form expr-f192680bfea27cb4

\Box(p \land q) \lif \Box p

Read as: if necessarily the conjunction of p and q, then necessarily p

Means: if necessarily the conjunction of p and q, then necessarily p

1 occurrence in this chapter

Occurrence projected-formula-0027443

Equation form expr-f1941b975ffcc891

\Delta

Read as: Delta

Means: Delta

4 occurrences in this chapter

Equation form expr-f427cdcccd62d1ab

\Box \lnot p \lif \Box(p \lif q)

Read as: if necessarily not p, then necessarily the conditional from p to q

Means: if necessarily not p, then necessarily the conditional from p to q

1 occurrence in this chapter

Occurrence projected-formula-0027440

Equation form expr-f4e29ee4ec46b067

\sFmla{\True}{\Diamond !A}[\sigma]

Read as: true possibly formula A at prefix sigma

Means: true possibly formula A at prefix sigma

1 occurrence in this chapter

Occurrence projected-formula-0027428

Equation form expr-f65af037e8662390

\Entails/ !A

Read as: formula A is not semantically valid

Means: formula A is not semantically valid

1 occurrence in this chapter

Occurrence projected-formula-0027868

Equation form expr-f6e49c596decc774

\Log{KT5} \Proves \Ax{4}

Read as: logic K T five derives axiom four

Means: logic K T five derives axiom four

1 occurrence in this chapter

Occurrence projected-formula-0027668

Equation form expr-f9baaf9f77711629

\False

Read as: false sign

Means: false sign

3 occurrences in this chapter

Equation form expr-fae0e8eec6e2c400

\TRule{\True}{\land}

Read as: true conjunction rule

Means: true conjunction rule

1 occurrence in this chapter

Occurrence projected-formula-0027515

Equation form expr-fbd3e9ce9e6e8f31

\mSat{M}{!B \land !C}[f(\sigma)]

Read as: the conjunction of formula B and formula C is true at interpretation f of prefix sigma in model M

Means: the conjunction of formula B and formula C is true at interpretation f of prefix sigma in model M

1 occurrence in this chapter

Occurrence projected-formula-0027520

Equation form expr-fc0a9fb41d713e25

P(\Gamma) \cup \{\sigma.n\}

Read as: the prefix set of Gamma union the set containing prefix sigma dot n

Means: the prefix set of Gamma union the set containing prefix sigma dot n

2 occurrences in this chapter

Equation form expr-fe655a6b4f57748d

\sFmla{\True}{!B \lif !C}[\sigma] \in \Gamma

Read as: true the conditional from formula B to formula C at prefix sigma belongs to Gamma

Means: true the conditional from formula B to formula C at prefix sigma belongs to Gamma

1 occurrence in this chapter

Occurrence projected-formula-0027600

Equation form expr-ff0ef5c23edbf7bf

!B_1

Read as: formula B sub one

Means: formula B sub one

1 occurrence in this chapter

Occurrence projected-formula-0027604

Equation form expr-ff881d692fa73729

V(p) = \Setabs{\sigma}{\sFmla{\True}{p}[\sigma] \in \Delta}.

Read as: valuation V of p is the set of prefixes sigma such that true p at prefix sigma belongs to Delta

Means: valuation V of p is the set of prefixes sigma such that true p at prefix sigma belongs to Delta

1 occurrence in this chapter

Occurrence projected-formula-0027806

Propositional prefixed-tableau rule table

Four source rows pair the true and false rules for negation, conjunction, disjunction, and the conditional. Branching and stacked conclusions are retained exactly.

Source

True-negation tableau rule

From true not A at prefix sigma, infer false A at prefix sigma.

Source

False-negation tableau rule

From false not A at prefix sigma, infer true A at prefix sigma.

Source

True-conjunction tableau rule

From true A and B at prefix sigma, stack true A and true B at the same prefix.

Source

False-conjunction tableau rule

From false A and B at prefix sigma, branch to false A or false B at the same prefix.

Source

True-disjunction tableau rule

From true A or B at prefix sigma, branch to true A or true B at the same prefix.

Source

False-disjunction tableau rule

From false A or B at prefix sigma, stack false A and false B at the same prefix.

Source

True-conditional tableau rule

From true if A then B at prefix sigma, branch to false A or true B at the same prefix.

Source

False-conditional tableau rule

From false if A then B at prefix sigma, stack true A and false B at the same prefix.

Source

Outer table for the four modal K rules

The source table wraps the inner two-column tabular. Listener authority belongs to that inner table so the four rules and used-or-new side conditions are not duplicated.

Source

Four modal K tableau rules

Two necessity rules and two possibility rules distinguish conclusions at used prefixes from conclusions at new prefixes.

Source

True-necessity used-prefix rule

From true necessarily A at prefix sigma, infer true A at prefix sigma dot n, where sigma dot n is used.

Source

False-necessity new-prefix rule

From false necessarily A at prefix sigma, infer false A at a new prefix sigma dot n.

Source

True-possibility new-prefix rule

From true possibly A at prefix sigma, infer true A at a new prefix sigma dot n.

Source

False-possibility used-prefix rule

From false possibly A at prefix sigma, infer false A at prefix sigma dot n, where sigma dot n is used.

Source

Closed necessity-versus-possibility tableau

A four-node linear tableau closes true necessarily A against false possibly A at prefix one by producing true and false A at prefix one point one.

Source

Closed possibility-versus-necessity tableau

A four-node linear tableau closes true possibly A against false necessarily A at prefix one by producing true and false A at prefix one point one.

Source

Closed tableau for distributing necessity over conjunction

The example gives the two-branch closed tableau deriving that necessarily A and necessarily B implies necessarily A and B.

Source

Tableau for necessity and conjunction

The tableau expands the negated conditional, creates a new prefix, branches on false A and B, and closes each branch against the corresponding boxed premise.

Source

Closed tableau for distributing possibility over disjunction

The example gives the two-branch closed tableau deriving that possibly A or B implies possibly A or possibly B.

Source

Tableau for possibility and disjunction

The tableau expands the negated conditional, creates one successor, branches on true A or B, and closes both branches against their false possibility premises.

Source

Exercise constructing four closed K tableaux

Find closed tableaux for the four printed modal formulas. The source supplies no solutions; the exercise remains unsolved.

Source

Interpretation of tableau prefixes in a model

An interpretation maps a set of nonempty positive-integer prefixes into model worlds and preserves each printed parent-to-child accessibility relation; truth and falsity of signed formulas are then defined through that map.

Source

Satisfaction and satisfiability of a prefixed set

A model satisfies Gamma with respect to an interpretation when it satisfies every prefixed formula in Gamma; Gamma is satisfiable when such a model and interpretation exist.

Source

Contradictory signed formulas are unsatisfiable

If Gamma contains true A and false A at the same prefix, then Gamma is unsatisfiable.

Source

Soundness of closed tableaux

If Gamma has a closed tableau, then Gamma is unsatisfiable.

Source

Exercise completing tableau soundness

Complete the preceding soundness proof. The source does not supply the omitted cases, so the exercise remains unsolved.

Source

Entailment soundness corollary

If Gamma derives A by the tableau system, then Gamma semantically entails A.

Source

Weak soundness corollary

If A is derivable, then A is true in every model.

Source

Outer table for additional modal rules

The source table wraps the inner listener table containing ten T, D, B, four, and four-r rules.

Source

Additional modal tableau rules

Five paired rows give the necessity and possibility forms of the reflexive, serial, symmetric, transitive, and euclidean-reverse rules, including the printed used-prefix condition.

Source

Reflexive true-necessity rule

Rule T necessity: from true necessarily A at prefix sigma, infer true A at prefix sigma.

Source

Reflexive false-possibility rule

Rule T possibility: from false possibly A at prefix sigma, infer false A at prefix sigma.

Source

Serial true-necessity rule

Rule D necessity: from true necessarily A at prefix sigma, infer true possibly A at prefix sigma.

Source

Serial false-possibility rule

Rule D possibility: from false possibly A at prefix sigma, infer false necessarily A at prefix sigma.

Source

Symmetric true-necessity rule

Rule B necessity: from true necessarily A at prefix sigma dot n, infer true A at prefix sigma.

Source

Symmetric false-possibility rule

Rule B possibility: from false possibly A at prefix sigma dot n, infer false A at prefix sigma.

Source

Transitive true-necessity rule

Rule four necessity: from true necessarily A at prefix sigma, infer true necessarily A at used prefix sigma dot n.

Source

Transitive false-possibility rule

Rule four possibility: from false possibly A at prefix sigma, infer false possibly A at used prefix sigma dot n.

Source

Euclidean reverse true-necessity rule

Rule four r necessity: from true necessarily A at prefix sigma dot n, infer true necessarily A at prefix sigma.

Source

Euclidean reverse false-possibility rule

Rule four r possibility: from false possibly A at prefix sigma dot n, infer false possibly A at prefix sigma.

Source

Outer logic-and-rule correspondence table

The source table wraps the inner three-column table. Listener authority belongs only to the inner tabular.

Source

Modal logics, frame conditions, and tableau rules

Six source rows associate T, D, K four, B, S four, and S five with their printed relation properties and rule families.

Source

Closed S five tableau for axiom five

The example proves necessarily A implies necessarily possibly A using the ordinary K rules and the four-r possibility rule, ending in a closure at prefix one point one.

Source

Tableau proof of axiom five in S five

A seven-node linear tableau applies false conditional, false necessity, four-r possibility, false possibility, and true necessity rules, then closes on A at prefix one point one.

Source

Exercise proving six modal derivabilities

Construct closed tableaux for the six displayed derivability claims. No tableaux are supplied; the exercise remains unsolved.

Source

Soundness of the reflexive rules

The T necessity and T possibility rules are sound for reflexive models.

Source

Exercise completing reflexive-rule soundness

Complete the proof of soundness for the selected T rule cases. The omitted work remains unsolved.

Source

Soundness of the serial rules

The D necessity and D possibility rules are sound for serial models.

Source

Exercise completing serial-rule soundness

Complete the proof of soundness for the selected D rule cases. The omitted work remains unsolved.

Source

Soundness of the symmetric rules

The B necessity and B possibility rules are sound for symmetric models.

Source

Exercise completing symmetric-rule soundness

Complete the proof of soundness for the selected B rule cases. The omitted work remains unsolved.

Source

Soundness of the transitive rules

The four necessity and four possibility rules are sound for transitive models.

Source

Exercise completing transitive-rule soundness

Complete the proof of soundness for the selected four-rule cases. The omitted work remains unsolved.

Source

Soundness of the euclidean rules

The four-r necessity and four-r possibility rules are sound for euclidean models.

Source

Exercise completing euclidean-rule soundness

Complete the proof of soundness for the selected four-r rule cases. The omitted work remains unsolved.

Source

Soundness of the listed modal tableau systems

The tableau systems in the logic-and-rule table are sound for their respective classes of models.

Source

Outer table for simplified S five rules

The outer table wraps the inner listener table; its four rules are not repeated as a second listener structure.

Source

Simplified S five tableau rules

Four rules use arbitrary used or new prefixes m rather than prefix extensions sigma dot n.

Source

Simplified S five true-necessity rule

From true necessarily A at prefix n, infer true A at any used prefix m.

Source

Simplified S five false-necessity rule

From false necessarily A at prefix n, infer false A at a new prefix m.

Source

Simplified S five true-possibility rule

From true possibly A at prefix n, infer true A at a new prefix m.

Source

Simplified S five false-possibility rule

From false possibly A at prefix n, infer false A at any used prefix m.

Source

Simplified S five tableau for axiom five

A six-node linear tableau derives possibly A implies necessarily possibly A and closes on A at prefix three.

Source

Simplified S five tableau proof

The tableau uses prefixes one, two, and three, applies false conditional, false necessity, true possibility, and false possibility, and closes at prefix three.

Source

Complete tableau branch

A branch is complete when every applicable propositional or modal rule has the required printed conclusions, including every used-prefix conclusion and at least one new-prefix conclusion.

Source

Existence of a complete tableau

Every finite Gamma has a tableau in which every branch is complete.

Source

Completeness of closed tableaux

If Gamma has no closed tableau, then Gamma is satisfiable.

Source

Exercise completing tableau completeness

Complete the proof of the preceding completeness theorem. The omitted proof remains unsolved.

Source

Entailment completeness corollary

If Gamma semantically entails A, then Gamma derives A.

Source

Weak completeness corollary

If A is true in every model, then A is derivable.

Source

Countermodel construction for failed box distribution

The example expands a nonderivable formula through three tableau stages, identifies one open complete branch, and reads a three-world countermodel from it.

Source

Initial unfinished countermodel tableau

Seven linear nodes expand the failed box-distribution formula and introduce prefixes one point one and one point two. The source explicitly says the tableau is unfinished.

Source

Second unfinished countermodel tableau

Nine linear nodes additionally apply true necessity at both used prefixes. The source continues the construction, so this tableau is unfinished.

Source

Complete countermodel tableau

The third tableau branches three ways: two branches close and the middle branch remains open and complete, supplying the countermodel valuation.

Source

Figure containing the three-world countermodel

The figure contains the source graph with three worlds, six printed p-and-q valuations, and two directed accessibility edges.

Source

Three-world countermodel graph

World one points to worlds one point one and one point two. The graph prints both p and q at every world and no other edge or valuation.

Source

Cross-reference reference-001107

the propositional prefixed-tableau rule table

Source occurrence

Cross-reference reference-001108

the four modal K tableau rules

Source occurrence

Cross-reference reference-001109

the tableau soundness theorem

Source occurrence

Cross-reference reference-001110

the tableau soundness theorem

Source occurrence

Cross-reference reference-001111

the additional modal tableau rule table

Source occurrence

Cross-reference reference-001112

the modal logics, frame conditions, and rules table

Source occurrence

Cross-reference reference-001113

the proposition on soundness of the reflexive rules

Source occurrence

Cross-reference reference-001114

the proposition on soundness of the serial rules

Source occurrence

Cross-reference reference-001115

the proposition on soundness of the symmetric rules

Source occurrence

Cross-reference reference-001116

the proposition on soundness of the transitive rules

Source occurrence

Cross-reference reference-001117

the proposition on soundness of the euclidean rules

Source occurrence

Cross-reference reference-001118

the modal logics, frame conditions, and rules table

Source occurrence

Cross-reference reference-001119

the simplified S five tableau rule table

Source occurrence

Cross-reference reference-001120

the tableau completeness theorem

Source occurrence

Cross-reference reference-001121

the proposition that every finite Gamma has a complete tableau

Source occurrence

Cross-reference reference-001122

the tableau completeness theorem

Source occurrence

Cross-reference reference-001123

the three-world countermodel figure

Source occurrence

Source disclosures

TR055-SAR-001: Source caveat. The contrapositive paragraph says A is true at w, while its preceding entailment claim and the next sentence describe a countermodel. The printed positive satisfaction statement is retained. source
TR055-SAR-002: Source caveat. The false-necessity case first calls its new conclusion false A at sigma dot n, then immediately constructs and proves satisfiable the set with false B there. Both source occurrences remain unchanged. source
TR055-SAR-003: Source caveat. The soundness-corollary proof ends by repeating derivability, although the contradiction was introduced to establish semantic entailment. The printed conclusion remains discoverable. source
TR055-SAR-011: Source caveat. The euclidean necessity proof places dot n outside the closing parenthesis of f of sigma. Speech preserves that source placement rather than silently changing it to f of sigma dot n. source
TR055-SAR-012: Source caveat. The four-r possibility case says its new signed formula is true necessarily B, while the case begins and ends with false possibility B. The true-necessity source formula is retained. source
TR055-SAR-004: Source caveat. The complete-branch example for a true disjunction prints false B as its first alternative and true C as its second. Those signs are retained exactly. source
TR055-SAR-005: Source caveat. The modal completeness examples print signed necessity or possibility operators without a formula operand. Speech explicitly identifies the missing printed operand rather than supplying A or B. source
TR055-SAR-006: Source caveat. The construction proposition claims every branch is complete, but its proof's final sentence says every branch is closed. The sentence is preserved as written. source
TR055-SAR-007: Source caveat. The duplicated source wording 'thas has' is preserved in prose and noted; no mathematical content is inferred from it. source
TR055-SAR-008: Source caveat. The false-conjunction induction case repeats false B in its second semantic alternative where the signed premises just named false B or false C. The repeated B remains unchanged. source
TR055-SAR-009: Source caveat. The false-disjunction induction case repeats false B in its second conjunct where the signed premises just named false B and false C. The repeated B remains unchanged. source
TR055-SAR-010: Source caveat. The false-conditional induction case prints true B and false B as its semantic pair, though the signed premises are true B and false C. The second B remains unchanged. source
TR055-SAR-013: Source caveat. The first countermodel-method sentence omits the usual formula-marker exclamation before A. Speech explicitly reports the source expression without supplying the missing marker. source

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

\sFmla{\True}{\Box !A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Read in context source

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

\TRule{\True}{\Box}

Read as: true necessity rule

Read in context source

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

\sFmla{\True}{!A}[\sigma.n]

Read as: true formula A at prefix sigma dot n

Read in context source

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

\sFmla{\False}{\Box !A}[\sigma]

Read as: false necessarily formula A at prefix sigma

Read in context source

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

\TRule{\False}{\Box}

Read as: false necessity rule

Read in context source

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

\sFmla{\False}{!A}[\sigma.n]

Read as: false formula A at prefix sigma dot n

Read in context source

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

\sFmla{\True}{\Diamond !A}[\sigma]

Read as: true possibly formula A at prefix sigma

Read in context source

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

\TRule{\True}{\Diamond}

Read as: true possibility rule

Read in context source

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

\sFmla{\True}{!A}[\sigma.n]

Read as: true formula A at prefix sigma dot n

Read in context source

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

\sFmla{\False}{\Diamond !A}[\sigma]

Read as: false possibly formula A at prefix sigma

Read in context source

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

\TRule{\False}{\Diamond}

Read as: false possibility rule

Read in context source

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

\sFmla{\False}{!A}[\sigma.n]

Read as: false formula A at prefix sigma dot n

Read in context source

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

\TRule{\True}{\Box}

Read as: true necessity rule

Read in context source

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

\sFmla{\True}{\Box \formula{A}}[1]

Read as: true necessarily formula A at prefix one

Read in context source

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

\sFmla{\False}{\Diamond \formula{A}}[1]

Read as: false possibly formula A at prefix one

Read in context source

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

\sFmla{\True}{\formula{A}}[1.1]

Read as: true formula A at prefix one point one

Read in context source

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

\sFmla{\False}{\formula{A}}[1.1]

Read as: false formula A at prefix one point one

Read in context source

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

\TRule{\False}{\Box}

Read as: false necessity rule

Read in context source

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

\sFmla{\True}{\Diamond \formula{A}}[1]

Read as: true possibly formula A at prefix one

Read in context source

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

\sFmla{\False}{\Box \formula{A}}[1]

Read as: false necessarily formula A at prefix one

Read in context source

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

\sFmla{\True}{\formula{A}}[1.1]

Read as: true formula A at prefix one point one

Read in context source

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

\sFmla{\False}{\formula{A}}[1.1]

Read as: false formula A at prefix one point one

Read in context source

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

\sFmla{\False}{(\Box\formula{A} \land \Box\formula{B}) \lif \Box (\formula{A} \land \formula{B})}[1]

Read as: false the conditional from the conjunction of necessarily formula A and necessarily formula B to necessarily the conjunction of formula A and formula B at prefix one

Read in context source

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

\sFmla{\True}{\Box\formula{A} \land \Box\formula{B}}[1]

Read as: true the conjunction of necessarily formula A and necessarily formula B at prefix one

Read in context source

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

\sFmla{\False}{\Box(\formula{A} \land \formula{B})}[1]

Read as: false necessarily the conjunction of formula A and formula B at prefix one

Read in context source

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

\sFmla{\True}{\Box\formula{A}}[1]

Read as: true necessarily formula A at prefix one

Read in context source

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

\sFmla{\True}{\Box\formula{B}}[1]

Read as: true necessarily formula B at prefix one

Read in context source

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

\sFmla{\False}{\formula{A} \land \formula{B}}[1.1]

Read as: false the conjunction of formula A and formula B at prefix one point one

Read in context source

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

\sFmla{\False}{\formula{A}}[1.1]

Read as: false formula A at prefix one point one

Read in context source

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

\sFmla{\True}{\formula{A}}[1.1]

Read as: true formula A at prefix one point one

Read in context source

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

\sFmla{\False}{\formula{B}}[1.1]

Read as: false formula B at prefix one point one

Read in context source

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

\sFmla{\True}{\formula{B}}[1.1]

Read as: true formula B at prefix one point one

Read in context source

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

\sFmla{\False}{\Diamond(\formula{A} \lor \formula{B}) \lif (\Diamond \formula{A} \lor \Diamond \formula{B})}[1]

Read as: false the conditional from possibly the disjunction of formula A and formula B to the disjunction of possibly formula A and possibly formula B at prefix one

Read in context source

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

\sFmla{\True}{\Diamond(\formula{A} \lor \formula{B})}[1]

Read as: true possibly the disjunction of formula A and formula B at prefix one

Read in context source

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

\sFmla{\False}{\Diamond\formula{A} \lor \Diamond\formula{B}}[1]

Read as: false the disjunction of possibly formula A and possibly formula B at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0037

\sFmla{\False}{\Diamond\formula{A}}[1]

Read as: false possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0038

\sFmla{\False}{\Diamond\formula{B}}[1]

Read as: false possibly formula B at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0039

\sFmla{\True}{\formula{A} \lor \formula{B}}[1.1]

Read as: true the disjunction of formula A and formula B at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0040

\sFmla{\True}{\formula{A}}[1.1]

Read as: true formula A at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0041

\sFmla{\False}{\formula{A}}[1.1]

Read as: false formula A at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0042

\sFmla{\True}{\formula{B}}[1.1]

Read as: true formula B at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0043

\sFmla{\False}{\formula{B}}[1.1]

Read as: false formula B at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0044

\sFmla{\True}{\Box !A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0045

\sFmla{\True}{!A}[\sigma]

Read as: true formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0046

\sFmla{\False}{\Diamond !A}[\sigma]

Read as: false possibly formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0047

\sFmla{\False}{!A}[\sigma]

Read as: false formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0048

\sFmla{\True}{\Box !A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0049

\sFmla{\True}{\Diamond!A}[\sigma]

Read as: true possibly formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0050

\sFmla{\False}{\Diamond !A}[\sigma]

Read as: false possibly formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0051

\sFmla{\False}{\Box!A}[\sigma]

Read as: false necessarily formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0052

\sFmla{\True}{\Box !A}[\sigma.n]

Read as: true necessarily formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0053

\sFmla{\True}{!A}[\sigma]

Read as: true formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0054

\sFmla{\False}{\Diamond !A}[\sigma.n]

Read as: false possibly formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0055

\sFmla{\False}{!A}[\sigma]

Read as: false formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0056

\sFmla{\True}{\Box !A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0057

\sFmla{\True}{\Box!A}[\sigma.n]

Read as: true necessarily formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0058

\sFmla{\False}{\Diamond !A}[\sigma]

Read as: false possibly formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0059

\sFmla{\False}{\Diamond!A}[\sigma.n]

Read as: false possibly formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0060

\sFmla{\True}{\Box !A}[\sigma.n]

Read as: true necessarily formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0061

\sFmla{\True}{\Box!A}[\sigma]

Read as: true necessarily formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0062

\sFmla{\False}{\Diamond !A}[\sigma.n]

Read as: false possibly formula A at prefix sigma dot n

Read in context source

Source-generated case expression tr055-source-macro-0063

\sFmla{\False}{\Diamond!A}[\sigma]

Read as: false possibly formula A at prefix sigma

Read in context source

Source-generated case expression tr055-source-macro-0064

\sFmla{\False}{\Box\formula{A} \lif \Box\Diamond \formula{A}}[1]

Read as: false the conditional from necessarily formula A to necessarily possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0065

\sFmla{\True}{\Box \formula{A}}[1]

Read as: true necessarily formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0066

\sFmla{\False}{\Box\Diamond \formula{A}}[1]

Read as: false necessarily possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0067

\sFmla{\False}{\Diamond \formula{A}}[1.1]

Read as: false possibly formula A at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0068

\sFmla{\False}{\Diamond \formula{A}}[1]

Read as: false possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0069

\sFmla{\False}{\formula{A}}[1.1]

Read as: false formula A at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0070

\sFmla{\True}{\formula{A}}[1.1]

Read as: true formula A at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0071

\sFmla{\True}{\Box !A}[n]

Read as: true necessarily formula A at prefix n

Read in context source

Source-generated case expression tr055-source-macro-0072

\TRule{\True}{\Box}

Read as: true necessity rule

Read in context source

Source-generated case expression tr055-source-macro-0073

\sFmla{\True}{!A}[m]

Read as: true formula A at prefix m

Read in context source

Source-generated case expression tr055-source-macro-0074

\sFmla{\False}{\Box !A}[n]

Read as: false necessarily formula A at prefix n

Read in context source

Source-generated case expression tr055-source-macro-0075

\TRule{\False}{\Box}

Read as: false necessity rule

Read in context source

Source-generated case expression tr055-source-macro-0076

\sFmla{\False}{!A}[m]

Read as: false formula A at prefix m

Read in context source

Source-generated case expression tr055-source-macro-0077

\sFmla{\True}{\Diamond !A}[n]

Read as: true possibly formula A at prefix n

Read in context source

Source-generated case expression tr055-source-macro-0078

\TRule{\True}{\Diamond}

Read as: true possibility rule

Read in context source

Source-generated case expression tr055-source-macro-0079

\sFmla{\True}{!A}[m]

Read as: true formula A at prefix m

Read in context source

Source-generated case expression tr055-source-macro-0080

\sFmla{\False}{\Diamond !A}[n]

Read as: false possibly formula A at prefix n

Read in context source

Source-generated case expression tr055-source-macro-0081

\TRule{\False}{\Diamond}

Read as: false possibility rule

Read in context source

Source-generated case expression tr055-source-macro-0082

\sFmla{\False}{!A}[m]

Read as: false formula A at prefix m

Read in context source

Source-generated case expression tr055-source-macro-0083

\sFmla{\False}{\Diamond\formula{A} \lif \Box\Diamond \formula{A}}[1]

Read as: false the conditional from possibly formula A to necessarily possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0084

\sFmla{\True}{\Diamond \formula{A}}[1]

Read as: true possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0085

\sFmla{\False}{\Box\Diamond \formula{A}}[1]

Read as: false necessarily possibly formula A at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0086

\sFmla{\False}{\Diamond \formula{A}}[2]

Read as: false possibly formula A at prefix two

Read in context source

Source-generated case expression tr055-source-macro-0087

\sFmla{\True}{\formula{A}}[3]

Read as: true formula A at prefix three

Read in context source

Source-generated case expression tr055-source-macro-0088

\sFmla{\False}{\formula{A}}[3]

Read as: false formula A at prefix three

Read in context source

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

!A \ident p

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

Read in context source

Source-generated case expression tr055-source-macro-0124

!A \ident \lnot !B

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

Read in context source

Source-generated case expression tr055-source-macro-0125

!A \ident !B \land !C

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

Read in context source

Source-generated case expression tr055-source-macro-0126

!A \ident !B \lor !C

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

Read in context source

Source-generated case expression tr055-source-macro-0127

!A \ident !B \lif !C

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

Read in context source

Source-generated case expression tr055-source-macro-0128

!A \ident \Box !B

Read as: Case: A is necessarily B.

Read in context source

Source-generated case expression tr055-source-macro-0129

!A \ident \Diamond !B

Read as: Case: A is possibly B.

Read in context source

Source-generated case expression tr055-source-macro-0089

\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]

Read as: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0090

\sFmla{\True}{\Box(p \lor q)}[1]

Read as: true necessarily the disjunction of p and q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0091

\sFmla{\False}{\Box p \lor \Box q}[1]

Read as: false the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0092

\sFmla{\False}{\Box p}[1]

Read as: false necessarily p at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0093

\sFmla{\False}{\Box q}[1]

Read as: false necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0094

\sFmla{\False}{p}[1.1]

Read as: false p at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0095

\sFmla{\False}{q}[1.2]

Read as: false q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0096

\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]

Read as: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0097

\sFmla{\True}{\Box(p \lor q)}[1]

Read as: true necessarily the disjunction of p and q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0098

\sFmla{\False}{\Box p \lor \Box q}[1]

Read as: false the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0099

\sFmla{\False}{\Box p}[1]

Read as: false necessarily p at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0100

\sFmla{\False}{\Box q}[1]

Read as: false necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0101

\sFmla{\False}{p}[1.1]

Read as: false p at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0102

\sFmla{\False}{q}[1.2]

Read as: false q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0103

\sFmla{\True}{p \lor q}[1.1]

Read as: true the disjunction of p and q at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0104

\sFmla{\True}{p \lor q}[1.2]

Read as: true the disjunction of p and q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0105

\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]

Read as: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0106

\sFmla{\True}{\Box(p \lor q)}[1]

Read as: true necessarily the disjunction of p and q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0107

\sFmla{\False}{\Box p \lor \Box q}[1]

Read as: false the disjunction of necessarily p and necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0108

\sFmla{\False}{\Box p}[1]

Read as: false necessarily p at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0109

\sFmla{\False}{\Box q}[1]

Read as: false necessarily q at prefix one

Read in context source

Source-generated case expression tr055-source-macro-0110

\sFmla{\False}{p}[1.1]

Read as: false p at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0111

\sFmla{\False}{q}[1.2]

Read as: false q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0112

\sFmla{\True}{p \lor q}[1.1]

Read as: true the disjunction of p and q at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0113

\sFmla{\True}{p \lor q}[1.2]

Read as: true the disjunction of p and q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0114

\sFmla{\True}{p}[1.1]

Read as: true p at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0115

\sFmla{\True}{q}[1.1]

Read as: true q at prefix one point one

Read in context source

Source-generated case expression tr055-source-macro-0116

\sFmla{\True}{p}[1.2]

Read as: true p at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0117

\sFmla{\True}{q}[1.2]

Read as: true q at prefix one point two

Read in context source

Source-generated case expression tr055-source-macro-0118

\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr055-source-macro-0119

\mFalse{q}

Read as: q is false

Read in context source

Source-generated case expression tr055-source-macro-0120

\mFalse{p}

Read as: p is false

Read in context source

Source-generated case expression tr055-source-macro-0121

\mTrue{q}

Read as: q is true

Read in context source

Source-generated case expression tr055-source-macro-0122

\mTrue{p}

Read as: p is true

Read in context source

Source-generated case expression tr055-source-macro-0123

\mFalse{q}

Read as: q is false

Read in context source

Ordered structures

Propositional prefixed-tableau rule table

Structure: table.

Propositional prefixed-tableau rule table. Propositional prefixed tableau rules. Row one, true negation: from true not A at prefix sigma, infer false A at prefix sigma. False negation: from false not A at prefix sigma, infer true A at prefix sigma. Row two, true conjunction: from true A and B at prefix sigma, stack true A and true B at that prefix. False conjunction: from false A and B at prefix sigma, branch to false A or false B at that prefix. Row three, true disjunction: from true A or B at prefix sigma, branch to true A or true B at that prefix. False disjunction: from false A or B at prefix sigma, stack false A and false B at that prefix. Row four, true conditional: from true if A then B at prefix sigma, branch to false A or true B at that prefix. False conditional: from false if A then B at prefix sigma, stack true A and false B at that prefix. End propositional rule table. End table.

Read the source-bound structure in context

Four modal K tableau rules

Structure: table.

Four modal K rules. Headers: true-sign rule; false-sign rule. Row one, necessity. Premise true necessarily formula A at prefix sigma. Rule true necessity rule. Conclusion true formula A at prefix sigma dot n. Premise false necessarily formula A at prefix sigma. Rule false necessity rule. Conclusion false formula A at prefix sigma dot n. Side conditions: prefix sigma dot n; prefix sigma dot n. Row two, possibility. Premise true possibly formula A at prefix sigma. Rule true possibility rule. Conclusion true formula A at prefix sigma dot n. Premise false possibly formula A at prefix sigma. Rule false possibility rule. Conclusion false formula A at prefix sigma dot n. Side conditions: prefix sigma dot n; prefix sigma dot n. End modal K rule table.

Read the source-bound structure in context

Closed necessity-versus-possibility tableau

Structure: tableau.

Closed necessity-versus-possibility tableau. Node one: true necessarily formula A at prefix one. Rule: tableau assumption. Node two: false possibly formula A at prefix one. Rule: tableau assumption. Node three: true formula A at prefix one point one. Rule: true necessity rule, depending on node one. Node four: false formula A at prefix one point one. Rule: false possibility rule, depending on node two; source close marker present. Branch one is closed, closed by nodes three and four. End tableau.

Read the source-bound structure in context

Closed possibility-versus-necessity tableau

Structure: tableau.

Closed possibility-versus-necessity tableau. Node one: true possibly formula A at prefix one. Rule: tableau assumption. Node two: false necessarily formula A at prefix one. Rule: tableau assumption. Node three: true formula A at prefix one point one. Rule: true possibility rule, depending on node one. Node four: false formula A at prefix one point one. Rule: false necessity rule, depending on node two; source close marker present. Branch one is closed, closed by nodes three and four. End tableau.

Read the source-bound structure in context

Tableau for necessity and conjunction

Structure: tableau.

Tableau for necessity and conjunction. Node one: false the conditional from the conjunction of necessarily formula A and necessarily formula B to necessarily the conjunction of formula A and formula B at prefix one. Rule: tableau assumption. Node two: true the conjunction of necessarily formula A and necessarily formula B at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily the conjunction of formula A and formula B at prefix one. Rule: false conditional rule, depending on node one. Node four: true necessarily formula A at prefix one. Rule: true conjunction rule, depending on node two. Node five: true necessarily formula B at prefix one. Rule: true conjunction rule, depending on node two. Node six: false the conjunction of formula A and formula B at prefix one point one. Rule: false necessity rule, depending on node three. Node seven: false formula A at prefix one point one. Rule: false conjunction rule, depending on node six. Node eight: true formula A at prefix one point one. Rule: true necessity rule, depending on node four; source close marker present. Node nine: false formula B at prefix one point one. Rule: false conjunction rule, depending on node six. Node one zero: true formula B at prefix one point one. Rule: true necessity rule, depending on node five; source close marker present. Branch one is closed, closed by nodes seven and eight. Branch two is closed, closed by nodes nine and one zero. End tableau.

Read the source-bound structure in context

Tableau for possibility and disjunction

Structure: tableau.

Tableau for possibility and disjunction. Node one: false the conditional from possibly the disjunction of formula A and formula B to the disjunction of possibly formula A and possibly formula B at prefix one. Rule: tableau assumption. Node two: true possibly the disjunction of formula A and formula B at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of possibly formula A and possibly formula B at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix one. Rule: false disjunction rule, depending on node three. Node five: false possibly formula B at prefix one. Rule: false disjunction rule, depending on node three. Node six: true the disjunction of formula A and formula B at prefix one point one. Rule: true possibility rule, depending on node two. Node seven: true formula A at prefix one point one. Rule: true disjunction rule, depending on node six. Node eight: false formula A at prefix one point one. Rule: false possibility rule, depending on node four; source close marker present. Node nine: true formula B at prefix one point one. Rule: true disjunction rule, depending on node six. Node one zero: false formula B at prefix one point one. Rule: false possibility rule, depending on node five; source close marker present. Branch one is closed, closed by nodes seven and eight. Branch two is closed, closed by nodes nine and one zero. End tableau.

Read the source-bound structure in context

Additional modal tableau rules

Structure: table.

Additional modal rules. Headers: necessity form; possibility form. Row one, reflexive T. Premise true necessarily formula A at prefix sigma. Rule label T the necessity operator. Conclusion true formula A at prefix sigma. Premise false possibly formula A at prefix sigma. Rule label T the possibility operator. Conclusion false formula A at prefix sigma. Row two, serial D. Premise true necessarily formula A at prefix sigma. Rule label D the necessity operator. Conclusion true possibly formula A at prefix sigma. Premise false possibly formula A at prefix sigma. Rule label D the possibility operator. Conclusion false necessarily formula A at prefix sigma. Row three, symmetric B. Premise true necessarily formula A at prefix sigma dot n. Rule label B the necessity operator. Conclusion true formula A at prefix sigma. Premise false possibly formula A at prefix sigma dot n. Rule label B the possibility operator. Conclusion false formula A at prefix sigma. Row four, transitive four. Premise true necessarily formula A at prefix sigma. Rule label four the necessity operator. Conclusion true necessarily formula A at prefix sigma dot n. Premise false possibly formula A at prefix sigma. Rule label four the possibility operator. Conclusion false possibly formula A at prefix sigma dot n. Both prefixes are used: prefix sigma dot n; prefix sigma dot n. Row five, euclidean four r. Premise true necessarily formula A at prefix sigma dot n. Rule label four r the necessity operator. Conclusion true necessarily formula A at prefix sigma. Premise false possibly formula A at prefix sigma dot n. Rule label four r the possibility operator. Conclusion false possibly formula A at prefix sigma. End additional-rule table.

Read the source-bound structure in context

Modal logics, frame conditions, and tableau rules

Structure: table.

Logic and tableau-rule correspondence. Headers: logic; accessibility relation R is; rules. Header formula accessibility relation R. Row one: T equals K T; reflexive; formulas logic T equals logic K T, then the necessity operator, then the possibility operator. Row two: D equals K D; serial; formulas logic D equals logic K D, then the necessity operator, then the possibility operator. Row three: K four; transitive; formulas logic K four, then the necessity operator, then the possibility operator. Row four: B equals K T B; reflexive and symmetric; formulas logic B equals logic K T B, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. Row five: S four equals K T four; reflexive and transitive; formulas logic S four equals logic K T four, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. Row six: S five equals K T four B; reflexive, transitive, and euclidean; formulas logic S five equals logic K T four B, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. End correspondence table.

Read the source-bound structure in context

Tableau proof of axiom five in S five

Structure: tableau.

Tableau proof of axiom five in S five. Node one: false the conditional from necessarily formula A to necessarily possibly formula A at prefix one. Rule: tableau assumption. Node two: true necessarily formula A at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix one point one. Rule: false necessity rule, depending on node three. Node five: false possibly formula A at prefix one. Rule: four r the possibility operator, depending on node four. Node six: false formula A at prefix one point one. Rule: false possibility rule, depending on node five. Node seven: true formula A at prefix one point one. Rule: true necessity rule, depending on node two; source close marker present. Branch one is closed, closed by nodes six and seven. End tableau.

Read the source-bound structure in context

Simplified S five tableau rules

Structure: table.

Simplified S five rules. Headers: true-sign rule; false-sign rule. Row one, necessity. Premise true necessarily formula A at prefix n. Rule true necessity rule. Conclusion true formula A at prefix m. Premise false necessarily formula A at prefix n. Rule false necessity rule. Conclusion false formula A at prefix m. Side conditions: prefix m; prefix m. Row two, possibility. Premise true possibly formula A at prefix n. Rule true possibility rule. Conclusion true formula A at prefix m. Premise false possibly formula A at prefix n. Rule false possibility rule. Conclusion false formula A at prefix m. Side conditions: prefix m; prefix m. End simplified S five rule table.

Read the source-bound structure in context

Simplified S five tableau proof

Structure: tableau.

Simplified S five tableau proof. Node one: false the conditional from possibly formula A to necessarily possibly formula A at prefix one. Rule: tableau assumption. Node two: true possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix two. Rule: false necessity rule, depending on node three. Node five: true formula A at prefix three. Rule: true possibility rule, depending on node two. Node six: false formula A at prefix three. Rule: false possibility rule, depending on node four; source close marker present. Branch one is closed, closed by nodes five and six. End tableau.

Read the source-bound structure in context

Initial unfinished countermodel tableau

Structure: tableau.

Initial unfinished countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Branch one is unfinished. End tableau.

Read the source-bound structure in context

Second unfinished countermodel tableau

Structure: tableau.

Second unfinished countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Node eight: true the disjunction of p and q at prefix one point one. Rule: true necessity rule, depending on node two. Node nine: true the disjunction of p and q at prefix one point two. Rule: true necessity rule, depending on node two. Branch one is unfinished. End tableau.

Read the source-bound structure in context

Complete countermodel tableau

Structure: tableau.

Complete countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Node eight: true the disjunction of p and q at prefix one point one. Rule: true necessity rule, depending on node two; source checkmark present. Node nine: true the disjunction of p and q at prefix one point two. Rule: true necessity rule, depending on node two; source checkmark present. Node one zero: true p at prefix one point one. Rule: true disjunction rule, depending on node eight; source checkmark present; source close marker present. Node one one: true q at prefix one point one. Rule: true disjunction rule, depending on node eight; source checkmark present. Node one two: true p at prefix one point two. Rule: true disjunction rule, depending on node nine; source checkmark present. Node one three: true q at prefix one point two. Rule: true disjunction rule, depending on node nine; source checkmark present; source close marker present. Branch one is closed, closed by nodes six and one zero. Branch two is open and complete. Branch three is closed, closed by nodes seven and one three. End tableau.

Read the source-bound structure in context

Three-world countermodel graph

Structure: diagram tikz.

Three-world countermodel graph. Node one is prefix one, with printed valuations p is false and q is false. Node two is prefix one point one, with printed valuations p is false and q is true. Node three is prefix one point two, with printed valuations p is true and q is false. Directed accessibility edges, in printed order: from world one to world one point one; then from world one to world one point two. No loop or further edge is printed. End graph.

Read the source-bound structure in context

True-negation tableau rule

Structure: proof tree.

From true not A at prefix sigma, infer false A at prefix sigma.

Read the source-bound structure in context

False-negation tableau rule

Structure: proof tree.

From false not A at prefix sigma, infer true A at prefix sigma.

Read the source-bound structure in context

True-conjunction tableau rule

Structure: proof tree.

From true A and B at prefix sigma, stack true A and true B at the same prefix.

Read the source-bound structure in context

False-conjunction tableau rule

Structure: proof tree.

From false A and B at prefix sigma, branch to false A or false B at the same prefix.

Read the source-bound structure in context

True-disjunction tableau rule

Structure: proof tree.

From true A or B at prefix sigma, branch to true A or true B at the same prefix.

Read the source-bound structure in context

False-disjunction tableau rule

Structure: proof tree.

From false A or B at prefix sigma, stack false A and false B at the same prefix.

Read the source-bound structure in context

True-conditional tableau rule

Structure: proof tree.

From true if A then B at prefix sigma, branch to false A or true B at the same prefix.

Read the source-bound structure in context

False-conditional tableau rule

Structure: proof tree.

From false if A then B at prefix sigma, stack true A and false B at the same prefix.

Read the source-bound structure in context

True-necessity used-prefix rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma. Rule true necessity rule. Conclusion true formula A at prefix sigma dot n.

Read the source-bound structure in context

False-necessity new-prefix rule

Structure: proof tree.

Proof diagram. Premise false necessarily formula A at prefix sigma. Rule false necessity rule. Conclusion false formula A at prefix sigma dot n.

Read the source-bound structure in context

True-possibility new-prefix rule

Structure: proof tree.

Proof diagram. Premise true possibly formula A at prefix sigma. Rule true possibility rule. Conclusion true formula A at prefix sigma dot n.

Read the source-bound structure in context

False-possibility used-prefix rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma. Rule false possibility rule. Conclusion false formula A at prefix sigma dot n.

Read the source-bound structure in context

Reflexive true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label T the necessity operator. Conclusion true formula A at prefix sigma.

Read the source-bound structure in context

Reflexive false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma. Rule label T the possibility operator. Conclusion false formula A at prefix sigma.

Read the source-bound structure in context

Serial true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label D the necessity operator. Conclusion true possibly formula A at prefix sigma.

Read the source-bound structure in context

Serial false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma. Rule label D the possibility operator. Conclusion false necessarily formula A at prefix sigma.

Read the source-bound structure in context

Symmetric true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma dot n. Rule label B the necessity operator. Conclusion true formula A at prefix sigma.

Read the source-bound structure in context

Symmetric false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma dot n. Rule label B the possibility operator. Conclusion false formula A at prefix sigma.

Read the source-bound structure in context

Transitive true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label four the necessity operator. Conclusion true necessarily formula A at prefix sigma dot n.

Read the source-bound structure in context

Transitive false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma. Rule label four the possibility operator. Conclusion false possibly formula A at prefix sigma dot n.

Read the source-bound structure in context

Euclidean reverse true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix sigma dot n. Rule label four r the necessity operator. Conclusion true necessarily formula A at prefix sigma.

Read the source-bound structure in context

Euclidean reverse false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix sigma dot n. Rule label four r the possibility operator. Conclusion false possibly formula A at prefix sigma.

Read the source-bound structure in context

Simplified S five true-necessity rule

Structure: proof tree.

Proof diagram. Premise true necessarily formula A at prefix n. Rule true necessity rule. Conclusion true formula A at prefix m.

Read the source-bound structure in context

Simplified S five false-necessity rule

Structure: proof tree.

Proof diagram. Premise false necessarily formula A at prefix n. Rule false necessity rule. Conclusion false formula A at prefix m.

Read the source-bound structure in context

Simplified S five true-possibility rule

Structure: proof tree.

Proof diagram. Premise true possibly formula A at prefix n. Rule true possibility rule. Conclusion true formula A at prefix m.

Read the source-bound structure in context

Simplified S five false-possibility rule

Structure: proof tree.

Proof diagram. Premise false possibly formula A at prefix n. Rule false possibility rule. Conclusion false formula A at prefix m.

Read the source-bound structure in context