Editing Method of analytic tableaux (section)

===Set-labeling tableaux===

The problem of interaction between formulae holding in different worlds can be overcome by using set-labeling tableaux. These are trees whose nodes are labeled with sets of formulae; the expansion rules explain how to attach new nodes to a leaf, based only on the label of the leaf (and not on the label of other nodes in the branch).

Tableaux for modal logics are used to verify the satisfiability of a set of modal formulae in a given modal logic. Given a set of formulae <math>S</math>, they check the existence of a model <math>M</math> and a world <math>w</math> such that <math>M,w \models S</math>.

The expansion rules depend on the particular modal logic used. A tableau system for the basic modal logic [[K (modal logic)|K]] can be obtained by adding to the propositional tableau rules the following one:

:<math>(K) \frac{\Box A_1; \ldots ; \Box A_n ; \neg \Box B}{A_1; \ldots ; A_n ; \neg B}</math>

Intuitively, the precondition of this rule expresses the truth of all formulae <math>A_1,\ldots,A_n</math> at all accessible worlds, and truth of <math>\neg B</math> at some accessible worlds. The consequence of this rule is a formula that must be true at one of those worlds where <math>\neg B</math> is true.

More technically, modal tableaux methods check the existence of a model <math>M</math> and a world <math>w</math> that make set of formulae true. If <math>\Box A_1; \ldots ; \Box A_n ; \neg \Box B</math> are true in <math>w</math>, there must be a world <math>w'</math> that is accessible from <math>w</math> and that makes <math>A_1; \ldots ; A_n ; \neg B</math> true. This rule therefore amounts to deriving a set of formulae that must be satisfied in such <math>w'</math>.

While the preconditions <math>\Box A_1; \ldots ; \Box A_n ; \neg \Box B</math> are assumed satisfied by <math>M,w</math>, the consequences <math>A_1; \ldots ; A_n ; \neg B</math> are assumed satisfied in <math>M,w'</math>: same model but possibly different worlds. Set-labeled tableaux do not explicitly keep track of the world where each formula is assumed true: two nodes may or may not refer to the same world. However, the formulae labeling any given node are assumed true at the same world.

As a result of the possibly different worlds where formulae are assumed true, a formula in a node is not automatically valid in all its descendants, as every application of the modal rule corresponds to a move from a world to another one. This condition is automatically captured by set-labeling tableaux, as expansion rules are based only on the leaf where they are applied and not on its ancestors.

Notably, <math>(K)</math> does not directly extend to multiple negated boxed formulae such as in <math>\Box A_1; \ldots; \Box A_n; \neg \Box B_1; \neg \Box B_2</math>: while there exists an accessible world where <math>B_1</math> is false and one in which <math>B_2</math> is false, these two worlds are not necessarily the same.

Differently from the propositional rules, <math>(K)</math> states conditions over all its preconditions. For example, it cannot be applied to a node labeled by <math>a; \Box b; \Box (b \to c); \neg \Box c</math>; while this set is inconsistent and this could be easily proved by applying <math>(K)</math>, this rule cannot be applied because of formula <math>a</math>, which is not even relevant to inconsistency. Removal of such formulae is made possible by the rule:

:<math>(\theta) \frac{A_1;\ldots;A_n;B_1;\ldots;B_m}{A_1;\ldots;A_n}</math>

The addition of this rule (thinning rule) makes the resulting calculus non-confluent: a tableau for an inconsistent set may be impossible to close, even if a closed tableau for the same set exists.

Rule <math>(\theta)</math> is non-deterministic: the set of formulae to be removed (or to be kept) can be chosen arbitrarily; this creates the problem of choosing a set of formulae to discard that is not so large it makes the resulting set satisfiable and not so small it makes the necessary expansion rules inapplicable. Having a large number of possible choices makes the problem of searching for a closed tableau harder.

This non-determinism can be avoided by restricting the usage of <math>(\theta)</math> so that it is only applied before a modal expansion rule, and so that it only removes the formulae that make that other rule inapplicable. This condition can be also formulated by merging the two rules in a single one. The resulting rule produces the same result as the old one, but implicitly discard all formulae that made the old rule inapplicable. This mechanism for removing <math>(\theta)</math> has been proved to preserve completeness for many modal logics.

Axiom [[T (modal logic)|T]] expresses reflexivity of the accessibility relation: every world is accessible from itself. The corresponding tableau expansion rule is:

:<math>(T) \frac{A_1;\ldots;A_n;\Box B}{A_1;\ldots;A_n; \Box B; B}</math>

This rule relates conditions over the same world: if <math>\Box B</math> is true in a world, by reflexivity <math>B</math> is also true ''in the same world''. This rule is static, not transactional, as both its precondition and consequent refer to the same world.

This rule copies <math>\Box B</math> from the precondition to the consequent, in spite of this formula having been "used" to generate <math>B</math>. This is correct, as the considered world is the same, so <math>\Box B</math> also holds there. This "copying" is necessary in some cases. It is for example necessary to prove the inconsistency of  <math>\Box(a \land \neg \Box a)</math>: the only applicable rules are in order <math>(T), (\land), (\theta), (K)</math>, from which one is blocked if <math>\Box a</math> is not copied.