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
 9739 If a proposition is necessarily true in a world, it is true in all worlds accessible from that world [Fitting/Mendelsohn]
 9740 If a proposition is possibly true in a world, it is true in some world accessible from that world [Fitting/Mendelsohn]
 13140 Bicon: a)if σ(X↔Y) then σ(X→Y) and σ(Y→X) b) [not biconditional, one or other fails] [Fitting/Mendelsohn]
 13138 Disj: a) if σ ¬(X∨Y) then σ ¬X and σ ¬Y b) if σ X∨Y then σ X or σ Y [Fitting/Mendelsohn]
 13143 Universal: a) if σ ¬◊X then σ.m ¬X b) if σ □X then σ.m X [m exists] [Fitting/Mendelsohn]
 13142 Existential: a) if σ ◊X then σ.n X b) if σ ¬□X then σ.n ¬X [n is new] [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]
 13137 Conj: a) if σ X∧Y then σ X and σ Y b) if σ ¬(X∧Y) then σ ¬X or σ ¬Y [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]
 13148 4r rev-trans: 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]
 13146 B symmetric: a) if σ.n □X then σ X b) if σ.n ¬◊X then σ ¬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]