Tableau Metatheorem for Modal Logics

The aim of the paper is to demonstrate and prove a tableau metatheorem for modal logics. While being effective tableau methods are usually presented in a rather intuitive way and our ambition was to expose the method as rigorously as possible. To this end all notions displayed in the sequel are couched in a set theoretical framework, for example: branches are sequences of sets and tableaus are sets of these sequences. Other notions are also defined in a similar, formal way: maximal, open and closed branches, open and closed tableaus. One of the distinctive features of the paper is introduction of what seems to be the novelty in the literature: the notion of tableau consequence relation. Thanks to the precision of tableau metatheory we can prove the following theorem: completeness and soundness of tableau methods are immediate consequences of some conditions put upon a class of models M and a set of tableau rules MRT. These conditions will be described and explained in the sequel. The approach presented in the paper is very general and may be applied to other systems of logic as long as tableau rules are defined in the style proposed by the author. In this paper tableau tools are treated as an entirely syntactical method of checking correctness of arguments [1, 2].