Method of Analytic Tableaux - Tableaux For Modal Logics

Tableaux For Modal Logics

In a modal logic, a model comprises a set of possible worlds, each one associated to a truth evaluation; an accessibility relation tells when a world is accessible from another one. A modal formula may specify not only conditions over a possible world, but also on the ones that are accessible from it. As an example, is true in a world if is true in all worlds that are accessible from it.

As for propositional logic, tableaux for modal logics are based on recursively breaking formulae into its basic components. Expanding a modal formula may however require stating conditions over different worlds. As an example, if is true in a world then there exists a world accessible from it where is false. However, one cannot simply add the following rule to the propositional ones.

In propositional tableaux all formulae refer to the same truth evaluation, but the precondition of the rule above holds in a world while the consequence holds in another. Not taking into account this would generate wrong results. For example, formula states that is true in the current world and is false in a world that is accessible from it. Simply applying and the expansion rule above would produce and, but these two formulae should not in general generate a contradiction, as they hold in different worlds. Modal tableaux calculi do contain rules of the kind of the one above, but include mechanisms to avoid the incorrect interaction of formulae referring to different worlds.

Technically, tableaux for modal logics check the satisfiability of a set of formulae: they check whether there exists a model and world such that the formulae in the set are true in that model and world. In the example above, while states the truth of in, the formula states the truth of in some world that is accessible from and which may in general be different from . Tableaux calculi for modal logic take into account that formulae may refer to different worlds.

This fact has an important consequence: formulae that hold in a world may imply conditions over different successors of that world. Unsatisfiability may then be proved from the subset of formulae referring to the a single successor. This holds if a world may have more than one successor, which is true for most modal logic. If this is the case, a formula like is true if a successor where holds exists and a successor where holds exists. In the other way around, if one can show unsatisfiability of in an arbitrary successor, the formula is proved unsatisfiable without checking for worlds where holds. At the same time, if one can show unsatisfiability of, there is no need to check . As a result, while there are two possible way to expand, one of these two ways is always sufficient to prove unsatisfiability if the formula is unsatisfiable. For example, one may expand the tableau by considering an arbitrary world where holds. If this expansion leads to unsatisfiability, the original formula is unsatisfiable. However, it is also possible that unsatisfiability cannot be proved this way, and that the world where holds should have been considered instead. As a result, one can always prove unsatisfiability by expanding either only or only; however, if the wrong choice is done the resulting tableau may not be closed. Expanding either subformula leads to tableau calculi that are complete but not proof-confluent. Searching as described in the "Searching for a closed tableau" may therefore be necessary.

Depending on whether the precondition and consequence of a tableau expansion rule refer to the same world or not, the rule is called static or transactional. While rules for propositional connectives are all static, not all rules for modal connectives are transactional: for example, in every modal logic including axiom T, it holds that implies in the same world. As a result, the relative (modal) tableau expansion rule is static, as both its precondition and consequence refer to the same world.