Logic for Computer Scientists/Modal Logic/Modal Logic Tableaux

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Modal Logic
Jump to: navigation, search

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.