Editing Method of analytic tableaux (section)

==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'' specifies 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, <math>\Box A</math> is true in a world if <math>A</math> 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 <math>\neg \Box A</math> is true in a world then there exists a world accessible from it where <math>A</math> is false. However, one cannot simply add the following rule to the propositional ones.

:<math>\frac{\neg \Box A}{\neg A}</math>

In propositional tableaux all formulae refer to the same truth evaluation, but the precondition of the rule above holds in one world while the consequence holds in another. Not taking this into account would generate incorrect results. For example, formula <math>a \land \neg \Box a</math> states that <math>a</math> is true in the current world and <math>a</math> is false in a world that is accessible from it. Simply applying <math>(\land)</math> and the expansion rule above would produce <math>a</math> and <math>\neg a</math>, 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 <math>M</math> and world <math>w</math> such that the formulae in the set are true in that model and world. In the example above, while <math>a</math> states the truth of <math>a</math> in <math>w</math>, the formula <math>\neg \Box a</math> states the truth of <math>\neg a</math> in some world <math>w'</math> that is accessible from <math>w</math> and which may in general be different from <math>w</math>. 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 a single successor. This holds  if a world may have more than one successor, which is true for most modal logics. If this is the case, a formula like <math>\neg \Box A \land \neg \Box B</math> is true if a successor where <math>\neg A</math> holds exists and a successor where <math>\neg B</math> holds exists. In the other way around, if one can show unsatisfiability of <math>\neg A</math> in an arbitrary successor, the formula is proved unsatisfiable without checking for worlds where <math>\neg B</math> holds. At the same time, if one can show unsatisfiability of <math>\neg B</math>, there is no need to check <math>\neg A</math>. As a result, while there are two possible way to expand <math>\neg \Box A \land \neg \Box B</math>, 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 <math>\neg A</math> 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 <math>\neg B</math> holds should have been considered instead. As a result, one can always prove unsatisfiability by expanding either <math>\neg \Box A</math> only or <math>\neg \Box B</math> only; however, if the wrong choice is made 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 [[Kripke semantics#Common modal axiom schemata|T]], it holds that <math>\Box A</math> implies <math>A</math> 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.

===Formula-deleting tableau===

A method for avoiding formulae referring to different worlds interacting in the wrong way is to make sure that all formulae of a branch refer to the same world. This condition is initially true as all formulae in the set to be checked for consistency are assumed referring to the same world. When expanding a branch, two situations are possible: either the new formulae refer to the same world as the other one in the branch or not. In the first case, the rule is applied normally. In the second case, all formulae of the branch that do not also hold in the new world are deleted from the branch, and possibly added to all other branches that are still relative to the old world.

As an example, in [[S5 (modal logic)|S5]] every formula <math>\Box A</math> that is true in a world is also true in all accessible worlds (that is, in all accessible worlds both <math>A</math> and <math>\Box A</math> are true). Therefore, when applying <math>\frac{\neg \Box B}{\neg B}</math>, whose consequence holds in a different world, one deletes all formulae from the branch, but can keep all formulae <math>\Box A</math>, as these hold in the new world as well. In order to retain completeness, the deleted formulae are then added to all other branches that still refer to the old world.

===World-labeled tableau===

A different mechanism for ensuring the correct interaction between formulae referring to different worlds is to switch from formulae to labeled formulae: instead of writing <math>A</math>, one would write <math>w:A</math> to make it explicit that <math>A</math> holds in world <math>w</math>.

All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label. For example, <math>w:A \land B</math> generates two nodes labeled with <math>w:A</math> and <math>w:B</math>; a branch is closed only if it contains two opposite literals of the same world, like <math>w:a</math> and <math>w:\neg a</math>; no closure is generated if the two world labels are different, like in <math>w:a</math> and <math>w':\neg a</math>.

A modal expansion rule may have a consequence that refers to different worlds. For example, the rule for <math>\neg \Box A</math> would be written as follows

:<math>\frac{w:\neg \Box A}{w':\neg A}</math>

The precondition and consequent of this rule refer to worlds <math>w</math> and <math>w'</math>, respectively. The various calculi use different methods for keeping track of the accessibility of the worlds used as labels. Some include pseudo-formulae like <math>wRw'</math> to denote that <math>w'</math> is accessible from <math>w</math>. Some others use sequences of integers as world labels, this notation implicitly representing the [[accessibility relation]] (for example, <math>(1,4,2,3)</math> is accessible from <math>(1,4,2)</math>.)

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

===Auxiliary tableaux===

A different method for dealing with formulae holding in alternate worlds is to start a different tableau for each new world that is introduced in the tableau. For example, <math>\neg \Box A</math> implies that <math>A</math> is false in an accessible world, so one starts a new tableau rooted by <math>\neg A</math>. This new tableau is attached to the node of the original tableau where the expansion rule has been applied; a closure of this tableau immediately generates a closure of all branches where that node is, regardless of whether the same node is associated other auxiliary tableaux. The expansion rules for the auxiliary tableaux are the same as for the original one; therefore, an auxiliary tableau can have in turns other (sub-)auxiliary tableaux.

===Global assumptions===

The above modal tableaux establish the consistency of a set of formulae, and can be used for solving the local [[logical consequence]] problem. This is the problem of telling whether, for each model <math>M</math>, if <math>A</math> is true in a world <math>w</math>, then <math>B</math> is also true in the same world. This is the same as checking whether <math>B</math> is true in a world of a model, in the assumption that <math>A</math> is also true in the same world of the same model.

A related problem is the global consequence problem, where the assumption is that a formula (or set of formulae) <math>G</math> is true in all possible worlds of the model. The problem is that of checking whether, in all models <math>M</math> where <math>G</math> is true in all worlds, <math>B</math> is also true in all worlds.

Local and global assumption differ on models where the assumed formula is true in some worlds but not in others. As an example, <math>\{P, \neg \Box (P \land Q)\}</math> entails <math>\neg \Box Q</math> globally but not locally. Local [[entailment]] does not hold in a model consisting of two worlds making <math>P</math> and <math>\neg P, Q</math> true, respectively, and where the second is accessible from the first; in the first world, the assumptions are true but <math>\neg \Box Q</math> is false. This counterexample works because <math>P</math> can be assumed true in a world and false in another one. If however the same assumption is considered global, <math>\neg P</math> is not allowed in any world of the model.

These two problems can be combined, so that one can check whether <math>B</math> is a local consequence of <math>A</math> under the global assumption <math>G</math>. Tableaux calculi can deal with global assumption by a rule allowing its addition to every node, regardless of the world it refers to.