# 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 $\Phi$ of formulae from $L$ , a tableau for $\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:

$(\land ){\frac {X;P\land Q}{X;P;Q}}$ $(\lor ){\frac {X;\lnot (P\land Q)}{X;\lnot P;\mid X;\lnot Q}}$ $(\bot ){\frac {X;P;\lnot P}{\bot }}$ $(\lnot ){\frac {X;\lnot \lnot P}{X;P}}$ $(\theta ){\frac {X;Y}{X}}$ $(K){\frac {\square X;\lnot \square P}{X;\lnot 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 ${\bot }$ , 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 $\lnot A$ .

As an example take the formula $\square (p\to q)\to (\square p\to \square 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;\square X;\lnot \square P}{X;\lnot 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;\lnot \square P}{X;\square P;P}}$ which obviously reflects reflexivity of the reachability relation, or

$(K4){\frac {\square X;\lnot \square P}{X;\square X;\lnot P}}$ reflecting transitivity.