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 Tableau system for Classical Propositional Logic

←26 | 27→

2Tableau system for Classical Propositional Logic

2.1Introductory remarks

In this chapter, we will define the tableau system for Classical Propositional Logic (for short CPL)1, treating this case as a basic one.

This system can be considered basic because in the definition of tableau system for CPL we will use the propositional logic formulas themselves as tableau expressions. In the case of CPL it is possible, in other cases it may not be possible.

The defined system also features the property that any branch that begins with a finite set of tableau expressions can be extended to a branch of finite length to which the tableau rule can no longer be applied. We will call this feature a finite branch property. However, it is not a feature specific to all the tableau systems described in the book. This feature also makes the presented system for CPL a basic case, although for many logics the tableau systems feature the same property.

At the end of the chapter, we show that we actually have defined a tableau system for the CPL, because the relation of tableau derivability it determines coincides with the consequence relation determined by the valuation of formulas.

Throughout this chapter, we establish certain conventions of notation and order of defining tableau concepts and proving facts, which conventions and order will guide us within the book.

2.2Language and semantics

The construction of a tableau system for the classical logic will start with the basic definitions. First, we will take up the language of CPL.

Definition 2.1 (Alphabet of CPL). Alphabet of the Classical Propositional Logic is the union of the following sets:

  • set of logical constants: Lc = {¬,∧,∨,→,↔}
  • set of propositional letters: Var = {p1,q1,r1,p2,q2,r2, . . .}
  • set of brackets: {),(}.
←27 | 28→

Although the set of propositional letters is infinite and includes indexed propositional letters, in practice we will use a finite number of the following letters: p, q, r, s.

Definition 2.2 (Formula CPL). Set of formulas of CPL is the smallest set X which meets conditions:

  1. Var ⊆ X
  2. if A, BX, then

a. ¬AX

b. (AB) ∈ X

c. (AB) ∈ X

d. (AB) ∈ X

e. (AB) ∈ X.

We specify this set as ForCPL, and its elements will be called formulas.

Remark 2.3. When considering different languages, we will use separate denotations for the sets of their formulas — though in a given context, we will use formulas of only one logic—so there will be no risk of mistake. However, in the chapter devoted to the generalisation of our considerations, we will use a denotation with no index. Additionally, sometimes, if possible, we will omit external brackets.

Let us proceed now to the semantics of classical logic. Valuation of propositional letters Var is any function v ∶ Var → {1,0}, that to each propositional letter assigns a value of truth or false. With function v, we can define valuation of formulas of CPL.

Definition 2.4 (Valuation of formulas of CPL). Valuation of formulas is function V ∶ ForCPL →{1,0}, which for any A,B ∈ ForCPL meets the following conditions:

  1. VA) = 1 iff V(A) = 0
  2. V(AB) = 1 iff V(A) = 1 and V(B) = 1
  3. V(AB) = 1 iff V(A) = 1 or V(B) = 1
  4. V(AB) = 1 iff V(A) =0 or V(B) = 1
  5. V(AB) = 1 iff V(A) = V(B).

We also call function V a valuation of formulas of CPL or shortly valuation.

Each function v, through conditions of definition 2.4, is unambiguously extendible to the valuation of formulas, i.e. function V ∶ ForCPL → {1,0} that to each formula assigns a value of truth or false.

←28 | 29→

Denotation 2.5. Let us adopt some abbreviations. Let ‘V(X)=1’ mean V(X)⊆{1} (i.e. if X ≠∅, then V(X) = {1}), while ‘V(X) ≠ 1’ means V(X) ⊈{1}, (i.e. if X ≠∅, then V(X) ≠ {1}) for any set of formulas X and for any valuation V.

Using the concept of valuation of formulas, we can now define the semantic consequence of CPL.

Definition 2.6 (Semantic consequence of CPL). Let set X ⊆ ForCPL and A ∈ ForCPL. Formula A follows from set X (for short: XA) iff for any valuation V, if V(X) = 1, then V(A) = 1. Relation ⊧ will be called relation of classical semantic consequence or shortly relation of semantic consequence.

Thus, classical semantic consequence ⊧ is such a relation that ⊧ ⊆ P(ForCPL)× ForCPL.

Remark 2.7. When considering different relations of consequences 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.8. For any set of formulas X and any formula A notation XA will mean that it is not the case that XA.

The last concept related to CPL, we will apply when constructing the tableau system is the concept of contradictory set of formulas.

Definition 2.9 (Contradictory set of formulas). Let X ⊆ ForCPL. Set X will be called contradictory iff there is no valuation V such that V(X) = 1. Set X will be called non-contradictory iff it is not contradictory.

2.3Basic concepts of the tableau system for CPL

One of the basic concepts used to describe a tableau system, due to the nature of tableau proofs, is the concept of a tableau inconsistent set of proof expressions. In the case of a defined system for CPL, the proof expressions are the formulas themselves, so a set of tableau inconsistent expressions boils down to a certain set of formulas.

Definition 2.10 (Tableau inconsistent set of formulas). Set X ⊆ ForCPL will be called tableau inconsistent (for short: t-inconsistent) iff there exists such formula A ∈ ForCPL that AAX. Set X will be called tableau consistent (for short: t-consistent) iff it is not t-inconsistent.

Corollary 2.11. For any XForCPL, if X is t-inconsistent, then X is contradictory.

Proof. By definition 2.10, 2.4, 2.9.

←29 | 30→

2.3.1Tableau rules for CPL

We will now proceed to defining the proof tools. The central concept is tableau rules. Usually, in an intuitive approach, tableau rules are presented as graphs illustrating the way in which proof expressions are distributed. Rules for CPL are most often presented in the following way.2

First, we present positive rules — for formulas that do not begin with the negation functor.

The negative rules, on the other hand, for formulas preceded by negation, are presented in the following drawings.

In all of these rules, the arrows show the formulas we obtain by applying given rule, while some rules provide alternative formulas. Such a concept of rule is figurative and very intuitive, but at the same time not very formal. As a result, it is difficult to base on it to define the concept of tableau or tableau proof more formally than the concept of rule itself.

The starting point for the construction of a tableau system can therefore be a precise definition of the concept of tableau rule. Let us start with the general concept of rule.

←30 | 31→

Definition 2.12 (Rule). Let P(ForCPL) be the set of all subsets of set of formulas. Let P(ForCPL)n be n-ry Cartesian product for

some n ∈ ℕ.

  • By a rule we understand any such subset RP(ForCPL)n that if ⟨X1, . . . ,Xn⟩ ∈ R, then X1Xi, for each 1 < in.
  • If n ≥ 2, each element R will be called ordered n-tuple (pair, triple, etc., respectively).
  • The first element of each n-tuple will be called an input set (set of premises) while the other elements output sets (sets of conclusions).3

Thus, according to the above definition, each rule is for some n ∈ ℕ a set of n-tuples in the form of ⟨X1, . . . ,Xn⟩, where X1, . . . , Xn ⊆ ForCPL. Not every rule is of course a tableau rule for CPL. A set of tableau rules for our tableau system for CPL shall be introduced by means of the following definition.

Definition 2.13 (Tableau rules for CPL). Tableau rules for CPL are the following rules:

R={⟨X ∪ {(AB)},X ∪ {(AB), A, B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {(AB)} is t-consistent}

R= {⟨X ∪ {(AB)},X ∪ {(AB), A}, X ∪ {(AB), B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {(AB)} is t-consistent}

R = {⟨X ∪ {(AB)},X ∪ {(AB), ¬A}, X ∪ {(AB), B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {(AB)} is t-consistent}

R = {⟨X ∪ {(AB)},X ∪ {(AB), A, B}, X ∪ {(AB), ¬A, ¬B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {(AB)} is t-consistent}

R¬¬ = {⟨X ∪ {¬¬A},X ∪ {¬¬A, A}⟩ ∶ X ⊆ ForCPL, A ∈ ForCPL, X ∪ {¬¬A} is t-consistent}

R¬∧={⟨X ∪ {¬(AB)},X ∪ {¬(AB),¬A}, X ∪ {¬(AB),¬B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {¬(AB)} is t-consistent}

←31 | 32→

R¬∨= {⟨X ∪ {¬(AB)},X ∪ {¬(AB),¬AB}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {¬(AB)} is t-consistent}

R¬→= {⟨X ∪ {¬(AB)},X ∪ {¬(AB), A, ¬B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {¬(AB)} is t-consistent}

R¬↔= {⟨X ∪ {¬(AB)},X ∪ {¬(AB), ¬A, B}, X ∪ {¬(AB), A, ¬B}⟩ ∶ X ⊆ ForCPL, A,B ∈ ForCPL, X ∪ {¬(AB)} is t-consistent}.

Set of tableau rules for CPL will be denoted as RCPL.

By definition 2.13 it follows that we have nine tableau rules for the tableau systembeing defined for CPL. Let us consider one of them, e.g. R¬∧. Take any x and assume that xR¬∧. By definitions 2.12 and 2.13, we get A, B ∈ ForCPL that:

  1. x = ⟨X ∪ {¬(AB)},X ∪ {¬(AB),¬A}, X ∪ {¬(AB),¬B}⟩
  2. X ∪ {¬(AB)} ⊂ X ∪ {¬(AB),¬A}
  3. X ∪ {¬(AB)} ⊂ X ∪ {¬(AB),¬B}
  4. X ∪ {¬(AB)} is t-consistent.

Therefore, there is such a set and such formulas that the rule contains the ordered triple of sets which was constructed on them and has the following properties:

(a) the first element — the input set — is a proper subset of both the second and third element—the output sets

(b) the first element is a t-consistent set.

Both these properties are important for the method of constructing tableau systems presented in the book. They also form an element which distinguishes this method from other ones. But before we proceed to a more detailed discussion of the properties, we will look at the notation of the rules itself. The provided method of notation is quite precise, but at the same time complicated. Thus, despite the fact that the case of CPL is the simplest of those considered in the book, the description of sets—rules is somewhat complicated.

In order to simplify the notation, we will propose a fractional one. With rule R = {⟨X1, . . . ,Xn⟩∶ X1 is t-consistent}, where n ≥ 2, we will write:

←32 | 33→

Heuristically speaking, the fraction bar in the above notation will tell us that from the input set X1 we can proceed to one of the output sets X2, . . . , Xn, described under the bar. In the fractional notation, the individual sets will also be described structurally, i.e. the fraction will be a scheme of infinitely many n-tuples, which are elements of rule R.

Remark 2.14. Further in the book, we will capture specific tableau rules with fractional notation only, but we will have introduced a general definition of the rule for a given type of tableau systems beforehand.

Now, using the above method of notation, we will once again present set of rules RCPL. Set of rules RCPL contains only rules defined by the following schemes in which the input sets are t-consistent:

Remark 2.15. The method of tableau rules defining we have presented — no matter what notation method is adopted — carries some benefits. The first is elimination of redundant applications of rule that may occur in the case of intuitive formulation of a tableau system. An redundant application of rule takes place when application of rule does not cause a new expression to appear on ←33 | 34→every branch it generates. In extreme cases, theoretically even intuitive rules can be applied without limitations, never receiving anything new. This is illustrated by the following example 2.16.

The rules defined according to our recipe exclude this type of situation, and the responsible factor is the condition that requires the input set to be a proper subset of each of the output sets. As per definition 2.12, for each rule R and n ∈ℕ, if ⟨X1, . . . ,Xn⟩ ∈ R, then X1Xi, for each 1 < in. Therefore, no rule RRCPL can be applied idly.

Example 2.16. Take formulas (pq), ¬¬r, p, q. Using the intuitive rules described at the beginning of this subchapter 2.3.1, we can apply to these formulas many times the rule for conjunction to formula (pq), although it does not bring anything new — in the meantime we have applied the rule for double negation to formula ¬¬r.

It is difficult to formally limit such redundant use, since the rule is illustrated in the formula scheme, whereas the proof consists of many elements. Therefore, it is necessary to refer to all previous elements in a limitation. However, some of these elements may have appeared after the earlier application of other rules. Hence, it is unclear at which level in this approach to formally exclude such application of the tableau rules.

Remark 2.17. Another benefit of the way the rules are defined is the exclusion of their applicability to the sets that are t-inconsistent. Within the classic approach to rules, there is nothing to prevent us from continuing to apply the rule, even if there is an explicit tableau inconsistency in the proof tree. Of course, one way to avoid this problem is to add a blocking rule to the set of tableau rules, which introduces a new element which closes the branch. Again, however, nothing formally excludes the application of further rules, even if there is a blocking element in the proof.

We illustrate this problem with example 2.18. In our approach, the informal “no use” directive makes technical sense: it is simply not possible—in the case of ←34 | 35→a t-inconsistent set, there are no rules that can be applied. Again, this is because of the rule definition. By definition 2.13 for each rule R and n ∈ℕ, if ⟨X1, . . . ,Xn⟩∈ R, then X1 is t-consistent, thus X1 contains no pair of formulas A, ¬A, by definition 2.10. Consequently, no rule RRCPL can be applied to a tableau inconsistent set.

Example 2.18. Take formulas (pq), ¬¬¬r, p, r. Using the intuitive rules described at the beginning of this subchapter 2.3.1, we can apply the rule for conjunction to formula (pq), even though previously we applied the rule for double negation to formula ¬¬¬r, which eventually produced a t-inconsistent set as we already had formula r.

Again, it is difficult to limit such application of rules if we do not have a precise concept of proof and rule.

Remark 2.19. Instead of set RCPL, we could use a different axiomatization to construct a tableau system. For instance, instead of rule R¬∧, we could consider the following tableau rule:

Similar proposals could be made for some other rules from set RCPL. Among many ideas, one of the simpler ones seems to be the replacement of rule R e.g., the following one:

Of course, the new rules—according to definition of tableau rule 2.13—would also have t-consistent input sets, plus the input set would be contained properly in the output sets. Various axiomatizations can be examined for dependencies between sets of tableau rules, lengths of proofs and intuitiveness of rules.

For three reasons, however, we will not be researching such alternative tableau axiomatizations.

←35 | 36→

First of all, we want to describe the method of constructing tableau systems on the example of selected cases and then try to generalize this method on different cases. So in each case of the tableau systems considered in the book, it is sufficient to describe a single case, e.g. the most typical one. If we were to investigate an alternative axiomatization for a tableau system for CPL, e.g. using set (RCPL ∖{R¬∧}) ∪ , then in order to formally demonstrate that both systems yield the same logical consequences, it would require defining both systems and demonstrating that the sets of their consequences are identical. Meanwhile, we want to define a sample system for set of rules RCPL and sample systems for logics specified in other languages, and then look for a general pattern for the construction of a tableau system that would simplify the construction of tableau systems and also help to study the equivalence of different sets of rules that axiomatize the same logic. So instead of describing consecutive tableau systems for the same semantically determined logic, we will try to seek common attributes of tableau systems for various semantically determined logic.

Secondly, the specified set of tableau rules RCPL corresponds to the intuitive and normally adopted tableau rules for CPL. Thus, they are typical, because in the simplest way they correspond to the semantic content related to the interpretation of the classical connectives.

Thirdly, rules such as do not seem good candidates for axiomatization. For example, the adoption of set (RCPL ∖{R¬∧}) ∪ , which is to replace rule R¬∧ with rule would extend some of proofs. Because rule R¬∧ allows to proceed from formula ¬(AB) to formulas ¬A or ¬B. Meanwhile, in the case of rule we proceed from formula ¬(AB) to formula (¬A∨¬B). Transition to formulas ¬A or ¬B still requires the use of rule R. Thus, introduction of rule in lieu of R¬∧ seems unnatural. It is not certain, however, that for the cases considered in the book there are no alternative rules that are not unnatural, or maybe even in some way they are better than the ones considered. In the next chapter, when describing the tableau system for term logic, we will show an example of alternative rules that seem at least equally good as the ones we will finally investigate there (see note 3.20).

However, among the reasons mentioned, the first one is conclusive. Therefore, although we will not examine alternative axiomatizations of tableau systems, it is worth stressing that the introduction of the general concept of rule 2.12 for a given set of tableau expressions Te is meaningful in overall. Most often it is possible to define different sets of tableau rules that define tableau systems corresponding to the same semantically determined logic.

←36 | 37→

2.3.2Branches for CPL

Another thing in our theory that needs discussion is the concept of branch. It is a concept that depends on the tableau rule because branches are created by applying rules. Although we are not currently introducing any formal concept of rule application, intuitively the point is that a given rule R is applied to a given set Y when among the elements contained in R there is such n-tuple ⟨X1, . . . ,Xn⟩ that X1 = Y. The result of application of R is some set Xi, where 1 < in, and consequently also sequence ⟨X1, Xi⟩, which forms precisely a branch. Branches are therefore setwise objects consisting of sets. Let us now proceed to the formal definition of branch in the tableau system for CPL.

Definition 2.20 (Branch). Let K = ℕ or K = {1,2, . . . ,n}, where n ∈ ℕ. Let X be any set of formulas. A branch (or a branch beginning with X) will be called any sequence ϕKP(ForCPL) that meets the following conditions:

  1. ϕ(1) = X
  2. for any iK: if i+1 ∈ K, then there exists such rule RRCPL 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 2.21. From now on—when speaking of branches—for convenience, we will use the following notations or designations:

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

Remark 2.22. As we can see, the concept of branch depends on some set of rules. In the case under consideration, the branch structure is based on the rules from set RCPL. Further described complex tableau concepts will also depend on some sets of rules. Because in this chapter we are studying tableau system for CPL, based on rules from set RCPL, 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 hinge upon some set of rules. In one of the further chapters, ←37 | 38→in the general description of the construction method itself, the set of rules will be a certain variable. In this chapter, it is specified as: RCPL, and the complex tableau concepts defined here depend on it.

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

Corollary 2.23. Each branch is an injective sequence.

We will now look at the issue of branch length. To investigate this problem, we need a function to measure the formula complexity. But, this is not about a syntactic complexity, but branch complexity. In practice, the branch complexity of the formula boils down to the maximal length of the branch, which is obtained by applying the tableau rules to a single formula only. First, we will give a definition of the function that measures this property and show that the function has been well defined, and then we will present an example. Assume that for any two natural numbers n, m, max{n, m} = n iff nm.

Definition 2.24 (Measure of the branch complexity of formula of CPL). The measure of the branch complexity is function ∗∶ ForCPL →ℕ, defined for each x ∈ Var and A, B ∈ ForCPL with the below conditions:

  1. ∗(x) = 1
  2. ∗(¬x) = 1
  3. ∗((AB)) = ∗(A)+∗(B)
  4. ∗((AB)) = max{∗(A),∗(B)}+1
  5. ∗((AB)) = max{∗(¬A),∗(B)}+1
  6. ∗((AB)) = max{∗(A)+∗(B),∗(¬(A))+∗(¬(B))}
  7. ∗(¬¬A) = ∗(A)+1
  8. ∗(¬(AB)) = max{∗(¬A),∗(¬B)}+1
  9. ∗(¬(AB)) = ∗(¬A)+∗(¬B)
  10. ∗(¬(AB)) = ∗(A)+∗(¬B)
  11. ∗(¬(AB)) = max{∗(¬A)+∗(B),∗(A)+∗(¬B)}.

Function ∗, tells us how at most long a branch can be obtained by applying the rules from RCPL to a given formula and its components. The following few facts clarify the problem. From the above definition and the definition of formula 2.2, it follows that:

Corollary 2.25. For any AForCPL: ∗(A) ∈ ℕ.

We will now formulate a fact that describes the relationship between the branches and the measure of the branch complexity of formula.

←38 | 39→

Proposition 2.26. Let AForCPL. Let X1 = X ∪{A},X2, . . . ,Xn be such a branch that Y1, . . . , Yn, where:

  • Y1 = {A}
  • Y2 = X2X
  • . . .
  • Yn = XnX

is a branch. Then n ≤∗(A).

Before we proceed to the proof of fact, let us try to explain its assumption. For each X ⊆ ForCPL and A ∈ ForCPL branch X1 = X ∪{A},X2, . . . ,Xn is constructed so that for each 1 < in, Xi = XYi. This means that X2 was created by applying a certain rule to formula A, X3 was created by applying a certain rule to formula from X2X, whereas Xi+1 was created by applying a certain rule to formula from XiX. So, to put it figuratively, the branch under consideration was created by applying the rules to formula A and the consequences of applying the rules to what was created previously. It is of course possible that at some point in time a certain rule may have been applied to a element of set X, but the effect must have been the same as applying the rule to A or its consequences.

Therefore, fact 2.26 tells us that a branch constructed through the application of rules to a single formula A and further effects of application of rules is not longer than ∗(A), thus the measure of the branch complexity is properly defined.

Let us now move on to the proof of fact. It has an inductive nature and is based on the branch complexity of the formulas found in branches. For the proof, we will use the definition of branch 2.20 the definition of measure of branch complexity 2.24.

Proof. Take any branch X1 = X ∪ {A},X2, . . . ,Xn that meets the theorem assumptions.

Initial step. Let A = x, for some x ∈ Var. There is then no rule to apply to X1, thus n = 1. Since ∗(x)=1, so n ≤∗(x). If A = ¬(x), for some x ∈ Var, then there is either no rule to apply to X1, so n = 1. Since ∗(¬x) = 1, thus n ≤∗(¬x).

Induction step. Assume that a fact thesis holds for each formula B such that ∗(A) > ∗(B). So, for each branch beginning with {B}, m long, it is the case that m ≤∗(B). The branches will be called B-branches, C-branches, etc., depending on the formula they start with.

←39 | 40→

Cases:

i) Let A ∶= ¬¬B. Then, by definition of function ∗, ∗(A) > ∗(B). Under the induction hypothesis ∗(B) ≥ m, where m is the length of any B–branch. Since n =m1 +1, for some m1 ≤∗(B), by definition of branch 2.20, so ∗(A) = ∗(B)+1 ≥ m1 +1 = n, by definition 2.24.

ii) Let A ∶= (BC). Then, by definition of function ∗, ∗(A) > ∗(B),∗(C). Under the induction hypothesis, ∗(B) ≥ m, where m is the length of any B-branch, and ∗(C) ≥ k, where k is the length of any C-branch. Consequently, since nm1 + k1, for some m1 ≤ ∗(B), k1 ≤ ∗(C), by definition of branch 2.20, so ∗(A) = ∗((BC)) = ∗(B)+∗(C) ≥m1 +k1n, by definition 2.24.

iii) Let A ∶= (BC). Then, by definition of function ∗, ∗(A) > ∗(B), ∗(C). Under the induction hypothesis, ∗(B)≥m, where mis the length of any B-branch, and ∗(C)≥k, where k is the length of any C-branch. Consequently, since n = m1+1 or n = k1 +1, for some m1 ≤∗(B), k1 ≤ ∗(C), by definition of branch 2.20, so:

  1. if max{∗(B),∗(C)} = ∗(B), then ∗(A) = ∗((BC)) = ∗(B)+1 ≥ m1 + 1 = n, by definition 2.24
  2. if max{∗(B),∗(C)} = ∗(C), then ∗(A) = ∗((BC)) = ∗(C) +1 ≥ k1 + 1 = n, by definition 2.24.

iv) Let A ∶= (BC). Then, by definition of function ∗, ∗(A) > ∗(¬B),∗(C). Under the induction hypothesis, ∗(¬B) ≥ m, where m is the length of any ¬B-branch, and ∗(C) ≥ k, where k is the length of any C-branch. Consequently, since n = m1 +1 or n = k1 +1, for some m1 ≤ ∗(¬(B)), k1 ≤∗(C), by definition of branch 2.20, so:

  1. if max{∗(¬B),∗(C)} = ∗(¬B), then ∗(A)=∗((BC)) = ∗(¬(B))+1 ≥m1 + 1 = n, by definition 2.24
  2. if max{∗(¬B), ∗(C)} = ∗(C), then ∗(A)=∗((BC)) = ∗(C)+1 ≥ k1 +1 = n, by definition 2.24.

v) Let A ∶= (BC). Then, by definition of function ∗, ∗(A) > ∗(B), ∗(C), ∗(¬B),∗(¬C). Under the induction hypothesis, ∗(B) ≥ m, ∗(C) ≥ k, ∗(¬B) ≥ l, ∗(¬C)≥o, where m, k, l, o are respectively lengths of any B, C, ¬B and ¬C-branch. Consequently, since nm1 + k1 or nl1 + o1, for some m1 ≤ ∗(B), k1 ≤ ∗(C), l1 ≤∗(¬B), o1 ≤∗(¬C), by definition of branch 2.20, so:

  1. if max{∗(B) + ∗(C),∗(¬B) + ∗(¬C)} = ∗(B) + ∗(C), then ∗(A) = ∗((BC)) = ∗(B)+∗(C) ≥m1 +k1n, by definition 2.24
  2. ←40 | 41→ if max{∗(B)+∗(C),∗(¬B)+∗(¬C)} = ∗(¬B)+∗(¬C), then ∗(A) = ∗(BC) = ∗(¬B)+∗(¬C) ≥ l1 +o1n, by definition 2.24.

vi) Let A∶= ¬(BC). Then, by definition of function ∗, ∗(A)>∗(¬B), ∗(¬C). Under the induction hypothesis, ∗(¬B) ≥ m, where m is the length of any ¬B-branch, and ∗(¬C) ≥ k, where k is the length of any ¬C-branch. Consequently, since n = m1 +1 or n = k1 + 1, for some m1 ≤ ∗(¬B), k1 ≤ ∗(¬C), by definition of branch 2.20, so:

  1. if max{∗(¬B),∗(¬C)} = ∗(¬B), then ∗(A)=∗(¬(BC)) = ∗(¬B)+1 ≥m1 + 1 = n, by definition 2.24
  2. if max{∗(¬B), ∗(¬C)} = ∗(¬C), then ∗(A) = ∗(¬(BC)) = ∗(¬C) + 1 ≥ k1 +1 = n, by definition 2.24.

vii) Let A∶= ¬(BC). Then, by definition of function ∗, ∗(A)>∗(¬B), ∗(¬C). Under the induction hypothesis, ∗(¬B) ≥ m, where m is the length of any ¬B-branch, and ∗(¬C) ≥ k, where k is the length of any ¬C-branch. Consequently, since nm1 +k1, for some m1 ≤∗(¬B), k1 ≤∗(¬C), by definition of branch 2.20, so ∗(A) = ∗(¬(BC)) = ∗(¬B)+∗(¬C) ≥m1 +k1n, by definition 2.24.

viii) Let A∶= ¬(BC). Then, by definition of function ∗, ∗(A)>∗(B), ∗(¬C). Under the induction hypothesis, ∗(B)≥m, where mis the length of any B-branch, and ∗(¬C) ≥ k, where k is the length of any ¬C-branch. Consequently, since nm1 +k1, for some m1 ≤ ∗(B), k1 ≤ ∗(¬C), by definition of branch 2.20, so ∗(A) = ∗(¬(BC)) = ∗(B)+∗(¬C) ≥m1 +k1n, by definition 2.24.

ix) Let A ∶= ¬(BC). Then, by definition of function ∗, ∗(A) > ∗(B),∗(C), ∗(¬B),∗(¬C). Under the induction hypothesis, ∗(B) ≥ m, ∗(C) ≥ k, ∗(¬B) ≥ l, ∗(¬C)≥o, where m, k, l, o are respectively lengths of any B, C, ¬B and ¬C-branch. Consequently, since nm1 +o1 or nl1 +k1, for some m1 ≤ ∗(B), k1 ≤ ∗(C),l1 ≤ ∗(¬B), o1 ≤∗(¬C), by definition of branch 2.20, so:

  1. if max{∗(¬B)+∗(C),∗(B)+∗(¬C)} = ∗(¬B)+∗(C), then ∗(A)=∗(¬(BC)) = ∗(¬B)+∗(C) ≥ l1 +k1n, by definition 2.24
  2. if max{∗(¬B)+∗(C),∗(B)+∗(¬C)} = ∗(B)+∗(¬C), then ∗(A)=∗(¬(BC)) = ∗(B)+∗(¬C) ≥m1 +o1n, by definition 2.24.

So the fact 2.26 tells us that if we create a branch based on a single A and make use of tableau rules in any order, then each produced branch will at most have a length of ∗(A). See the example below.

←41 | 42→

Example 2.27. Let us consider set of formulas Y ∪{¬(p↔¬q)}. We decompose the highlighted formula using rule R¬↔ to this set. Due to two initial sets in the rule, we get two branches:

  1. = Y ∪{¬(p↔¬q)},= Y ∪{¬(p↔¬q),¬pq}
  2. = Y ∪{¬(p↔¬q)},= Y ∪{¬(p↔¬q),p,¬¬q)}.

In the first case, we can no longer decompose the components of the initial formula, but in the case of we can still apply rule R¬¬, which produces: = Y ∪{¬(p↔¬q),p,¬¬q,q}. (Of course, we assume that are t-consistent. Otherwise, we could not use the tableau rules.) The last sequence—— is the longest among the sequences based on the decomposition of formula ¬(p↔ ¬q). At most, is has length of ∗(¬(p↔¬q)). Let us calculate: ∗(p) = ∗(¬q) = ∗(¬p) = 1, ∗(¬¬q) = 1+∗(q) = 2. Thus max{∗(¬p)+∗(¬q),∗(p)+∗(¬¬q)} = max{2,3}. Hence ∗(¬(p↔¬q)) = 3.

Another fact generalizes our observations on the relationship between the length of the branch and the branch complexity of the formula on the finite sets of formulas.

Proposition 2.28. If X is a finite set of formulas, then each such branch ϕKP(ForCPL) that ϕ(1) = X is finite.

We will carry out an inductive proof with respect to the number of elements X by applying the previous fact 2.26.

Proof. Let X be a finite set of formulas, and ϕKP(ForCPL) any such branch that ϕ(1) = X.

Initial step. Assume that ∣X∣ = 1, so some formula AX. From the previous fact 2.26, we know that each branch based on decomposition of A has at most the length of ∗(A). Hence, ∣K∣ ≤ ∗(A), so branch ϕ is finite, under 2.25.

Induction step. Assume that the fact thesis is true for each such set of formulas Y that ∣Y∣ = n. Let us consider a situation where ∣X∣ = n + 1. So X = Y′ ∪{A} for certain set of formulas Y′ such that ∣Y′∣ = n, and some new formula A.

From fact 2.26, we know that each branch based on the decomposition of A has at most the length of ∗(A), which means it is finite. From the inductive assumption, we also know that each branch beginning with set of formulas Y′ is finite.

Consequently, each branch ϕ beginning with X = Y′∪{A} is finite as it is composed of elements of some branch which begins with A and elements of some branch which begins with Y′, by definition of branch 2.20, hence ∣K∣ ≤ n+∗(A).

←42 | 43→

By virtue of the last fact, we know that there are no infinite branches beginning with finite sets of formulas, which is expressed by the following conclusion.

Corollary 2.29. Let X be a finite set of formulas. Then there is no such branch ϕKP(ForCPL) that:

  • K =ℕ
  • ϕ(1) = X.

Proof. From the previous fact 2.28 and by definition of branch 2.20.

2.3.3Maximal branches

Another important concept in the construction of a tableau system is the concept of a maximal branch. Intuitively, the maximal branch is a branch to which no rule can be applied anymore, extending it to some super-branch. The definition of the maximal branch for the currently defined system is as follows.

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

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

Before we discuss this definition, let us consider an example.

Example 2.31. Consider a branch beginning with set X1 = n = m ⋅ 3, where m ∈ ℕ}. Set X1 contains an infinite number of formulas in the form of i.e. an infinite number of instances of propositional letter r, preceded in each instance by such number of instances of negation functor that is a multiple of 3.

We now define a branch based on set X1 and rule R¬¬, according to the following algorithm: for any m ∈ ℕ,

So, transition from set Xi to its superset Xi+1 is an effect of addition through rule R¬¬ to set Xi of formula

The branch can be illustrated as follows:

←43 | 44→

The defined branch is infinite. There is no super-branch to contain it. However, there is still an infinite number of formulas to which we might apply rule R¬¬. As a matter of fact, already in the area of set X4 we could obtain t-contradictory set, thereby closing the door on further extension of branches, defining X4 = X3 ∪ {¬¬r} , with respect to R¬¬, since ¬rX2X3.

Seemingly, we could limit the definition of maximal branch 2.30 to the second condition, i.e. to the non-existence of super-branch. However, we would then allow branches that contain non-decomposed expressions to which the tableau rules can still be applied.

Leaving out the first condition of the definition of maximal branch 2.30, would not change anything with respect to the cases of finite sets, but example 2.31 proves that we would allow cases of infinite branch that:

  • begin with an infinite set
  • meet the second condition of definition because they are infinite branches
  • but not all expressions contained were decomposed, in particular those responsible for the emergence of t-inconistent subset.

Remark 2.32. The definition of maximal branch 2.30 is suitable for those tableau systems where only finite branches are obtained from finite sets of expressions. So it is i.a. good for the tableau system we construct for CPL.