Tableau Methods for Propositional Logic and Term Logic

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:

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.

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.

1Introduction

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.

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:

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:

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.

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:

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.