Show Less
Open access

Tableau Methods for Propositional Logic and Term Logic

Series:

Tomasz Jarmużek

The book aims to formalise tableau methods for the logics of propositions and names. The methods described are based on Set Theory. The tableau rule was reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are its supersets.

Show Summary Details
Open access

5 Metatheory of tableau systems for propositional logic and term logic

←152 | 153→

5Metatheory of tableau systems for propositional logic and term logic

5.1Introductory remarks

In this chapter, we establish general tableau concepts for systems constructed using the method described in the book. These concepts make it possible to utter and justify a number of basic facts, the specific cases of which we have been proving in the previous chapters.

Using the further defined general concepts of the tableau systems, we will be able to utter and prove a general theorem on the relationship between the tableau systems and the semantics adopted for them. The construction of the tableau system, which is adequate in terms of the adopted semantics, will boil down to defining the basic concepts of this system in such a way that they are special cases of the general concepts and meet certain general conditions which we will define further. In this way, we will shorten the definition of the tableau systems to a minimal — in comparison to the previous chapters — number of procedures that describe the features of the considered system that distinguish it from other tableau systems.

5.2Language and semantics

By set For we mean any set of formulas of some language. We call its elements formulas.

Remark 5.1. For our considerations, we adopt any but fixed such set of formulas For that ∣For∣ is an even number or For is an infinite set. Set For will remain unchanged until the end of this chapter.

We will now look at the issue of interpretation of formulas. In the cases presented in the previous chapters, the interpretations were the valuations of formulas or models. However, we will deliberately use the concept of interpretation in order to cover all those cases. We intend to describe in general the concept of interpretation which will be applicable in the presented metatheory of the construction of tableau systems that will allow us to draw conclusions on the general relationships between the semantic form of a given logic and its tableau approach.

In our considerations, we will make use of the fact that we only look into such logics whose interpretations assign exactly one of the two logical values to each formula. So, a given interpretation divides a set of formulas in an unambiguous, disjoint and exhaustive way into a subset of true formulas and a subset of false ←153 | 154→formulas under this interpretation. This division coincides with some division of the set of formulas into mutually contradictory formulas, because for any formula, a formula is true in a given interpretation if and only if the formula contradicting it is false in that interpretation.

The interpretation of a set of formulas can therefore be identified with the segment of the logical division of a set of formulas in terms of the contradiction of formulas which contains exactly all the formulas that are true in this interpretation. The starting point, however, will be a function that assigns a contradictory formula to each formula, thus always dividing the set of formulas into two segments of the logical division. At least one of those segments may correspond to some interpretation of a set of formulas in which all and only those formulas that belong to this segment of the division are true. We will illustrate this with an example.

Example 5.2. Let us consider the case of TL discussed in Chapter Three. Function ○ (definition 3.12) assigns a contradictory formula to each formula from set ForTL (fact 3.13). Let us now divide set of formulas ForTL into the following pairs of sets: X′ and complement of X′ to set of formulas ForTL, i.e. X′′ = ForTLX′, as per the principle of division, for each formula A ∈ ForTL:

(†) AX′ iff ○(A) ∉ X′.

The division of set of formulas ForTL into sets X′ and X′′ is a logical division as X′∩X′′=∅and X′∪X′′ = ForTL, and what is more, sets X′ and X′′ are non-empty.

Let us denote the set of all models 𝔐TL for TL as MTL, while the set of all such segments of division by function ○ that meet equivalence (†) as X.

Let 𝔐TL be any model. We define subset of formulas 𝔐'TL = {A ∈ ForTL∶𝔐TLA}. A complement of set 𝔐'TL to set ForTL is set ForTL, i.e. set= {A ∈ ForTL∶𝔐TLA}.

Function ○ assigns a contradictory formula to each formula from set ForTL (fact 3.13), since for any model 𝔐TL for TL and for any formula A ∈ ForTL it is the case that:

(††)𝔐TLA iff𝔐TL ⊭○(A).

Since setsandare disjoint, exhaustive and non-empty, so they make up one of many logical divisions of set ForTL by function ○ according to principle (†), for any formula A ∈ ForTL:

(†††) Aiff ○(A) ∉.

and belong to set X.

←154 | 155→

So with function ○we can unambiguously identify each model 𝔐TL (and more precisely the set of all formulas that are true in this model) with some segment of the logical division of the set of formulas by the contradiction of formulas, determined by function ○ with equivalence (††).

For each 𝔐TLMTL, there exists precisely one set XX such that 𝔐'TL = X. Therefore, we can identify set of all models MTL with some subset of set X, that is with some subset of set of all subsets of set of formulas P(ForTL).

However, the opposite dependence does not occur. The segments of logical division that belong to X may correspond to many models that vary in terms of the domain cardinality, but not formulas which are true in them.

In some cases, a segment of logical division that belongs to X may not be determined by any models. If, for instance, we take such segments of division Y′ and Y′′ that belong to X that for certain name letters P, Q ∈ Ln, PePY′ and PiQY′, then there is no such model 𝔐TLMTL that 𝔐TLY′, since the truth of set of formulas Y′ would require the denotation of letter P to be an empty set and non-empty one at the same time. Further, we will also provide an example for CPL (example 5.6).

Therefore, models/valuations, that is the set of interpretations should be identified with a certain subset of the set of logical divisions of the set of formulas determined by a certain function that assigns a contradictory formula to each formula. Whether or not it is a proper subset, may vary from one case to another (see example 5.7).

In the definition of interpretation of formulas, we will employ a reference to the sets of formulas that are true in a given model or valuation, because in the general approach to the tableau metatheory we cannot penetrate the structure of particular types of interpretations for different logics. At the same time, we must retain the general aspects, in particular those that correspond to the tableau proof, i.e. adopting in the proof a formula that is contradictory to the formula we are proving.

We will now propose the general definition of set of divisions of set of formulas For. There is a function in this definition that implicitly assigns a contradictory formula to each formula. In many cases, however, even if this function is well established, we will identify a set of initial valuations/ models with a proper subset of some sort of a set of all divisions.

Definition 5.3. Let f ∶ For → For be an injective function and X ⊆ For. We shall state that X is a division of For iff for any formula A ∈ For the following condition is met: AX iff f(A) ∉ X.

By set Xf we will mean a set of all divisions of set of formulas For determined by the established function f.

←155 | 156→

Remark 5.4. In some cases, function f may result in the non-existence of any division X ⊆ For, and then, consequently, set of all divisions Xf is empty. It is the case for instance when for some formula A ∈ For f(A) = A. Thus, not each function f is suitable for the definition of set Xf .

In some cases, such function may fail to determine divisions corresponding to all models/valuations (example 5.7). For these cases, the specified method cannot be used to define a tableau system.

Function f is determined by default by the way of adopting an equivalent of formula contradictory to the formula being proved. So, function f can correspond to negation—it does in the case of CPL and S51. Moreover, it may not correspond to any functor from the language — as it does not in the event of the tableau system for TL, where it could be identified with function ○ 3.13 (example 5.2) that assigns a contradictory formula to each formula. Generally speaking, function f, to each formula, assigns such formula that for any division X it is the case that exactly one of those formulas belongs to X.

Remark 5.5. For our considerations, we adopt any but fixed and non-empty set of all divisions Xf, for some function f ∶ For → For that meets the conditions of the last definition 5.3. The set will remain unchanged until the end of this chapter. We will, on the other hand, refer to function f.

As stated in example 5.2, for a given set of all valuations/models and given function f, it does not have to be the case that each element of set Xf corresponds to some valuation/model. Below, we provide an example for CPL (example 5.6). Example 5.6. Take set of formulas of CPL ForCPL. We will define function f as follows f(A) = ¬A, for any formula A ∈ ForCPL. Function f meets the condition from definition of division of set of formulas 5.8, i.e. it is an injective function. Now, let Xf be a set of all divisions of set of formulas determined by function f.

The set contains such division X that (pq) ∈ X, ¬pX and ¬qX. Obviously, no valuation of formulas V corresponds to set X, since for each V, if V((pq))=1, then Vp) = 0. Therefore, there does not exist such valuation V that V′ = {A ∈ For ∶ V(A) = 1} and V′ = X.

Moreover, no valuation corresponds to set ForCPLX, since for each V, if V(¬(pq)) = 1, then V(¬¬p) = 0 or V(¬¬q) = 0, and V(p) = 0 or V(q) = 0. Therefore, there does not exist such valuation V that V′ = {A ∈ For ∶ V(A) = 1} and V′ = ForCPLX.

←156 | 157→

On the other hand, however, for each valuation V there exists such set V′ ={A∈ For ∶ V(A) = 1} that for some division YXf, V′ = Y, because for each formula A ∈ ForCPL it is the case that AV′ iff ¬AV′.

By virtue of the above, we can identify the set of all valuations of formulas with a proper subset of set of all divisions Xf by function f .

In some cases and for some functions f it may be the case that the set of divisions corresponding to all models/valuations is identical to given set Xf(example 5.7).

Example 5.7. Consider two similar cases. In the first one, function f cannot be established in such a way that each model has a corresponding division that determines f. In the second case, for each division by function f there exists at least one corresponding model.

Take such subset X of set of all formulas ForTL that X = {P1aQ1,P1eQ1}. Consider set of all models MX for a new, more sparing language. They will be analogous to the models for TL, but their denotation sets will only be assigned to two name letters that occur in a new, more sparing language—letters P1 and Q1.

Next, in a usual manner we will define the relation of semantic consequence determined on set P(XX (in a sense truncating the relation of semantic consequence of TL to set X) and denote it as ⊧′. Only four arguments are correct in such logic:

{P1aQ1,P1eQ1}⊧′ P1aQ1

{P1aQ1,P1eQ1}⊧′ P1eQ1

{P1aQ1}⊧′ P1aQ1

{P1eQ1}⊧′ P1eQ1

since:

{P1aQ1} ⊭′ P1eQ1

{P1eQ1} ⊭′ P1aQ1

due to the fact that in MX there exist models in which the denotation of letters P1 is a non-empty set. In the event when that set is contained in the set of denotations Q1 proposition P1aQ1 is true, while proposition P1eQ1 is not true. Instead, in the event when the set of denotations of name letter P1 is disjoint with the set of denotations of letter Q1, proposition P1eQ1 is true, while proposition P1aQ1 is not true.

←157 | 158→

In turn, due to the fact that in MX there exist models in which the denotation of letter P1 is an empty set, set X = {P1aQ1,P1eQ1} is not a contradictory set. Therefore, we are unable to establish function f in such a way that each model has a division of set X determined by function f . For there exists only one injective function fXX such that for any yX f(y) ≠ y. It is defined as follows:

f(P1aQ1) = P1eQ1

f(P1eQ1) = P1aQ1.

Now, take any division Y of set X by function f. It meets condition: AY iff f(A) ∉ Y, for any AX. If P1aQ1Y, then f(P1aQ1) ∉ Y, i.e. P1eQ1Y, thus P1eQ1XY. If, in turn, P1aQ1Y, then f(P1aQ1)∈ Y, i.e. P1eQ1Y, thus P1eQ1XY. An analogous sequence of implications occurs for the other formula. Thus, for model in which set of formulas X = {P1aQ1,P1eQ1} is true, there does not exist any corresponding division of set X by function f . So, for such relation of consequence like ⊧′, we will not construct a tableau system using the provided method2.

On the other hand, take such subset Y of set of all formulas ForTL, that Y = {P1aQ1,P1oQ1}, and set of all models MY (which is identical to set MX, as we still have the same letters in the alphabet), and then define in a usual manner the relation of semantic consequence on set P(YY (in a sense truncating the relation of semantic consequence of TL to set Y) and denote it as ⊧′′. In such logic, there occur analogous implications like for relation ⊧′. However, in MY there does not exist model such that set Y = {P1aQ1,P1oQ1} is true in it, because formulas P1aQ1, P1oQ1 are contradictory. We establish function fYY as follows: f(P1aQ1) = P1oQ1 and f(P1oQ1) = P1aQ1. We only get two divisions of set Y by function f , Y′ = {P1aQ1} and Y′′ = {P1oQ1} 3.

Note that for each model 𝔐Y there exists division Z of set Y by function f such that 𝔐′Y = {AY ∶𝔐Y ⊧′′ A} = Z. On the other hand, for each division Z of set Y by function f there exists model 𝔐Y such that 𝔐′Y = {AY ∶𝔐Y ⊧′′ A} = Z.

←158 | 159→

For the reasons we mentioned, in further semantic considerations we will refer to some established set IXf . So, let us proceed to the definition.

Definition 5.8 (Interpretation of formulas). A set of interpretations determined by function f(for short: interpretations) is each subset IXf . The elements of set I will be called interpretations of formulas (or for short: interpretations) and denoted by letter ℑ, possibly with indices.

Denotation 5.9. Let IXf . Let ℑ ∈ I be any interpretation of formulas. Let us adopt the following denotations:

  • for any formula A ∈ For, the fact that A ∈ ℑ will be put as ℑ ⊧ A, whereas the fact that A ∉ ℑ will be put as ℑ ⊭ A
  • for any subset of formulas X ⊆ For, ℑ ⊧X iff for any formula AX, ℑ ⊧A; while ℑ ⊭ X iff it is not the case that ℑ ⊧ X.

We will now proceed to the concept of relation of semantic consequence.

Definition 5.10 (Semantic consequence). Let IXf be a set of interpretations. Let X ⊆ For and A ∈ For.

  • Formula A follows from X under I (for short: XI A) iff for any interpretation ℑ ∈ I, if ℑ ⊧ X, then ℑ ⊧ A. Whereas formula A does not follow from X under I (for short: XI A) iff it is not the case that XI A.
  • When set I is fixed, we apply notation XA and respectively XA.
  • Relation ⊧ will be called a relation of semantic consequence (defined by set of interpretations I).

With an established relation ⊧ we can proceed to the concept of semantically defined logic.

Definition 5.11. Let set IXf be a set of interpretations of formulas For. Pair ⟨For,⊧I⟩ will be called a semantically defined logic.

Another fact says that two relations of consequence defined on set of formulas For are identical iff they are defined with the same set of interpretations IXf , so when speaking of relation ⊧, we do not have to refer to set I, as it is unambiguously determined by relation ⊧.

Proposition 5.12. Let I1Xf and I2Xf be sets of interpretations of formulas For. Let pairs be semantically defined logics. In such case

Proof. Take any sets of interpretations of formulas I1Xf , I2Xf , and logics they semantically defined. Assume that I1I2.We have two cases:

←159 | 160→

(1) there exists such interpretation ℑ ∈ I1 that ℑ ∉ I2

or

(2) there exists such interpretation ℑ ∈ I2 that ℑ ∉ I1.

Let us only consider case (1) as case (2) is analogous.

Now, take any such interpretation ℑ ∈ I1 that ℑ ∉ I2.

Assume that I2 is an empty set. By definition of relation of semantic consequence 5.10, On the other hand, since ℑ ∈ I1, so by definition 5.3, for certain formula A, ℑ ⊧ A and ℑ ⊭ f(A), so by definition of relation of semantic consequence 5.10,

(∗) Now, assume that I2 is not an empty set.

Since ℑ ∉ I2, then by definition 5.3 for each interpretation ℑ′ ∈ I2 there exists such formula B ∈ For that:

(a) ℑ′ ⊧ B and ℑ ⊭ B

or

(b) ℑ′ ⊭ B and ℑ ⊧ B.

Take any interpretation ℑ′ ∈ I2 and such formula B ∈ For that there occurs case (a) ℑ′ ⊧ B and ℑ ⊭ B. It is the case when and only when—by definition 5.3—(a)’ ℑ′ ⊭ f(B) and ℑ ⊧ f(B), thus there exists such formula C ∈ For that f(B) = C and (a)” ℑ′ ⊭ C and ℑ ⊧ C.

Now, we define set of formulas X ⊆ For as follows: for any formula A, AX iff there exists such interpretation ℑ′ ∈ I2 that ℑ′ ⊭ A and ℑ ⊧ A.

From (∗), (a)”, (b) it follows that set X is non-empty and for each interpretation ℑ′ ∈ I2, there exists such formula DX that ℑ′ ⊭ D. What is more, for each formula DX, ℑ ⊧ D, so ℑ ⊧ X.

Therefore, there does not exist such interpretation ℑ′ ∈ I2 that ℑ′ ⊧ X. From the above and from definition of relation of semantic consequence 5.10, we get that D, for any formula D ∈ For, since ℑ′ ⊭ X, for any interpretation of formulas ℑ′ ∈ I2.

While since ℑ⊧X, so ℑ ⊭f(E), for each EX, by definition 5.3. From the above and from definition of semantic consequence 5.10, for certain EX. And at the same time since D, for any formula D ∈ For, thus

Now, assume that I1 = I2. Then obviously

Remark 5.13. For our considerations, we adopt any, but fixed set of interpretations IXf. The set will remain unchanged until the end of this chapter. We will, on the other hand, refer to function f.

←160 | 161→

Remark 5.14. For our considerations, we adopt any, but fixed, semantically defined logic ⟨For,⊧⟩. Due to fact 5.12, since relation of consequence ⊧ determines exactly one set of interpretations of formulas IXf, we do not have to include a reference to set I in the notation. Logic ⟨For,⊧⟩ will remain unchanged until the end of this chapter. On the other hand, we will from time to time refer to the set of interpretations of formulas I determined by ⊧.

5.3Basic concepts of the tableau system

Now, we will define the set of conditions that should be satisfied by the tableau expressions.

Definition 5.15 (Tableau expressions). The set of tableau expressions will be called any set Te that meets the following conditions:

  1. there exists such injective function g ∶ For → P(Te) that for any formula A ∈ For, g(A) is a countable subset of set Te and for any formula B ∈ For, if AB, then g(A)∩g(B)=∅
  2. there exists at least one distinguished and finite set Te′ ⊆ Te such that for any subset X ⊆ For, if there exists interpretation of formulas ℑ ∈ I such that ℑ ⊧ X, then Te′ ⊈ ⋃{g(A) ∶ AX} (the set of all such distinguished sets will be specified as Tein).

The elements of set Te will be called tableau expressions or simply expressions.

Making use of condition 2 of definition of set of tableau expressions 5.15, we will now introduce the general concept of t-inconsistent set (and concept of t-consistent set).

Definition 5.16. Let Te be a set of tableau expressions and let Te′′ ⊆ Te. Set Te′′ will be called tableau inconsistent (for short: t-inconsistent) iff there exists such Te′ ∈ Tein that Te′ ⊆ Te′′. Set Te′′ will be called tableau consistent (for short: t-consistent) iff Te′′ is not t-inconsistent.

Remark 5.17. For any set of expressions Te we assume that the values of function g ∶ For → P(Te) are sets of indexed elements of set Te, i.e. for any formula A ∈ For, there exists such countable set {x1,x2,x3, . . .} ⊆ Te that g(A) = {x1,x2,x3, . . .}. At the same time, we do not assume that for any xi, xjg(A), if ij, then xixj. The numbers visible in the indices of tableau expressions x1,x2,x3, . . . will be called indices.

Remark 5.18. As we remember, in the case for CPL considered in the book, the set of expressions was identical to the set of formulas. In this case, we would adopt ←161 | 162→Te={AiA∈ ForCPL, i ∈ℕ}4. In a more complex case, i.e. TL, set {AiA∈ ForTL, i ∈ℕ}⊆Te. In both those cases, we associate a little artificially with each formula an infinite set of expressions that correspond to it, whereas for each formula A, if g(A) = {x1,x2,x3, . . .}, then for any indices i, j we would have: xi = xj.

In the case of S5 such association is more natural, as the elements of set along with indices {AiA ∈ ForS5, i ∈ℕ}⊆Te would correspond to the ordered couples ⟨A,i⟩ we use in the proofs.

In both latter cases (TL, S5), in order to obtain entire set Te we would have to still define additional auxiliary expressions. Our definition does not specify what these expressions would be, but in order to get a complete tableau system, they would have to meet further conditions that we will provide. This reservation also applies to the concept of an inconsistent set of expressions, which in some cases could even contain one element. This is the case in those systems where the branch containing certain expressions (considered to be inconsistent) is closed with a special sign by means of an additional rule or rules, e.g. × (refer for example [23]) and only then the branch is considered closed.

Ultimately, however, the role of these expressions which, through function g represent formulas in a tableau proof, could be fulfilled by any other symbols, not structurally (graphically) related to formulas, yet meeting the conditions from definition of set of tableau expressions 5.15.

New denotations will be useful for further work.

Denotation 5.19. Let us adopt the following denotations:

  • for any formula A ∈ For and any i ∈ℕ, Ai = xi iff xig(A)
  • for any subset X ⊆ For, X i = {AiAX}.

Remark 5.20. For our considerations, we adopt any, but fixed set of tableau expressions Te and included in Te at least one tableau contradictory set Te′. These arrangements will remain unchanged until the end of this chapter.

Remark 5.21. We also assume the option of inclusion in set Te of auxiliary expressions which correspond to expressions such as irj in case of the described tableau system for S5, or such as expressions Pi and P+i in case of the described tableau system for TL, for any i, j ∈ℕ and any name letter P ∈ Ln. The auxiliary expressions also feature indices.

Such expressions will be specified by means of set TeA, subset of Cartesian product {α1,α2,α3, . . .}× {β1, β2, β3, . . . }, where for any i,j ∈ℕ, if ⟨αi, βj,⟩ ∈ TeA, ←162 | 163→then βj is an ordered n-tuple ⟨k1,k2, . . . ,kn⟩ of indices present in that sequence in expression αi, for some n,k1,k2, . . . ,kn ∈ ℕ.

Set TeA ⊆ Te, moreover TeA may be empty, because the construction of tableau proof for a given logic may not require at all a richer set than what is required by definition 5.15, or its definition uses a different set of auxiliary expressions than TeA.

Definition 5.22 (Function selecting indices). Function selecting indices will be called function ∗∶ P(Te)→ P(ℕ) defined for any i,j ∈ ℕ with conditions:

  • for any formula A ∈ For, ∗({Ai}) = {i}
  • for any ⟨αi, βj⟩∈ TeA, ∗({⟨αi, βj⟩}) = {kk is an element of βj}
  • for any X ⊆ Te, if ∣X∣ > 1, then ∗(X) =⋃{∗({y}) ∶ yX}.

Therefore, for any subset of set {AiA ∈ For,i ∈ ℕ} ⊆ Te function ∗ selects all indices present in the expressions from that set.

We will now proceed to the general conditions that specify the relation of similarity between the sets of expressions, regardless of whether or not set TeA is non-empty and set Te contains any other specific auxiliary expressions. Therefore, in the definition of similarity we assume the condition of having the same cardinality.

Definition 5.23 (Similar set of expressions). Let X, Y ⊆ Te. We shall state that X is similar to Y iff:

  • X is t-consistent iff Y is t-consistent
  • X and Y have the same cardinality
  • there exists such bijection h ∶ ∗(X)→∗(Y) that:

for any formula A ∈ For and i ∈ℕ, AiX iff Ah(i)Y.

for any i,n,k1, k2, . . . , kn ∈ℕ, there exist such j ∈ ℕ, ⟨αi, βj⟩∈ TeA that ⟨αi, βj⟩ ∈ X and βj = ⟨k1, k2, . . . , kn⟩ iff there exist such l ∈ ℕ, ⟨αi, βl⟩ ∈ TeA that ⟨αi, βl⟩∈ Y and βl = ⟨h(k1), h(k2), . . . , h(kn)⟩.

From definition of similarity 5.23 the following conclusion results.

Corollary 5.24. Let X,YTe. If X is similar to Y, then Y is similar to X.

For further work, we need a definition of relation that occurs between interpretation of formulas ℑ and subset of tableau expressions {AiA ∈ For,i ∈ ℕ} ⊆ Te.

Definition 5.25. Let i ∈ℕ. By⊩i we mean any such relation specified on Cartesian product I ×For that for any formula A ∈ For and any interpretation ℑ ∈ I:

←163 | 164→
  • if ℑ ⊧ A, then ℑ ⊩i A.
  • ℑ ⊩i A iff it is not the case that ℑ ⊩i f(A) (for short: ℑ /⊩i A).
  • if for certain j ∈ ℕ, ℑ ⊩j A, then ℑ ⊩i A.

By ⊩ we will mean set {⟨ℑ,A⟩ ∶ ℑ ∈ I,A ∈ For and for some i ∈ ℕ ℑ ⊩i A}.

Remark 5.26. For our considerations, we adopt any, but fixed relation ⊩. It will remain unchanged until the end of this chapter.

Remark 5.27. Intuitively, relation ⊩is in a sense expansion of relation ⊧ onto set of tableau expressions {AiA ∈ For,i ∈ ℕ}⊆ Te. We used “in a sense”, because in the cases of CPL and TL we can identify it with relation ⊧, as for each formula A, of one of these logics, Ai =A, for any i ∈ ℕ. On the other hand, in the event of modal logic (e.g. S5), notation ℑ ⊩i A may indicate that if based on model 𝔐, that we identify with interpretation ℑ, we construct model 𝔐′, where the distinguished world will be corresponded by index i, then 𝔐′ ⊧ A.

We will now specify the general conditions describing the interpretation appropriate for set of expressions.

Definition 5.28 (Interpretation appropriate for set of expressions). Let ℑ ∈ I be an interpretation, and let X ⊆ Te be a set of tableau expressions. We shall state that interpretation ℑ is appropriate for set X iff:

  1. X is t-consistent
  2. for any i ∈ ℕ and any A ∈ For, if AiX, then ℑ ⊩i A.

5.4Tableau rules

Now, we will proceed to the conditions that should be satisfied by the tableau rules. So, let us define the general concept of rule.

Definition 5.29 (Rule). Assume that P(Te) is a set of all subsets of set Te. Let P(Te)n be n-element of Cartesian product for some n ∈ ℕ, whereas ⋃n∈N P(Te)n be a union of all n-ary products such that n ≥ 2.

Rule will be called any subset R ⊆ ⋃n∈N P(Te)n such that if ⟨X1, . . . ,Xn⟩∈ R, then the following conditions are satisfied:

X1Xi, for any 1 < in

X1 is a t-consistent set

ifkl, then XkXl, for any 1 < k,ln

(Closure under similarity) for any set of expressions Y1 such that Y1 is similar to X1, there exist such sets of expressions Y2, . . . , Yn that ⟨Y1, . . . , Yn⟩∈ R and for any 1 < in, Yi is similar to Xi

←164 | 165→

– (Existence of core of rule) for some finite set YX1 there exists ordered n-tuple ⟨Z1, . . . , Zn⟩∈ R such that:

  1. Z1 = Y
  2. for any 1 < in, Zi = Z1 ∪(XiX1)
  3. there does not exist proper subset U1Y and n-tuple ⟨U1, . . . , Un⟩∈ R

(Closure under expansion) for any t-consistent set of expressions Z1, such that X1Z1 and for each 1 < in, Xi is not similar to any subset Z1 containing X1, there exist such set of expressions Z2, . . . , Zn that ⟨Z1, . . . , Zn⟩∈ R and for any 1 < in, Xi is similar to X1 ∪(ZiZ1)

(Closure under finite sets) if X1 is a finite set, then for each 1 < in, Xi is a finite set

(Closure under subsets) for any subset X′ ⊆X1, if for certain set YX1 there exists such n-tuple ⟨W1, . . . , Wn⟩ ∈ R that:

  1. W1 = Y
  2. for any 1 < in,Wi =W1 ∪(XiX1)
  3. W1X

then there exist such sets of expressions Z1, . . . , Zn that:

  1. Z1, . . . , Zn⟩∈ R
  2. Z1 = X
  3. for any 1 < in, Zi = Z1 ∪(XiX1).
  4. • We shall state that rule R has been applied to set X1 iff for certain 1 < in, exactly one set Xi was selected from certain n-tuple ⟨X1, . . . ,Xn⟩ ∈ R.

Remark 5.30. Note that the general concept of rule we have introduced with definition 5.29, is in a way less general than the general concepts of rules used in the previous chapters—since we have added several additional conditions that were not present before. For we will not use a specific set of rules in further proofs, but we will define another conditions that should be jointly met by the set of tableau rules selected for axiomatization of the tableau system.

However, in some respects, definition 5.29 is more general than the definitions of rules in the previous chapters. In those cases, the rule was to be a subset of Cartesian product RP(Te)n, where n ≥ 2. And here, the rule is defined as a subset of the union under Cartesian products R ⊆ ⋃n∈N P(Te)n, where n ≥ 2. Of course, the rules that meet the first condition also meet the second one. The more general condition was provided for a number of reasons.

First of all, even in the case of structural definition of tableau rules—as we have done so far—there may be a situation in which ordered pairs of different numbers of elements belong to a single rule. An example is a logic with relating connectives, in which we sometimes have to describe relationships between propositional ←165 | 166→letters when distributing expressions in tableaux. In this case, the number of elements in a given n-tuple may depend on the number of propositional letters in a given formula.5

Secondly, even if we define the tableau rules structurally, it is also possible to define them for some system in a more complex way. We could, for example, sum up some (or even all) of the rules described in the chapter on the tableau system for CPL, to get for instance rule R′ = R¬¬R. That rule would consist of two types of n-tuples: ordered pairs and ordered triples.

Finally, we can build tableau systems for non-classical reasoning (inferences), in which we draw conclusions in a non-deductive way. In such systems, there may occur a need for unstructured definition of tableau rules, e.g. in such a way that from a given structurally described set of premises it is possible to move in the tableau to one or more branches, depending on which subformulas the premises are composed of. Excluding certain conditions from definition 5.29, that definition may be useful in such cases.

We will now frame a general definition of the core of rule in a given set.

Definition 5.31 (Core of rule). Let R be a rule and n ∈ ℕ. Let ⟨X1, . . . ,Xn⟩ ∈ R and ⟨Z1, . . . ,Zn⟩ ∈ R. We shall state that ⟨Z1, . . . , Zn⟩∈ R is a core of rule R in setX1, . . . ,Xn⟩ iff

  1. Z1X1
  2. there do not exist proper subset U1Z1 and n-tuple ⟨U1, . . . ,Un⟩ such that ⟨U1, . . . ,Un⟩∈ R and UiU1 = ZiZ1, for any 1 < in
  3. for any 1 < in, Zi = Z1 ∪(XiX1).

By definition of rule 5.29 (Existence of core of rule), we get the following conclusion.

←166 | 167→

Corollary 5.32. Let R be a rule and n ∈ ℕ. If n-tupleX1, . . ., Xn⟩∈ R, then there exists n-tupleY1, . . . ,Yn⟩ ∈ R such thatY1, . . . ,Ynis the core of rule R in setX1, . . . ,Xn.

We will now define two additional technical concepts that will allow us to frame a general definition of a set of tableau rules.

Let X ⊆ Te be a set of tableau expressions and let R be a set of rules. By RX we will mean a set of all and only such rules from set R that are applicable to set X. Formally, RRX iff RR and there exists such n-tuple ⟨Y1, . . . ,Yn⟩∈ R that Y1 =X.

Let RRX, by RX we will mean a set of all and only such n-tuples from R that their first element equals X, and if some of the remaining elements of two n-tuples that belong to RX differ, then these two n-tuples have different input sets of the core of rule. Formally, for any n ∈ ℕ, ⟨Y1, . . . ,Yn⟩ ∈ RX iff:

  • Y1, . . . ,Yn⟩ ∈ R and Y1 = X
  • for any set of expressions Z1, . . . , Zn, if:

Z1, . . . ,Zn⟩ ∈ RX

Y1, . . . ,Yn⟩ ≠ ⟨Z1, . . . ,Zn

is the core of rule R in set ⟨Y1, . . . ,Yn

is the core of rule R in set ⟨Z1, . . . ,Zn

then

The limitations in the definition of set RX are the results of the fact that some rules, e.g. R in the described tableau system for S5, may introduce completely new expressions that are absent in any form in the previous portions of the proof.

In the case of rule R, we can introduce to the branch some set {⟨A,i⟩,irj}, where A ∈ ForS5 and i,j ∈ ℕ, selected from among many such sets. Usually, there exist multiple such n-tuples that belong to R which are applicable to set X, if ⟨◇A,i⟩ ∈ X, after even one application we cannot apply rule R to set X anymore due to expression ⟨◇A,i⟩ ∈ X, because of the limitations in the application of this rule (see example 4.24). So, we want set RX to include only one such n-tuple, since we can only use one.

With the above concepts, we can proceed to the definition of set of tableau rules.