Show Less
Open access

Tableau Methods for Propositional Logic and Term Logic

Series:

Tomasz Jarmużek

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.

Show Summary Details
Open access

4 Tableau system for modal logic S5

←98 | 99→

4Tableau system for modal logic S5

3.1Introductory remarks

Chapter Four will be devoted to a case extremely different than, presented in Chapter One, the case of tableau system for CPL. For we consider modal logic S5 (for short: S5), defining the set of tableau expressions in such a way for it neither to concur with the set of formulas of logic S5, nor to be its proper superset—both sets are disjoint1.The proofs in the tableau system that we are going to construct will therefore be carried out in a language different from the one in which we want to determine whether or not a given consequence relation holds.

Another important difference between the previous systems and the one currently being defined is that the systems described previously featured the property of a finite branch, which is not the case for the presented tableau system for S5.

Therefore, it may happen that when constructing a branch and consequently a tableau which begins with a finite set of expressions, it is not possible to finish it as some sequences of application of the rules become cyclical. The lack of a finite branch property forces changes in a concept of maximal branch and in dependent concepts.

So, the tableau concepts defined in previous chapters will become special cases of tableau concepts for systems that do not feature the property of a finite branch. The leading change is the generalisation of the concept of maximal branch. Still, the maximal branch is a branch to which no rule can be applied anymore in order to extend it as it contains everything tableau rules are capable of introducing to it. Previously, however, for the cases of finite sets this meant that the maximal branch was of a finite length. It does not have to be the case this time. A maximal branch can be infinite even though the infinity of a branch does not imply its maximal nature. For there exist cases of infinite-length branches that are not maximal.

It is worth noting that the systems that feature the property of a finite branch are decidable. For theoretically, always in a finite number of steps it is possible to construct a complete tableau for them—closed or open one, thus answering the question whether a given formula is or is not tableau derivable on the grounds of given premises. In the case of tableau systems that do not feature a finite branch ←99 | 100→property, these systems may not be decidable. So, although we prove that they are complete and consistent in relation to the initial, semantically defined relation, there does not have to exist a general way of constructing a complete tableau even though such a tableau can exist.

So, we treat the case of a tableau system for S5 logic as a model for two reasons:

  • the set of tableau expressions is naturally different than the set of formulas
  • branches beginning with finite sets of expressions can feature an infinite lengths.

Both reasons lead to the need of generalization of the so-far applied tableau concepts, affecting the formalisation of tableau methods offered in the book.

4.2Language and semantics

As usual, for the start we will define the basic concepts for the logic S5. First, we will take up the language of S5.

Definition 4.1 (Alphabet of S5). Alphabet of the modal logic S5 is the sum of the following sets:

  • set of logical constants: Lc = {¬,∧,∨,→,↔,◇,◻}
  • set of propositional letters: Var = {p1,q1,r1,p2,q2,r2, . . .}
  • set of brackets: {),(}.

Although the set of propositional letters is infinite and includes indexed letters, in practice we will use a finite number of the following letters: p, q, r, s.

Definition 4.2 (Formula S5). Set of formulas of modal logic S5 is the smallest set X which meets conditions:

  1. Var ⊆ X
  2. if A, BX, then

a. ¬AX

b. ◻AX

c. ◇AX

d. (AB) ∈ X

e. (AB) ∈ X

f. (AB) ∈ X

g. (AB) ∈ X.

We specify this set as ForS5, and its elements will be called formulas.

We will now proceed to the interpretation of set ForS5. To begin with, let us recall some properties of binary relations.

←100 | 101→

Definition 4.3. Let R be a binary relation defined on Cartesian product X × X, for some set X. We shall state that:

  1. R is a universal relation iff ∀x, yX xRy
  2. R is an equivalence relation iff

a. R is a reflexive relation, i.e. ∀xX xRx

b. R is a symmetric relation, i.e. ∀x, yX (xRyyRx)

c. R is a transitive relation, i.e. ∀x, y, zX (xRy&yRzxRz).

From the above definition 4.3, the following conclusion follows.

Corollary 4.4. Each universal relation is an equivalence relation.

We will now proceed to the concept of model for formulas S5.

Definition 4.5 (Model for language of S5). Model 𝔐S5 for language of S5 will be called such ordered quadruple ⟨W,R,V,w⟩ that:

  • W is a non-empty set
  • R is a universal relation defined on Cartesian product W×W, i.e. R =W ×W
  • V is a function valuating propositional letters in the elements of set W, i.e. V ∶ Var×W → {0,1}
  • wW.

From definition of model 4.5 and conclusion 4.4 another conclusion results.

Corollary 4.6. Each model with a universal relation is a model with an equivalence relation.

Models with equivalence relation will be denoted as

Now, we shall define truth in model. This definition also applies to models with equivalence relation

Definition 4.7 (Truth in model). Let 𝔐S5 = ⟨W,R,V,w⟩ be a model and let A ∈ ForS5. Formula A is true in model 𝔐S5 (for short: 𝔐S5A) iff for any formulas B,C ∈ ForS5 the below conditions are met:

  1. if A ∈ Var, then V(A,w) = 1
  2. if A ∶= ¬B, then formula B is not true in model 𝔐S5 (for short: 𝔐S5B)
  3. if A ∶= (BC), then 𝔐S5B and𝔐S5C
  4. if A ∶= (BC), then 𝔐S5B or𝔐S5C
  5. if A ∶= (BC), then 𝔐S5B or 𝔐S5C
  6. if A ∶= (BC), then 𝔐S5B iff 𝔐S5C
  7. ←101 | 102→ if A ∶= ◻B, then ∀uW(wRu⇒⟨W,R,V,u⟩ ⊧ B)
  8. if A ∶= ◇B, then ∃uW(wRu&⟨W,R,V,u⟩ ⊧ B).

Formula A is false in model 𝔐S5 (for short: 𝔐S5A) iff it not true.

Let X ⊆ ForS5. Set of formulas X is true in model 𝔐S5 (for short: 𝔐S5X) iff for any formula AX, 𝔐S5A. Set of formulas X is false in model 𝔐S5 (for short: 𝔐S5X) iff it is not the case that 𝔐S5X.

Now, we will show a fact that displays an connection between models with equivalence relation and those with universal relation.

Proposition 4.8. For any model there exists such model 𝔐S5 = ⟨W,R,V,wthat for any formula AForS5,

Proof. Take any model with equivalence relation Next, define model with universal relation 𝔐S5 = ⟨W, R, V, w⟩ as follows:

  • W = {xW′ ∶ wRx}
  • R = {⟨x,y⟩ ∶ x,yW}
  • where is a restriction of function V′ to set Var ×W
  • w = w ′.

R′ is an equivalence relation, RR′, where constitutes a restriction of relation R′ to set W={xW′ ∶wRx}, so is a universal relation. Since relation R′ is reflexive, so obviously w′ ∈ W, thus model 𝔐S5 is well defined.

Consider any propositional letter q ∈ Var. By definition of model 𝔐S5, since so for any uW it is the case that (∗) V′(q,u) = 1 iff V(q,u) = 1.

Now, take any formula A∈ ForS5. We will consider various construction possibilities for formula A, carrying out an inductive proof in respect of the complexity of formula A and showing that for any uW, the below thesis occurs:

(∗∗) ⟨W′,R′,V′,u⟩ ⊧ A iff ⟨W,R,V,u⟩ ⊧ A.

Initial step. Take any uW. Assume that A ∈ Var. By (∗) and definition of truth in model 4.7, we get ⟨W′,R′,V′,u⟩ ⊧ A iff ⟨W,R,V,u⟩ ⊧ A.

Induction step. Take any formulas B, C ∈ ForS5 and assume that (∗∗∗) for B, C and for any uW, the following occurs:

W′,R′,V′,u⟩ ⊧ B iff ⟨W,R,V,u⟩ ⊧ B

W′,R′,V′,u⟩ ⊧ C iff ⟨W,R,V,u⟩ ⊧ C.

Take any uW and consider the following cases:

  1. A = ¬B, A = (BC), A = (BC), A = (BC) or A = (BC); then by virtue of assumption (∗ ∗ ∗) and definition of truth in model 4.7, we get ⟨W′,R′,V′,u⟩ ⊧ A iff ⟨W,R,V,u⟩ ⊧ A
  2. ←102 | 103→ A =◻B; then, by virtue of definition of truth in model 4.7, ⟨W′,R′,V′,u⟩⊧◻B iff ∀zW'(uRz ⇒ ⟨W′,R′,V′,z⟩ ⊧ B), by definition of set W and relation R and by assumption (∗ ∗ ∗), it is the case iff ∀zW(uRz ⇒ ⟨W,R,V,z⟩ ⊧ B), while by virtue of definition of truth in model 4.7, iff ⟨W,R,V,u⟩ ⊧ ◻B, thus ⟨W′,R′,V′,u⟩ ⊧ A iff ⟨W,R,V,u⟩ ⊧ A
  3. A = ◇B; then, by virtue of definition of truth in model 4.7, ⟨W′,R′,V′,u⟩ ⊧ ◇B iff ∃zW'(uRz&⟨W′,R′,V′,z⟩ ⊧ B), by definition of set W and relation R and by assumption (∗∗∗), it is the case iff ∃zW(uRz&⟨W,R,V,z⟩ ⊧ B), while by virtue of definition of truth in model 4.7, iff ⟨W,R,V,u⟩⊧◇B, thus ⟨W′,R′,V′,u⟩ ⊧A iff ⟨W,R,V,u⟩ ⊧ A.

Consequently, we get thesis:

for any uW, ⟨W′,R′,V′,u⟩ ⊧ A iff ⟨W,R,V,u⟩ ⊧ A. However, since w = w′ and wW,

Making use of the concept of model, we can now define the concept of semantic consequence relation in S5. For the entire class of models with universal relation, in a normal way on set P(ForS5)×ForS5 we define the consequence relation.

Definition 4.9 (Semantic consequence of S5). Let A ∈ ForS5 and X ⊆ ForS5. We shall state that from set X follows formula A (for short: XA) iff for any model 𝔐S5, if 𝔐S5X, then 𝔐S5A. Relation ⊧ will also be called semantic consequence relation of logic S5 or for short semantic consequence relation.

Denotation 4.10. For any set of formulas X and any formula A notation XA will mean that it is not the case that XA.

Let us remind that we defined models for S5 with the use of universal relations. It is known, however, we could define models for S5 using equivalence relations — since both classes of models determine the same semantic relation of consequence, which is expressed by another fact.

Proposition 4.11. Let AForS5 and XForS5. Then, XA iff for any model with equivalence relation 𝔐′, if 𝔐′ ⊧ X, then 𝔐′ ⊧ A.

Proof. Let A ∈ ForS5 and X ⊆ ForS5.

First, we will prove the implication “from the left to the right”. Assume that XA and take any model with equivalence relation such that From fact 4.8 we know that for certain model with universal relation 𝔐S5 it is the case that for any formula B ∈ ForS5, iff 𝔐S5B. Thus 𝔐S5X, and consequently, by assumption 𝔐S5A. Again, making use of fact 4.8, we get

←103 | 104→

We prove implication ‘from the left to the right’ with the use of conclusion 4.6. Assume that for any model with equivalence relation 𝔐′, if 𝔐′ ⊧X, then 𝔐′ ⊧A, and take any model 𝔐S5 such that 𝔐S5X. But, by conclusion 4.6, model 𝔐S5 is a model of equivalence relation, thus 𝔐S5A.

The above issue will be discussed in subchapter devoted to the axiomatization with tableau rules as it directly suggests the possibility of two different axiomatizations.

Let us now go to the concept of contradictory set of formulas.

Definition 4.12. Let X ⊆ ForS5. Set of formulas X is contradictory iff for any model 𝔐S5X. Set X is non-contradictory iff X it is not contradictory.

Another conclusion follows from definition of contradictory set of formulas 4.12 and definition of truth in model 4.7.

Proposition 4.13. Let XForS5 and AForS5. If {AA} ⊆ X, then X is contradictory.

4.3Basic concepts of the tableau system for S5

Unlike the tableau system for CPL, in the case of tableau system for TL the tableau proofs were carried out in a more rich language than the set of formulas. In the case of tableau system for S5, the language of tableau proof has no common elements with the language of logic S5 — thus in this respect, the described system constitutes a completely new case.

Let us now define the proof language for the tableau system for logic S5.

Definition 4.14 (Tableau expressions for S5). Set of tableau expressions is the union of two following sets:

  • Cartesian product: ForS5 ×ℕ
  • {irji,j ∈ ℕ}.

We specify this set as TeS5, and its elements will be called tableau expressions or simply expressions. Numbers present in the expressions will be called indices.

In the event of tableau systems for the modal logic, sometimes there is a need of “selecting” indices from the tableau expressions. Thus, let us define an appropriate function to enable the above. Before that, however, we will introduce an auxiliary function h ∶ TeS5P(ℕ) defined for any A ∈ ForS5 and i,j ∈ℕ with conditions:

  • h(⟨A,i⟩) = {i}
  • h(irj) = {i,j}.
←104 | 105→

Definition 4.15 (Function selecting indices). Function selecting indices will be called function ∗∶ P(TeS5)→ P(ℕ) defined for any X ⊆ TeS5 with condition:

• ∗(X) =⋃{h(y) ∶ yX}.

For any subset TeS5, function ∗ selects all indices present in the expressions from that set.

Let us now proceed to the concept of similar sets of expressions. Intuitively, two sets of expressions are similar iff their expressions contain exactly the same formulas and all expressions in both sets are structurally similar with respect to the indices. Formally:

Definition 4.16 (Similar set of expressions). Let X, Y ⊆ TeS5. X is similar to Y iff there exists such bijection g ∶ ∗(X) →∗(Y) that for any A ∈ ForS5 and indices i,j ∈ ℕ:

  • A,i⟩ ∈ X iff ⟨A,g(i)⟩ ∈ Y
  • irjX iff g(i)rg(j) ∈ Y.

Based on definition 4.16, we can draw the following conclusion.

Corollary 4.17. The relation of similarity is symmetric, i.e. For any sets of expressions X, Y, if set X is similar to Y, then Y is similar to set X.

Proof. By definition of similar sets of expressions 4.16, by the fact that function g is bijection and by the equivalences present in both conditions.

Next, we introduce a definition of tableau inconsistent set.

Definition 4.18 (Tableau inconsistent set of expressions). Set X ⊆ TeS5 will be called tableau inconsistent (for short: t-inconsistent) iff for some formula A ∈ ForS5 and some index i ∈ ℕ, ⟨A,i⟩ ∈ X and ⟨¬A,i⟩ ∈ X. Set X is tableau consistent (for short: t-consistent) iff X is not t-inconsistent.

From this definition, the following conclusion results.

Corollary 4.19. Let X, YTeS5. If set X is similar to set Y, then X is t-consistent iff Y is t-consistent.

Proof. Let X, Y ⊆ TeS5, and assume that X is similar to set Y. Also, assume that set X is t-inconsistent. Then, by definition of t-inconsistent set 4.18, set X contains expressions ⟨A,i⟩, ⟨¬A,i⟩, for some A ∈ ForS5 and i ∈ ℕ. By definition of similar set 4.16, there exists bijection g ∶ ∗(X) → ∗(Y) and set Y contains expressions ⟨A,g(i)⟩, ⟨¬A,g(i)⟩, thus by definition of t-inconsistent set 4.18, set Y ←105 | 106→is t-inconsistent. On the other hand, since relation of set similarity is symmetric 4.17, then by assumption, set Y is similar to set X. Also, assume that set Y is t-inconsistent. Then, by definition of t-inconsistent set 4.18, set Y contains expressions ⟨A,i⟩, ⟨¬A,i⟩, for some A ∈ ForS5 and i ∈ℕ. By definition of similar set 4.16, there exists bijection g′ ∶ ∗(Y)→∗(X) and set X contains expressions ⟨A,g′(i)⟩, ⟨¬A,g′(i)⟩, thus by definition of t-inconsistent set 4.18, set X is t-inconsistent.

For further studies, we also need a concept that would combine models with the set of expressions.

Definition 4.20 (Model appropriate for set of expressions). Let 𝔐S5 = ⟨W,R,V,w⟩ be a model and let X ⊆ TeS5. We shall state that model 𝔐S5 is appropriate for X iff there exists such function f ∶ ℕ → W, that for any A ∈ ForS5 and i,j ∈ ℕ:

  • if ⟨A,i⟩ ∈ X, then ⟨W,R,V,f(i)⟩ ⊧ A
  • if irjX, then f(i)Rf(j).

Another fact follows from the above definition.

Proposition 4.21. Let X be a t-inconsistent set of expressions. Then, there exists no model 𝔐S5 appropriate for X.

Proof. Take any set of expressions X and any model 𝔐S5 = ⟨W,R,V,w⟩ and assume that X is t-inconsistent. Then, by definition of tableau inconsistent set of expressions 4.18, for some formula A ∈ ForS5 and for some index i ∈ ℕ, ⟨A,i⟩ ∈ X and ⟨¬A,i⟩ ∈ X. If model 𝔐S5 were appropriate for set of expressions X, then by definition of model appropriate for the set of expressions 4.20, there would exist such function f ∶ℕ→ W that if ⟨A,i⟩ ∈ X, then ⟨W,R,V,f(i)⟩ ⊧A and if ⟨¬A,i⟩ ∈ X, then ⟨W,R,V,f(i)⟩ ⊧ ¬A, and so ⟨W,R,V,f(i)⟩ ⊧ A and ⟨W,R,V,f(i)⟩ ⊧ ¬A. However, from fact 4.13 and definition 4.12, it follows that there exists no such a model. Hence, model 𝔐S5 is not appropriate for set of expressions X.

4.3.1Tableau rules for S5

As in the previous cases of described tableau systems, we first provide the general concept of rule. Not only because it facilitates provision of the general features that a tableau rule must meet. In the case of system construction for S5 we will provide—as in the case of TL—alternative sets of tableau rules that are suitable for construction of tableau system for logic S5.This means that within the below general concept of rule, we can define different sets of tableau rules that define various, however equivalent in terms of scope of branch consequence, tableau systems for S5 (see note 2.19 and 3.20).

←106 | 107→

Definition 4.22 (Rule). Let P(TeS5) be a power set of the set of tableau expressions. Let P(TeS5)n be n-aryCartesian product for some

n ∈ℕ.

• By a rule we understand any subset RP(TeS5)n such that if ⟨X1, . . . ,Xn⟩∈ R, then:

a. X1 is t-inconsistent

b. X1Xi, for each 1 < in.

  • If n ≤ 2, then each element R will be called an ordered n-tuple (pair, triple, etc., respectively).
  • The first element of each n-tuple will be called an input set (set of premises), while its remaining elements output sets (sets of conclusions).

In the case of S5, the rule definition differs from the rule definition for TL (definition 3.18) only in that it is specified on a different set of expressions and in a different nature of t-inconsistency. Beyond that, these definitions are structurally similar, because we are seeking to formulate general concepts. A set of tableau rules for the tableau system for CPL we describe, shall be introduced by means of another definition.

Definition 4.23 (Tableau rules for S5). Tableau rules for S5 are the following rules:

←107 | 108→

  1. j ∉ ∗(X ∪ {⟨◇A,i⟩})
  2. for any k ∈ ℕ, {irk,⟨A,k⟩} ⊈ X.

where i,j ∈ ∗(X).

Set of tableau rules for S5 will be defined as RS5.

Let us now devote a few words to discussing the described rules. Although in many ways they resemble the rules from set RTL, there are also some differences.

According to the definition of rule 4.22, the input sets of each rule are t-consistent. In addition, in each rule, the input set is basically contained in each output set. Again, there appears the two-premise rule—rule R.

On the other hand, similar to the case of rules Ri and Ro for TL, we have a rule with limitations on introducing new expressions. Wemean rule R. This rule says that the expressions introduced are to have a new index (condition 1), moreover, the input set must not contain expressions similar to the one entered, beginning with the index appearing in the expression with ◇ (condition 2).

←108 | 109→

The semantic intuitions on which condition 1 is based are as follows. Theobject denoted by a new index is also to be new and its relationship with other objects that are denoted by the other indices is to remain unresolved.

Condition 2 prevents unnecessary expressions from being entered in the proof. In practice, it also prevents the proof from being unnecessarily extended indefinitely — so it prevents the creation of infinite branches when this is not a consequence of logic itself, but of the wrong definition of tableau system(example 4.24).

The last rule is a rule that corresponds to universal relation in the models. With rule Rr, each two indices that appear in the expressions found in the proof may cause the addition to the proof of another expression that contains those indices. These indices do not have to be different, of course.

Example 4.24. Consider the following set of expressions X ∪{⟨◇p,1⟩} and rule R without condition 2. The use of rule R without condition 2 can result in infinite branches by entering expressions with new indices.

The example presented above could be part of some kind of proof in which we could still apply rule R to each new set without condition 2, utilizing the fact that it contains expression ⟨◇A,1⟩.

In a standard, informal and intuitive approach to the logic within a tableau approach2, we can find an equivalent of rule R — below, we denote it in a conventional form:

A,j, where j is new in the branch.

However, this formulation of the rule causes various problems. The basic problem — a fundamental one, we can say — is that the rule refers to the concept of ←109 | 110→branch, although the concept of branch is connected with the concept of set of rules—in our approach a branch is determined by the application of rules from the output set of rules. So, this way of defining a rule has the features of circularity — we define a rule by reference to a branch, whereas the definition of branch requires the definition of set of rules.

In addition, this formulation of rule R seems too weak. In literature, it is only the comments to the rule that prohibit its application to the same expression more than once3.

In the view presented in the book, rule R formally requires a new index when applied (condition 1 allows only such pairs of sets), but also blocks the creation of catch-22 situation of applications (due to condition 2). In the approach we offer, we formally subsume the fact that index must be new and the rule can only be applied to the same formula once. Besides, the latter formulation is not precise either; in some cases condition 2 does not allow us to apply rule R to given formula even once (example 4.25).

Example 4.25. Consider the following set of expressions X ∪ {⟨◇p,1⟩, ⟨◇(pq),1⟩} and rule R with condition 2.

To set X1 we applied rule R, drawing conclusions from expression ⟨◇(pq),1⟩. Next, to set X2 we applied rule R by decomposing expression ⟨(pq),2⟩. However, to set X3 we cannot anymore apply rule R in order to decompose expression ⟨◇p,1⟩, since X3 contains expressions 1r2 and ⟨p,2⟩. So, to expression ⟨◇p,1⟩ we did not apply rule R even once.

However, as noted before, in modal logic, even application of conditions blocking the unnecessary use of rules may not prevent the emergence of infinite branches, which will be proven later, having defined the concept of modal branch.

Remark 4.26. We can consider alternative sets of rules for the construction of a tableau system for S5. The following rules would help (on their right side we put the condition that fulfils the relation in the model).

←110 | 111→(Reflexivity)
(Symmetry)
(Transitivity)

The above rules correspond to the properties of equivalence relations: reflexivity, transitivity and symmetry. Fact 4.11 states that a class of models with universal relation and a class of models with equivalence relation define exactly the same logic. Therefore, an alternative set of tableau rules could be defined through the above three rules: (RS5Rr)∪{Rref ,Rsym,Rtrans}.

Although both sets of rules seem to be interesting, for the reasons we have already described, we will not investigate the second one—for we intend to provide a generalisation further in the book which will also include this approach. So, now we will focus on the tableau system determined by set of rules RS5. The example provided indicates that the general definition of rule 4.22 makes sense. There may exist many sets of tableau rules that potentially — to determine this always requires a proof—define the same logic.

The adopted set of tableau rules—in our case set RS5 —specifies the content of the range of successive concepts of the tableau system. Formally, the concepts we will describe will be analogous to those from the previous chapter. However, each of them will depend on set of tableau rules RS5.

4.3.2Branches for S5

With a fixed set of tableau rules, we can proceed to the concept of branch. Branches are such sequences of sets that each two adjacent elements constitute an input set and an output set of some n-tuple that belongs to the set of tableau rules. Branches are therefore setwise objects consisting of sets. Let us now proceed to the formal definition of branch in the tableau system for S5 and derived concepts. The individual concepts will be similar to those from the previous chapters, and all of them will be defined on the currently adopted set TeS4.

Definition 2.27 (Branch). Let K = ℕ or K = {1,2, . . . ,n}, where n ∈ ℕ. Let X be any set of expressions. A branch (or a branch beginning with X) will be called any sequence ϕKP(TeS5) that meets the following conditions:

←111 | 112→
  1. ϕ(1) = X
  2. for any iK, if i +1 ∈ K, then there exists such rule RRS5 and such n-tuple ⟨Y1, . . . ,Yn⟩∈ R, that ϕ(i) = Y1 and ϕ(i+1) = Yk, for certain 1 < kn.

Having two branches ϕ, ψ such that ϕψ we shall state that:

  • ϕ is a sub-branch of ψ
  • ψ is a super-branch of ϕ.

Denotation 4.28. From now on—when speaking of branches—for convenience, we will use the following notations or designations:

  1. X1, . . . ,Xn, where n ≥ 1
  2. X1, . . . ,Xn⟩, where n ≥ 1
  3. abbreviations: ϕK, where K is a domain ϕ, i.e. ϕKP(TeS5)
  4. or—to denote branches—small Greek letters: ϕ, ψ, etc.

The sets of branches, in turn, we shall denote with capital Greek letters: Φ, Ψ, etc. Furthermore, the domain cardinality of a given branch K we shall sometimes call a length of that branch.

The concept of branch depends on the initial set of tableau rules. In the case under consideration, the branch structure is based on the rules from set RS5. Further described tableau concepts also depend on that set of rules. In harmony with the adopted convention, we will not entangle the notations since alls the subsequent concepts depend on set RS5.

By definition of rules 4.22, through the fact that they are defined by proper inclusion of the input set in each of the output sets in any n-tuple, we get a conclusion.

Corollary 4.29. Each branch is an injective sequence.

4.3.3Closed and open branches

Unlike usual, we will first take up a certain type of maximal branches, and only then we will introduce the concept of maximal branch. The reason for this is that because of the emergence of infinite branches beginning with finite sets of expressions, we will have to extend the concept of maximal branch. The concept of a closed branch will be useful for the extension, so we start with it. In addition, the set of closed branches is completed by the set of open branches, so we will also introduce the concept of open branch.

As we remember, intuitively a branch is closed when we get a t-inconsistent set having decomposed expressions by rules.

←112 | 113→

Definition 4.30 (Closed/open branch). Branch ϕKP(TeS5) will be called closed iff ϕ(i) is a t-inconsistent set for some iK. Branch ϕ will be called open iff it is not closed.

From the above definition, the definition of tableau rules for S5 4.23 and the definition of branch 4.27, we get the fact.

Proposition 4.31. If branch ϕKP(TeS5) is closed, thenK∣ ∈ ℕ and ϕ(∣K∣) is a t-inconsistent set.

In the case of a closed branch, the t-inconsistent sequence element is the last element because no rule can be applied to it anymore to extend the branch. For the rules are defined in such a way that they cannot be applied to t-inconsistent sets.

4.3.4Maximal branches

We will commence the issue of maximal branches for the tableau system for S5 with an initial and non-proper concept of maximal branch. By analogy to the definitions of maximal branch in tableau systems for CPL and TL (definitions 2.30 and 3.26), we could adopt the following definition.

Definition 4.32 (Maximal branch — variant one). Let ϕKP(TeS5) be a branch. We shall state that ϕ is maximal iff

  1. K = {1,2,3, . . . ,n}, for some n ∈ℕ
  2. there is no branch ψ such that ϕψ.

Unfortunately, there are cases where the first set is finite, but this does not guarantee the finiteness of branch. So, regardless of either we used all the rules from set RS5 which could have been applied to some expressions appearing in the branch, or we still have expressions to which no rules were applied, the branch can be infinite.

Example 4.33. Consider an example of set {⟨¬(◇p →◇◻p),1⟩}. It is a finite set. Below, we describe an infinite branch beginning with set X and constructed by applying the rules from set of tableau rules RS5.

←113 | 114→

The branch of infinite length is obtained by applying by turns the following rules R, Rr, R, R¬◻ to set X10 and to each subsequent set that is created following the application of the given sequence of rules.

The definition of maximal branch in the given version specifies that the maximal branch is finite and there exists no super-branch for it. This definition is good for those systems where applying tableau rules to finite sets of expressions always produces finitely long branches. In these cases, using the tableau rules for a given system, we can decompose all the initial expressions from a finite set of tableau expressions in a finite number of steps. It is therefore not a good definition for modal logic because of the following fact.

Proposition 4.34. There exists such finite set of expressions X that a branch beginning with X is infinite.

Proof. Example 4.33.

It would appear that removal of the first condition from definition 4.32 will improve the situation. Removal of the first condition would mean that the branch does not have to be of finite length. Its maximality would be based on the fact that there exists no super-branch of it. However, the lack of a super-branch for the branch beginning with a finite set does not mean that all the tableau rules that could be used to construct the branch were actually used. Even in example 4.33, in individual sequences, we did not make use of all the possibilities of using rule Rr.

←114 | 115→

Note that by adding to set X = {⟨¬(◇p →◇◻p),2⟩} any new expression—e.g. ⟨(q∧¬q),2⟩, we get a finite set again. For this set, there exists a branch of infinite length in which the rule for this new expression has not been applied in any of the subsets (example 4.35).

Therefore, even though the branch may satisfy the second condition from definition 4.32—there is no branch to be contained in it — it does not, however, draw all the possible conclusions from the expressions that belong to the elements of this branch, including the initial set.

Example 4.35. Consider an example of set of expressions X = {⟨¬(◇p →◇◻ p),1⟩,⟨(q ∧¬q),1⟩}. It is a finite set. Below, we describe an infinite branch beginning with set X and constructed by applying the rules from set of tableau rules RS5. This branch is similar to the one in example 4.33, except that each of its elements contains expression ⟨(q∧¬q),1⟩ from which in none of the branch elements conclusions have been drawn applying rule R .

A branch of infinite length is obtained by applying by turns the following rules R, Rr, R, R¬◻ to set X10 and to each subsequent set that is created following the application of the given sequence of rules. Whereas, in no step we apply rule R.

Before we can introduce a somewhat more general and ultimate definition of maximal branch, we still need a few auxiliary concepts.

←115 | 116→

Definition 4.36 (Core of rule). Let rule RRS5 and n ∈ ℕ. Let ⟨X1, . . . ,Xn⟩∈ R and ⟨Y1, . . . ,Yn⟩∈ R. We shall state that set ⟨Y1, . . . ,Yn⟩∈ R is a core of rule R in setX1. . . . ,Xn⟩ iff

  1. Y1X1
  2. there exists no such proper subset U1Y1 that for some n-tuple ⟨U1, . . . ,Un⟩∈ R
  3. for any 1 < in, Yi = Y1 ∪(XiX1).

Remark 4.37. Note that in the case of tableau rules from set RRS5:

  • the cores of rule for given n-tuple are expressions that play important roles at given stage of the tableau proof—most often, the core input set is one-element set
  • in a special case, the core input set for the rule for given n-tuple is two-element set of expressions—it is the case, for instance, in the event of rule R.

Even though the rules have been defined on sets, the concept of core of rule in set indicates an essential element or elements which enable drawing conclusions through the use of rule.

The above concepts result in the following conclusion.

Corollary 4.38. Let rule RRS5, n ∈ℕ, and letX1, . . ., Xn⟩∈ R. Then, there exists such n-tupleY1, . . . ,Yn⟩ ∈ R thatY1, . . ., Ynis the core of rule R insetX1, . . . ,Xn.

Proof. By definition of tableau rules 4.23 and by definition of core of rule 4.36.

Now, we can proceed to the concept of strong similarity between the sets of expressions. It is a speciality of the concept of similarity (definition 4.16).We will need the concept of strong similarity for the definition of maximal branch.

Definition 4.39 (Strong similarity). Let rule RRS5 and let ⟨X1, . . . ,Xn⟩∈ R, for some n ∈ ℕ. On any set of expressions W ⊆ TeS5, we will state that it is strongly similar to set Xi, where 1 < in, iff

  1. W is similar to Xi
  2. for certain n-tuple ⟨Y1, . . . ,Yn⟩, which is the core of rule R in set ⟨X1, . . . ,Xn⟩, and for certain WW, the following conditions are met:

a. Y1W

b. W′ is similar to Y1 ∪(XiX1).

←116 | 117→

Having adopted the concept of strong similarity, we can proceed to the concept of maximal branch in the final version.

Definition 4.40 (Maximal branch). Let ϕKP(TeS5) be a branch. We shall state that ϕ is maximal iff it meets one of the below conditions:

  1. ϕ is closed
  2. for any rule RRS5, any n ∈ℕ and any n-tuple ⟨X1, . . . ,Xn⟩ ∈ R, if ϕ(k)=X1, for certain kK, then for some jK, there exist ϕ(j) and such set of expressions W ⊆ TeS5 that for some 1 < in,W is strongly similar to Xi and Wϕ(j).

Remark 4.41. According to the above definition, a maximal branch is closed or, in a sense, closed under application of rules (both conditions do not necessarily have to be mutually exclusive). Closure under rules means that if a branch is not closed and it was possible to apply some rule to one of its elements, then some of the branch elements includes a set strongly similar to the one that could have been a result of application of that rule. There are two things worth clarifying.

In the definition, we mention a strongly similar set W because the application of rule R, in subsequent stages, can result in different sets than the ones we would have gotten by applying this rule earlier.

Set W is to be contained in one of the elements of branch ϕ(j), and not necessarily be identical to it, since the rule could have been applied to set ϕ(j−1) which can be a proper superset of set X.

Therefore, maximal branches can be either finite or infinite. Of course, if a branch is maximal in terms of the first definition 4.32, that means it is maximal in terms of the definition we have adopted—4.40.

Corollary 4.42. Each branch which is maximal in terms of definition 4.32 is maximal in terms of definition 4.40.

Proof. Take any branch ϕ maximal in terms of definition 4.32 and assume that ϕ is not closed. If it does not meet the second condition of definition 4.40, then since ϕ is finite — the first condition of definition 4.32, so there exists branch ψ such that ϕψ which obviously contradicts the second condition of definition 4.32.

We know, therefore, that the concept of maximal branch as used so far, expressed in definition 4.32 is a special case of the concept defined by the definition of maximal branch 4.40. The latter definition is therefore taken as a model definition for the theory of tableau systems.

Important cases for the theory of tableaux that meet the definition of maximal branch used in the chapters on the tableau system for CPL and TL, also meet definition 4.40. Important cases, both for the branch consequence relation and the ←117 | 118→tableau, are those where the initial set—a set of tableau expressions or formulas — is finite. Therefore, since we know that from finite sets in the tableau system for CPL and in the tableau system for TL only emerge finite branches (see fact 2.34 and fact 3.31), so we can state that definitions like 4.40 by virtue of conclusion 4.42 — we mean like since even though obviously, constructively the same idea stands behind them, in both cases we face different rules and different sets of expressions—are appropriate for the system with the property of a finite branch.