# 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.

# 6.2.7 Estimation of cardinality of model for MTL

We have eight rules for formulaswithmodal functors. However, we will restrict our considerations to four cases as they are analogous in terms of application. So, take ●∈ {◻,◇}.

- Let R = , then ⟨X,Y⟩ = ⟨Z∪{Pa●Q, P+i}, Z∪{Pa●Q, P+i, }⟩, for some Z ⊆ TeMTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, 𝔐MTL ⊧ Pa●Q and there exists function γ ∶ ℕ → D i.a. such that for each name letter S ∈ Ln and each j ∈ ℕ: if S+j ∈ X, then γ(j) ∈ d(S) and if ∈ X, then γ(j) ∈ d●(S); due to the fact that P+i ∈ X, also γ(i) ∈ d(P), while since 𝔐MTL ⊧ Pa●Q, hence by definition of truth in model 6.5, γ(i) ∈ d●(Q), since d(P) ⊆ d●(Q); consequently, by definition of model appropriate for the set of expressions 6.22,model𝔐MTL is appropriate for set of expressions Y = Z ∪{Pa●Q,P+i,}.
- Let R = Ri●, then ⟨X,Y⟩ = ⟨Z ∪ {Pi●Q},Z ∪ {Pi●Q, P+i, ⟩, for some Z ⊆ TeMTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, 𝔐MTL ⊧ Pi●Q and there exists function γ ∶ ℕ → D i.a. such that for each name letter S ∈ Ln and each j ∈ ℕ: if S+j ∈ X, then γ(j) ∈ d(S) and if ∈ X, then γ(j) ∈ d●(S); however, rule Ri● enriches set X with expressions P+i,and index i is new, it has not occurred in any of expressions from set X, while since 𝔐MTL ⊧ Pi●Q, so by definition of truth in model 6.5, in the domain there exists certain object x such that x ∈ d(P)∩d●(Q); we define function γ′ ∶ ℕ → D such that for any k ∈ ℕ, if k ≠ i, then γ′(k) = γ(k) and γ′(i) = x, consequently, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL is appropriate for set of expressions Y = Z∪{Pi●Q,P+i,}.
- Let R = Re−●, then ⟨X,Y⟩ = ⟨Z ∪{Pe●Q,P+i},Z ∪{Pe●Q, P+i, }⟩, for some Z ⊆ TeMTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, 𝔐MTL ⊧ Pe●Q and there exists function γ ∶ ℕ → D such that i.a. for each name letter S ∈ Ln and each j ∈ ℕ: if S+j ∈ X, then γ(j) ∈ d(S) and if ∈ X, then γ(j) ∉ d●'(S); due to the fact that P+i ∈ X, also γ(i) ∈ d(P), while since 𝔐MTL ⊧ Pe●Q, hence by definition of truth in model 6.5 γ(i) ∉ d●'(Q), since d(P) ∩ d●'(Q) = ∅; consequently, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL isappropriate for set of expressions Y = Z ∪{Pe●Q,P+i,}.
- Let R = Ro●, then ⟨X,Y⟩ = ⟨Z ∪{Po●Q},Z ∪{Po●Q,P+i, }⟩, for some Z ⊆ TeMTL, P,Q∈ Ln and i ∈ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22,𝔐MTL ⊧Po●Q and there exists function γ ∶ℕ→ Dsuch that for each name letter S ∈ Ln and each j ∈ℕ: if S+j ∈ X, then γ(j)∈ d(S) and if ∈ X, then γ(j) ∉ d●'(S); however, rule Ro● enriches set X with expressions ←204 | 205→P+i,and index i is new, it has not occurred in any expression from set X, while since 𝔐MTL ⊧ Po●Q, so by definition of truth in model 6.5, in thedomain there exists certain object x such that x ∈ d(P), but x ∉ d●'(Q); we define function γ′ ∶ℕ→ D such that for any k ∈ℕ, if k ≠ i, then γ′(k) = γ(k) and γ′(i) = x, consequently, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL is appropriate for set of expressions Y = Z∪{Po●Q,P+i,}.

We have four cases for the bridging rules.

- Let R = , then ⟨X,Y⟩ = ⟨Z ∪{}, Z ∪{,P+i}⟩, for some Z ⊆ TeMTL, P ∈ Ln and i ∈ ℕ; since model 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, there exists function γ ∶ℕ→ D such that γ(i) ∈ d◻(P); furthermore d◻(P)⊆d(P), by definition of model 6.3, so γ(i) ∈ d(P); thus, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL is appropriate for set of expressions Y = Z∪{,P+i}.
- Let R = R+, then ⟨X,Y⟩ = ⟨Z ∪{P+i}, Z ∪{P+i,}⟩, for some Z ⊆ TeMTL, P ∈ Ln and i ∈ ℕ; since model 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, there exists function γ ∶ ℕ → D such that γ(i) ∈ d(P); furthermore d(P)⊆d◇(P), by definition of model 6.3, so γ(i) ∈ d◇(P); thus, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL is appropriate for set of expressions Y = Z ∪{P+i,}.
- Let , then ⟨X,Y⟩ = ⟨Z∪{}, Z∪{,P−i}⟩, for some Z ⊆ TeMTL, P ∈ Ln and i ∈ ℕ; since model 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, there exists function γ ∶ ℕ → D such that γ(i) ∉ d◇(P); furthermore d(P)⊆d◇(P), by definition of model 6.3, so γ(i) ∉ d(P); thus, by definition of model appropriate for the set of expressions 6.22, model 𝔐MTL is appropriate for set of expressions Y = Z ∪{,P−i}.
- Let R = R−, then ⟨X,Y⟩ = ⟨Z ∪{P−i}, Z ∪{P−i,}⟩, for some Z ⊆ TeMTL, P ∈ Ln and i ∈ ℕ; since model 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, there exists function γ ∶ ℕ → D such that γ(i) ∉ d(P); furthermore d◻(P) ⊆ d(P), by definition of model 6.3, so γ(i) ∉ d◻(P); thus, by definition of model appropriate for the set of expressions 6.22,model 𝔐MTL is appropriate for set of expressions Y = Z∪{P−i,}.

From lemma 6.30 and definition 5.59 applied to set of tableau rules RMTL we get a conclusion.

←205 | 206→Corollary 6.31. Set of tableau rules RMTL is good for set of models for the language of MTL.

Applying both conclusions: 6.29 and 6.31, concepts defined in this chapter and general tableau theorem5.62, from the previous chapter, we get the completeness theorem for system of MTL.

Theorem 6.32 (Completeness theorem for MTL). For any set X ⊆ ForMTL and any formula A ∈ ForMTL the following statements are equivalent:

- X ⊧ A
- X ⊳ A
- there exists finite set Y ⊆ X and closed tableau ⟨Y,A,Φ⟩

Thus, we have shown how — with application of the general tableau concepts —we can shorten the proof of completeness theorem to the appropriate definition of specific concepts and application of the general theorem.

### 6.2.7Estimation of cardinality of model for MTL

When applying the tableau methods to TL we received a possibility of estimation of the limitation of cardinality of models that can be countermodels for the considered inference (theorem3.57). The situation is similar in the case of system for MTL. We can get an identical outcome nearly directly from the completeness theorem of the tableau system for MTL, carrying out a proof analogous to the one for theorem 3.57.

By existential formula, we mean any formula in form PiQ, PoQ, Pi●Q, Po●Q , where P, Q, ∈ Ln and ●∈ {◻,◇}.

Next, we define function λ′∶P(ForTL)→ P(ForTL) with the following condition: for any set Φ∈ P(ForTL), λ′(Φ) = {x ∈Φ∶ x is an existential formula}. So, from each set of rules, function λ′ “selects” all existential formulas that belong to a given set.

Now, in turn, we shall specify function σ∶{Ψ ∈ P(ForTL)∶ Ψ is a finite set}→ ℕ with the following condition: for any finite set Ψ ∈ P(ForTL), σ′(Ψ) = ∣λ′(Ψ)∣. So, function σ′ “counts” the number of existential formulas that are found in any finite set of formulas.

With the use of the defined functions, we can frame the following theorem.

Theorem 6.33. Let X be a finite set of formulas and let A∈ ForMTL. Then, the below statements are equivalent:

- for any model 𝔐MTL = ⟨D,d◻,d,d◇⟩, if ∣D∣ = σ′(X ∪{○(A)}) and 𝔐MTL ⊧ X, then𝔐MTL ⊧ A
- X ⊧ A.

## 6.3Tableau systems for modal logics

In this subchapter, we will investigate the application of the theory of tableau systems we covered in Chapter Five to the general case. We will show how to apply the general concepts described previously to construct tableau systems for modal logics determined by models with possible worlds.

By using general concepts, we will provide the conditions whose occurrence demonstration is sufficient to get a complete tableau system for a given modal logic.5

### 6.3.1Language and semantics

We adopt the set of formulas for modal logic defined in one of the previous chapters with definition 4.2 for logic S5. We will denote that set as ForML.

Next, we adopt the general concept of model with possible worlds 𝔐ML, in accordance with definition of model 4.5 for logic S5 — with any relation of accessibility. We will denote the set of all such models as M.

We define the concept of truth (and falsehood) of formula in model, analogously to definition 4.7.

According to definition 5.8, each model 𝔐ML ∈ Mcan be identified with interpretation of formulas as for function f ∶ ForML → ForML defined with condition f(A) = ¬A, for any A ∈ ForML it is the case that A ∈ {B ∈ ForML ∶𝔐ML ⊧ B} iff f(A) ∉ {B ∈ ForML ∶𝔐ML ⊧ B}.

Taking any subset M′ ⊆ M, we conventionally define relation of semantic consequence ⊧M' . Based on that relation, we semantically define modal logic ⟨ForML,⊧M' ⟩.

### 6.3.2Tableau expressions

Now, we will proceed to the issue of expressions representing formulas and other properties in the tableau proof.

First, we define the set of expressions. Next, we will show that it meets the general conditions imposed on the set of tableau expressions (definition 5.15).

Definition 6.34 (Expressions). Set of expressions Ex is a set that is the union of the below sets:

←207 | 208→- ForML ×ℕ
- {irj ∶ i,j ∈ ℕ}
- {∼ irj ∶ i,j ∈ ℕ}
- {i = j ∶ i,j ∈ ℕ}
- {∼ i = j ∶ i,j ∈ ℕ}.

The elements of set ℕ are called indices.

Remark 6.35. New types of expressions appeared in the set of expressions, which in the proof correspond to the negation of relation occurrence, the identity and negation of identity. They are not needed in all constructed systems, but in some systems they will be used by the tableau rules.

We can define the following function g ∶ ForML → P(Ex), for any A ∈ ForML, g(A) = {⟨A,i⟩ ∶ i ∈ ℕ}. Function g has important properties, for any two formulas A, B: A ≠ B iff g(A)∩g(B)=∅, and g(A) is a countable subset of set Ex.

Note, furthermore, that each expression ⟨A,i⟩ can be identified with expression Ai, which corresponds to function g from general definition of tableau expressions 5.15.

Definition 6.36. Let X ⊆ Ex. We shall state that X is tableau inonsistent (for short: t-inconsistent) iff for some A ∈ ForML, i,j ∈ℕ at least one of the below conditions is met:

- ⟨A,i⟩, ⟨¬A,i⟩ ∈ X
- irj, ∼ irj ∈ X
- i = j, ∼ i = j ∈ X.

We shall state that X is tableau consistent (for short: t-consistent) iff it is not tableau inconsistent.

From definition 6.36 results the following conclusion.

Corollary 6.37. LetX ⊆ForML and 𝔐ML ∈ M. If 𝔐ML ⊧X, then {xi ∶ xi ∈ g(A),A∈ X} is a t-consistent set.

By virtue of definition of expressions 6.34, definition 6.36, existence of function g, conclusion 6.37 and general definition of tableau expressions 5.15, we can assume that set of expressions Ex is a set of tableau expressions. The set will be denoted as TeML.

Now, we will define more auxiliary concepts.

Definition 6.38 (Function selecting indices). Function ∗∶ P(TeML)→ P(ℕ) is a function selecting indices iff for any A ∈ ForML, i,j ∈ ℕ and X ⊆ TeML the below conditions are met:

←208 | 209→- ∗({⟨A,i⟩}) = {i}
- ∗({irj}) = {i,j}
- ∗({∼ irj}) = {i,j}
- ∗({i = j}) = {i,j}
- ∗({∼ i = j}) = {i,j}
- if ∣X∣ > 1, then ∗(X) =⋃{∗({x}) ∶ x ∈ X}.

For any subset Y of set of expressions TeML function ∗ selects all indices present in Y.

Now, we will define binary relation ≡ specified on Cartesian product P(TeML)×P(TeML), that will correspond to the general definition of similarity of sets of expressions (5.23).

Definition 6.39. Let X, Y ⊆ TeML. We define relation ≡ with condition: X ≡ Y iff there exists bijection h ∶ ∗(X)→∗(Y) (where ∗(X), ∗(Y) are sets of indices present in the expressions from X and from Y) such that for anyA∈ ForML, i,j ∈ℕ:

- ⟨A,i⟩ ∈ X iff ⟨A,h(i)⟩ ∈ Y
- irj ∈ X iff h(i)rh(j) ∈ Y
- ∼ irj ∈ X iff ∼ h(i)rh(j) ∈ Y
- i = j ∈ X iff h(i) = h(j) ∈ Y
- ∼ i = j ∈ X iff ∼ h(i) = h(j) ∈ Y.

From definition 6.39 results the following conclusion.

Corollary 6.40. Let X, Y ⊆ TeML. If X ≡ Y, then:

• X is t-consistent iff Y is t-consistent

• sets X and Y have the same cardinality.

By virtue of conclusion 6.40 and definition of relation ≡ 6.39 we claim that relation ≡meets the conditions of general definition of similarity of sets of expressions 5.23.

We will now define the concept that describe the relation between the models and sets of expressions.

Definition 6.41. Let 𝔐ML = ⟨W,Q,V,w⟩ and X ⊆TeML. We shall state that model 𝔐ML is appropriate for set of expressions X iff there exists such function γ ∶ℕ→ W, that for any A ∈ ForML, i,j ∈ ℕ the following conditions occur:

←209 | 210→- if ⟨A,i⟩ ∈ X, then ⟨W,Q,V,γ(i)⟩ ⊧ A
- if irj ∈ X, then γ(i)Qγ(j)
- if ∼ irj ∈ X, then it is not the case that γ(i)Qγ(j)
- if i = j ∈ X, then γ(i) is identical to γ(j)
- if ∼ i = j ∈ X, then γ(i) is different from γ(j).

From definition of tableau inconsistent set of expressions 6.36 and definition of model appropriate for set of expressions 6.41 the following conclusion results.

Corollary 6.42. For any set of expressions X ⊆ TeML, if X is t-inconsistent, then there exists no model 𝔐ML appropriate for X.

Note that relation ⊧ defined by any subset M′ ⊆ M meets the conditions of relation ⊩(definition 5.25).Thus, by conclusion 6.42 and definition of appropriate model 6.41 we get a fact.

Proposition 6.43. The notion of model appropriate for set of expressions meets the general conditions of interpretation appropriate for set of expressions described in definition 5.25.

Thus, we have demonstrated that the presented concepts for the modal logics, determined with the semantics of possible worlds, are special cases of the general concepts described in the previous chapter.

### 6.3.3Rules, branches and tableaux for modal logics

First, we will adopt the concept of tableau rule, originating by the application of concept of tableau expression TeML and other presented concepts for modal logics to the general concept of rule 5.29 and general concept of tableau rule 5.33. Set of tableau rules for a given modal logic will be denoted as RML.

Furthermore, we adopt all general definitions from the previous chapter:

• branch 5.35

• closed/open branch 5.39

• maximal branch 5.42

• tableau 5.48

• complete tableau 5.50

• closed/open tableau 5.51

• branch consequence 5.46

assuming that these concepts are always dependent on some fixed set of tableau rules RML for a given modal logic.

### 6.3.4Generating of model

As we mentioned in the previous chapter, in remark 5.54, it is difficult to establish a general method for transition from the maximal and open branch to the generated model. For we do not know how the model is constructed and what types of ←210 | 211→expressions are used in the proof which leads to the maximal and open branch. Nonetheless, for a single logic it is possible — we did so in the case of a tableau system for MTL.

We can try to do the same in the case discussed, i.e. in relation to certain class of logics which in many respects are similar. The definition provided below is quite broad and on its basis we can define many types of models for modal logics determined by the semantics of possible worlds. For we have the general concept of model and the concept of set of tableau expressions TeML which determines the range and elements used to define the model.

Definition 6.44 (Branch generating model). Let RML be a set of tableau rules and ϕ be RML-branch. Let X = {⟨A,k⟩ ∶ A ∈ Y} ⊆ ⋃ϕ, for some k ∈ ℕ and non-empty subset Y ⊆ ForML. We define set AT(ϕ) as follows: x ∈ AT(ϕ) iff one of the below conditions occurs

- x ∈⋃ϕ∩({irj ∶ i,j ∈ ℕ}∪{i = j ∶ i,j ∈ ℕ})
- x ∈⋃ϕ∩(Var×ℕ).

We shall state that branch ϕ generates model 𝔐ML = ⟨W,Q,V,w⟩ iff

• W is a maximal subset of set {i ∶ i ∈ ∗(AT(ϕ))} such that:

a. for any i,j ∈ ℕ, if i = j ∈ AT(ϕ), then i ∉W or j ∉W

b. k ∈ W

• for any i,j ∈ ℕ

a. ⟨i,j⟩ ∈ Q iff irj ∈ AT(ϕ) and i,j ∈ W

b. V(x,i) = 1 iff ⟨x,i⟩ ∈ AT(ϕ) and i ∈ W

• w = k.

Remark 6.45. In definition of branch generating model 6.44, the domain of model W was specified i.a. as follows: W is a maximal subset of set {i ∶ i ∈ ∗(AT(ϕ))} such that for any i,j ∈ℕ, if i = j ∈ AT(ϕ), then i ∉Wor j ∉W. Model generated by an open and maximal branch consists of indices included in the tableau expressions. In the event when the branch contains expression i = j, for some i,j ∈ ℕ, we must select one of the indices that belong to ∗({i = j}), since expression i = j is expected to state that it is about the same object in the domain.

Definition 6.44 obviously meets the general conditions of the definition of branch generating interpretation, since by virtue of the next conclusion, each open and maximal branch can be assigned a model.

Corollary 6.46. Let RML be a set of tableau rules. Let ϕ be an open and maximal RML-branch and let X ={⟨A,k⟩ ∶A∈ Y}⊆⋃ϕ, for some k ∈ℕ and non-empty subset Y ⊆ ForML. Then there exists model 𝔐ML such that branch ϕ generates 𝔐ML. ←211 | 212→Proof. We get that conclusion from definition of open branch 5.39 applied to the modal tableau rules and definition of branch generating model 6.46.

So, checking for a given set of tableau rules RML and given class of models M′ ⊆M, if set M′ is good for set of rules RML, does not require demonstration of the existence of model. We only have to — in accordance with definition 5.55 — demonstrate that in the generated model true are those formulas whose equivalents belonged to the branch and were used for the definition of model and that this model belongs to set M′.

### 6.3.5Completeness theorem of tableau systems for modal logics

We will now verbalize a general theorem on completeness of tableau systems for modal logics defined with the semantics of possible worlds.

Applying the general definitions of set of interpretations good for set of rules 5.55 and set of rules good for set of interpretations 5.59, the concepts defined in this chapter and general tableau theorem 5.62 we proved in the previous chapter, we obtain a general theorem on completeness for modal logics of defined with the semantics of possible worlds.

In order to frame the theorem, let us assume that for any set of models M′ ⊆M and any set of tableau rules RML notation X ⊧M' A means relation ⊧ defined by set of models M′, whereas notation A means relation ⊳ defined by set of tableau rules RML. Similarly, when writing RML-tableau ⟨Y,A,Φ⟩, we mean that tableau ⟨Y,A,Φ⟩ and branches that belong to set of branches Φ originated merely by the application of rules from set RML to the expressions from set TeML.

Let us proceed to the theorem.

Theorem6.47. LetM′ ⊆Mbe a set of models. Let RML be a set of tableau rules. If:

- set M′ is good for set of rules RML
- set RML is good for set of models M′,

then for any set X ⊆ ForML and any formula A ∈ ForML the following statements are equivalent:

- X ⊧M' A
- there exists such finite set Y that Y ⊆X and closed RML-tableau ⟨Y,A,Φ⟩.

Theorem 6.47 reduces the constitution of complete tableau system for modal logic defined by the semantics of possible worlds to the demonstration of two facts that form the assumptions of this theorem. So, with the established set of models M′ we must define the set of tableau rules so RML as to these two facts ←212 | 213→occur. Analogously, we may start from set of tableau rules RML and specify subset M′ ⊆Mof all models with possible worlds so as to the theorem assumptions occur. In both cases we will get a complete tableau system.

## 6.4Tableau system

In this study, we have often used term tableau system, even though the emphasis was on the concept of tableau and branch consequence. Ultimately, however, it is the tableau system that constitutes the tableau recognition of given logic. Therefore, we will now try to clarify the concept of tableau system.

By a tableau system we may mean pair ⟨For,⊳R⟩, where For is a set of formulas of given logic, Rset of tableau rules, whereas ⊳ is a relation of branch consequence, defined based on the set of all maximal R-branches.

Such approach of the tableau system indirectly contains all concepts we have defined when constructing relation ⊳. To define the relation of branch consequence, it takes i.a. the concept of tableau expressions, t-inconsistent set, concept of tableau rules, description of relationship between the formulas and tableau expressions as well as the concepts of open/ closed and maximal branches.

The concept of tableau and its various variants (open/closed tableau, complete/incomplete tableau) can be, in turn, regarded as an apprehension of the method for choosing a relatively small subset of set of branches that allows to determine the occurrence of relation of branch consequence ⊳.

The concepts presented here enable the investigation of the relationships between different tableau systems defined by the method described, e.g. related to the questions about the dependency of sets of tableau rules or to the economics of sets system construction in general. For example, using the modification of the proof of the general completeness theorem 5.62 (for one set of tableau rules, considering the implication (a), and for another, considering the implications (b) and (c)), we can frame a theorem on the relationships between the tableau systems.

Theorem 6.48. Let ⟨For,⊧M⟩ be a logic semantically defined with set of interpretations M. Let ⟨For,⊳R⟩ and ⟨For,⊳R’⟩ be tableau systems. If:

- set M is good for set of rules R’
- set R is good for set of interpretations M

then for any set of formulas X ⊆ For and any formula A ∈ For, if X ⊳R A, then X ⊳R’ A.

Note that sets of tableau rules R and R’ can be defined on completely different sets of tableau expressions, using different auxiliary concepts, so that the rules they include can be directly incomparable. But comparing their deductive power ←213 | 214→can be done by checking the dependencies between the sets of tableau rules and the set of interpretations M.

## 6.5Transition from the formalized tableaux to the standard tableaux

The last issue we will be dealing with is the problem of the relationship between the concepts presented in the book — the concept of branch and the concept of tableau—and the conventionally comprehended tableaux.

We discuss this problem in the part devoted to the application of the theory of tableaux, guided by the belief that standard tableaux are a practical application of abstract concepts.6

However, since in most cases tableaux and tableau systems are presented primarily in graphic form, our goal was to create a formalization, and thus the theory of tableaux, independent of the tableaux comprehended in this way. The theory described here is precisely an abstract approach to the tableau methods for which the standard tableaux can be considered as applications.

Take any tableau system ⟨For,⊳R⟩, where For is a set of formulas, whereas R is a set of tableau rules. From general definition of tableau rules 5.33, it follows that the set of rules R is associated to a minimal set of tableau expressions Te which was used for the definition of rules from set R.

Consider any branch created by the application of rules from set R. In accordance with general definition of branch 5.35, that branch is a certain injective function ϕ ∶K → P(Te), where K =ℕ or K ={1,2,3, . . . ,n}, for some n ∈ ℕ, while P(Te) is a set of all subsets of the set of tableau expressions.

We will now define an intuitive branch that will correspond to branch ϕ. Let M be linearly ordered by relation ≤M set of points such that there exists bijection α ∶ K → M that meets condition α(i) ≤M α(j), if i ≤ j, for any i,j ∈ K.

Now, we define function ϕ′ ∶M → P(Te) from the set of points into the set of all subsets of the set of tableau expressions by the following condition for any i ∈ M:

- ϕ′(i) = ϕ(1), if α−1(i) = 1
- ϕ′(i) = ϕ(n)∖ϕ(n−1), if α−1(i) = n and n > 1, for any n ∈ K.

Function ϕ′ specifies a linearly ordered set of points in which each point has a certain subset Te assigned. Anyway, point α(1) has assigned entire set ϕ(1) from ←214 | 215→branch ϕ — the literature usually refers to that point as root — while the other points have assigned sets of elements that make up the difference between the elements of branch ϕ and their immediate predecessors.

In this way, we can assign to each branch ϕ at least one branch ϕ′, with some established domain—set of points M linearly ordered by relation ≤M.

Example 6.49. Take set of tableau expressions {⟨◇p,1⟩, ⟨◇(p ∧ q),1⟩, ⟨¬¬q,1⟩}. Applying rules from RS5 in the order described on left hand side, we get the following branch which will be defined as ψ.

Transition from branch ϕ to function ϕ′ will be called a branch translation or simply translation. If function ϕ′ ∶ M→ P(Te) is a translation, then notation ϕ′M indicates domain of ϕ′.

The result of certain translation ϕ′ will be presented in the graphs below. Example 6.49 described branch ψ. Now, if we carry out the translation of branch ψ, then we can get the following graph presenting branch ψ′. This time—unlike so far — we will put the application of the rule on the right hand side and next to the points of branch that resulted from the application of given rule.

And if we remove the numbering, brackets of sets and brackets from the tableau expressions, and in lieu of numbers we will insert points ●, then we will get a graph of branch ψ′ corresponding to the graphs usually used to present branches.

←215 | 216→So we can see that we can move from the branch defined in our theory — the formalized branch — to the standard branch, and the other way round — from the intuitive branch to the formalized branch. However, moving in the other direction requires a more precise determination of what a branch is, as well as determination of what the tableau rules are. Nonetheless, these issues are clarified by the theory that has just been presented — so it is easier to apply the general concepts in practice.

Since we already have a certain method of applying the general concept of branch in practice, we can now describe the transition from formalized tableaux to standard ones.

We are still considering an arbitrary tableau system ⟨For,⊳R⟩—where For is a set of formulas, while R is a set of tableau rules—and set of tableau expressions Te on which the tableau rules from set R were defined.

Consider tableau ⟨X,A,Φ⟩, where X ⊆ For, A ∈ For, whereas Φ is a set of branches—in accordance with general definition of tableau 5.48.

Based on set Φ we can define sets that only include translations of branches from set Φ — one for each branch from Φ. We impose condition: (∗) Ψ is such set of translations of branches from Φ that for each branch ϕ ∈ Φ, Ψ contains precisely one translation of ϕ. Since for each branch ϕ ∈ Φ, Ψ contains precisely one translation of ϕ, so the translation of branch ϕ in given set Ψ will be denoted as ϕ′.

Among the sets that meet condition (∗) there is at least one such set Φ′ that the distribution of points and assigned in the translations included in set Φ′ sets of expressions corresponds to the distribution of differences between the consequents and antecedents in the relevant branches contained in Φ as well as the inclusion of sub-branches of some branches in another ones.

We can carry out the following action on set Φ′. Define set ⟨Φ′′,≤Φ" ⟩:

- Φ′′ =⋃Φ′
- ⟨n,X⟩ ≤Φ" ⟨k,Y⟩ iff there exists such translation ∈ Φ′ that n,k ∈ M, (n) = X, (k) = Y and n ≤M k.

In set Φ′′ there exists an element which is the smallest in terms of relation ≤Φ" — that element is included in a set that is identical to the first element of each branch that belongs to set of branches Φ, i.e. the first step in the proof of fact that X ⊳ A.

Set ⟨Φ′′,≤Φ" ⟩ is an application of the definition of abstract concept of tableau ⟨X,A,Φ⟩. In this way, to each tableau ⟨X,A,Φ⟩ we can assign at least one tableau ⟨Φ′′,≤Φ" ⟩.

←216 | 217→The transition from tableau ⟨X,A,Φ⟩ to tableau ⟨Φ′′,≤Φ" ⟩ will be called tableau translation or simply translation.

Here is an example. Again, consider set of tableau rules RS5 described in Chapter Four.

Example 6.50. Consider the following set of expressions {⟨(r ∨ q),1⟩, ⟨¬¬p,1⟩, ⟨(◇p∧q),1⟩}. By the use of rule R∨, and then on left hand side—rules R¬¬ and R ∧, and on the right have side—rules R¬¬, we get the following branches.

In the light of definition of tableau 4.47, the set of these two branches is a tableau for pair ⟨{(r ∨q),(◇p∧q)},¬p⟩, although it is not complete tableau.

And if we remove the brackets of sets and brackets from the tableau expressions, then we will get a graph of tableau corresponding to the graphs usually used to present tableaux.

This will be a result of some translation of set of branches Φ, i.e. some partially ordered set with the smallest element which is the root of the proof tree. Wedonot insert the denotations of points ●. Instead of the denotations, there are individual lines with expressions.

←217 | 218→1 The idea for the system presented here was offered first in [14]. A simplified and better developed in some respects version of this material is presented in [22]. Also other variants of syllogistic are studied there.

2 The application of this type of semantics was launched in [14].

3 Function is superfluous in this semantics. This is also evident in studies of Thomason [26] and [27] who disregards that function.

4 For instance, propositions Si◻P and Pi◻S are to be equivalent in this semantics.

5 The issues described in this subchapter were partially presented in article [8].However, the general tableau theorem 5.62 was not used there. In addition, some concepts were defined differently in that paper.

6 So we share the remark of Melvin Fitting who wrote in Handbook of Tableau Methods that the proof trees (graphs), applied as proofs in the tableau systems, make up an application of a more abstract approach to logics (p. 5, [2]).