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 · Bs 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.