Logic for Computer Scientists/Modal Logic/Modal Logic Tableaux

< Logic for Computer Scientists‎ | Modal Logic

Modal Logic TableauxEdit

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.