**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.