Editing Method of analytic tableaux (section)

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