The book aims to formalise tableau methods for the logics of propositions and names. The methods described are based on Set Theory. The tableau rule was reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are its supersets.
The aim of the book—according to its title—is to formalise the tableau methods for the propositional logic and term logic. By tableau methods we mean both ways of defining tableau systems and concepts which enable us to determine the occurrence of logical relationships within these systems.
In the book, we look into the problem of formal definition of concepts that are typical for such logical systems in which the occurrence of the logical relationships is examined by means of constructing the so-called tableau or proof tree.
Our considerations only apply to those systems that:
- firstly, are built for logics defined by bivalent semantics—the interpretation of formulas assigns to each formula either the value of truth or the value of false
- secondly, are systems of propositional logic or term logic.
Both conditions, as we will see later, have an important influence on the nature of the defined general concepts for the tableau methods. We write about establishing the overlapping relations of logical consequences in the tableau system because, in the presented approach, the starting point of the tableau system structure is the semantically defined logic for which the tableau system is constructed. We want to construct the tableau system in such a way that the relation of derivability determined by this system coincides with the relation of the semantic consequence for which the system was determined. In other words, we want the defined tableau system to be sound and complete to the initial semantics.
In many cases, it is of course possible to take the opposite approach—we can first define a tableau system and then determine the appropriate semantics for it. The methods presented in the book also make it possible to achieve this goal.
The formalisation of tableau methods described in this paper is based on the set theory — all concepts important for the theory of tableau methods are therefore defined as sets. The book analyses, among other things, the concepts of tableau rule, branch and tableau, offering their general and purely formal view. For example, the concept of a tableau rule is reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are the supersets of the set of premises — ways of drawing conclusions from it. At the same time, however, branches are defined as sequences of sets in which subsequent elements form the result of the application of the tableau rule. Finally, tableaux are sets of branches that meet certain additional conditions.←9 | 10→
Still, the presented general and formal concepts do not interfere with the tableau concepts which are intuitive, standard and used in didactics. As we will show at the end of the book, the latter can be regarded as the application of formal concepts. The advantage of the formal approach is the possible generalization of conditions whose fulfilment by the tableau system is sufficient for its completeness and adequacy to the adopted semantics.
In Chapter One, the Reader will have the opportunity to get acquainted with the adopted strategy of formalisation of tableau concepts and an intuitive approach which is developed in the book.
In the following three chapters, three different cases are discussed in detail — different in terms of both syntax of the language in which we carry out the tableau proof and semantics. Contained in these chapters, structure of formal tableau systems for Classical Propositional Logic, Term Logic and modal logic S5 is the starting point for the generalization of tableau methods which is done in the next chapter.
In Chapter Five, we describe the general theory of the structure of tableau systems and tableau concepts. The result of that chapter considerations is a theoremformulating sufficient conditions for the tableau system constructed with the given method to be adequate in relation to the initial semantics.
The final chapter describes the applications of the theory presented in Chapter Five. There, we will find the theory application to the construction of Modal Term Logic in the interpretation de re and the application to the theory of tableau systems for modal logics determined by the semantics of possible worlds. Another issue that we discuss in that chapter is the concept of the tableau system itself and the concepts that should be defined during its construction, as well as the resulting possibilities of examining the relations between the tableau systems. In the chapter, we also present a description of the transition from the abstractly understood concepts of tableau and branches to the standard, informal concepts of branches and tableau. This transition can also be considered as the application of general tableau concepts.
The author of the book would like to send greatest appreciation for the editorial reviewers of this book: prof. Andrzej Pietruszczak (Nicolaus Copernicus University in Toruń) and prof. Marcin Tkaczyk (The John Paul II Catholic University of Lublin). Moreover, the author would also like to express his gratitude to dr. Mateusz Klonowski (Nicolaus Copernicus University in Toruń), for the discussions and valuable remarks.