3.2 Modal logic

Any of MacLogic's basic logics---classical, intuitionistic and minimal---may be extended by rules for modal operators. The modal operators are ‘ˆ’, where ˆA means "necessarily A", ‘’ where A means "possibly A", and ‘·’ where A·B means "A strictly implies B". MacLogic treats all three as primitive, although when using a classical base (though not an intuitionistic or modal one) some authors use ‘ˆ’ to define the others, since classically Ê (A Í ÒˆÒA) and universally Ê ((A·B) Í ˆ(AÁB)).

There are many systems of modal logic, characterising different notions and strengths of modality. MacLogic implements two of the most famous: Lewis’ systems S4 and S5.

The ˆ-Elimination rule is the same in both systems: ˆE says that A may be inferred from ˆA, the assumptions staying the same. Similarly, the rule I allows A to be inferred from A, and ·E allows B to be inferred from A·B and A (pooling the assumptions). But when may ˆA be inferred from A? Answer: when the assumptions on which A depends are suitably strong. ˆI has the same form in both systems, to infer ˆA from A, the difference lying in the restriction that the assumptions on which A depends are appropriately modal---S4-modal in the one case, S5-modal in the other. The notions of S4- and S5-modal are defined in Section 5.2. ·I makes similar use of the notion ‘modal’, in line with A · B’s possible definition as ˆ(A Á B), while E uses in addition a notion of co-modality, also defined in Section 5.2.

The rules for ‘ˆ’ and ‘’ may usefully be compared with those for ‘Ë’ and ‘’ respectively. For, semantically, ˆA means that "A is true in all (accessible) possible worlds", and A means "A is true in some (accessible) possible world".

For further details of these modal logics, see the books (referenced in the bibliography, section 4.6), by Lewis & Langford, Hughes & Cresswell, Zeman and Prawitz.