# Tableau Methods for Propositional Logic and Term Logic

by Tomasz Jarmużek (Author)
Open Access
Series:
• eBook

## Summary

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.

• Cover
• Title Page
• This eBook can be cited
• Contents
• Preface
• 1 Introduction
• 1.1 Tableau methods
• 1.2 Terminology and problems in the book
• 1.2.1 Study schedule and goals
• 1.2.2 Terminology and issues in the book
• 1.3 Notations and concepts of the set theory
• 2 Tableau system for Classical Propositional Logic
• 2.1 Introductory remarks
• 2.2 Language and semantics
• 2.3 Basic concepts of the tableau system for CPL
• 2.3.1 Tableau rules for CPL
• 2.3.2 Branches for CPL
• 2.3.3 Maximal branches
• 2.3.4 Closed and open branches
• 2.3.5 Branch consequence relation
• 2.4 Relations of semantic consequence and branch consequence
• 2.4.1 Soundness theorem
• 2.4.2 Completeness theorem
• 2.5 Tableaux for CPL vs. semantic consequence relation
• 2.6 Summary
• 3 Tableau system for Term Logic
• 3.1 Introductory remarks
• 3.2 Language and semantics
• 3.3 Basic concepts of the tableau system for TL
• 3.3.1 Tableau rules for TL
• 3.3.2 Branches for TL
• 3.3.3 Maximal branches
• 3.3.4 Closed and open branches
• 3.3.5 Relation of branch consequence
• 3.4 Tableaux for TL
• 3.5 Completeness theorem for the tableau system for TL
• 3.5.1 Estimation of cardinality of model for TL
• 4 Tableau system for modal logic S5
• 4.1 Introductory remarks
• 4.2 Language and semantics
• 4.3 Basic concepts of the tableau system for S5
• 4.3.1 Tableau rules for S5
• 4.3.2 Branches for S5
• 4.3.3 Closed and open branches
• 4.3.4 Maximal branches
• 4.3.5 Relation of branch consequence
• 4.4 Tableaux for S5
• 4.5 Theorem on the completeness of the tableau system for S5
• 5 Metatheory of tableau systems for propositional logic and term logic
• 5.1 Introductory remarks
• 5.2 Language and semantics
• 5.3 Basic concepts of the tableau system
• 5.4 Tableau rules
• 5.4.1 Branches
• 5.4.2 Closed and open branches
• 5.4.3 Maximal branches
• 5.4.4 Branch consequence relation
• 5.5 Tableaux
• 5.6 Completeness theorem
• 6 Examples of applications
• 6.1 Introductory remarks
• 6.2 Tableau system for Modal Term Logic de re
• 6.2.1 Language
• 6.2.2 Semantics
• 6.2.4 Tableau expression
• 6.2.4 Rules for the tableau system for logic MTL
• 6.2.5 Branches and tableaux for MTL
• 6.2.6 Theorem on the completeness of the tableau system for MTL
• 6.2.7 Estimation of cardinality of model for MTL
• 6.3 Tableau systems for modal logics
• 6.3.1 Language and semantics
• 6.3.2 Tableau expressions
• 6.3.3 Rules, branches and tableaux for modal logics
• 6.3.4 Generating of model
• 6.3.5 Completeness theorem of tableau systems for modal logics
• 6.4 Tableau system
• 6.5 Transition from the formalized tableaux to the standard tableaux
• Glossary
• Bibliography
• Index

←8 | 9→

## Preface

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.

## Details

Pages
228
Year
2020
ISBN (PDF)
9783631846537
ISBN (ePUB)
9783631846667
ISBN (MOBI)
9783631846674
ISBN (Hardcover)
9783631833728
DOI
10.3726/b18008
Open Access
CC-BY-NC-ND
Language
English
Publication date
2021 (June)
Keywords
logic tableu methods proof theory philosophical logic propositional logic logic of names
Published
Berlin, Bern, Bruxelles, New York, Oxford, Warszawa, Wien, 2020. 228 pp.

230 pages