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

3.3.3 Maximal branches

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.

Remark 3.24. We will repeat here in part the remark from the previous chapter. As we can see, the concept of branch depends on some set of tableau rules. In the case under consideration, the branch structure is based on the rules from set RTL. Further described complex tableau concepts will also depend on some sets of rules. Because in this chapter we are studying tableau system for TL based on rules from set RTL, so we are not going to make it any more complicated.

In practice, however, the tableau concepts of systems constructed according to the presented idea always base on some set of rules. In one of the subsequent chapters, at the general description of the construction way itself, the set of rules will be a variable. In this chapter it is specified as: RTL and the complex tableau concepts defined here depend on it. And since set RTL only includes such rules that constitute sets of ordered pairs, so in the definition of branch for TL we specified that it is about pairs, contrary to the definition of tableau system in the previous chapter, where in the definition of branch 2.20, we wrote about the existence of an appropriate n-tuple.

This remark applies to the rest of the study.

By definition of rule 3.18, through the fact that the rules are defined by proper containing of the input set in each of the output sets, in any n-tuple, there is a conclusion.

Corollary 3.25. Each branch is an injective sequence.

3.3.3Maximal branches

Among the branches constructed through applying the rules from set RTL, we will distinguish such branches to which no more rules from set RTL can be applied, expanding them into some super-branches. As we already know, such branches are called maximal branches. The definition of maximal branch is the same as in the previous chapter, except that of course the maximal branches here are branches for TL.

←80 | 81→

Definition 3.26 (Maximal branch). Let ϕKP(TeTL) be a branch. We shall state that ϕ is maximal iff

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

As in the case described in the previous chapter, definition 3.26 could be shortened to the second condition. This would not change anything with regard to the cases of finite sets, but we would allow cases of infinite branches that:

  • begin with an infinite set
  • meet the second condition of definition because they are infinite branches
  • do not, however, “resolve” all expressions.

The following example 3.27 illustrates a situation where without the first condition in the definition of maximal branch 3.26, we would consider a presented branch to be maximal. This branch would be infinite and, at the same time, would still contain expressions that were not used in the proof.

Example 3.27. Let us consider the following branch, beginning from set {P1iQ1} ∪ {PniQnn > 1}.

This branch is infinite, although rule Ri has never been applied to any of the sets in such a way as to draw conclusions from formula P1iQ1.

Thus, the definition of maximal branch 3.26 says that if sequence X1, . . . , Xn, for some n ≥ 1, is a branch, then we call it a maximal branch iff there does not exist branch X1, . . . , Xn, Xn+1.

Extending the concept of branch onto infinite sets is unnecessary in practice, because important concepts for our metatheory — the concept of branch consequence and tableau — we apply to cases of finite sets. At this stage of the book, the finite sets of tableau expressions do not begin the branch of infinite length.

However, the definition of maximal branch will change in the study. To the above concept of branch applicable are all reservations from note 2.32, concerning the maximal branch for the tableau system for CPL. Definition 3.26 is suitable for ←81 | 82→those tableau systems where only finite branches are obtained from finite sets of expressions. For other systems this definition is too narrow. It does not include cases of branches which, even though they begin with a finite set of expressions, are not finite.

In the following chapter, we will proceed to defining the system for modal logic, and we will generalize this definition. Hence, the above definition 3.26, and especially definition 2.20 will describe special cases of maximal branches which appear in the construction by the described method of such tableau systems as system for CPL or TL. Besides, also in the case of TL we will show that from finite sets of expressions we always get branches of finite length (fact 3.32).

3.3.4Closed and open branches

Among the maximal branches, the closed branches deserve special attention. In addition, set of open branches complements the set of closed branches. As we remember, intuitively a branch is closed when we get a t-inconsistent set having decomposed tableau expressions.

Definition 3.28 (Closed/open branch). Abranch ϕKP(TeTL) 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, the definition of tableau rules for TL 3.19 and the definition of branch 3.22 the following conclusion follows.

Corollary 3.29. If branch ϕKP(TeTL) 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. Therefore, from the definition of maximal 3.26 another conclusion follows.

Corollary 3.30. If branch fKP(TeTL) is closed, then it is maximal.

We are now going to show two facts that are needed for further proofs. The first one says that a branch that begins with a finite set of expressions is also finite in length, not greater than a certain number.

Proposition 3.31. Let X be a finite set of expressions. Let ϕKP(TeTL) be any such branch that ϕ(1) = X. Then, there exists number n ∈ℕ such thatK∣ ≤ n.

Proof. Take any finite set of expressions X and such branch ϕKP(TeTL) that ϕ(1) = X. We will carry out an inductive proof due to the cardinality of the first element of the branch.

←82 | 83→

Initial step. Assume that ∣X∣ = 1. We have six types of cases that can take place. There exist name letters P, Q ∈ Ln and index i ∈ ℕ such that one of the following cases occurs:

  1. P+iX, then, however, ∣K∣ = 1 ∈ ℕ, by definition of branch 3.22, since there does not exist such rule RRTL that would allow to extend branch ⟨X
  2. PiX, then, however, ∣K∣ = 1 ∈ ℕ, by definition of branch 3.22, since there does not exist such rule RRTL that would allow to extend branch ⟨X
  3. PaQX, then, however, ∣K∣ = 1 ∈ ℕ, by definition of branch 3.22, since there does not exist such rule RRTL that would allow to extend branch ⟨X
  4. PiQX, then, however, ∣K∣ ≤ 2 ∈ ℕ, by definition of branch 3.22, since there only exists one rule RRTL, rule Ri that allows to extend branch ⟨X⟩ with set Y = {PiQ,P+j,Q+j}, for some j ∈ℕ, whereas there does not exist such rule RRTL that would allow to extend branch ⟨X, Y
  5. PeQX, then, however, ∣K∣ = 1 ∈ ℕ, by definition of branch 3.22, since there does not exist such rule RRTL that would allow to extend branch ⟨X
  6. PoQX, then, however, ∣K∣ ≤ 2 ∈ ℕ, by definition of branch 3.22, since there only exists one rule RRTL, rule Ro that allows to extend branch ⟨X⟩ with set Y = {PiQ,P+j,Q+j}, for some j ∈ℕ, whereas there does not exist such rule RRTL that would allow to extend branch ⟨X, Y⟩.

Thus, when ∣X∣ = 1, then ∣K∣ ≤ 2. So, if ∣X∣ = 1, then there exists such number n ∈ℕ that ∣K∣ ≤ n.

Induction step. Assume that the theorem thesis holds for each such set of expressions Y that ∣Y∣ = m. Thus, for any branch ψMP(TeTL) such that ψ(1) = Y, there exists number l such that ∣M∣ ≤ l.

We will show that the theorem thesis also occurs for ∣X∣ = m+1. Take any set of expressions Y such that YX and ∣Y∣ = m. Thus, for any branch χNP(TeTL) such that χ(1) = Y there exists number l such that ∣N∣ ≤ l.

We have six types of cases that can take place. There exist name letters P, Q ∈ Ln and index i ∈ ℕ such that one of the following cases occurs:

  1. X =Y ∪{P+i}, then, however, ∣K∣ ≤ l+k ∈ℕ, where k is the number of propositions in form RaS and TeU that belong to set Y, by definition of branch 3.22, since set RTL contains rules Ra+ and Re which allow to extend each branch containing additional expression P+i at most with k elements
  2. X = Y ∪{Pi}, then, however, ∣K∣ ≤ l ∈ ℕ, by definition of branch 3.22, since set RTL does not comprise any rule which would allow to extend a branch containing additional expression Pi
  3. X =Y∪{PaQ}, then, however, ∣K∣ ≤ l+((k+1)⋅o)∈ℕ, where k is the number of propositions in form RaS and TeU that belong to set Y, while o is the number ←83 | 84→of particular propositions that belong to set Y and in the subject or predicate have name letter P, and expressions P+j, for some index j, by definition of branch 3.22, since set RTL contains rules Ra+ and Re which allow to extend each branch containing additional expression PaQ at most with (k+1)⋅o elements
  4. X = Y ∪ {PiQ}, then, however, ∣K∣ ≤ l + k + 1 ∈ ℕ, where k is the number of propositions in form RaS and TeU that belong to set Y, by definition of branch 3.22, since set RTL contains rules Ri, Ra+ and Re, which allow to extend each branch containing additional expression PiQ at most with k +1 elements
  5. X = Y ∪{PeQ}, then, however, ∣K∣ ≤ l + k ∈ ℕ, where k is the number of particular propositions that belong to set Y and in the subject or predicate have name letter P, and expressions P+j, for some index j, by definition of branch 3.22, since set RTL contains rule Re, which allows to extend each branch containing additional expression PeQ at most with k elements
  6. X = Y ∪{PoQ}, then, however, ∣K∣ ≤ l + k + 1 ∈ ℕ, where k is the number of propositions in form RaS and TeU that belong to set Y, by definition of branch 3.22, since set RTL contains rules Ro, Ra+ and Re,which allow to extend each branch containing additional expression PoQ at most with k +1 elements.

So, if ∣X∣ = m + 1, then there exists such number n ∈ ℕ that ∣K∣ ≤ n. Then, there exists such number n ∈ ℕ that ∣K∣ ≤ n.

The second fact says that for each finite set of expressions, there exists a maximal branch which begins with this set.

Proposition 3.32. Let XTeTL be a finite set of expressions. Then, there exists maximal branch ϕKP(TeTL) such that ϕ(1) = X.

Proof. Let X ⊆ TeTL be a finite set of expressions. Then, by fact 3.31, for each branch ϕKP(TeTL) such that ϕ(1)=X, there exists such number n ∈ℕ that ∣K∣ ≤ n.

Indirectly assume that no branch ϕ beginning with set X is a maximal branch. By an inductive proof through the branch length we will show that this assumption leads to a contradiction.

Initial step. We know there exists at least one branch. This is the branch that begins with set X and that a length of 1. However, by indirect assumption, it is not a maximal branch, so by definition of maximal branch 3.26, there exists a branch that begins with X, with length of 2.

Induction step. Now, let us take a branch beginning with X, of length m, and assume there exists a branch of length m +1 beginning with set X. Again, by indirect assumption, it is not a maximal branch, so by definition of maximal branch 3.26, there exists a branch that begins with X of length m +2.

←84 | 85→

Thus for any m ∈ ℕ, there exists a super-branch of length m +1 beginning with finite set of expressions X. This, however, contradicts the fact that for any branch beginning with set X there exists such number n ∈ ℕ that bounds the length of that branch.

3.3.5Relation of branch consequence

We will now define the concept of branch consequence using the concepts of branch, maximal branch and closed branch.

Definition 3.33 (Branch consequence of TL). Let X ⊆ ForTL and A ∈ ForTL. Formula A is a branch consequence of X (for short: XA) iff there exists such finite set YX that each maximal branch beginning with set Y ∪ {○(A)} is closed.

Denotation 3.34. For any set of formulas X and any formula A notation XA means that it is not the case that XA.

In the definition of branch consequence, we refer to the function specified by definition 3.12. Function ○ to each formula assigns a formula which contradicts it 3.13. The above concept of branch consequence differs from the analogous concept for CPL in the fact that (apart from defining on a different language — set of expressions) in the previous case negation was used, and here we use a contradictory formula. In fact, however, it can be assumed that in both cases the point is to start with a formula contradictory to the formula which could potentially be a branch consequence of a certain set of premises, but in the case of CPL a contradictory formula could be obtained directly by preceding the formula with a negation.

Also in the present case, we will refer to the example of the branch consequence occurrence.

Example 3.35. Let us consider an example — Barbara syllogism — premises {PaQ,QaR}, conclusion PaR5. We want to answer the question whether {PaQ,QaR} ⊳ PaR?

The first set of each branch we need to examine is set {PaQ,QaR,○(PaR)}, by definition of function ○, equal to set {PaQ, QaR, PoR}. On the left side, we put the branch elements, on the right side, we put the rules we use to transform the sets. There exists one type of maximal branches beginning with this last set:

1.{PaQ,QaR,PoR} ⊂Ro, where i ∈ ℕ
←85 | 86→2.{PaQ,QaR,PoR,P+i,Ri} ⊂Ra+
3.{PaQ,QaR,PoR,P+i,Ri,Q+i} ⊂Ra+
4.{PaQ,QaR,PoR,P+i,Ri,Q+i,R+i}t-inconsistency Ri,R+i

We said one type since i is any natural number. So, actually there exists an infinite number of branches beginning with set {PaQ,QaR,PoR}.6 The described branches are maximal ones because their last element is t-inconsistent as it contains expressions Ri, R+i, always for some i ∈ ℕ.

So we showed that all maximal branches beginning with set {PaQ,QaR, ○(PaR)} are closed. Thus {PaQ,QaR} ⊳ PaR.

The tableau concepts we have described for TL are very similar to their equivalents for CPL, despite the fact that we have dealt with a different language of proof and with indices.

3.4Tableaux for TL

As in the case of the tableau system for CPL, the practical examining of the branch consequence occurrence should boil down to building of an appropriate tableau.

Nevertheless, we are going to have a discussion on the definition of the concepts of tableau, complete tableau, closed/open tableau of a tableau system for TL. We will define all these concepts in two variants.

The first variant will make a direct reference to the fact that among the rules belonging to set RTL there are no rules that contain an ordered n-tuples longer than two, and as a consequence there never occur any branchings. The second variant of the concepts will be based on the relevant definitions already provided in the tableau system for CPL, however related to the set of branches of the tableau system for TL.

Although in each case the first definition variant will appear to be a special and simplified case of the second variant, in fact the two variants will prove to be equivalent, as we will demonstrate. In this way we will also show that the book considerations aim to describe certain general concepts for the tableau systems, independent of many specific properties of a given system, and thus to the general theory of tableau systems.

←86 | 87→

Therefore, the first variant of each definition will always be a specific version, defined according to the needs of the current system, while the second one will be a definition analogous to the one used in the previous chapter. As usual, we will start with the definition of tableau.

Definition 3.36 (Tableau — variant one). Let X ⊆ ForTL, A ∈ ForTL and Φ be a set of branches. Ordered triple ⟨X,A,Φ⟩ will be called a tableau forX,A⟩ (or for short tableau) iff Φ is an one-element subset of the set of branches beginning with set X ∪{○(A)} (i.e. if ϕ ∈ Φ, then ϕ(1) = X ∪{○(A)}).

Remark 3.37. According to the definition of tableau 3.36, a tableau for pair ⟨X,A⟩ is ordered triple ⟨X,A,Φ⟩ in which Φ is such an one-element set of branches that any branch in this set begins with set X ∪{○(A)}. This definition could be technically simplified.

Such simplification would consist in the fact that in an ordered triple, instead of set of branches Φ, we would simply place a branch belonging to set Φ.However, as we strive for a general theory of tableaux, so we use a general notation of a tableau as a triple in which we distinguish a set of premises, a potential conclusion and a set of branches that meet the conditions from the definition. The case of the system described in the present chapter is in terms of the number of branches—as we wrote at the beginning of the chapter — a borderline case, so we will not alter the convention for it.

Let us now define the concept of tableau for TL in a similar way the concept of tableau for CPL. Similar, since this definition is analogous to the corresponding definition for the tableau system for CPL. However, we cannot say that it is identical, because it pertains to the objects that were constructed from other sets, in spite of similarity of the same objects, i.e. branches. This definition uses—just like the definition of tableau 2.53 in the tableau system for CPL — the concept of maximal branch in the set of branches which we will adapt to the current situation. Here, the analogous remarks apply as in the case of definition 2.36 from Chapter Two — so we will not reiterate those here.

Definition 3.38 (Maximal branch in the set of branches). Let Φ be a set of branches and let branch ψ ∈ Φ. Branch ψ will be called maximal in Φ (or Φ–maximal) iff there is no such branch ϕ ∈Φ that ψϕ.

With the concept of maximal branch in the set of branches, we can proceed to the second variant of the tableau definition.

Definition 3.39 (Tableau — variant two). Let X ⊆ ForTL, A ∈ ForTL 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:

←87 | 88→
  1. Φ is a non-empty subset of set of branches beginning with X ∪{○(A)} (i.e. if ϕ ∈ Φ, then ϕ(1) = X ∪{○(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 RRTL 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.

The above tableau definition for TL seems too complex. It is not too broad because—as we will see—it does not cover setwise constructions that we would not consider as tableaux for the tableau system for TL. However, condition 3 of this definition seems to be overly expanded. Note the conclusion that follows from the definition of tableau in variant two and the definition of set of tableau rules RTL.

Corollary 3.40. LetX,A,Φ⟩ be a tableau in variant two 3.39. Then, set Φcontains precisely one branch.

Proof. Let ⟨X,A,Φ⟩ be a tableau. In the proof, we will make use of definition of tableau 3.39. Assume that set Φ contains two branches ϕ1 and ϕ2. Point 1. of the tableau definition implies that ϕ1(1) = ϕ2(1) = X ∪ {○(A)}. While point 2. and definition of maximal branch in the set of branches 3.38 imply that ϕ1ϕ2 and ϕ2ϕ1 since each branch in set Φ is Φ-maximal.

Now, take any such number i ∈ ℕ that for any oi, ϕ1(o) = ϕ2(o), plus i + 1 belong to domains of functions ϕ1 and ϕ2. From point 3. it follows that there exists such rule RRTL and such ordered m-tuple ⟨Y1, . . . ,Ym⟩∈ R, where 1 < m≤ 3 that for any 1 ≤ k ≤ 2:

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

And yet, since for each rule RRTL, for each ordered m-tuple ⟨Y1, . . . ,Ym⟩∈ R, where 1 <m≤ 3, m= 2, so ϕ1(i+1) = Yl = ϕ2(i+1). Hence ϕ1 = ϕ2.

This conclusion shows that the concept of tableau in the second variant for TL system could be simpler. Nonetheless, it is not too broad since both definitions of tableau for the tableau system for TL are equivalent, which gets proven by the below fact.

←88 | 89→

Proposition 3.41. Let XForTL, AForTL and Φ be a set of branches. ⟨X,A,Φ⟩ is a tableau in variant one 3.36 iffX,A,Φ⟩ is a tableau in variant two 3.39.

Proof. Let X ⊆ ForTL, A ∈ ForTL and Φ be a set of branches.

Assume that ⟨X,A,Φ⟩ is a tableau in variant one 3.36. In view of this definition, Φ is a non-empty subset of set of branches beginning with X ∪{○(A)} (i.e. if ϕ ∈ Φ, then ϕ(1) = X ∪{○(A)}), so the first condition from definition 3.39 is satisfied. Definiens of definition 3.36 also claims that Φ contains precisely one branch. So, each branch that belongs to Φ is Φ-maximal by virtue of definition 3.38,which is the second condition of definition 3.39. Finally, also the third condition of definition 3.39 is met as Φ contains precisely one branch ψ. Thus, ⟨X,A,Φ⟩ is a tableau in variant two.

Now, assume that ⟨X,A,Φ⟩ is a tableau in variant two 3.39. Due to the first condition of this definition, Φ is a non-empty subset of set of branches beginning with X ∪{○(A)} (i.e. if ϕ ∈ Φ, then ϕ(1) = X ∪{○(A)}). While due to conclusion 3.40, Φ contains precisely one branch. Thus, as per definition 3.36 ⟨X,A,Φ⟩ is a tableau in variant one.

Therefore, any of the definitions of tableau in the tableau system considered here can be adopted for TL, although due to the economy of phrasing, definition 3.36 seems better. Its scope covers exactly the same objects as in the definition of tableau that was created by applying analogies to the definition of tableau in the system for CPL.

We will now take up the issue of the complete tableau, also considering simpler and more complex variants, modelled on the system for CPL. Here is variant one.

Definition 3.42 (Complete tableau — variant one). Let triple ⟨X,A,Φ⟩ be a tableau. We shall state that ⟨X,A,Φ⟩ is complete iff a branch contained in Φ is maximal. A tableau is incomplete iff it is not complete.

In a complete tableau, a branch that belongs to it is maximal, so it cannot be extended. In variant two, which in a moment will be adapted to the context of TL, in a complete tableau all branches are maximal, not only those maximal ones in a given set. In addition, a complete tableau contains such set of branches that it is no longer possible to add any new branches to it, without causing the set to cease to be a tableau. More specifically, a complete tableau contains such set of maximal branches that any non-redundant superset of it ceases to co-create the tableau, similar to definition 2.60.

Consideration of the second variant, based on the tableau definition from the previous chapter, requires the introduction of an auxiliary definition, including the definition of a redundant superset.

←89 | 90→

Definition 3.43 (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 an redundant variant of branch ϕ iff:

  • there exists such rule RRTL and such pair ⟨X,Y⟩ ∈ R that X = ϕ(i) and Y = ϕ(i+1)
  • there exists such rule RRTL and such triple ⟨X,W,Z⟩ ∈ R that X = ϕ(i) and:
  • W = ϕ(i+1) and Z = ϕ′(i+1)

    or
  • Z = ϕ(i+1) and W = ϕ′(i+1).

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

However, in the case of our system, the concept of redundant variant of branch is empty. It is covered by another conclusion.

Corollary 3.44. For no branch ϕ there exists such branch ψ that ψ is a redundant variant of branch ϕ.

Proof. Let us consider any branch ϕ and indirectly assume that there exists such branch ψ that ψ is a redundant variant of branch ϕ. According to definition of redundant variant of branch 3.43, for some numbers i and i + 1 that belong to domains ϕ and ψ, it is the case that ϕ(i) = ψ(i), but ϕ(i+1) ≠ ψ(i+1), and there exists such rule RRTL and such triple ⟨X,Y,Z⟩ ∈ R that X = ϕ(i) and Y = ϕ(i+1), Z = ψ(i+1) or Y = ψ(i+1), Z = ϕ(i+1). However, this leads to a contradiction to the fact that there exists no rule RRTL to comprise any triple ⟨X,Y,Z⟩.

And since there exist no redundant variants of branches, there are neither redundant nor proper supersets of sets of branches, which is confirmed by another conclusion.

Corollary 3.45. Let Φ be a set of branches. There exists no set of branches Ψ such that Φ ⊂ Ψ and Ψ is a redundant superset of Φ.

Proof. Take any set of branches Φ and indirectly assume that there exists set of branches Ψ such that Φ⊂Ψ and Ψ is a redundant superset of Φ. Thus—according to definition of redundant variant of branch 3.43—for any branch ψ ∈Ψ∖Φ, there exists such branch ϕ ∈Φ that ψ is a redundant variant of ϕ. Since Φ⊂ Ψ, so there exists some branch ψ ∈ Ψ ∖ Φ. Assume that set Φ is non-empty. Consequently, there exists such branch ϕ ∈ Φ that some ψ is a redundant variant of ϕ, which contradicts the previous conclusion 3.44.

←90 | 91→

We have shown that both concepts — of a redundant variant of branch and a redundant superset, in the phrasing appropriate for our tableau system for TL, are empty. After considering the redundant variants of branches and redundant supersets of branches, we can proceed to the definition of complete tableau in variant two.

Definition 3.46 (Complete tableau — variant two). 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 it is not complete.

Let us note that, once again, the two variants of the concept are equivalent. This is covered by another fact.

Proposition 3.47. Let XForTL, AForTL and Φbe a set of branches. ⟨X,A,Φ⟩ is a complete tableau in variant one 3.36 iffX,A,Φ⟩ is a complete tableau in variant two 3.46.

Proof. Let X ⊆ ForTL, A ∈ ForTL and Φ be a set of branches.

Assume that ⟨X,A,Φ⟩ is a complete tableau in variant one 3.42. Since by virtue of the definition of tableau 3.36, set Φ contains precisely one branch and according to definition 3.42, that branch is maximal, so each branch contained in set Φ is maximal, which constitutes condition 1 of being a complete tableau in variant two of the definition of complete tableau 3.46. Let us now check if condition 2 of the definition in variant two holds. It claims that for any set of branches Ψ such that:

(a) Φ ⊂ Ψ

(b) ⟨X,A,Ψ⟩ is a tableau

Ψ is a redundant superset of Φ.

So, take any such set of branches Ψ that Φ ⊂ Ψ. However, by definition of tableau 3.36, triple ⟨X,A,Ψ⟩ is not a tableau since Ψ is a set of at least two elements, whereas in a tableau, a set of branches includes precisely one branch. Thus, condition 2 of the definition of complete tableau in variant two 3.46 is satisfied in the empty way.

←91 | 92→

Now, assume that ⟨X,A,Φ⟩ is a complete tableau in variant two 3.46.According to definition 3.46, each branch contained in Φ is maximal, and what is more, by virtue of definition of tableau 3.36, Φ contains precisely one branch. Thus, a branch contained in Φ is a maximal branch, and consequently, tableau ⟨X,A,Φ⟩ is complete according to the definition of complete tableau in variant one 3.42.

Evidently, both concepts of a redundant variant of branch and a redundant superset, and their conclusions for the tableau system for TL play no role whatsoever in the equivalence proof.

When constructing a complete tableau, we may face a situation where a branch not only becomes maximal, but also finishes with a t-inconsistent set. Such a tableau is called a closed tableau. Let us, again, consider two variants. Variant one to begin with.

Definition 3.48 (Closed/open tableau—variant one). Assume that ⟨X,A,Φ⟩ is a tableau. We shall state that ⟨X,A,Φ⟩ is closed iff a branch contained in Φ is closed. A tableau is open iff it is not closed.

Variant two, in turn, corresponding to the definition aiming at the general definition of a closed tableau, has the following form.

Definition 3.49 (Closed/open tableau—variant two). 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 it is not closed.

Proposition 3.50. Let XForTL, AForTL and Φ be a set of branches. ⟨X,A,Φ⟩ is a closed tableau in variant one 3.48 iffX,A,Φ⟩ is a closed tableau in variant two 3.49.

Proof. Let X ⊆ ForTL, A ∈ ForTL and Φ be a set of branches.

Assume that ⟨X,A,Φ⟩ is a closed tableau in variant one 3.48. Thus, in the light of the definition of complete tableau 3.42, ⟨X,A,Φ⟩ is a complete tableau—since branch which is contained in it is, by conclusion 3.30, maximal — which constitutes condition 1 of being a closed tableau in variant two of the definition of closed tableau 3.49. Since by virtue of the definition of tableau 3.36, set Φ contains precisely one branch and according to definition 3.48, that branch is closed, so each branch contained in set Φ is closed, which constitutes condition 2 of being a closed tableau in variant two of the definition of closed tableau 3.49.

←92 | 93→

Now, assume that ⟨X,A,Φ⟩ is a closed tableau in variant two 3.49. Thus, by condition 2 of definition 3.49, each branch contained in Φ is closed, and, what is more, by virtue of definition of tableau 3.36, Φ contains precisely one branch, which constitutes a condition of being a closed tableau in variant one of the definition of closed tableau 3.48.

To sum up, we have shown that specific tableau concepts of the tableau system for TL are special cases of more general concepts applied earlier (modulo set of tableau rules RTL and resulting sets of branches), and in the considered cases are equivalent to them.

By virtue of the definition of closed tableau and the definition of complete tableau, and conclusion 3.30, we get another conclusion.

Corollary 3.51. Each closed tableau is a complete tableau.

Further, we will show that the concept of tableau is significantly helpful in determining the occurrence of relation ⊳, while this concept, in terms of range, is equal to the concept of implication ⊧.

3.5Completeness theorem for the tableau system for TL

Let us begin with the definition of model generated by a branch.

Definition 3.52 (Model generated by branch). Let ϕ be any branch. We define the following function At(ϕ) =⋃ϕ∩(TeTL ∖ForTL).

We shall state that model 𝔐TL = ⟨D,d⟩ is generated by branch ϕ iff:

  • D = {x ∈ ℕ ∶ x ∈ ∗(At(ϕ))}
  • for any name latter P ∈ Ln, xd(P) iff P+xAt(ϕ).

From this definition, we get the following conclusion.

Corollary 3.53. Let ϕ be an open branch. Then, there exists a model generated by ϕ.

Proof. By definition of open branch 3.28, definition of model generated by branch 3.52 and definition of model 3.3.

Lemma 3.54 (On generation of model). Let ϕ be an open and maximal branch. Then, there exists model 𝔐TL generated by ϕ such that 𝔐TL ⊧⋃ϕForTL.

Proof. Take any open and maximal branch ϕ. Since branch ϕ is open, so by previous conclusion 3.53, there exists model 𝔐TL = ⟨D,d⟩ generated by ϕ.

←93 | 94→

We will now show that for any formula A contained in ⋃ϕ, it is the case that 𝔐TLA, i.e.𝔐TL ⊧⋃ϕ∩ForTL. The proof will be carried out with consideration of all the possible cases of construction of formula A. Now, assume that A ∈ ⋃ϕ. By definition of formula, for some name letters P, Q ∈ Ln, there must occur one of the following cases.

  1. A = PaQ. Take any object iD such that id(P). By definition of model generated 3.52, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ra+, ⋃ϕ also contains tableau expression Q+i. By definition of model generated 3.52, id(Q). Hence, d(P) ⊆ d(Q), and by definition of truth in model 3.4, we thus get that 𝔐TLPaQ. In turn, if there exists no such iD that id(P), then ∅=d(P) ⊆ d(Q), so by definition of truth in model 3.4, we get 𝔐TLPaQ.
  2. A= PiQ. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ri, set ⋃ϕ also contains tableau expressions P+i,Q+i, for some i ∈ℕ. By definition of model generated 3.52, id(P) and id(Q). Since d(P)∩d(Q) ≠∅, so by definition of truth in model 3.4, we get that 𝔐TLPiQ.
  3. A = PeQ. Take any object iD such that id(P). By definition of model generated 3.52, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule Re, ⋃ϕ also contains tableau expression Qi. Since branch ϕ is open, so expression Q+i ∉ ⋃ϕ, and consequently, by definition of model generated 3.52, id(Q). Thus, d(P)∩d(Q)=∅ and by definition of truth in model 3.4, we get 𝔐TLPeQ. In turn, if there exists no object iD such that id(P), then d(P)∩d(Q)=∅, so by definition of truth in model 3.4, we get that 𝔐TLPeQ.
  4. A = PoQ. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ro, set ⋃ϕ also contains tableau expressions P+i, Qi, for some i ∈ ℕ. By definition of model generated 3.52, id(P) and — since branch ϕ is open and, consequently, expression Q+i ∉⋃ϕid(Q), so d(P) ⊈ d(Q). Thus, by definition of truth in model 3.4, we get 𝔐TLPoQ.

We will now move on to a lemma which claims that application of tableau rules for the extension of branches does not reach beyond the model which is appropriate. In other words, according to the definition of model appropriate for the set of expressions 3.16, if we have a set of expressions such that the formulas contained in this set of expressions are true in given model and expressions stating inclusion or non-inclusion of a denotation of given index in the scope of name are interpretable in the model (they do not contradict the state of affairs in the ←94 | 95→model), then the extension of that set with the use of rules produces a set that still has the above properties.

Lemma 3.55. Let𝔐TL be any model,X, YTeTL, and let RRTL. Then, ifX,Y⟩∈ R and 𝔐TL is appropriate for set of expressions X, then 𝔐TL is appropriate for Y.

Proof. In the proof, wewillmake use of definition of model appropriate for the set of expressions 3.16. Let 𝔐TL = ⟨D,d⟩ be any model and X, Y ⊆ TeTL. We will consider all cases of rules RRTL, assuming that ⟨X,Y⟩ ∈ R and 𝔐TL is appropriate for set of expressions X, and showing that then 𝔐TL is appropriate for Y.

  1. Let R = Ra+, then ⟨X,Y⟩ = ⟨Z ∪{PaQ,P+i}, Z ∪{PaQ,P+i, Q+i}⟩, for some Z ⊆ TeTL, P, Q ∈ Ln and i ∈ℕ; since 𝔐TL is appropriate for set of expressions X, so by definition 3.16, 𝔐TLPaQ and there exists function γ ∶ℕ→ D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); due to the fact that P+iX, also γ(i) ∈ d(P), while since 𝔐TLPaQ, hence by definition of truth in model 3.4, γ(i) ∈ d(Q), since d(P) ⊆ d(Q); consequently, by definition of model appropriate for the set of expressions 3.16, model 𝔐TL is appropriate for set of expressions Y = Z∪{PaQ,P+i,Q+i}.
  2. Let R = Ri, then ⟨X,Y⟩ = ⟨Z∪{PiQ},Z∪{PiQ,P+i,Q+i}⟩, for some Z ⊆ TeTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐TL is appropriate for set of expressions X, so by definition 3.16,𝔐TLPiQ and there exists function γ ∶ℕ→ D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j)∈ d(S) and if SjX, then γ(j) ∉ d (S); however, rule Ri enriches set X with expressions P+i,Q+i and index i is new, it has not occurred in any expression from set X, while since 𝔐TLPiQ, so by virtue of definition of truth in model 3.4, in the domain there exists certain object x such that xd(P)∩d(Q); so we define function γ′ ∶ ℕ → D such that for any k ∈ ℕ, if ki, then γ′(k) = γ(k) and γ′(i) = x, consequently, by definition of model appropriate for the set of expressions 3.16, model 𝔐TL is appropriate for set of expressions Y = Z∪{PiQ,P+i,Q+i}.
  3. Let R = Re, then ⟨X,Y⟩ = ⟨Z ∪ {PeQ,P+i},Z ∪ {PeQ,P+i, Qi}⟩, for some Z ⊆ TeTL, P, Q ∈ Ln and i ∈ℕ; since 𝔐TL is appropriate for set of expressions X, so by definition 3.16, 𝔐TLPeQ and there exists function γ ∶ ℕ → D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); due to the fact that P+iX, also γ(i) ∈ d(P), while since 𝔐TLPeQ, hence by virtue of definition of truth in model 3.4 γ(i) ∉ d(Q), since d(P) ∩ d(Q) = ∅; consequently, by definition of model appropriate for the set of expressions 3.16, model 𝔐TL is appropriate for set of expressions Y = Z∪{PeQ,P+i,Qi}.
  4. ←95 | 96→ Let R =Ro, then ⟨X,Y⟩=⟨Z∪{PoQ},Z∪{PoQ,P+i,Qi}⟩, for some Z ⊆TeTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐TL is appropriate for set of expressions X, so by definition 3.16, 𝔐TLPoQ and there exists function γ ∶ ℕ → D such that for each name letter S ∈ Ln and each j ∈ ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); however, rule Ro enriches set X with expressions P+i,Qi and index i is new, it has not occurred in any expression from set X, while since 𝔐TLPoQ, so by virtue of definition of truth in model 3.4, in the domain there exists certain object x such that xd(P), but xd(Q); so we define function γ′ ∶ℕ→ D such that for any k ∈ℕ, if ki, then γ′(k) = γ(k) and γ′(i) = x, consequently, by definition of model appropriate for the set of expressions 3.16, model 𝔐TL is appropriate for set of expressions Y = Z∪ {PoQ,P+i,Qi}.