Modal Systems

In modal systems, two dual operators are introduced: Necessity ('M') and Possibility ('L'). Propositions are evaluated at different "possible worlds" (here indicated numerically) which are connected by an accessibility relation. If 'Mp' ('Necessarily p') is true at a given possible world, then 'p' is true at all accessible possible worlds. If 'Lp' ('Possibly p') is true at a world, then 'p' is true at some accessible possible world.

In the simplest modal system, K, no further assumptions are made about the accessibility relation. However, this basic system does not appear capable of modeling all modal talk. Other systems of modal logic are introduced by adding constraints on the accessibility relation, or by introducing special inference rules. In the strongest modal system, S5, the accessibility relation is reflexive, transitive, and symmetric (i.e., it is an equivalence relation).
NOTE: The following breakdown of logical systems is derived from (Fitting & Mendelsohn 1998).

In modal tableaux, worlds are assigned numerical indices as "names." The indices convey information about the accessibility relation. Thus, for any world labeled n, all worlds labeled n.m are accessible to it. A branch of the tableau is closed just in case it contains a contradiction at a given world.

NOTE: If a tableau begins to repeat itself, without closing, then the tableau generator will terminate and the argument will be deemed invalid. This is because in some cases where a branch fails to close, modal rules can be iteratively applied indefinitely.