# 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 ${\displaystyle L}$ as a finitely branching tree whose nodes are formulas from ${\displaystyle L}$. Given a set ${\displaystyle \Phi }$ of formulae from ${\displaystyle L}$, a tableau for ${\displaystyle \Phi }$ was constructed by a (possibly infinite) sequence of applications of a tableau rule schema:

${\displaystyle \rho {\frac {\psi }{D_{1}\mid D_{2}\mid \cdots \mid D_{n}}}}$

where the premise ${\displaystyle \psi }$ as well as the denominators ${\displaystyle D_{1},\cdots ,D_{n}}$ are sets of formulae; ${\displaystyle \rho }$ is the name of the rule. We introduce ${\displaystyle K}$-tableau with the help of the following rules:

${\displaystyle (\land ){\frac {X;P\land Q}{X;P;Q}}}$           ${\displaystyle (\lor ){\frac {X;\lnot (P\land Q)}{X;\lnot P;\mid X;\lnot Q}}}$

${\displaystyle (\bot ){\frac {X;P;\lnot P}{\bot }}}$           ${\displaystyle (\lnot ){\frac {X;\lnot \lnot P}{X;P}}}$

${\displaystyle (\theta ){\frac {X;Y}{X}}}$                       ${\displaystyle (K){\frac {\square X;\lnot \square P}{X;\lnot P}}}$

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

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

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

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

As an example take the formula ${\displaystyle \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 ${\displaystyle K}$-axiom.

Some remarks are in order:

• The ${\displaystyle \theta }$- rule, called the thinning rule, is necessary in order to construct the premisses for the application of the ${\displaystyle K}$-rule.
• Both can be combined by a new rule
${\displaystyle (K\theta ){\frac {Y;\square X;\lnot \square P}{X;\lnot P}}}$
• In order to get tableau calculi for the other mentioned calculi, like ${\displaystyle T}$ or ${\displaystyle K4}$ one has to introduce additional rules:
${\displaystyle (T){\frac {X;\lnot \square P}{X;\square P;P}}}$

which obviously reflects reflexivity of the reachability relation, or

${\displaystyle (K4){\frac {\square X;\lnot \square P}{X;\square X;\lnot P}}}$

reflecting transitivity.