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

5.4.1 Branches

Definition 5.33 (Tableau rules). Let R be a set of rules. We shall state that R is a set of tableau rules iff

  1. R is a finite set
  2. for any X ⊆ Te, if X is a finite set, then for any rule RRX, each set RX is a finite set.
←167 | 168→

So, set of tableau rules R must include a finite number of rules, and what is more, for any finite set of expressions, each of rules R that belong to R can be applied a finite number of times — taking account of the set of n-tuples that belong to RX.

Remark 5.34. We adopt any, but fixed set of tableau rules R. That set will remain unchanged until the end of this chapter. It is worth noting again that all further tableau concepts: branches and tableaux of different types will depend on set R.

5.4.1Branches

Conventionally, another concept in our theory that will be discussed is the concept of branch. It is a concept that depends on the notion of the tableau rule because branches are created by applying rules. Branches — as mentioned before—are setwise objects consisting of sets. The below definition corresponds to all the definitions of branch used so far, only that it depends on the general notion of set of tableau rules R.

Definition 5.35 (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(Te) 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 some 1 < kn.

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

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

Denotation 5.36. From now on—when speaking of the branches constructed by the application of rules from set R—for the sake of convenience, we will use the following notations or denotations:

  1. X1, . . . ,Xn, where n ≥ 1
  2. X1, . . . ,Xn⟩, where n ≥ 1
  3. abbreviations: ϕM (where M is a domain ϕ, i.e. ϕMP(Te))
  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.

←168 | 169→

All the so far considered branches have been specific cases of the above concept, assuming an appropriate set of rules R.

Let us now introduce the general definition of addition of branches.

Definition 5.37 (Addition of branches). Let ϕ ∶ {1, . . . , n}→ P(Te) and ψMP(Te) be branches, for some n ∈ℕ andM ⊆ ℕ, and let ϕ(n) = ψ(1). The results of the operation ϕψ is function φKP(Te) 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 branch 5.35 and definition of addition of branches 5.37, follows an analogous conclusion as in the case of the tableau system for logic S5.

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

5.4.2Closed and open branches

An important classification of branches is the division into closed and open branches. A branch is closed when, applying the rules in subsequent steps, we have reached a t-inconsistent set. Below, we present the definition which is directly based on set of tableau rules R, as it refers to definition of branch 5.35.

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

From the above definition 5.39, definition of tableau rules 5.33 and definition of branch 5.35, the following conclusion results.

Corollary 5.40. If branch ϕKP(Te) is closed, thenK∣ ∈ ℕ.

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

5.4.3Maximal branches

One more important concept in the construction of a tableau system is the concept of a maximal branch. The definition of maximal branch is based on the ←169 | 170→concept of strong similarity. As we already know from the previous chapter, the concept of strong similarity of sets of expressions is a special case of the similarity of sets. Below, we provide its version that is generalized to the context of rules from set R.

Definition 5.41 (Strong similarity). Let rule RR and let ⟨X1, . . . ,Xn⟩∈ R, for some n ∈ ℕ. On any set of expressions W ⊆ Te 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⟩, the following conditions are satisfied:

a. for certain W′ ⊆W, Y1W

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

Having adopted the concept of strong similarity, we can proceed to the concept of maximal branch in the general version, also referred to set of tableau rules R.

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

  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 ⊆ Te that for some 1 < in, W is strongly similar to Xi and Wϕ(j).

Remark 5.43. We will repeat here the remark from the previous chapter. According to the above definition, a maximal branch is closed or, in a sense, closed under effect 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. Set W is to be contained in one of the elements of branch ϕ(j), and not necessarily be identical to it, since we applied the rule to set ϕ(j−1), which can be a proper superset of set X, and consequently we obtained more expressions, and what is more, those elements could have been obtained as a result of application of another rule.

Maximal branches as defined by the definition 5.42 can be either finite or infinite. There occurs an analogous case here as in the considerations on logic S5: if the branch is finite and there does not exist super-branch, then it is also a maximal branch.

←170 | 171→

Corollary 5.44. If branch ϕ is finite in length, and there does not exist such branch ψ that ϕψ, then ϕ is a maximal branch.

Proof. Take any branch ϕ which is finite and there does not exist such branch ψ that ϕψ. Now, assume that ϕ is not closed. If it does not meet the second conditions of definition 5.44, then since ϕ is finite, so there exists branch ψ such that ϕψ, which obviously contradicts the assumption.

So we have a general definition of maximal branch, which includes both finite cases — especially in systems that feature the finite branch property, and infinite cases, such as those that occur, for example, in modal logics.

The described concepts, therefore, apply to systems in which, by building a tableau proof using tableau tools and looking for maximal branches, we may be dealing with infinite branches. This is the case when a branch cannot be closed or certain rule application sequences are repeated.

From definitions 5.39 and 5.42 we get the following conclusion again.

Corollary 5.45. Each closed branch is maximal.

5.4.4Branch consequence relation

We will now move on to the general concept of branch consequence which we will define using the following concepts: branch, maximal branch, closed branch, and denotation 5.19.

Definition 5.46 (Branch consequence). Let X ⊆ For and A ∈ For. We shall state that A is branch consequence of X (for short: XA) iff there exists such finite set YX and such index i ∈ ℕ that each maximal branch beginning with set Yi ∪ {f(A)i} is closed. By XA, we mean that A is not branch consequence X.

The general concept of branch consequence relation corresponds to the so far defined concepts of branch consequence relation, taking account of remark 5.18.This remark is valid for all tableau concepts defined hereafter. So, when constructing a branch or tableau for some set of formulas X ∪{A}, we begin with set Xi∪{f(A)i}, for some index i ∈ ℕ.

5.5Tableaux

In this subchapter, we will move on to the general definition of tableau and various variants of tableaux. However, we will start with an auxiliary concept of maximality in set of branches which we already have used in the previous chapters.

←171 | 172→

Definition 5.47 (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 general concept of tableau.

Definition 5.48 (Tableau). Let X ⊆ For, A∈ For a Φ 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 set X i ∪{f(A)i}, for some index i ∈ ℕ (i.e. if ψ ∈ Φ, then ψ(1) = X i ∪{f(A)i})
  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 RR and such ordered m-tuple ⟨Y1, . . . , Ym ⟩∈ R, where 1 < m, that for any 1 ≤ kn:

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

The above concept of tableau covers all notions of tableau considered so far in a book, with a properly defined set of tableau rules R.

When considering the tableaux in general, we can also generalize the concept of redundant branch which is useful for the definition of complete tableau.

Definition 5.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 RR and such n-tuple ⟨X1, . . . ,Xn⟩∈ R that ϕ(i)=X1 and ϕ(i+1) = Xj, for certain 1 < jn

• there exists rule RR and such m-tuple ⟨Y1, . . . ,Ym⟩ ∈ R, where m > n, that X1 = ψ(i) = Y1 and:

1. ψ(i+1) = Yk, for certain 1 < km

2. for any 1 < ln there exists such 1 < om that ok and Xl = Yo.

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 ϕ.

Making use of the general concept of redundant superset of branches we can define the general concept of complete tableau.

←172 | 173→

Definition 5.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 Φ.

A tableau is incomplete iff the tableau is not complete.

Now we can define the general concept of closed and open tableaux.

Definition 5.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.

A tableau is open iff the tableau is not closed.

By virtue of the above definitions of closed tableau and complete tableau, we get a conclusion which makes up a generalization of the analogous conclusions from the preceding chapters.

Corollary 5.52. Each closed tableau is a complete tableau.

5.6Completeness theorem

In this chapter, we will define several general concepts and establish facts that will allow us to prove a claim from which we can deduce the theorem on completeness for the tableau system that meets the conditions given below.

In the first place, we will address the concepts used to demonstrate the relationship between relation ⊧ and ⊳. We will begin with the definition of branch generating interpretation.

Definition 5.53 (Branch generating interpretation). Let Φ be a set of all open and maximal branches that contain some tableau equivalents of formulas and let ℑ be an interpretation of formulas. We shall state that branch ϕ ∈ Φ generates interpretation ℑ iff there exists such function ≽∶ Φ → I that ≽ (ϕ) = ℑ.

Remark 5.54. The general definition of generating interpretation of formulas by branch is purely auxiliary and redundant in nature. For it is difficult to generally establish a definition of function ≽.However, in the case of specific logics or whole ←173 | 174→classes of logics, this concept takes on a very specific meaning — we can then describe the transition from the open and maximal branch to the construction of interpretation. We will present this issue in the next chapter, describing examples of application.

Another important concept is the concept of set of interpretations good for rules.

Definition 5.55 (Interpretations good for rules). Let

  • R be a set of tableau rules
  • ϕ be an open and maximal branch
  • X i ⊆⋃ ϕ, for some non-empty X ⊆ For and some i ∈ ℕ
  • I be a set of interpretations of formulas.

We shall state that set I is good for set of rules R iff branch ϕ generates such interpretation ℑ that:

  • ℑ ∈ I
  • ℑ ⊧ X.

We will now define the general concept of closure under rules.

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

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

On set Y we will also state that is a closure.

For any set of expressions, there exists at least one closure, at times there may exist more closures.

Using the above concept of closure, we can move on to the verbalization and proof of the following lemma.

Lemma 5.57 (On the existence of open and maximal branch). Let XFor and i ∈ ℕ. If for each finite YX, there exists a maximal and open branch beginning with Yi, then there exists a closure of set X i under rules R which is an open and maximal branch.

Proof. Take any X ⊆ For, i ∈ ℕ, and assume that (∗) for each finite YX there exists an open and maximal branch beginning with set Yi.

Next, we specify the set of all maximal and open branches that begin with set Yi, for some finite YX —we will denote that set as X.

←174 | 175→

We define set X, through the following conditions:

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

There exists at least one set X such that XX. We take one of such sets X and denote it as X.

Consider set ⋃{ϕ(1) ∶ ϕX}. Note that (∗∗) X i ⊆ ⋃{ϕ(1) ∶ ϕX}. For when Xi ⊈ ⋃{ϕ(1) ∶ ϕX}, there would exist such xXi that x ∉ ⋃{ϕ(1) ∶ ϕX} and, consequently, for any such branch ψX that xψ(1), ψ(1) ⊆ X i and ψ(1) is a finite set, it would be the case that ψX. Then, however, for some finite set YiXi there would exist no maximal and open branch beginning with set Yi∪{x} which would contradict assumption (∗).

We define the condition that specifies new set

Uiff there exists such branch ϕ that ϕX and U =⋃ ϕ

Now, we can define set Z =⋃

We claim that Z is a closure of set X i under tableau rules R (definition 5.56), and that Z is an open and maximal branch.

First, we will show that Z is a closure of set Xi, thus that it meets conditions of definition of closure 5.56.

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

Now, take any rule RR and any n-tuple ⟨U1, . . . , Un⟩ ∈ R, for some n ∈ ℕ, and assume that X iU1Z. From definition 5.33, it follows that there exists such n-tuple R that:

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

Consequently, assuming thatwe must show that for certain 1<ln,since U1 = Ul. Since Z and is a finite set, thus there exists a finite number of such branches ϕ1,ϕ2, . . . , ϕo in set X that for certain k ∈ ℕ, ϕ1(k)∪ ϕ2(k)∪⋅ ⋅ ⋅∪ϕo(k). So, set X contains such branch ψ that ψ(1) = ϕ1(1)∪ ϕ2(1)∪ ⋅ ⋅ ⋅∪ϕo(1) and U'1ψ(m), for certain m ∈ ℕ, and since ϕ1(k)∪ϕ2(k)∪⋅ ⋅ ⋅∪ϕo(k) is a t-consistent set, so set X contains such maximal branch ψ′ that—by definition 5.42 — for certain 1 < ln, ⊆ ⋃ ψ′. Finally, Z, since by construction Z, ⋃ψZ.

←175 | 176→

We will now move on to showing that Z is an open and maximal branch.

From the definition of branch—5.35 —it follows that Z is a branch.

Whereas by construction of Z, Z is an open branch, i.e. no subset Z is t-inconsistent, by definition X.

Let us now check if Z is a maximal branch. According to definition 5.42, we assume that there exists such rule RR and such n-tuple ⟨X1, . . . ,Xn⟩ ∈ R, for some n ∈ ℕ that X1 = Z. By definition of tableau rules 5.33 (Existence if core) and (Closure under subsets), there exists such n-tuple R that for any 1 < jn, and Since Z is a closure for certain 1 < jn, by definition 5.56.Therefore, XjZ, since Xj = X1But then X1Xj, which by definition 5.33 is out of the question. Consequently, there exists no such tableau rule R and n-tuple ⟨X1,. . . ,Xn⟩ ∈ R that X1 = Z, for some n ∈ ℕ. Therefore, Z is a maximal branch, by definition 5.42.

Now, we will verbalize and prove a fact that is needed to demonstrate the relationship between relation ⊳ and the existence of a closed tableau.

Proposition 5.58. Let XTe. If X is a finite set, then there exists such maximal branch ϕ that ϕ(1) = X.

Proof. Take any subset X ⊆ Te. The set of all branches beginning with set of expressions X will be denoted as X. Set X is non-empty as by definition of branch 5.35, such mapping ψ ∶ {1} → P(Te) that ψ(1) = X, is a branch.

We have two options: (1) there exists a closed branch in set X, or (2) there does not exist any closed branch in set X.

If case (1) occurs, then by definition of maximal branch 5.42, there exists such maximal branch ϕ that ϕ(1) = X.

Assume that case (1) does not occur.

Let Y ⊆ Te be any finite set of expressions. By definition 5.33, the number of tableau rules that belong to set RY is finite and different from zero. Now, assume there is j of them, for some j ∈ ℕ. We assign to each number from range 1 ≤ ij exactly one of rules that belong to set RY, to obtain the sequence of all rules from set RY: R1, . . . , Rj.

By definition of tableau rules 5.33, for each rule R iRY, there exists a finite number of n-tuples ⟨Y,X1, . . . ,Xn−1⟩ in set Therefore, each set where R iRY, is finite — contains at most k of ordered n-tuples, for some k ≥ 1. We take account of some sets one for each RiRY.

We assign to each number from range 1 ≤ ik exactly one n-tuple from set and denote given n-tuple as ri to obtain the sequence of all n-tuples from set r1, . . . , rk.

←176 | 177→

Consequently, in any there exists a finite number of ordered n-tuples ⟨Y,X1, . . . ,Xn−1⟩ that we can arrange in sequence: for certain k ≥ 1.

Next, we define a list of all n-tuples from each imposing a kind of lexicographical order on that list:

where 1 ≤ m,n, . . . ,o.

Such defined list of ordered n-tuples from set of expressions Y will be called Y-list and denoted as LY. Of course, there may exist multiple Y-lists. Still, there exists at least one Y-list that can be empty.

Let LY be Y-list and let riLY. We know that riRkYRk, for some kj. Let ri = ⟨X1, . . . ,Xn⟩. We shall state that ordered n-tuple ⟨Z1, . . . ,Zn⟩ is an expansion of ri iff:

• ⟨Z1, . . . , Zn⟩∈ Rk

• for each 1 ≤ ln the following conditions are satisfied:

1. XlZl.

2. Xl is a set that is similar to X1 ∪(ZlZ1).

If ⟨Z1, . . . ,Zn⟩ is the considered expansion ri, instead of ⟨Z1, . . . , Zn⟩ we will write

(∗) From definition of rules 5.29 (Closure under expansion), (Existence of core of rule), we know that for any ri = ⟨X1, . . . ,Xn⟩ that belongs to rule R and for any t-consistent set of expressions Z1, such that X1Z1 and for each 1 < in, X i is not similar to any subset Z1 that contains X1, there exists such rjR that rj is an expansion of ri, where rj = ⟨Z1, . . . ,Zn⟩, for some Z2, . . .Zn ⊆ Te.

Let LY be certain Y-list. By induction we define the closure of set Y under LY. LY(Y) is a maximally long sequence of sets of expressions Z1, . . . ,Zo, such that for some o ∈ ℕ and for any 1 ≤ no:

  1. if n = 1, then Zn = Y
  2. if n = 2, then Zn = Xj, where:

a. r1 is the first n-tuple in LY

b. r1 = ⟨Y,X1, . . . ,Xn⟩, for n ≥ 1

c. Xj = X1

3. if n > 2, then

a. Zn−1 belongs to sequence LY(Y)

b. Zn−1 is a consequence of expansion of certain m-tuple rlLY applied to Zn−2, thus for m ≥ 1, and Zn−1 = W1 and Zn = Xj, where:

←177 | 178→

a. there exists rl+m, for some m ≥ 1, and it is the first element after rl in LY such that:

b. is an expansion of rl+m

c. = ⟨Zn−1,X1, . . . ,Xi⟩, for i ≥ 1

d. Xj = X1.

By definition of branch 5.35, each closure LY(Y) ∶=Z1, . . . ,Zn, for some n ∈ ℕ, is a branch.

Now, let us investigate the initial set of expressions X. By virtue of the previous findings, we conclude:

  • X is a finite set, so we have such branch X) ∶= X1, . . . ,Xk, for some X-list and some k ∈ℕ that:
  • Xk is a finite set of expressions as set of tableau rules R is closed under finite sets 5.29 (Closure under finite sets).

Let us investigate a sequence of closures under some number of lists Lj — where j ∈ ℕ — and assume that the last set from the last closure Xo is a finite set:

for some k ≥ 1, where k ∈ ℕ
for some lk, where k ∈ ℕ
(Xl+m) = Xl+m, . . . ,Xnfor some n and m ∈ ℕ, where
nl+m
(Xn) = Xn, . . . ,Xofor some on, where o ∈ ℕ.

Since set of expressions Xo is finite, so we can define another branch ∶= Xo, . . . ,Xr, for some Xo-list and certain r ∈ ℕ such that:

  1. by definition of addition of branches 5.37 and conclusion on addition of branches 5.38, (((. . . ⊕. . .) ⊕ (Xl+m)) ⊕ (Xn))⊕(Xo) is a branch.
  2. Xr is a finite set of expressions as set of tableau rules R is closed under finite sets by definition of tableau rules 5.29 (Closure under finite sets).

Consequently, for any j ∈ ℕ there exists such branch (Xm) that (Xl) = Xl, . . . ,Xm, (X) = X1, . . . ,Xk, and for some k ≤ ⋅ ⋅⋅ ≤ lm∈ℕ, X1Xk ⊆ ⋅ ⋅⋅ ⊆ XlXm. We can extract all those branches:

←178 | 179→

After removal of all duplicates of elements, we get a branch — let us call it χ — which begins with initial set X. We claim that branch χ is a maximal branch. There exist two options:

  1. branch χ is finite in length
  2. branch χ is infinite.

If the first option occurs, then from the construction of branch χ we know that there does not exist super-branch χ. And from conclusion 5.44 we deduce that branch χ is maximal.

Assume that the second case occurs — so branch χ is infinite in length. Let us investigate if χ is a maximal branch. Taking account of definition of maximal branch 5.42, assume that there exists such tableau rule RR and such sets of expressions Y1, . . . Yn ⊆ Te, for some 1 < n ∈ ℕ, that:

  • Y1, . . . ,Yn⟩ ∈ R
  • for some 1 ≤ i, Xi = Y1 and Xiχ.

We must demonstrate that there exists such index j ∈ ℕ that for certain 1 < kn, some subset W of element of branch Xjχ is strongly similar to set Yk.

From the construction of branch χ we know that for some k ≥ 1 and mi.

By definition of tableau rules 5.33 and construction of branch χ two cases are possible:

(a) i =m and

(b) i >m and there exist:

  1. some l ∈ℕ, where m < l
  2. subsequent sequence (Xl) and

Assume the first case, meaning i =m and By virtue of construction of branch χ we have three options:

  1. Xi+1 = Yk, for some 1 < kn
  2. there exist: n-tuple ⟨W1, . . . , Wn⟩ ∈ R which is an expansion of the initial n-tuple ⟨Y1, . . . ,Yn⟩, and such element of branch χ Xi+o = W1, for some o ≥ 1 that Xi+o+1 =Wk and additionally certain subset Wk is strongly similar to set of expressions Yk, for some 1 < kn
  3. ←179 | 180→ there exist: set of expressions Xi+oχ, for some o ≥ 1, and such rule that certain ordered n-tuple ⟨Xi+o−1, Y2, . . . , Yn⟩∈ R′, for some n ∈ ℕ, Xi+o = for some 1 < n1n, and certain subset Xi+o is strongly similar to Yk, for some 1 < kn.

Case (b) consists of similar options, only that we consider such expansion of n-tuple ⟨Y1, . . . ,Yn⟩ ∈ R that the first set of that expansion contains set Xl.

Therefore, χ is a maximal branch.

We still need a few additional concepts for the proof of the theorem on completeness. We will utilize them for demonstration of relationship between the existence of closed tableau an relation ⊧.

Now, we will define a successive concept relevant for the general theorem on completeness.

Definition 5.59 (Rules good for interpretations). We shall state that set of rules R is good for set of interpretations I iff for any sets X1, . . . ,Xi ⊆ Te (where 1 < i), any interpretation ℑ ∈ I and any rule RR, if:

  • X1, . . . ,Xi⟩∈ R
  • ℑ is appropriate for X1,

then ℑ is appropriate for Xj, for some 1 < ji.

We will use the above definition 5.59 for the proof of another lemma, assuming the property it defines. This lemma determines the relationship between the finite sets of formulas and the existence of maximal and open branches.

Lemma 5.60. Let XFor be a finite set of formulas, i ∈ ℕ and let ℑ ∈ I be an interpretation of formulas. If set of rules R is good for set of interpretations I and ℑ ⊧ X, then there exists a maximal and open branch beginning with set {AiAX}.

Proof. Take any finite set of formulas X ⊆ For, any index i ∈ ℕ and any interpretation of formulas ℑ, and then assume that set of rules R is good for set of interpretations I and ℑ ⊧ X. We define the following set {AiAX}. Set {AiAX} will be denoted as Xi.

Since ℑ ⊧ X, so from definition of relation ⊩i 5.25 it follows that ℑ ⊩ X. Moreover, by definition of tableau expressions 5.15, set X is t-consistent.

Consequently, due to definition 5.28, interpretation ℑ is appropriate for set X i.

Now, indirectly assume that each maximal branch beginning with set X i is closed.

As Φ(Xi) we will denote the set of all maximal branches beginning with set Xi. From fact 5.58,we know that for each finite set of tableau expressions Y there exists a maximal branch beginning with set Y. Thus, set Φ(Xi) is non-empty.

←180 | 181→

Since set Φ(Xi) is a set of all maximal branches beginning with set Xi, so it has the following property.

Now, assume that for some branch χ ∈ Φ(Xi). Let for certain n ∈ ℕ exist such rule RR and such m-tuple ⟨Z1, . . . ,Zm⟩ ∈ R that χ(n) = Z1 and χ(n+1) = Zj, for some 1 < jm.

Note that each set Zj is a finite set of expressions since each rule expands the finite input set to the finite output set (by definition of tableau rules 5.29 (Closure under finite sets)), branch χ begins with finite set Xi, and we investigate its n-th element. Thus, from fact 5.58 we know that:

• for each set Zj there exists maximal branch ϕj beginning with set X i such that ϕi(n+1) = Zj.

(∗) Consequently, set Φ(Xi) contains such branches χ, ϕ2, . . . , ϕm that χ = ϕj, for some 1 < jm.

Thus for any n ∈ ℕ, if there exist: such rule RR, such m-tuple ⟨Z1, . . . ,Zm⟩∈ R, and branch χ ∈ Φ(Xi) such that χ(n) = Z1 and χ(n + 1) = Zj, then there exists branch ψ ∈ Φ(Xi) such that ψ(n+1) = Zj and for any kn +1, χ(k) = ψ(k).

(∗∗) By assumption, each branch that belongs to set Φ(Xi) is closed, thus by virtue of fact 5.40, each branch that belongs to set Φ(Xi) has a finite length of m, for some m ∈ ℕ.

From the initial assumption, we know that each of branches in set Φ(Xi) begins with set Xi.

Since interpretation ℑ is appropriate for set of expressions Xi, so due to the definition of interpretation appropriate for set of expressions 5.28, set X i is not t-inconsistent. Hence, we get a conclusion that there are no branches of length one in set Φ(Xi).

Due to the assumption that set of rules R is good for set of interpretations I and definition 5.59, for any rule RR and any l-tuple ⟨Z1, . . .Zl⟩∈ R, if interpretation of formulas ℑ is appropriate for set Z1, then it is also appropriate for some set Zj, where 1 < jl, and by virtue of(∗), there exists branch χ ∈ Φ(Xi) such that interpretation of formulas ℑ is appropriate for set χ(2) and χ(1) = Xi.

The set of those branches that belong to Φ(Xi), and simultaneously interpretation of formulas ℑ is appropriate for their k-th element, will be denoted as Φ(Xi)k.

So, we have Φ(Xi) = Φ(Xi)1 ⊇ Φ(Xi)2 ≠∅.

Now, assume that for some n ∈ ℕ, where n > 1, set Φ(Xi)n−1 ⊇ Φ(Xi)n ≠ ∅. Since set Φ(Xi)n is non-empty, so take some branch ψ ∈ Φ(Xi)n.

←181 | 182→

By assumption, interpretation of formulas ℑ is appropriate for set of expressions ψ(n), so due to the definition of interpretation appropriate for set of expressions 5.28, set ψ(n) is not t-inconsistent.

Due to the assumption that set of rules R is good for set of interpretations I and definition 5.59 which claims that for any rule RR and any l-tuple ⟨Z1, . . .Zl⟩∈ R, if interpretation of formulas ℑ is appropriate for set Z1, then it is also appropriate for some set Zj, where 1 < jl, and (∗), there exists branch ϕ ∈Φ(Xi)n+1 such that interpretation ℑ is appropriate for set ϕ(n + 1) and ϕ ∈ Φ(Xi)n. Thus, Φ(Xi)n ⊇ Φ(Xi)n+1 and Φ(Xi)n+1 ≠∅.