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.3.5 Relation of branch consequence

From definitions 4.30 and 4.40, we get a self-evident conclusion.

Corollary 4.43. Each closed branch is maximal.

Therefore, sometimes when constructing a tableau proof using tableau tools for logic S5, when we seek maximal branches, we can deal with infinite branches. It is understandable that those branches cannot be described with anything different than a scheme. In general, branches, as part of a tableau proof, are not sequences put on paper, but sequences of abstract objects that we can or cannot say are or are not maximal.

4.3.5Relation of branch consequence

As in the case of previous tableau systems, we will also define the concept of branch consequence for the presently described system using the following terms: branch, maximal branch and closed branch.

Definition 4.44 (Branch consequence S5). Let X ⊆ ForS5 and A∈ ForS5. Formula A is a branch consequence of X (for short: XA) iff there exists such finite set YX and index i ∈ ℕ that each maximal branch beginning with set {⟨B,i⟩ ∶ BY ∪{¬A}} is closed.

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

The above concept of branch consequence relation differs from the analogous concept for tableau system for CPL and TL in the fact that (obviously, apart from defining on a different language — different set of expressions) when determining whether given pair belongs to the relation of branch consequence we can encounter a problem of branches that are maximal and infinite alike.

4.4Tableaux for S5

It is usually inconvenient, or even infeasible, to investigate whether a pair belongs to the relation of branch consequence. As we remember, in the approach ←118 | 119→presented in the book, it is the construction of tableau that is supposed to solve this problem.

When defining a tableau for logic S5, we will readdress the auxiliary concept of maximality in a set of branches. It is necessary because, unlike the case of tableau system for TL, and like the case of CPL, a tableau can contain many branches. So for the sake of order, we must avoid a situation in which sub-branches belong to the same tableau as their super-branches.

Definition 4.46 (Maximal branch in the set of branches). Let Φ be a set of branches and let branch ψ ∈ Φ. We shall state that ψ is maximal in set Φ (for short: Φ–maximal) iff there is no such branch ϕ ∈Φ that ψϕ.

We can now move on to the concept of tableau. Tableau is a special and non-empty set of branches that i) begin with the same set of expressions and ii) each branching requires a tableau rule that allows for such branching, and what is more iii) each branch that belongs to the tableau must be maximal in this set.

Definition 4.47 (Tableau). Let X ⊆ ForS5, A ∈ ForS5 and Φ be a set of branches. Ordered triple ⟨X,A,Φ⟩ will be called a tableau forX,A⟩ (or for short: tableau) iff the below conditions are met:

  1. Φ is a non-empty subset of set of branches beginning with {⟨B,i⟩ ∶ BX ∪ {¬A}}, for some index i ∈ℕ (i.e. if ψ ∈ Φ, then ψ(1) = {⟨B,i⟩ ∶ BX ∪{¬A}})
  2. each branch contained in Φ is Φ-maximal
  3. for any n,i ∈ ℕ and any branches ψ1, . . . , ψn ∈ Φ, if:
  4. i and i+1 belong to domains of functions ψ1, . . . , ψn
  5. • for any 1 < kn and any oi, ψ1(o) = ψk(o)

then there exists such rule RRS5 and such ordered m-tuple ⟨Y1, . . . , Ym⟩ ∈ R, where 1 <m≤ 3 that for any 1 ≤ kn:

  • ψk(i) = Y1
  • and there exists such 1 < lm that ψk(i+1) = Yl.

Again, the concept of tableaux has been defined in such a way that tableaux can also begin with infinite sets. Practicably, however, the construction of tableau is to show that a given formula is a branch consequence of given finite set of premises — according to the definition of branch consequence 4.44. To this end, we must construct tableaux containing all elements that are sufficient to solve the problem. Such tableaux are called complete tableaux. Before that, we will consisder the problem of redundant branches.

The definition of redundant branches resembles a similar definition, worded for CPL, while the difference, as usual, boils down to the fact that its subject are ←119 | 120→branches composed of other objects. Let us consider an example analogous to the one we discussed in the chapter devoted to the classical logic (example 4.48).

Example 4.48. Consider set of expressions {⟨pq,1⟩,⟨¬¬p,1⟩}. Through the use of rule R, we get two branches, and then to set X2.2 we apply rule R¬¬. Then we get the following branches.

In the light of definition of tableau 4.47, the set of these two branches is a tableau for pair ⟨{pq},¬p⟩.

However, from the viewpoint of a tableau complexity, the branch on the right seems unnecessary. This is because if we fail to get t-inconsistent set in the right-hand branch, we will also fail to get t-inconsistent set in the left-hand branch. Therefore, the branch on the right seems superfluous, and since it brings nothing important, it can be conventionally called redundant.

Let us also repeat that such branchings do not form a formal obstacle. We suggest their bypassing merely for the sake of the economy of a construction. Therefore, further concepts will be defined in a similar way as in Chapter Two, i.e. so that the tableau with or without redundant branches can be considered a complete tableau. Practically, we know that when we try to write or draw out a tableau proof, we endeavour to take account of all possibilities. If required, however, the redundant branches can be bypassed. Let us now update the concept of redundant variant of branch for the current context.

Definition 4.49 (Redundant variant of branch). Let ϕ and ψ be such branches that for some numbers i and i+1 that belong to their domains, it is the case that for any ji, ϕ(j) = ψ(j), but ϕ(i + 1) ≠ ψ(i + 1). We shall state that branch ψ is a redundant variant of branch ϕ iff:

  • there exists such rule RRS5 and such pair ⟨X,Y⟩ ∈ R that X = ϕ(i) and Y = ϕ(i+1)
  • there exists such rule RRS5 and such triple ⟨X,W,Z⟩ ∈ R that X = ϕ(i) and:
←120 | 121→

1. W = ϕ(i+1) and Z = ψ(i+1)

or

2. Z = ϕ(i+1) and W = ψ(i+1).

Let Φ, Ψ be sets of branches and Φ ⊂ Ψ. We shall state that Ψ is a redundant superset Φ iff for any branch ψ ∈ Ψ∖Φ there exists such branch ϕ ∈ Φ that ψ is a redundant variant of ϕ.

Having adopted the concept of redundant superset of branches, we can proceed to the definition of complete tableau.

Definition 4.50 (Complete tableau). Let ⟨X,A,Φ⟩ be a tableau. We shall state that ⟨X,A,Φ⟩ is complete iff:

  1. each branch contained in Φ is maximal
  2. any set of branches Ψ such that:

a. Φ ⊂ Ψ

b. ⟨X,A,Ψ⟩ is a tableau

is a redundant superset of Φ.

We shall state that a tableau is incomplete iff it is not complete.

A complete tableau contains such set of branches that it is no longer possible to add any new branches to it, without causing the ordered triple to cease to be a tableau, or there appears a redundant variant of some branch. Aswe already know, in a complete tableau, all branches are maximal, not only the maximal ones in a given set. Thus, a complete tableau contains such set of maximal branches that any of its supersets does not anymore produce a tableau, or it features at least one redundant variant of some branch that already earlier belonged to the tableau.

When constructing a complete tableau, we can face a situation in which all the branches are closed, meaning each branch ends with a set that is t-inconsistent. Such a tableau will be called a closed tableau.

Definition 4.51 (Closed/open tableau). Let ⟨X,A,Φ⟩ be a tableau. We shall state that ⟨X,A,Φ⟩ is closed iff the below conditions are met:

  1. X,A,Φ⟩ is a complete tableau
  2. each branch contained in Φ is closed.

We shall state that a tableau is open iff it is not closed.

By the above definition of closed tableau, we get another conclusion on the relation of closed tableaux with complete ones.

Corollary 4.52. Each closed tableau is a complete tableau.

←121 | 122→

4.5Theorem on the completeness of the tableau system for S5

Further, we will show that the concept of tableau is significantly helpful in determining the occurrence of relation ⊳, and that the existence of a closed tableau is equivalent to the occurrence of semantic consequence ⊧. But before we move on to these problems, we must introduce a few definitions and determine a few facts.

First, we will show that for any X ⊆ ForS5, A ∈ ForS5, if XA, then XA. Let us begin with the definition of closure under tableau rules.

Definition 4.53 (Closure under tableau rules). Let X ⊆ TeS5. We shall state that set Y ⊆ TeS5 is a closure of set X under tableau rules iff Y is a set that meets the following conditions:

  • XY
  • for any rule RRS5 and any n-tuple ⟨Z1,Z2, . . . ,Zn⟩∈ R, where n ∈ℕ, if XZ1Y, then ZjY, for some 2 ≤ jn.

If set Y is a closure of set X under tableau rules, then it will be denoted as XY. Sometimes, on set Y we will simply state that it is a closure.

Obviously, each set of expressions X has its closure Y such that XY ⊆ TeS5. Some sets can have more that one closure. Note that by definition of branch 4.27, the following fact occurs.

Proposition 4.54. Each closure under tableau rules is a branch of length one.

Making use of the concept of closure, we will now show a relationship between the existence of maximal and open branches originating from finite subsets of some set of expressions and the existence of closure of that set which is an open and maximal branch.

Lemma 4.55 (On the existence of maximal and open branch). Let XForS5 and i ∈ ℕ. If for any finite subset YX there exists an open and maximal branch beginning with set of expressions Yi ={⟨A,i⟩ ∶ AY}, then there exists such closure Z of set of expressions Xi ={⟨A,i⟩ ∶AX} under tableau rules that Z is an open and maximal branch.

Proof. Take any X ⊆ ForS5 and i ∈ ℕ. Next, assume that (∗) for any finite subset YX there exists open and maximal branch beginning with set of expressions Yi = {⟨A,i⟩ ∶ AY}.

Now, we take the set of all maximal and open branches beginning with set Yi = {⟨A,i⟩ ∶ AY}, for any finite subset YX. The set will be denoted as X.

Next, we will define set X with the following conditions:

←122 | 123→
  1. XX
  2. for any two branches ϕ and ψ contained in X, if there exist such two numbers i,k ∈ℕ that ϕ(i)∪ψ(k) is a t-inconsistent set, then ϕX or ψX
  3. X is a maximal set among subsets X that meet conditions 1 and 2.

There exists at least one such set X that XX. Take one such set X and denote it as X.

Consider set ⋃{ϕ(1) ∶ ϕX}. Note that (∗∗) X i ⊆⋃{ϕ(1) ∶ ϕX}. If that was not the case, there would exist such xX i that x ∉ ⋃{ϕ(1) ∶ ϕX} and for each such branch ψX that xψ(1), ψ(1) ⊆ X i and ψ(1) is a finite set, it would be the case that ψX. And then, for some finite subset YiXi there would exist no maximal and open branch beginning with set Yi ∪{x} which contradicts assumption (∗)

Now, using condition:

we define set Further, we define set

We claim that set Z is a closure of set of expressions Xi = {⟨A,i⟩ ∶ AX} under tableau rules, according to definition 4.53, and that Z is an open and maximal branch.

First, we will show that Z is a closure of set of expressions Xi = {⟨A,i⟩ ∶ AX}. Thus, we will show that Z meets conditions of closure, according to definition 4.53.

Note that X iZ, since by (∗∗) X i ⊆ ⋃{ϕ(1) ∶ ϕX}, and by construction of set Z, ⋃{ϕ(1) ∶ ϕX} ⊆ Z.

Now, take any rule RRS5 and any n-tuple ⟨U1, . . . , Un⟩∈ R, for some n ∈ ℕ, and assume that X iU1Z. From the definition of tableau rules for S5 4.23, it follows that there exists such n-tuple R that:

  • for any 1 ≤ jn, is a minimal finite set such that if Uj is not such a minimal finite set that ⟨U1, . . . , Un⟩∈ R, then Uj
  • for any 1 < jn, UjU1 =

Therefore, assuming that Z, we must show that for some 1 < ln, Z, since U1 = Ul. Since for finite set of expressions , it is the case that Z, there exists such finite number of branches ϕ1,ϕ2, . . . ,ϕo in set X that for some k ∈ ℕ, ϕ1(k) ∪ ϕ2(k) ∪ ⋅⋅ ⋅ ∪ ϕo(k). So, set X contains branch ψ such that ψ(1) = ϕ1(1)∪ ϕ2(1)∪⋅ ⋅ ⋅∪ ϕo(1) and ψ(m), for certain m ∈ ℕ, since ψ is a maximal branch and ϕ1(k)∪ϕ2(k)∪⋅⋅⋅∪ϕo(k) is a t-consistent set. But, from the fact that ψ is a maximal branch and from definition of maximal branch 4.40, it ←123 | 124→follows that for certain 1 < ln, ⊆⋃ψ, and thus Z, since by construction Z, ⋃ψZ.

We will now show that Z is an open and maximal branch.

By conclusion 4.54, set Z is a branch. By construction of set Z, Z is an open branch, that is none of the subsets of Z is t-inconsistent, by virtue of definition of set X.

Let us now check if Z is a maximal branch. Making use of the definition of maximal branch 4.40, assume that there exists a tableau rule RRS5 and n-tuple ⟨X1, . . . ,Xn⟩∈ R, for some n ∈ ℕ, such that X1 = Z. By definition of tableau rules 4.23, there exists n-tuple R such that for any 1 < jn, XjX1 =and X iZ. Since Z is a closure under tableau rules of set Xi, so Z, for certain 1 < jn, by definition 4.53. Therefore, also XjZ, since Xj = X1. But then X1Xj, which by definition of tableau rules 4.23 is out of the question. Consequently, there exists no tableau rule and n-tuple ⟨X1,. . . ,Xn⟩∈ R such that X1 = Z, for some n ∈ ℕ. Therefore, Z is a maximal branch, by definition of maximal branch 4.40

Let us define the concept of model generated by branch.

Definition 4.56 (Model generated by branch). Let ϕ be a branch. Let X be a non-empty subset of set of formulas ForS5 and {⟨A,k⟩ ∶ AX} ⊆ ⋃ϕ, for some k ∈ ℕ. We define function AT(ϕ)⊆TeS5 as follows, xAT(ϕ) iff one of the below conditions is met:

  • x ∈⋃ϕ∩{irji,j ∈ ℕ}
  • x ∈⋃ϕ∩(Var×ℕ).

We shall state that model 𝔐S5 = ⟨W,R,V,w⟩ is generated by branch ϕ iff:

  • W = {ii ∈ ∗(AT(ϕ))}∪{k}
  • for any i,j ∈ ℕ, ⟨i,j⟩ ∈ R iff irjAT(ϕ)
  • V(x,i) = 1 iff ⟨x,i⟩ ∈ AT(ϕ)
  • w = k.

Let model 𝔐S5 be generated by ϕ. Then, we shall state that ϕ generates the model.

From the definition of generated model, another conclusion results.

Corollary 4.57. Let ϕ be such an open branch that for certain non-empty set of formulas X and some index i ∈ ℕ, {⟨A,i⟩ ∶ AX} ⊆ ⋃ϕ. Then, ϕ generates model 𝔐S5 = ⟨W,R,V,i.

Proof. By definition of open branch 4.30, definition of model 4.5 and definition of model generated by branch 4.56.

←124 | 125→

Lemma 4.58 (On generation of model). Let ϕ be an open and maximal branch. Then, for any non-empty XForS5 and any index i such that {⟨A,i⟩ ∶ AX}⊆⋃ϕ there exists model 𝔐S5 such that for any formula A, if AX, then𝔐S5A.

Proof. Take any maximal and open branch ϕ such that for certain set X ⊆ ForS5 and certain index i, {⟨A,i⟩ ∶ AX}⊆⋃ϕ. Since ϕ is open, then according to conclusion 4.57, there exists, generated by ϕ, model 𝔐S5 = ⟨W,R,V,w⟩, specified in accordance with definition 4.56, where w = i.

We will carry out an inductive proof due to the construction of formulas, showing that for any formula E and any k ∈ ℕ, if ⟨E,k⟩∈⋃ϕ, then 𝔐S5 = ⟨W,R,V,k⟩⊧E.

Initial step. Take any x ∈ Var and some index j ∈ ℕ.

If ⟨x,j⟩ ∈ ⋃ϕ, then — according to the definition of generated model 𝔐S5V(x,j) = 1, thus by definition of truth in model 4.7, ⟨W,R,V,j⟩ ⊧ x.

If ⟨¬x,j⟩ ∈ ⋃ϕ, then since branch ϕ is open, ⟨x,j⟩ ∉ ⋃ϕ, and — according to the definition of generated model 𝔐S5V(x,j) = 0, thus by definition of truth in model 4.7, ⟨W,R,V,j⟩ ⊧ ¬x.

Induction step. (†) Take any formula E ∈ ForS5 and indices j,k ∈ ℕ and assume that for each tableau expression ⟨D,n⟩, where D ∈ ForS5 and n ∈ℕ that belongs to set ⋃ϕ as a result of application of some tableau rule to set {⟨E,j⟩} ⊆ ⋃ϕ or set {⟨E,j⟩,jrk} ⊆⋃ϕ, it is the case that ⟨W,R,V,n⟩ ⊧ D.

Making use of the inductive assumption, let us consider all cases of construction of formula E. Take some index j ∈ℕ.

  1. Let E = (BC) and ⟨(BC),j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R, both ⟨B,j⟩ and ⟨C,j⟩ belong to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ (BC).
  2. Let E = (BC) and ⟨(BC),j⟩ ∈⋃ϕ. Then, since ϕ is a maximal branch, due to rule R, ⟨B,j⟩ or ⟨C,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ (BC).
  3. Let E = (BC) and ⟨(BC),j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R, ⟨¬B,j⟩ or ⟨C,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ (BC).
  4. Let E = (BC) and ⟨(BC),j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R, ⟨B,j⟩, ⟨C,j⟩ belong to ⋃ϕ or ⟨¬B,j⟩, ⟨¬C,j⟩ belong to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ (BC).
  5. Let E = ¬¬B and ⟨¬¬B,j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬¬, ⟨B,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬¬B.
  6. ←125 | 126→ Let E = ¬(BC) and ⟨¬(BC),j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬∧, ⟨¬B,j⟩ or ⟨¬C,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬(BC).
  7. Let E = ¬(BC) and ⟨¬(BC),j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬∨, ⟨¬B,j⟩ and ⟨¬C,j⟩ belong to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬(BC).
  8. Let E =¬(BC) and ⟨¬(BC),j⟩ ∈⋃ϕ.Then, since ϕ is a maximal branch, due to rule R¬→, ⟨B,j⟩ and ⟨¬C,j⟩ belong to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬(BC).
  9. Let E =¬(BC) and ⟨(BC),j⟩ ∈⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬↔, ⟨¬B,j⟩, ⟨C,j⟩ belong to ⋃ϕ or ⟨B,j⟩, ⟨¬C,j⟩ belong to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ (BC).
  10. Let E = ¬◻B and ⟨¬◻B,j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬◻, ⟨◇¬B,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬◻B.
  11. Let E = ¬◇B and ⟨¬◇B,j⟩ ∈ ⋃ϕ. Then, since ϕ is a maximal branch, due to rule R¬◻, ⟨◻¬B,j⟩ belongs to ⋃ϕ. From assumption (†) and definition of truth in model 4.7, we get that ⟨W,R,V,j⟩ ⊧ ¬◇B.
  12. Let E = ◻B and ⟨◻B,j⟩ ∈ ⋃ϕ. We have theoretically two cases: either (i) for none l ∈ ℕ expression jrl belongs to ⋃ϕ, or (ii) there exists such l ∈ ℕ that expression jrl belongs to ⋃ϕ. However, case (i) does not hold, because by rule Rr, expression jrj belongs to ⋃ϕ at least. In case (ii) we take set {ljrl ∈⋃ϕ}— by assumption, this set is non-empty. Since branch ϕ is maximal, by virtue of rule R for any m ∈ {ljrl ∈⋃ϕ} set ⋃ϕ contains expression ⟨B,m⟩. Whereas due to construction of model 𝔐S5 and (†), we know that ⟨W,R,V,m⟩ ⊧ B. Therefore, by definition of truth in model 4.7, we get that ⟨W,R,V,j⟩⊧◻B.
  13. Let E = ◇B and ⟨◇B,j⟩ ∈ ⋃ϕ. Since branch ϕ is maximal, due to rule R, there exists index l ∈ ℕ such that expressions ⟨B,l⟩ and jrl belong to ⋃ϕ. From the construction of model 𝔐S5 and (†), we know that lW, ⟨j,l⟩ ∈ R and ⟨W,R,V,l⟩ ⊧ B. Therefore, by definition of truth in model 4.7, we get ⟨W,R,V,j⟩⊧◇B.

Thus, we have proven that for any formula E and any index j, if ⟨E,j⟩ ∈ ⋃ϕ, then ⟨W,R,V,j⟩⊧E. Therefore, there exists such model 𝔐S5 that for any formula A, if AX, then 𝔐S5A since 𝔐S5 = ⟨W,R,V,i⟩.

The above concepts and facts allow us to demonstrate a partial relationship between the relation of semantic consequence and the relation of branch consequence in the tableau system for S5.

←126 | 127→

Lemma 4.59. For any XForS5, AForS5, if XA, then XA.

Proof. Take any X ⊆ ForS5 and A ∈ ForS5. Assume that XA. We must show that XA. From the assumption and definition of ⊳, 4.44, we know that there exists no such index i ∈ ℕ and such finite set YX that each maximal branch beginning with set {⟨B,i⟩ ∶ BY ∪ {¬A}} is closed. Therefore, for each index i ∈ ℕ and each finite set YX, there exists a maximal branch beginning with set {⟨B,i⟩ ∶ BY ∪{¬A}} which is open. By lemma 4.55, for some index i ∈ ℕ, there exists such closure Z of set of expressions Xi ={⟨B,i⟩ ∶ BX∪{¬A}} under tableau rules that Z is an open and maximal branch. Since Z = ⋃Z and {⟨B,i⟩ ∶ BX ∪{¬A}} ⊆ Z, from lemma 4.58, we know that there exists model 𝔐S5 such that 𝔐S5X ∪{¬A}. Hence, by definition of ⊧, 4.9, XA.

We will now proceed to the determination of relationship between the branch consequence relation and the existence of a closed tableau. However, this will require some introduction of another concepts.

Let us now define the concept of R-branch, that is such branch that originated by the application of rules exclusively from set RRS5, for some R.

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

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

Having established set R, the resultant branch will be then called R-branch.

Definition of R-branch differs from definition of branch 4.27 in the fact that the applied rules come from a subset of set of tableau rules RS5. In a special case when R = RS5, both definitions would be identical. But, since set R does not have to be identical with set RS5, so we have a conclusion.

Corollary 4.61. For any RRS5, each R-branch is a branch.

In a similar manner, we will define another auxiliary concept, namely the concept of quasi-maximal branch.

Definition 4.62 (Quasi-maximal branch). Let RRS5 and let ϕKP(TeS5) be a branch. We shall state that ϕ is a quasi-maximal branch iff it meets one of the below conditions:

←127 | 128→
  1. ϕ is closed
  2. for any rule RR, 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 (according to R) and Wϕ(j).

Having established set R, the resultant quasi-maximal branch will be called R-quasi-maximal branch.

The provided definition of quasi-maximal branch also resembles the definition of maximal branch 4.40, while in a special case, when R = RS5, both definitions would be identical. Again, the difference pertains to the reference to the set of rules which is some subset RRS5, so possibly proper subset of tableau rules. Since a maximal branch must be a sequence closed under all rules, so the relationship that occurs between the quasi-maximal branches and maximal branches is one-directional. That relationship is expressed by another conclusion which follows from the definition of maximal branch 4.40 and definition of quasi-maximal branch 4.62.

Corollary 4.63. Each maximal branch is R-quasi-maximal branch, for any RRS5.

The next conclusion is consequential for further considerations. It follows directly from the definition of quasi-maximal branch 4.62. In the proofs of further facts, the content of that conclusion shall be deemed self-evident.

Corollary 4.64. For any RRS5, each R-quasi-maximal branch is a branch.

Let us now introduce the definition of addition of branches.

Definition 4.65 (Addition of branches). Let ϕ ∶ {1, . . . ,n} → P(TeS5) and ψMP(TeS5) be branches, for some n ∈ℕ and M ⊆ℕ, and let ϕ(n) = ψ(1). The results of the operation ϕψ is function φKP(TeS5) defined as follows:

  1. if M= ℕ, then K =ℕ
  2. if ∣M∣ ∈ ℕ, then K = {1, . . . ,n,n+1,n+2, . . . ,n +∣M∣−1}
  3. for each iK

a. if 1 ≤ in, φ(i) = ϕ(i)

b. if i > n, then φ(i) = ψ((in)+1).

From definition of addition of branches 4.65, definition of tableau rules 4.23 and definition of branches 4.27, another conclusion follows.

Corollary 4.66. Let ϕ ∶ {1, . . . ,n}→ P(TeS5) and ψMP(TeS5) be branches, for some n ∈ℕ and M ⊆ℕ, and let ϕ(n) = ψ(1). Then ϕψ is also a branch.

←128 | 129→

Now, we have several facts concerning the relationship between the quasi-maximal branches and the finite sets of expressions.

Proposition 4.67. Let RCPL = {R, R, R, R, R¬¬, R¬∧, R¬∨, R¬→, R¬↔}. Let XTeS5 be a finite set of tableau expressions. Then, there exists a RCPL-quasi-maximal branch beginning with set X.

Proof. Take set of rules RCPL = {R, R, R, R, R¬¬, R¬∧, R¬∨, R¬→, R¬↔} and set of tableau expressions X ⊆ TeS5.

If set X is t-inconsistent, then — by definition 4.62 — one-element sequence ⟨X⟩ is a RCPL-quasi-maximal branch beginning with set X. Then, assume that X is not t-inconsistent.

Since X is a finite set, then ∗(X), that is a set of indices that appear in the expressions in set X (definition of function selecting indices 4.15), is also finite.

If ∗(X) is an empty set, because X = ∅, then — by definition 4.62 — one-element sequence ⟨X⟩ is a RCPL-quasi-maximal branch beginning with set X.

Assume that ∗(X) is a non-empty set. By quasi-modal formula we will mean each such formula A of logic S5 that A is different from each following formula◇B, ◻B, ¬◇B, ¬ ◻B, where B is a formula of S5. The set of all quasi-modal formulas will be denoted with symbol . We will divide set of propositional letters Var into two disjoint subsets Var1 and Var2 so that propositional letter x ∈ Var1 iff x = pi, for some i ∈ ℕ. From definitions of set Var it follows that both set Var1 and Var2 are infinite sets, plus their union equals to set Var.

Since set ForS5and set of propositional letters Var1 are infinite and countable sets, we can determine bijection ●∶ ForS5→ Var1 that assigns exactly one propositional letter to each formula which is not quasi-modal.

Now, for each index i ∈ ∗(X), we define set X i = {⟨A,i⟩ ∶ ⟨A,i⟩ ∈ X and A is a quasi-modal formula}. Set Xi contains all and only those expressions that belong to set of expressions X which constitute an ordered pair: some quasi-modal formula A, i.e., in terms of structure, formula corresponding to some formula of CPL, and index i. Since set X is finite, so for any i, set X i is also finite.

If for any i ∈ ∗(X), set X i is an empty set, then initial set X does not comprise any subset to which we could apply one of rules RCPL. Therefore—by definition 4.62 — one-element sequence ⟨X⟩ is a RCPL-quasi-maximal branch beginning with set X.

Assume that it is not the case that for any i ∈ ∗(X), set X i is an empty set. Now, note that set of rules RCPL includes analogons of tableau rules from the set of tableau rules for CPL — from set RCPL. In other words, rules for CPL“split” formulas into subformulas, and at the same time rules RCPL for the expressions ←129 | 130→constructed from quasi-modal formulas and index identically “split” formulas preserving the initial index in the new expression.

For rules RCPL, we have fact 2.34 stating that each finite set of formulas of the classical logic, that is non-modal formulas, is the first element of some such branch of a finite length ϕ that there does not exist super-branch ϕψ.

Now, for any formulas A, B and C, we will define substitution e ∶ ForS5 → ForS5 using the following conditions:

1. if A ∈ Var, then for any i ∈ ℕ:

a. if A = pi and i = 1, then e(A) = q1

b. if A = pi and i ≠ 1, then e(A) = qj, where j is the smallest odd number greater that index in e(pi−1)

c. if A = qi, then e(A) = qj, where j = i ⋅ 2

d. if A = ri, then e(A) = ri

2. if A = ¬B, A is a quasi-modal formula and there is no such formula D that BD, then e(A) = ¬e(B)

3. in the other cases:

a. if A=¬¬B, then e(A) = ¬¬e(B)

b. if A = (BC), then e(A) = (e(B)∧e(C))

c. if A = (BC), then e(A) = (e(B)∨e(C))

d. if A = (BC), then e(A) = (e(B)→ e(C))

e. if A = (BC), then e(A) = (e(B)↔e(C))

f. if A=◇B, then e(A) = ●(◇B)

g. if A=◻B, then e(A) = ●(◻B)

h. if A=¬◇B, then e(A) = ●(¬◇B)

i. if A=¬◻B, then e(A) = ●(¬◻B).

Note that for any formula A, its images under function e, i.e. e(A) is a formula of CPL, that is e(A) ∈ ForCPL. Let us define function e′ ∶ ForS5 → ForCPL with condition: for any formula A ∈ ForS5, e′(A) = e(A).

Due to the fact that function ● is a bijection and that function e is injective, function e′ is also a bijection. Hence, there exists inverse function e′−1 such that for any formula A ∈ ForS5, e′−1(e(A)) = A.

For any i ∈ ∗(X), we now define set Xi = {e(A) ∶ ⟨A,i⟩ ∈ Xi}.

Obviously, Xi is, by virtue of the construction of set Xi, a finite subset of formulas CPL. So, from the mentioned fact 2.34, it follows that there exists such a finite branch of length n beginning with set X i that it cannot be anymore extended using the tableau rules for tableau system for CPL:

(1)

←130 | 131→

Hence, there exists such finite RCPL-branch of length n, beginning with set Xi:

(2)

where for any 1 ≤ jn, = {⟨A,i⟩ ∶ Ae′−1, that it cannot be anymore extended using the tableau rules from set RCPL. If branch (2) was extendible by some of rules from set RCPL, also branch (1) would be extendible by an equivalent of that rule from set RCPL. But this would contradict fact 2.34.

Note that branch:

is 4.62 quasi-maximal as it was created using rules that belonged to set of rules RCPL and no rule from set of rules RCPL can be applied to set