structure for 'Formal Logic'    |     alphabetical list of themes    |     expand these ideas

4. Formal Logic / D. Modal Logic ML / 2. Tools of Modal Logic / c. Derivation rules of ML

[rules which are allowed in various modal logics]

15 ideas
If a proposition is necessarily true in a world, it is true in all worlds accessible from that world [Fitting/Mendelsohn]
If a proposition is possibly true in a world, it is true in some world accessible from that world [Fitting/Mendelsohn]
Conj: a) if σ X∧Y then σ X and σ Y b) if σ (X∧Y) then σ X or σ Y [Fitting/Mendelsohn]
Bicon: a)if σ(X↔Y) then σ(X→Y) and σ(Y→X) b) [not biconditional, one or other fails] [Fitting/Mendelsohn]
Existential: a) if σ ◊X then σ.n X b) if σ □X then σ.n X [n is new] [Fitting/Mendelsohn]
Negation: if σ X then σ X [Fitting/Mendelsohn]
Implic: a) if σ (X→Y) then σ X and σ Y b) if σ X→Y then σ X or σ Y [Fitting/Mendelsohn]
Disj: a) if σ (X∨Y) then σ X and σ Y b) if σ X∨Y then σ X or σ Y [Fitting/Mendelsohn]
Universal: a) if σ ◊X then σ.m X b) if σ □X then σ.m X [m exists] [Fitting/Mendelsohn]
D serial: a) if σ □X then σ ◊X b) if σ ◊X then σ □X [Fitting/Mendelsohn]
T reflexive: a) if σ □X then σ X b) if σ ◊X then σ X [Fitting/Mendelsohn]
B symmetric: a) if σ.n □X then σ X b) if σ.n ◊X then σ X [n occurs] [Fitting/Mendelsohn]
4 transitive: a) if σ □X then σ.n □X b) if σ ◊X then σ.n ◊X [n occurs] [Fitting/Mendelsohn]
4r rev-trans: a) if σ.n □X then σ □X b) if σ.n ◊X then σ ◊X [n occurs] [Fitting/Mendelsohn]
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]