Logic for Computer Scientists/Modal Logic/Modal Logic Tableaux

Modal Logic Tableaux

In classical propositional logics we introduced a tableau calculus (Definition) for a logic $L$ as a finitely branching tree whose nodes are formulas from $L$. Given a set $\mathrm{\Phi }$ of formulae from $L$, a tableau for $\mathrm{\Phi }$ was constructed by a (possibly infinite) sequence of applications of a tableau rule schema:

$\rho \frac{\psi }{D_1\mid D_2\mid \cdots \mid D_n}$

where the premise $\psi$ as well as the denominators $D_1,\cdots ,D_n$ are sets of formulae; $\rho$ is the name of the rule. We introduce $K$-tableau with the help of the following rules:

$(\wedge )\frac{X;P\wedge Q}{X;P;Q}$           $(\vee )\frac{X;\mathrm{\neg }(P\wedge Q)}{X;\mathrm{\neg }P;\mid X;\mathrm{\neg }Q}$

$(\mathrm{\perp })\frac{X;P;\mathrm{\neg }P}{\mathrm{\perp }}$           $(\mathrm{\neg })\frac{X;\mathrm{\neg }\mathrm{\neg }P}{X;P}$

$(\theta )\frac{X;Y}{X}$                       $(K)\frac{◻X;\mathrm{\neg }◻P}{X;\mathrm{\neg }P}$

A tableau for a set $X$ of formulae is a finite tree with root $X$ whose nodes carry finite formulae sets. The rules for extending a tableau are given by:

• choose a leaf node $n$ with label $Y$, where $n$ is not an end node, and choose a rule $\rho$, which is applicable to $n$;
• if $\rho$ has $k$ denominators then create $k$ successor nodes for $n$, with successor $i$ carrying an appropriate instance of denominator $D_i$;
• if a successor $s$ carries a set $Z$ and $Z$ has already appeared on the branch from the root to $s$ then $s$ is an end node.

A branch is called closed if its end node is carrying $\mathrm{\perp }$, otherwise it is open.

As in the classical case, a formulae $A$ is a theorem in modal logic $K$, iff there is a closed $K$-tableau for the set $\mathrm{\neg }A$.

As an example take the formula $◻(p\to q)\to (◻p\to ◻q)$: its negation is certainly unsatisfiable, because the formula is an instance of our previously given $K$-axiom.

Some remarks are in order:

• The $\theta$- rule, called the thinning rule, is necessary in order to construct the premisses for the application of the $K$-rule.
• Both can be combined by a new rule

$(K\theta )\frac{Y;◻X;\mathrm{\neg }◻P}{X;\mathrm{\neg }P}$

• In order to get tableau calculi for the other mentioned calculi, like $T$ or $K4$ one has to introduce additional rules:

$(T)\frac{X;\mathrm{\neg }◻P}{X;◻P;P}$

which obviously reflects reflexivity of the reachability relation, or

$(K4)\frac{◻X;\mathrm{\neg }◻P}{X;◻X;\mathrm{\neg }P}$

reflecting transitivity.