Editing Method of analytic tableaux (section)

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