Logic for Computer Scientists/Modal Logic/Modal Logic Tableaux

edit

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 by:

  • 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 open.


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

 

reflecting transitivity.