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