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.3.4 Closed and open branches

For other systems, including modal logics, the definition is too narrow, because it does not include cases of branches that are not finite even though they start with a finite set of expressions.

We have now deliberately adopted definition 2.30, as sufficient for CPL. When we move on to defining the system for modal logic, we will generalize this definition. So it is going to describe special cases of infinite maximal branches which appear in the construction of tableau systems using the described method.

Extending the concept of branch onto infinite sets is problematic for many reasons, and what is more, it is unnecessary in practice, because important and sufficient concepts for our metatheory — the concept of branch consequences and tableau—we apply in practice to cases of finite sets.

←44 | 45→

Besides, we showed that a finite sets of expressions, using the rules from set of rules RCPL we get branches of finite length (conclusion 2.29), so for the case of CPL the definition of maximal branch 2.30 is good enough.

The definition of maximal branch 2.30 in practice says that branch X1, . . . , Xn, for some n ≥ 1, we shall call maximal iff there is no branch X1, . . . , Xn, Xn+1.

In the subsequent fact, we state that each finite set of formulas is the first element of some maximal branch.

Proposition 2.33. Let X be a finite set of formulas. Then, there exists such maximal branch X1, . . . ,Xn that X1 =X and n≥ 1.

Proof. Take any finite set of formulas X, and then indirectly assume that there is no maximal branch X1, . . . ,Xn, where X1 = X and n ≥ 1.

However, by definition of branch 2.20 we know that there exists at least one branch that starts with set X, i.e. ⟨X1⟩, where X1 = X. From the indirect assumption and from the definition of maximal branch 2.30 it follows, however, that ⟨X1⟩ is not a maximal branch and it has some super-branch, so by definition of branch 2.20 there is some branch: X1,X2.

Let us now consider branch X1, . . . , Xm m long, for some m ∈ ℕ. From the indirect assumption and from the definition of maximal branch 2.30 it follows, however, that X1, . . . , Xm is not a maximal branch and it has some super-branch, so by definition of branch 2.20 there is some branch: X1, . . . , Xm, Xm+1.

So, from the indirect assumption and from the definition of maximal branch 2.30 results in a conclusion that (†) for any n ∈ ℕ there exists branch X1, . . . , Xn, Xn+1 such that X1 = X and n ≥ 1.

Let Φ be such a minimal set of branches that:

  1. X1⟩∈ Φ
  2. if ⟨X1, . . . ,Xn⟩∈ Φ, then ⟨X1, . . . ,Xn,Xn+1⟩ ∈ Φ, for any n ∈ ℕ.

Since Φ is a minimal set that meets conditions 1 and 2, then from(†) it follows that for any n ∈ℕ, there exists precisely one branch ⟨X1, . . . ,Xn⟩∈ Φ, where X1 = X.

Ki will now denote a domain of such branch ϕK contained in Φ that ∣K∣ = i ∈ℕ. From the above considerations it follows that for each i ∈ ℕ there exists precisely one set Ki that constitutes a domain of some branch which belongs to Φ. Then let K =⋃{KiϕK ∈ Φ}. Since 1 ∈ K and n+1 ∈ K, if nK, so K =ℕ.

Let us now define sequence ψKP(ForCPL) such that for any iK: ψ(i)= From the definition of branch 2.20, that sequence is an infinite branch beginning with a finite set of formulas X1 = X, which contradicts conclusion 2.29.

Using the above fact, we can prove another fact important for our theory.

←45 | 46→

Proposition 2.34. If X is a finite set of formulas, then for each branch Y1, . . . , Yn such that Y1 = X and n≥ 1, there exists maximal branch Z1, . . . , Zn, . . . , Zn+m, where for any in Yi = Zi and m≥ 0.

Proof. Let X be a finite set of formulas. Now, take any branch Y1, . . . .,Yn such that Y1 = X and n ≥ 1. From the definition of branch 2.20 and definition of tableau rules for CPL 2.13, we know that Yn is a finite set. So, due to the last fact 2.33, for some m ≥ 0 there exists such maximal branch that = Yn, hence by virtue of definition of branch 2.20 there also exists maximal branch Z1, . . . , Zn, . . . , Zn+m, where for any in Yi = Zi and m ≥ 0.

This fact tells us that any branch beginning with a finite set of formulas can be extended to the maximal branch in which it is included as a sequence.

For further consideration, the concept of branch which is maximal in a given set of branches, will be useful.

Definition 2.35 (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 ψϕ. Having some set of formulas X, B(X) will denote the set of all branches X1, . . . ,Xn such that X1 = X and n ≥ 1, while MB (X) will denote the set of all maximal branches in B(X).

Remark 2.36. The above concept of a maximal branch in a certain set of branches could be a starting point instead of the concept described in the definition of maximal branch 2.30. The latter is its special case in a situation when set Φ is identical to set B(X), for some finite set of formulas X, considering fact 2.33.

However, we deliberately separated these concepts, because in one of the subsequent chapters we will change the definition of maximal branch in such a way that its scope will not be identical to the scope of definition 2.35 in relation to finite sets. This new concept of a maximal branch will also include cases where branches can be infinitely long, even though they start with a finite set of expressions. So, consequently, it can be the case that for a given branch ϕ there is no such branch ψ that ϕψ, and yet ϕ it will not be considered maximal for other reasons. Although we will continue to use the concept of a maximal branch in a given set, we will eventually extend the concept of a maximal branch.

Corollary 2.37. Let X be a finite set of formulas. Then B(X) contains a non-empty subset MB(X).

Proof. Take any finite set of formulas X. Due to fact 2.34, there exists maximal branch ψ beginning with X. Of course, branchψ belongs to MB(X), so set MB(X) is non-empty. Since each branch contained in MB(X) belongs to B(X), so nonempty set MB(X) is contained in B(X).

←46 | 47→

2.3.4Closed and open branches

Another concept important for the tableau theory is the concept of a closed branch and an open branch. Intuitively, a branch is closed when we have reached a t-inconsistency set by decomposing formulas.

Definition 2.38 (Closed/open branch). Branch ϕKP(ForCPL) 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 CPL 2.13 and the definition of branch 2.20, the following conclusion follows.

Corollary 2.39. If branch ϕKP(ForCPL) is closed, thenK∣ ∈ ℕ.

Proof. Let branch ϕKP(ForCPL) be closed. From the definition of closed branch 2.38 we know that there exists such iK that ϕ(i) is a t-inconsistent set. From the definition of tableau rules for CPL it follows that there is no branch element ϕ(i+1), since the rules do not contain n-tuples with t-inconsistent input sets, hence none of the rules can be applied to set ϕ(i). So, from the definition of branch 2.20 we get: K = {1,2,3, . . . i}, which means that ∣K∣ ∈ ℕ.

In the case of a closed branch, the t-inconsistent element of sequence is therefore the last element. It is so because no more rule can be applied for branch extensions, because the tableau rules are defined in such a way that they cannot be applied to t-inconsistent sets. Therefore, from the definition of maximal branch 2.30 another conclusion follows.

Corollary 2.40. If branch ϕKP(ForCPL) is closed, then it is maximal.

2.3.5Branch consequence relation

We will now proceed to the metalogical concept which occurs in each of the systems defined in the book. This concept seems to be a novelty, seemingly so far not defined in the studies on tableau systems.

As we wrote, the tableau method is treated and defined in the book in a purely syntactic manner, i.e. as a method of transforming the notations of a given language in order to answer the question whether the considered inference is correct.

A concept that corresponds to this question is the concept of branch consequence relation, specified with another definition.

Definition 2.41 (Branch consequence relation of CPL). Let X ⊆ ForCPL and A ∈ ForCPL. We shall state that Ais a branch consequence of X (or short: XA) iff there←47 | 48→exists such finite set YX that each maximal branch beginning with Y ∪ {¬A} is closed. Relation ⊳ will be called branch consequence relation of CPL.

Remark 2.42. When considering different branch consequence relations in the following chapters, we will not use separate denotations for them. In a given context, we will only examine one relation, so there will be no risk of mistake.

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

In order to explain what is meant by definition 2.41, we will refer to an example.

Example 2.44. Let us consider the following example of occurrence of the relation of branch consequence. Take set {p} and formula (pq). Relation {p} ⊳ (pq) occurs since each maximal branch in the form X1 ={p,¬(pq)}, . . . ,Xn is closed. In fact, there is only one maximal branch in this form. It is branch: X1 ={p,¬(pq)}, X2 = {p,¬(pq),¬pq}, which originates through rule R¬∨. It is closed because pX2 and ¬pX2.

The above example shows the mechanism of the relation of branch consequence. It is based on the impossibility of finding a branch that would be both maximal and open. However, this example is somewhat misleading. We deliberately chose a set of formulas and a formula so that the branches beginning with this set and negation of the formula are neither too long nor too many. In practice, none of these features may actualize and most often they do not.

2.4Relations of semantic consequence and branch consequence

Before we proceed to the issue of how to reduce as much as possible the number of branches, which suffice to consider to show the occurrence of the relation of branch consequence, we will first show that the concept of the branch consequence relation defines the same set of objects as the concept of the semantic consequence relation — it is thus the branch, syntactic counterpart of the semantic consequence relation.

2.4.1Soundness theorem

In this subchapter, we will show that the relation of branch consequence is contained in the relation of semantic consequence, hence for any set of formulas X and any formula A it is the case that if XA, then XA.

We will use abbreviations concerning the valuations of the formulas adopted in denotation 2.5.

←48 | 49→

We will start with a lemma that tells us about the relationship between valuations of formulas and tableau rules.

Lemma 2.45. Let X be a set of formulas and V be any valuation such that V(X)=1. For any rule RRCPL:

  • ifX,Y⟩ ∈ R, then V(Y) = 1
  • ifX,Y,Z⟩ ∈ R, then V(Y) = 1 or V(Z) = 1.

Proof. We carry out the proof by checking the rules one by one. We will use the definition of valuation of CPL formulas, 2.4.

Take any set of formulas X and any valuation V such that V(X) = 1. Take any rule R from set RCPL. If set X is an input set of some ntuple contained in R, there must exist: certain set of formulas X′ and formulas A, B such that there occurs at least on of the below cases.

  • X = X′ ∪{(AB)}, V(X′ ∪{(AB)}) = 1, R = R and ⟨X′ ∪{(AB)},X′ ∪ {(AB),A,B}⟩ ∈ R. Since V((AB)) = 1, so V(A) = V(B) = 1.Thus V(X′ ∪ {(AB),A,B}) = 1.
  • X = X′ ∪{(AB)}, V(X′ ∪{(AB)}) = 1, R = R and ⟨X′ ∪{(AB)},X′ ∪ {(AB),A},X′ ∪ {(AB),B}⟩ ∈ R. Since V((AB)) = 1, so V(A) = 1 or V(B) = 1. Thus V(X′ ∪{(AB),A}) = 1 or V(X′ ∪{(AB),A}) = 1.
  • X = X′ ∪{(AB)}, V(X′∪{(AB)}) = 1, R = R and ⟨X′ ∪{(AB)},X′ ∪ {(AB),¬A},X′ ∪{(AB),B}⟩ ∈ R. Since V((AB)) = 1, so V(A) = 0 or V(B) = 1. Hence VA) = 1 or V(B) = 1.Thus V(X′ ∪{(AB),¬A}) = 1 or V(X′ ∪{(AB),B}) = 1.
  • X =X′∪{(AB)}, V(X′∪{(AB)}) = 1, R =R and ⟨X′∪{(AB)},X′∪ {(AB),A,B},X′ ∪ {(AB),¬AB}⟩ ∈ R. Since V((AB)) = 1, so V(A) = V(B). Hence V(A) = V(B) = 1 or V(A) = V(B) = 0. Thus V(A) = V(B) = 1 or VA) = VB) = 1. Consequently V(X′ ∪{(AB),A,B}) = 1 or V(X′ ∪{(AB),¬AB}) = 1.
  • X = X′ ∪ {¬¬A}, V(X′ ∪ {¬¬A}) = 1, R = R¬¬ and ⟨X′ ∪ {¬¬A},X′ ∪ {¬¬A,A}⟩ ∈ R¬¬. Since V(¬¬A) = 1, so VA) = 0, and V(A) = 1. Thus V(X′ ∪{¬¬A,A}) = 1.
  • X = X′ ∪ {¬(AB)}, V(X′ ∪ {¬(AB)}) = 1, R = R¬∧ and ⟨X′ ∪ {¬(AB)},X′ ∪{¬(AB),¬A},X′ ∪{¬(AB),¬B}⟩ ∈ R¬∧. Since V(¬(AB)) = 1, so V((AB)) = 0. Hence V(A) =0 or V(B) = 0, and consequently VA) = 1 or VB) = 1.Thus V(X′ ∪{(AB),¬A}) = 1 or V(X′ ∪{(AB),¬B}) = 1.
  • X = X′ ∪ {¬(AB)}, V(X′ ∪ {¬(AB)}) = 1, R = R¬∨ and ⟨X′ ∪ {¬(AB)},X′∪{¬(AB),¬AB}⟩ ∈ R¬∨. Since V(¬(AB)) = 1, so V((AB)) = 0, thus V(A) = V(B) = 0, and consequently VA) = VB) = 1. Thus V(X′ ∪ {¬(AB),¬AB}) = 1.
  • ←49 | 50→ X = X′ ∪{¬(AB)}, V(X′ ∪{¬(AB)}) = 1, R = R¬→ and ⟨X′ ∪{¬(AB)},X′∪{¬(AB),AB}⟩ ∈ R¬→. Since V(¬(AB)) = 1, so V((AB)) = 0, so V(A) = 1 and V(B) = 0. Thus V(A) = 1 and VB) = 1. Consequently V(X′ ∪{¬(AB),AB}) = 1.
  • X = X′ ∪{¬(AB)}, V(X′ ∪{¬(AB)}) = 1, R = R¬↔ and ⟨X′ ∪{¬(AB)},X′∪{¬(AB),¬A,B},X′∪{¬(AB),AB}⟩ ∈ R¬↔. Since V(¬(AB)) = 1, so V(A) ≠V(B). Hence V(A)=0 and V(B)=1 or V(A)=1 and V(B)= 0.Thus VA)=V(B)=1 or V(A)=VB)=1. Consequently, V(X′∪{(AB),¬A,B}) = 1 or V(X′ ∪{(AB),AB}) = 1.

Another lemma describes the relationship between finite, non-contradictory sets of formulas and the branches that originate from them. In this lemma we state that for a finite and non-contradictory set of formulas there is always at least one branch, beginning with this set, which is open and maximal.

Lemma 2.46 (On the existence of maximal and open branch). Let X be a finite set of formulas, and V be a valuation. If V(X) = 1, then there exists at least one maximal and open branch X1, . . . ,Xn such that X1 = X and n ≥ 1.

Proof. Take any finite set of formulas X and valuation V such that V(X)=1. Based on conclusion 2.37, we know that set of all maximal branches MB(X) is nonempty. Indirectly assume that none of the branches contained in MB(X) is open.

Now, consider the branches beginning with set X, taking accounts of their lengths. Through inductive proof, we will show that for any n ∈ ℕ there exists such open branch X1, . . . , Xn that X1 = X and there exists such set of formulas Y that sequence X1, . . . , Xn, Xn+1, where Xn+1 = Y, is also an open branch.

Initial step. There exists an open branch with the length of 1 beginning with set X. It is branch X1 = X. Since V(X) = 1, by definition 2.9, set X is not contradictory, while by virtue of conclusion 2.11, set X is not t-inconsistent. So, by definition of open branch 2.38 branch X1 is open. Hence, by virtue of the indirect assumption, X1 is not a maximal branch. Thus, by definition of maximal branch 2.30 and lemma 2.45, there exists branch X1,X2 such that V(X2) = 1. By definition 2.9, set X2 is not contradictory, while by virtue of conclusion 2.11, set X2 is not t-inconsistent. So, by definition of open branch 2.38, branch X1,X2 is open.

Induction step. Assume that for some n ∈ℕ, there exists such open branch X1, . . . , Xn that X1 = X, V(Xn) = 1 and n ≥ 2. Hence, by the indirect assumption, X1, . . . , Xn is not a maximal branch.

Since V(Xn)=1, by definition 2.9, set Xn is not contradictory, while by virtue of conclusion 2.11, set Xn is not t-inconsistent. Thus, by definition of maximal branch ←50 | 51→2.30and lemma 2.45, there exists branch X1, . . . , Xn, Xn+1 such that V(Xn+1) = 1. By definition 2.9, set Xn+1 is not contradictory, while by virtue of conclusion 2.11, set Xn+1 is not t-inconsistent. So, by definition of open branch 2.38, branch X1, . . . , Xn, Xn+1 is open.

Consequently, for any n ∈ ℕ, there exists such open branch X1, . . . , Xn that X1 = X and there exists such set of formulas Y that sequence X1, . . . , Xn, Xn+1, where Xn+1 = Y, is also an open branch and is not a maximal branch.

From this it follows that there exists an infinite branch Y1, Y2, . . . such that

  1. Y1 = X
  2. Yn+1 = Xn+1, where Xn+1 is such set that sequence X1, . . . , Xn, Xn+1, is also an open branch.

But, since X is a finite set of formulas, so the fact of existence of infinite branch Y1, Y2, . . . contradicts fact 2.28. So, the indirect assumption that each branch contained in MB(X) is closed, is false. So there exists a branch beginning with X, which is maximal and open.

With a lemma on the existence of maximal and open branch, we can now prove the soundness theorem.

Theorem 2.47 (Soundness).ForanyXForCPL,AForCPL, if XA, then XA.

Proof. Take any X ⊆ ForCPL, A ∈ ForCPL and assume that XA. So by definition 2.6 there exists such valuation V that V(X ∪{¬A}) = 1. Hence for any finite set YX, V(Y ∪{¬A}) = 1. From the previous lemma 2.46 it follows that for any finite Y ∪{¬A} there exists at least one maximal and open branch X1, . . . ,Xn such that X1 = Y ∪{¬A} i n ≥ 1. So there is no such finite set ZX that each maximal branch beginning with Z ∪{¬A} is closed. Hence by definition 2.41 XA.

2.4.2Completeness theorem

In this section, we will show that the relation of semantic consequence is contained in the relation of branch consequence, hence for any set of formulas X and any formula A it is the case that if XA, then XA.

Also here, we will use abbreviations concerning the valuations of the formulas adopted in denotation 2.5.

In our proofs, we will use the fact that the classical consequence relation ⊧ is compact. However, let us first recall the general definition of compactness of a binary relation, because the concept of a compact relation will be useful in the next chapter.

←51 | 52→

Definition 2.48 (Compact relation). Take any set of objects X and binary relation R, specified as follows RP(XX. We shall state that relation R is compact iff for any YX and for any xX: YRx ⇔there exists a finite set Y′ such that Y′ ⊆ Y and YRx.

The well-known fact of the compactness of semantic consequence relation of CPL is expressed in the next fact.

Proposition 2.49 (Compactness). For any XForCPL, AForCPL, XA iff there exists such finite set YX that YA.

We will start with a lemma which says about the relationship between the valuation of propositional letters and the negation of propositional letters in a maximal branch and the valuation of formulas from some initial set.

Lemma 2.50. Let X1, . . ., Xn, for some n ≥ 1, be a maximal and open branch. Let L(Xn) = {xXnx = y or x = ¬y, for some yVar}. Then for any valuation V, if V(L(Xn)) = 1, then V(Xn) = 1.

Proof. We will carry out an inductive proof, taking account of the complexity of formulas in a branch.

Take any maximal and open branch X1, . . . , Xn, for some n ≥ 1, and valuation V such that V(L(Xn)) = 1, where L(Xn)={xXnx = y or xy, for some y ∈ Var}. Let AXn.

Initial step. If A= y or Ay, for some y ∈ Var, then V(A)=1, since AL(Xn).

Induction step. Assume that for all formulas B, CXn that have the lesser complexity than A, V(B)=V(C)=1.Our proofwill be based on possible cases of constructing formula A and on the initial assumption that X1, . . . , Xn is a maximal branch. Since the branch is maximal, so if A could be decomposed by some of the tableau rules, then its component (components) are already in Xn (as for all in, XiXn).

Now, for some formulas B, C occurs one of the cases:

  • A ∶= (BC), and so B,CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that V(B) = V(C) = 1 = V((BC))
  • A∶= (BC), and so B or CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that V(B) = 1 or V(C) = 1, therefore V((BC)) = 1
  • A ∶= (BC), and so ¬B or CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that VB) = 1 or V(C) = 1, therefore V((BC)) = 1
  • ←52 | 53→ A ∶= (BC), and so B, C or ¬B, ¬CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that V(B) = 1 = V(C) or VB) = 1 = VC), therefore V((BC)) = 1
  • A ∶= ¬¬B, and so BXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that V(B) = 1 = V(¬¬B)
  • A ∶= ¬(BC), and so ¬B or ¬CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that VB)=1 or VC)=1, therefore V(¬(BC)) = 1
  • A ∶= ¬(BC), and so ¬BCXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that VB) = VC) = 1 = V(¬(BC))
  • A ∶= ¬(BC), and so BCXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that V(B)=VC)=1 =V(¬(BC))
  • A ∶= ¬(BC), and so ¬B, C or B, ¬CXn, on the inductive assumption and by definition of valuation of formulas 2.4 we then get that VB) = 1 = V(C) or V(B) = 1 = VC), therefore V(¬(BC)) = 1.

Consequently, V(Xn) = 1, since V(A) = 1, for all AXn.

The next lemma will show that a maximal and open branch allows to define a valuation that assigns the value of truth to each formula contained in the first element of branch.

Lemma 2.51 (Lemma on the existence of valuation). Let X1, . . ., Xn, for some n≥ 1, be a maximal and open branch. Then, there exists valuation V such that V(X1)=1.

Proof. Take any maximal and open branch X1, . . . , Xn, for some n ≥ 1. Now, we define L(Xn) = {xXnx = y or x = ¬y, for some y ∈ Var}. Since L(Xn) is t-consistent, we define valuation v ∶ Var → {1,0} such that for any x ∈ Var:

  • v(x) = 1, if xL(Xn)
  • v(x) = 0, if xL(Xn).

We see that both v(L(Xn)) = 1 and V(L(Xn)) = 1, where V is an extension of function v to the set of all formulas.

Now, using lemma 2.50, we get thesis V(X1) = 1, since X1Xn.

The lemma on the existence of valuation allows us to prove the completeness theorem.

←53 | 54→

Theorem 2.52 (Completeness). For any XForCPL, AForCPL, if XA, then XA.

Proof. Take any X ⊆ ForCPL, A ∈ ForCPL and assume that XA. Thus, by definition of branch consequence relation 2.41 for each finite subset YX there exists a maximal branch beginning with Y ∪{¬A} which is open. By virtue of the lemma on the existence of valuation 2.51 for each finite set YX there exists valuation V such that V(Y ∪{¬A}) = 1. Thus, by definition of valuation of formulas 2.4 and consequence classical relation 2.6, for each finite set YX, YA. Hence and by virtue of the compactness property of relation of consequence ⊧, fact 2.49, we get thesis XA.

2.5Tableaux for CPL vs. semantic consequence relation

So we can see that the concepts of relation of semantic consequence and relation of branch consequence denote exactly the same set of pairs ⟨X,A⟩, where X is a set of formulas, while A is a formula. In practice, however, it is not easy to determine whether a pair belongs to relation ⊳. According to definition 2.41, in order to achieve this, we need to select from X its finite subset Y such that each maximal branch beginning with set Y ∪{¬A} is closed. The first stage of this activity, i.e. the selection of an appropriate set, is difficult to study in general, since further we will deal with various different logics, and the relation of branch consequence has been defined for any sets, particularly infinite ones. However, if the set of premises is a finite set, we can proceed straight to the second stage, i.e. reviewing all maximal branches and checking if they are closed branches.

Unfortunately, although their number in the case of a finite set of premises will also be finite, it may be so large that their construction and examination are only theoretically possible. Therefore, we need a method that allows to select and study a sufficiently small number of maximal branches, the closure of which guarantees the occurrence of branch consequence relation.

In our theory, this method is based on the concept of a tableau. By tableau we mean a finite and minimal set of branches beginning with the same set. Of course, such a concept of tableau is far from its graphic presentation or one based on graphs. Due to its formal nature, it specifies the standard concept of tableau, plus its scope at least includes a set of those objects which are traditionally called semantic or analytical trees or tableaux. The problem of this relation will be dealt with in the last chapter of the book.

Let us now proceed to the definition of tableau.

←54 | 55→

Definition 2.53 (Tableau). Let X ⊆ ForCPL, A ∈ ForCPL, while Φ will be a set of branches. Ordered triple ⟨X,A,Φ⟩ will be called a tableau forX,A⟩ (or shortly tableau) iff the below conditions are met:

  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 the domains of functions ψ1, . . . , ψn
  5. • for any 1 < 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.

Remark 2.54. The first two conditions in the tableau definition are standard ones. Each branch in the tableau begins with a set which is the sum of the set of premises and the negation of the presumed conclusion. In addition, the tableau contains only Φ-maximal branches, so it does not include sub-branches of the branches belonging to Φ.

However, the third condition is particularly worth discussing. This condition says that branching can occur in a tableau only if there is a suitable rule and its ordered triple which contains two output sets corresponding to the branching.

We have deliberately reduced number m to range {2,3}, since the rules in set RCPL have at least two elements each, but not more than three. In the case of tableau systems for other logics, however, it may happen that m will be any number greater than 1 which will allow for several branchings at a given stage of the tableau construction. In general, the upper range of number m minus 1 means the number of branchings that can appear in the tableau at a given stage of construction.

Therefore, definition of tableau 2.53 excludes such sets of branches from being considered tableaux as in example 2.55.

Example 2.55. We consider set {¬p,(pq),(qr)} and create three branches.

←55 | 56→

Although there exists a rule — it is rule R∨ — which contains ordered triples ⟨X1,X2.1,X2.2⟩ and ⟨X1,X2.2,X2.3⟩, set RCPL includes no rule to comprise a ordered quadruple ⟨X1,X2.1,X2.2,X2.3⟩, therefore the presented set of branches {⟨X1,X2.1⟩,⟨X1,X2.2⟩,⟨X1,X2.3⟩} does not meet the third condition of the definition of tableau 2.53.

As we can see, the concept of tableaux has been defined in such a way that tableaux can also begin with infinite sets.

In practice, the construction of tableau is to show that a given formula is a branch consequence of a given finite set of premises. To this end, we must construct tableaux that have all the elements necessary to solve the problem. Tableaux with these properties are called complete tableaux. But, before we proceed to the definition of complete tableau, we will consider one more issue.

When constructing a tableau, it may happen that branchings and branches are formed which are redundant variants of the already existing branches. Let us consider the following two examples.

Example 2.56. Consider set {pq, ¬¬p} and create a branch using a rule R¬¬ to this set. We get the following branch.

Branches X1, X2 cannot be any more extended since ordered triple ⟨X1 ∪ {p},X1∪{p},X1∪{p,q}⟩ does not belong to rule R due to the fact that X1∪{p} ⊈ X1 ∪{p}, whereas the input set should be contained in each output set.

We can, however, starting from set {pq, ¬¬p}, through the use of rule R, produce two branches, and than apply rule R¬¬ to set X2.2. Then we get the following branches.

In the light of definition of tableau 2.53, the set of these two branches is, obviously, a tableau. However, from the viewpoint of a tableau complexity and information it provides, 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 ←56 | 57→to get t-inconsistent set in the left-hand branch. On each set of formulas Y we generally know from the definition of tableau inconsistent set of formulas 2.10 that Y is not t-inconsistent iff each of its subsets is not t-inconsistent, and the point of constructing a tableau is precisely finding a t-inconsistency. Therefore, the branch on the right seems superfluous, and since it brings nothing important, it can be called redundant.

Such branchings are not a formal obstacle, hence they can be accepted. However, due to the economy of a tableau construction, they can be disregarded. Further concepts will be defined 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. So there is no reason to further restrict this process—and we allow both options. Let us now proceed to the formal concept of a redundant variant of branch.

Definition 2.57 (Redundant variant of branch). Let ϕ and ψ be such branches that if there exists number i that i and i+1 belong to their domains, then for any ji, ϕ(j)=ψ(j), but ϕ(i+1) ≠ ψ(i+1). We shall state that branch ψ is a redundant variant of branch ϕ iff:

  1. there exist such rule RRCPL and such pair ⟨X,Y⟩ ∈ R that X = ϕ(i) and Y = ϕ(i+1)
  2. there exist such rule RRCPL and such triple ⟨X,W,Z⟩ ∈ R that X = ϕ(i) and:

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

or

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

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

Let us consider another example of tableau with redundant branches.

Example 2.58. Take set {¬¬p, ¬¬q, pq}. By applying rules R and R¬¬ successively, we will get an interesting case of tableau.

←57 | 58→

Sets X3.1 and X3.2 are identical. So, we face an interesting situation where both branches “diverged” (sets X2.1 and X2.2 are different), and then “converged” (sets X3.1 and X3.2 are identical). Due to the definition of redundant variant of branch 2.57, each of those two branches is a redundant variant of the other.

Remark 2.59. The concept of a redundant variant of branch can be extended onto other cases of branchings where one of branches brings no expressions into the tableau that are necessary to obtain the answer to the question whether given inference is correct. Nevertheless, we will not expand this concept. After all, we are not interested in the economy of tableau proof. We introduced this concept in order to show that the adopted concepts of tableau and branch allows us to distinguish certain types of branches, and consequently, to distinguish certain sets of tableaux that are less complex.

Now, we will move on to the definition of complete tableau.

Definition 2.60 (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 it is not complete.

In a complete tableau, all branches are maximal, not only the maximal ones in a given set. In addition, a complete tableau is such set of branches that adding a new branch to it at most gives us a redundant superset or the set ceases to be a tableau. In other words, a complete tableau is such set of maximal branches that any of its supersets ceases to be a tableau or is a redundant superset.

When constructing a complete tableau, we can come across a situation in which all the branches are closed, meaning each branch ends with a t-inconsistent set. Such a tableau is called closed tableau. Let us first define a closed/open tableau, and then discuss the definition.

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

1. each branch contained in Φ is closed

2. any set of branches Ψ such that:

a. Φ ⊂ Ψ

←58 | 59→

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

is a redundant superset of Φ.

A branch is open iff it is not closed.

As we have said, by the above definitions—the definition of complete tableau 2.60 and the definition of closed tableau 2.61—and the conclusion 2.40, we have another conclusion.

Corollary 2.62. Each closed tableau is a complete tableau.

Moreover, among complete tableaux, those tableaux that only contain sets of closed branches are closed tableaux. So we have another conclusion.

Corollary 2.63. Each complete tableau in which the set of branches only contains closed branches is a closed tableau.

Making use of conclusions 2.62 and 2.63, we can, therefore, simplify the definition of closed/open tableau by formulating another conclusion.

Corollary 2.64 (Closed/open tableau). LetX,A,Φ⟩ be a tableau. TableauX,A,Φ⟩ is closed iff the below conditions are met:

1. ⟨X,A,Φ⟩ is a complete tableau

2. each branch contained in Φ is closed.

A branch is open iff it is not closed.

Conclusion 2.64 can be adopted as an equivalent version of the definition of closed/open tableau.