Loading...

Tableau Methods for Propositional Logic and Term Logic

by Tomasz Jarmużek (Author)
Monographs 228 Pages

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.

Table Of Content

  • Cover
  • Title Page
  • Copyright
  • About the author
  • About the book
  • 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.

←10 | 11→

1Introduction

1.1Tableau methods

In the book, we look into the tableau methods. These methods are used to define logical systems in which through proofs—called tableau proofs—it is possible to show the occurrence of logical relations between sets of premises and conclusions.

Tableau methods in many ways constitute an interesting alternative to other methods of constructing logical systems. They are also interesting because the tableau systems have many advantages over other types of systems. Unfortunately, they also have their drawbacks. The aim of the book is to define tableau methods in such a way that for a certain class of tableau systems these drawbacks are minimized or, where possible, completely eliminated.

Let us briefly expose some features of tableau systems, comparing them with axiomatic systems.

One of the advantages of tableau systems is a fairly intuitive and simple mechanism of theorem proving. In most cases, knowing the tableau rules and the way they work, we can mechanically search for answers to the question whether a given formula is a logical consequence of a given set of premises. Such action does not require any particular ingenuity. Another advantage is the fact that if the answer is negative, most often—also intuitively—on the basis of an unsuccessful tableau proof we can build so-called countermodel, i.e. a model in which the premises are true, but the conclusion is false.

Unfortunately, the disadvantages of tableau systems are the complications that arise when trying to construct them precisely—there are many complex theoretical concepts. Obviously, we can use intuitive concepts of branch/track of proof, tableau/tree, open or closed tableau, complete tableau, etc. However, firstly, we are not dealing with a formal system, but with a preformal one, and thus potentially more or less burdened with serious logical errors. Secondly, it is difficult, if at all possible, to generalize our results by looking for metalogical dependencies between different tableau systems, as well as dependencies between classes of systems as for such actions we need general concepts whose specific cases occur within the construction of specific tableau systems.

In turn, axiomatic systems feature precisely defined basic concepts and these concepts can be generalized. For example, it can be assumed that each axiomatic system consists of a decidable set of formulas of a certain language For and a set of rules of proving R. Since the system axioms can be described as zero-premiss ←11 | 12→rules, the general concept of rule of proving in the axiomatic system can be, for a given set of formulas For, defined as follows:

R = {⟨X,A⟩ ∶ X is a subset of For, A is a formula}.

An axiomatic system is most often a ordered pair ⟨For, R⟩, where For is a decidable set of formulas, whereas R is non-empty set of rules of argumentation. When a rule is an axiomatic rule, it contains pairs ⟨X,A⟩, where X is an empty set, whereas A is a formula being introduced to the proof without premises.

With an axiomatic system ⟨For,R⟩ we can now define the general concept of proof of formula A on the basis of set of premises X. We shall state that A is provable on the basis of premises X iff there exists finite sequence of formulas B1, . . . , Bn such that:

1.Bn = A

2.for any 1 ≤ in at least one of two cases occurs:

BiX

there exist: rule RR and such pair ⟨Y,C⟩ ∈ R that

C = Bi

Y is an empty set or for certain m > 0 and certain 0 < k1, . . . , km < i, Y =

With a defined axiomatic system and the concept of provability, we can proceed to the argumentation. However, unlike the tableau systems, inmost cases it is not easy as it requires intuition, ingenuity and other skills. Moreover, it is usually difficult to move from an unsuccessful proof to a countermodel construction.

The above comparison could be summarised by saying that:

  • axiomatic systems are simpler to define (which does not imply that a system with the required properties is easy to define, but the general definition of system and proof is simple) and can be defined precisely, however producing proofs on their ground and finding a countermodel is usually difficult
  • tableau systems are more complicated to define and are usually not defined with sufficient precision (which makes it impossible to generalize tableau concepts and create metatheories of whole classes of tableau systems), but producing proofs in tableau systems is most often simple and in many cases enables finding a countermodel.

One of the primary goals of this study is to define the tableau concepts—concepts that seem necessary — that occur when defining various tableau systems precisely, and then try to generalize them within the scope determined by the use of tableau methods to construct propositional logic and term logic specified by bivalent semantics.

←12 |
 13→

Therefore, we would like the tableau methods—similarly to axiomatic methods — to be based on certain constants and general concepts, and the construction of a given tableau system boiled down only to specifying those components that distinguish this tableau system from other tableau systems.

Such an approach will result not only in general and precise tableau concepts that can be used in the construction of different systems but also in proving metatheorems not of individual systems, but of entire classes of tableau systems. These metatheorems will apply to those properties of tableau systems that are independent of their specific features and concern all systems in a given class, constructed on the basis of general, developed tableau concepts.

By a tableau system — by analogy to the axiomatic system — we can understand a certain ordered triple of sets ⟨For, Te, Rt⟩ where:

As distinct from the axiomatic system, the tableau system therefore features an additional element — a set of tableau expressions Te. In the specific case — such a case will be described in the next chapter — it may be so that Te = For. Most often, however, these sets are different because although we look for a logical relationship between a set of formulas and a given formula, we carry out a tableau proof based on tableau expressions Te for which a set of formulas alone is often insufficient.

Every axiomatic system ⟨For,R⟩ unambiguously determines a relation of derivability ⊢R which occurs between such sets of premises and such formulas that on the grounds of this system the latter are derivable from the former. The axiomatic system can therefore be understood as pair ⟨For,⊢R⟩.

It should be similar for any tableau system ⟨For,Te,Rt⟩, and thus it should unambiguously determine the tableau derivability relationship ▷Rt which contains such pairs of premises and conclusions ⟨X,A⟩ that in the system on grounds X we can tableau prove A. We call relationship ▷ a tableau consequence, and more ←13 | 14→often branch consequence, showing that its occurrence can be identified with the existence of a tableau with specific properties.

We should therefore aim at such definitions of tableau concepts so that we can understand a tableau system as pair ⟨For,▷Rt⟩. We have deliberately left aside the set of tableau expressions here Te as it will only serve as a domain for defining tableau rules, and as a consequence of creating proofs — since the tableau expressions are included in tableau rules.

Therefore, the problem of defining a tableau system should be reduced to defining a set of formulas, defining a set of tableau rules and the relationship between formulas and rules. The remaining tableau concepts — as in the case of the concept of provability in the axiomatic system — should be special cases of more general tableau concepts. All the more so as the concept of tableau proof is not a simple one, but—as we will show—dependent on many simpler concepts.

Hence, we want to define tableau concepts in such a way that tableau systems are simpler to define and at the same time more precise (which will enable the generalization of tableau concepts and the work on metatheories of entire classes of tableau systems), while maintaining the intuitiveness and automaticity present in producing proofs in tableau systems and, where possible, retaining the property of finding a countermodel.

Biographical notes

Tomasz Jarmużek (Author)

Tomasz Jarmużek is a Professor at the Nicolaus Copernicus University in Toruń. His activity concerns i.a. philosophical logic and its applications in philosophical problems. He is interested in metatheory, the use of binding and positional logic, and proof theory with emphasis on tableau methods.

Previous

Title: Tableau Methods for Propositional Logic and Term Logic