In classical propositional logics we introduced a tableau calculus (Definition) for a logic as a finitely branching
tree whose nodes are formulas from .
Given a set of formulae from , a tableau for was constructed
by a (possibly infinite) sequence of applications of a tableau rule schema:
where the premise as well as the denominators are sets
of formulae; is the name of the rule.
We introduce -tableau with the help of the following rules:
A tableau for a set of formulae is a finite tree with root whose
nodes carry finite formulae sets. The rules for extending a tableau are given
choose a leaf node with label , where is not an end node, and choose a rule , which is applicable to ;
if has denominators then create successor nodes for , with successor carrying an appropriate instance of denominator ;
if a successor carries a set and has already appeared on the branch from the root to then is an end node.
A branch is called closed if its end node is carrying , otherwise it is
As in the classical case, a formulae is a theorem in modal logic ,
iff there is a closed -tableau for the set .
As an example take the formula :
its negation is certainly unsatisfiable, because the formula is an instance of
our previously given -axiom.
Some remarks are in order:
The - rule, called the thinning rule, is necessary in order to construct the premisses for the application of the -rule.
Both can be combined by a new rule
In order to get tableau calculi for the other mentioned calculi, like or one has to introduce additional rules:
which obviously reflects reflexivity of the reachability relation, or