more from this thinker
|
more from this text
Single Idea 13143
[filed under theme 4. Formal Logic / D. Modal Logic ML / 2. Tools of Modal Logic / c. Derivation rules of ML
]
Full Idea
General tableau rules for universal modality: a) if σ ¬◊ X then σ.m ¬X b) if σ □ X then σ.m X , where m refers to a world that can be seen (rather than introducing a new world).
Gist of Idea
Universal: a) if σ ¬◊X then σ.m ¬X b) if σ □X then σ.m X [m exists]
Source
M Fitting/R Mendelsohn (First-Order Modal Logic [1998], 2.2)
Book Ref
Fitting,M/Mendelsohn,R: 'First-Order Modal Logic' [Synthese 1998], p.49
A Reaction
Note that the universal rule of □, usually read as 'necessary', only refers to worlds which can already be seen, whereas possibility (◊) asserts some thing about a new as yet unseen world.
The
15 ideas
with the same theme
[rules which are allowed in various modal logics]:
9740
|
If a proposition is possibly true in a world, it is true in some world accessible from that world
[Fitting/Mendelsohn]
|
9739
|
If a proposition is necessarily true in a world, it is true in all worlds accessible from that world
[Fitting/Mendelsohn]
|
13137
|
Conj: a) if σ X∧Y then σ X and σ Y b) if σ ¬(X∧Y) then σ ¬X or σ ¬Y
[Fitting/Mendelsohn]
|
13140
|
Bicon: a)if σ(X↔Y) then σ(X→Y) and σ(Y→X) b) [not biconditional, one or other fails]
[Fitting/Mendelsohn]
|
13143
|
Universal: a) if σ ¬◊X then σ.m ¬X b) if σ □X then σ.m X [m exists]
[Fitting/Mendelsohn]
|
13139
|
Implic: a) if σ ¬(X→Y) then σ X and σ ¬Y b) if σ X→Y then σ ¬X or σ Y
[Fitting/Mendelsohn]
|
13141
|
Negation: if σ ¬¬X then σ X
[Fitting/Mendelsohn]
|
13138
|
Disj: a) if σ ¬(X∨Y) then σ ¬X and σ ¬Y b) if σ X∨Y then σ X or σ Y
[Fitting/Mendelsohn]
|
13142
|
Existential: a) if σ ◊X then σ.n X b) if σ ¬□X then σ.n ¬X [n is new]
[Fitting/Mendelsohn]
|
13144
|
T reflexive: a) if σ □X then σ X b) if σ ¬◊X then σ ¬X
[Fitting/Mendelsohn]
|
13145
|
D serial: a) if σ □X then σ ◊X b) if σ ¬◊X then σ ¬□X
[Fitting/Mendelsohn]
|
13146
|
B symmetric: a) if σ.n □X then σ X b) if σ.n ¬◊X then σ ¬X [n occurs]
[Fitting/Mendelsohn]
|
13147
|
4 transitive: a) if σ □X then σ.n □X b) if σ ¬◊X then σ.n ¬◊X [n occurs]
[Fitting/Mendelsohn]
|
13149
|
S5: a) if n ◊X then kX b) if n ¬□X then k ¬X c) if n □X then k X d) if n ¬◊X then k ¬X
[Fitting/Mendelsohn]
|
13148
|
4r rev-trans: a) if σ.n □X then σ □X b) if σ.n ¬◊X then σ ¬◊X [n occurs]
[Fitting/Mendelsohn]
|