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

2.6 Summary

Further, we will show that the concept of tableau is significantly helpful in determining the occurrence of relation ⊳.

Now, we will focus on the fact that the initial, finite set of formulas allows to construct a complete tableau.

Proposition 2.65. Let X be a finite subset of set ForCPL and let AFor. Then, there exists at least one complete tableauX,A,Φ⟩.

Proof. Consider a set of all branches B(X∪{¬A}). We know that the set of maximal branches MB(X ∪ {¬A}) is non-empty (fact 2.37). In addition, for each branch ϕB(X ∪{¬A}) there exists branch ψMB(X ∪{¬A}) such that ϕψ, by 2.34.

Let us now define such set Φ ⊆MB(X∪{¬A}) that Φ is a maximal set among the sets that meet the following condition:

←59 | 60→

• for any n,i ∈ ℕ and any branches ϕ1, . . . , ϕn ∈ Φ, if:

i and i+1 belong to domains of functions ϕ1, . . . , ϕn

for any1< kn and any oi, ϕ1(o) = ϕk(o),

then there exists such rule RRCPL 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.

By definition of tableau 2.53, ⟨X,A,Φ⟩ is a tableau. What is more, since Φ is a maximal set among those meeting the given condition, then by the definition of complete tableau 2.60, ⟨X,A,Φ⟩ is a complete tableau. Since MB(X ∪ {¬A}) is non-empty, there exists at least one Φ that meets the given condition.

We will now move on to a lemma that defines the relationship between the existence of a closed tableau and complete tableaux.

Lemma 2.66. Let X be a finite subset of set ForCPL and AForCPL. Then, the following two statements are equivalent:

  1. there exists closed tableauX,A,Φ′⟩
  2. each complete tableauX,A,Φ′′⟩ is closed.

Proof. Take any finite subset X of set ForCPL and any formula A ∈ ForCPL.

First, we will take up the proof of implication (1)⇒(2). Indirectly assume that there exists closed tableau ⟨X,A,Φ′⟩ and not every complete tableau ⟨X,A,Φ′′⟩ is closed. Hence, there exists complete tableau ⟨X,A,Φ′′⟩ which is not closed. By definition of open tableau 2.61, ⟨X,A,Φ′′⟩ is an open tableau. And since ⟨X,A,Φ′′⟩ is a complete tableau, then each branch contained in Φ′′ is maximal. Hence, there exists branch ψ ∈ Φ′′ such that:

  1. ψ begins with X ∪{¬A}
  2. ψ is a maximal branch
  3. ψ is an open branch.

Since ψ is an open branch, then by definition of open branch 2.38, there is no such formula A that A and ¬A belong to the union of all the elements of branch ⋃ψ

Note that since branch ψ is maximal and open, then it is also closed under tableau rules in this regard that for any RRCPL and any n-tuple ⟨X1, . . . ,Xn⟩∈ R, where n > 1, if X1 ⊆ ⋃ψ, then for some 1 < jn, Xj ⊆ ⋃ψ. For if that was not the case, there would exist rule RRCPL and such n-tuple ⟨X1, . . . ,Xn⟩ ∈ R, where n > 1, that X1 ⊆ ⋃ψ, but for none 1 < jn, Xj ⊈ ⋃ψ. And it would mean that branch ψ ←60 | 61→is not maximal, because ⋃ψ is identical to the last element of open and maximal branch ψ, by definition of branch 2.20.

We assumed that there existed closed tableau ⟨X,A,Φ′⟩. By virtue of conclusion 2.64, ⟨X,A,Φ′⟩ is a complete tableau. Hence, each branch contained in Φ′ is maximal and Φ′ contains all such branches without which ordered triple ⟨X,A,Φ′⟩ would not be a complete tableau. Let us adopt designation X ∪{¬A} = Y1.

We will carry out an inductive proof with respect to n-th elements of branches contained in Φ′, showing that they enable construction of an infinite branch beginning with set Y1.

Initial step. Consider the first element of each branch contained in Φ′. It is set Y1. Since Y1 ⊆⋃ψ, and ψ is an open branch, then there must exist a rule RRCPL such that ⟨Y1,Z1, . . . ,Zn⟩∈ R, where n ≥ 1, and — since ⟨X,A,Φ′⟩ is a complete tableau — for each 1 ≤ jn there exists a branch in Φ′ such that it contains Zj. Since branch ψ is also closed under tableau rules, then certain Zj ⊆ ⋃ψ. So, Φ′ includes such branch that its first element is Y1, and second Y2 = Zj, and Y2 ⊆⋃ψ

Induction step. Assume that set Φ′ includes such branch that its first n elements Y1, . . . , Yn are contained in set ⋃ψ. Since Yn ⊆ ⋃ψ, and ψ is an open branch, then there must exist a rule RRCPL such that ⟨Yn,Z1, . . . ,Zk⟩∈ R, where k ≥ 1, and — since ⟨X,A,Φ′⟩ is a complete tableau — for each 1 ≤ jk there exists a branch in Φ′ such that it contains Zj. Since branch ψ is also closed under tableau rules, then certain Zj ⊆⋃ψ. So, Φ′ includes such branch that its first n +1 elements Y1, . . . , Yn,Yn+1 are contained in set ⋃ψ.

So, for each branch in Φ′, the first element equals Y1 and Y1 ⊆ ⋃ψ and for each n ∈ ℕ if there exists in Φ′ such branch that its first n elements Y1, . . . , Yn are contained in set ⋃ψ, then also in Φ′ there exists such branch that its first n elements equal Y1, . . . , Yn, and its n +1-element Yn+1 is contained in set ⋃ψ.

Now, we take all elements Yi, where i ∈ ℕ and we put them in increasing sequence Y1, Y2, Y3, . . . .This sequence is a branch, because for any Yj there exists a rule RRCPL such that ⟨Yj,Z1, . . . ,Zk⟩∈ R, where k ≥ 1, and Yj+1 = Zl, for some 1 ≤ lk.

There exists therefore an infinitely long branch Y1, . . . , Yn, . . . such that Y1 = X∪{¬A}. But, since set X∪{¬A}, by assumption, is finite, then it contradicts fact 2.28.

Let us now move on to the proof of implication (2)⇒(1). Assume that each complete tableau ⟨X,A,Φ′′⟩ is closed. From fact 2.65, we know that for finite set of formulas X there exists at least one complete tableau ⟨X,A,Φ⟩. Therefore, there exists closed tableau ⟨X,A,Φ′⟩.

←61 | 62→

We will now consider the relationship between complete and closed tableaux and the occurrence of branch consequence relation.

Lemma 2.67 (On relation between complete tableaux and branch consequence). Let XForCPL and AForCPL. Then, the two below statements are equivalent:

  1. there exists such finite set YX that each complete tableauY,A,Φ⟩ is closed
  2. XA.

Proof. The proof of the above equivalence is based on the definition of the notion tableau 2.60, notion of a closed tableau 2.61 and notion of a relation of branch consequence ⊳.

Take X ⊆ ForCPL and A ∈ ForCPL, and assume there exists such finite set YX that each complete tableau ⟨Y,A,Φ⟩ is closed. Therefore, each maximal branch that begins with set Y ∪{¬A} is closed. So, there exists such finite set YX that each maximal branch that begins with set Y ∪{¬A} is closed. Hence, XA.

On the other hand, if XA, then there exists such finite set YX that each maximal branch that begins with set Y ∪{¬A} is closed. Hence, there exists such finite set YX that each complete tableau ⟨Y,A,Φ⟩ is closed.

We now proceed to the most important theorem of this subchapter. The occurrence of this theorem, or at least of its part “from the left to the right,” may be a criterion for the correctness of tableau system construction. When constructing a tableau emerging from a given set of formulas, we can usually do it in many ways. In practice, however, we construct one tableau, checking whether each branch ends with a contradictory set. Usually we also assume that it is sufficient to state that given formula belongs to the set of correct conclusions from the initial set of formulas.

Intuitively, however, it seems doubtful. Why should one closed tableau be a proof if it is potentially possible to construct more tableaux? After all, usually, we have to rule out all cases in indirect proofs, and this is what the construction of a tableau is. Another theorem removes this doubt by saying that in order to determine the occurrence of relation of branch consequence, it is sufficient to construct one closed tableaux.

Theorem 2.68 (Theorem on the tableau arbitrariness). Let XForCPL and AForCPL. Then, the two below statements are equivalent:

  1. 1. there exists finite set YX and closed tableauY,A,Φ⟩

2. XA.

←62 | 63→

Proof. Take any X ⊆ ForCPL and A ∈ ForCPL and assume there exists such finite set YX and closed tableau ⟨Y,A,Φ⟩. By virtue of lemma 2.66, we get the conclusion that there exists such finite set YX that each complete tableau ⟨Y,A,Φ′⟩ is closed. And from the above, and from lemma 2.67, it follows that XA.

Now, assume that XA. By virtue of lemma 2.67, there exists such finite set YX that each complete tableau ⟨Y,A,Φ′⟩ is closed. So, from lemma 2.66, it follows that there exists finite set YX and closed tableau ⟨Y,A,Φ⟩.

The construction of one closed tableau which begins with a finite subset of set of premises X and negation of formula A is, therefore, equivalent to the fact that XA. Because previously, through the theorems on soudness and completeness, we proved that relations ⊧ and ⊳ are identical, i.e. they define the same set of pairs, now we can put in words the semantic form of the theorem on the tableau arbitrariness.

Theorem 2.69 (Theorem on the tableau arbitrariness—semantic form). Let XForCPL and AForCPL. Then, the two below statements are equivalent:

1. there exists finite set YX and closed tableauY,A,Φ⟩

2. XA.

This theorem says that the logical relation occurs between the premises and conclusion if and only if it is possible to select a finite set of premises, and then by attaching to it the negation of conclusion, construct a closed tableau emerging from that set.

2.6Summary

In this chapter we presented a theory for the construction of a tableau system for CPL, using the method of defining tableau rules as rules that extend sets.

For the purposes of presentation, we separately showed the relationships between the semantic consequence relation, the branch consequence relation and the existence of a closed tableau, proving the theorems on the equivalence of these concepts. In practice, however, it is easier to prove a theorem equivalent to the conjunction of the above theorems, i.e. the following theorem.

Theorem 2.70 (Theorem on the completeness of tableau system of CPL). For any XForCPL, AForCPL, the below statements are equivalent.

  • XA
  • XA
  • there exists finite YX and closed tableauY,A,Φ⟩.
←63 | 64→

Although this theorem is equivalent to the conjunction of earlier theorems—as we can see—its demonstration requires a proof of three implications. Certain proof transitions may therefore be omitted.

Theorem 2.70, was named a theorem on the completeness of tableau system of CPL, referring to the usual name to define the relationship between the semantic characteristics of given logic and its deductive definition. Often, when speaking on the completeness of a given deductive system, we mean not only a one-way relationship, but a relationship occurring two ways, that is, both soundness and completeness in the strict sense.

In the presentation of other tableau systems constructed using the presented method, we will always strive to demonstrate that there occurs a relevant theorem on the completeness of the tableau system, formulated in an analogous way as theorem 2.70. The proof of such theorem will be a positive criterion for the good formulation of the tableau system.


1 In the chapter we develop the approach that appeared for the first time in an English-language article [6]. In that study, both the concepts of tableau rules and the branches arising from the application of the rules were defined in a rather complicated way. In the meantime, these concepts have been simplified, so we present them here in an improved version. Of course, these changes affect the construction of the entire system.

2 See e.g. Priest G., [23], p. 5-6.

3 The property of rule that the first set is contained properly in every subsequent set seems to correspond well to the name proposed in the literature expansion rule (p. 60, [4]).