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

6 Examples of applications

←188 | 189→

6Examples of applications

6.1Introductory remarks

In this chapter, we will show exemplary applications of the general tableau concepts we defined in Chapter Five. Thanks to the general concepts we have at our command, and their interrelationships we have demonstrated, we can significantly shorten the construction of a complete tableau system.

We already have the general concepts:

  • set of tableau rules
  • branches
  • closed/ open branch
  • relation of branch consequence
  • tableau
  • open/ closed tableau.

We also know that there exists a general connection between a properly defined set of tableau rules R and properly defined semantics. Further work on the construction of the complete tableau system must therefore focus solely on defining the detailed concepts of tableau system in such a way that the general conditions are met—if that is the case, then we get a tableau system that is complete in terms of the initial semantics.

In the next four subchapters, we will describe three different applications. The first one will be of a detailed nature. We will consider an example of the logic of categorical propositions with modalities de re. We will define the basic concepts and then show that they meet the sufficient conditions for the general theorem on completeness 5.62, which will allow us to reach the conclusion that the defined tableau system is adequate to the initial semantics. This kind of application of the general theorem on completeness can be considered paradigmatic, because the theorem is intended primarily to shorten the construction of complete tableau systems when we want to construct a tableau system for a logic that is already semantically defined.

The second application, described in subsequent subchapter, has a general character. In this subchapter, we describe how to apply the general tableau concepts and general tableau theorem to the entire class of logics defined with the same type of semantics. Using an example of modal logics specified with the semantics of possible worlds, we will show how to obtain a less general theorem on completeness, specified for this class of logics. It allows even simpler proof of the ←189 | 190→completeness of specific tableau systems, because some more general properties are fulfilled by the entire class of modal logics specified with the semantics of possible worlds. Similar general applications can occur in all cases where we consider the classes of logic defined with a common type of semantics.

The next subchapter is devoted to the concept of a tableau system. We will try to define the general concept of tableau system and show what benefits to the investigation of dependencies between tableau systems brings the way the book describes tableau systems.

In the last subchapter, we will outline the transition between the formalised tableaux and standard tableaux/ trees. Therefore, we will try to show that the approach presented in the book corresponds to the standard approach, as to the practical construction of proof itself, while at the same time emphasizing the general nature of concepts that the standard approach does not bear.

6.2Tableau system for Modal Term Logic de re

We will now turn to the logic of categorical propositions de re.1 It is an extension of logic TL with new categorical propositions with modalities in the interpretation de re. This logic will be called Modal Term Logic de re, for short MTL.

When defining set of formulas of MTL on the right hand side we will provide schemes of propositions in English which correspond to particular formulas and may occur in the reasonings described by MTL.

6.2.1Language

Let us begin with the alphabet of MTL.

Definition 6.1 (Alphabet of MTL). Alphabet of Modal Term Logic is made up by the sum of the following sets:

  • set of logical constants Lc = {a,i,e,o,a, i, e, o, a, i, e, o}
  • set of name letters Ln = {P1,Q1,R1,P2,Q2,R2, . . .}.

Even though the set of name letters is infinite and contains indexed letters, practicably we will use a finite number of the following letters: P, Q, R, S, T, U, treating them as metavariables ranging over set Ln.

Let us now proceed to the definition of formula of MTL. Modal Term Logic is defined on the following set of formulas.

←190 | 191→

Definition 6.2 (Formula of MTL). Set of formulas of MTL is the smallest set containing the following expressions.

PaQEach P is Q.
PiQSome P is Q.
PeQNo P is Q.
PoQSome P is not Q.
PaQEach P must be Q.
Each P is necessarily Q.
PiQSome P must be Q.
Some P is necessarily Q.
PeQNo P may be Q.
No P is possibly Q.
PoQSome P must not be Q.
Some P is not possibly Q.
PaQEach P may be Q.
Each P is possibly Q.
PiQSome P may be Q.
Some P is possibly Q.
PeQNo P must be Q.
No P is necessarily Q.
PoQSome P may not be Q.
Some P is not necessarily Q.

where P,Q ∈ Ln.

We specify set of formulas as ForMTL, and its elements will be called formulas.

6.2.2Semantics

Let us define the concept of model. We will use semantics without possible worlds.

Definition 6.3 (Model for language of MTL). Model will be called ordered quadruple 𝔐MTL = ⟨D,d,d,d⟩, where:

  1. D is a set
  2. d, d, d are such functions from set of name letters Ln in set P(D) that for any name letter P ∈ Ln, d(P) ⊆ d(P) ⊆ d(P).

Remark 6.4. The proposed concept of model expresses the following intuitions. Functions d,d,d assign to each name letter P those sets of objects that are — respectively — necessarily P-s, are P-s, and can be P-s. The objects that are necessarily P-s, are also simply P-s and are contained in the set of those objects that can be P-s. Hence, we have a chain of inclusions: d(P) ⊆ d(P) ⊆ d(P).

←191 | 192→

Now, we proceed to the concept of truth in model.

Definition 6.5 (Truth in model). Let 𝔐MTL = ⟨D,d,d,d⟩ be a model and let A ∈ ForMTL. We shall state that formula A is true in model 𝔐MTL (for short 𝔐MTLA) iff for some name letters P, Q ∈ Ln, one of the below conditions is met:

  1. A = PaQ and d(P) ⊆ d(Q)
  2. A = PiQ and d(P)∩d(Q)≠∅
  3. A = PeQ and d(P)∩d(Q)=∅
  4. A = PoQ and d(P) ⊈ d(Q)
  5. A = PaQ and d(P) ⊆ d(Q)
  6. A = PiQ and d(P)∩d(Q)≠∅
  7. A = PeQ and d(P)∩d(Q)=∅
  8. A = PoQ and d(P) ⊈ d(Q)
  9. A = PaQ and d(P) ⊆ d(Q)
  10. A = PiQ and d(P)∩d(Q)≠∅
  11. A = PeQ and d(P)∩d(Q)=∅
  12. A = PoQ and d(P) ⊈ d(Q).

If for any propositional letters P, Q ∈ Ln none of the conditions is met, then we shall state that formula A is false in model 𝔐MTL (for short 𝔐MTLA). Let X ⊆ ForMTL. We shall state that set of formulas X is true in model 𝔐MTL (for short: 𝔐MTLX) iff for any formula AX, 𝔐MTLA. We shall state that set of formulas X is false in model 𝔐MTL (for short: 𝔐MTLX) iff it is not the case that 𝔐MTLX.

Remark 6.6. The semantics for modal syllogistic we offer in this study refers to the semantics presented in studies of F. Johnson [16] and S. K. Thomason [26] i [27].2

In [16] Johnson introduced model in form ⟨W,Ve,Va,,⟩ where Ve, Va, and are functions that assign subsets of set W to name letters, where W is treated as a set of all objects (“world”); Ve(S) is a set of objects that essentially are S-s; Va(S) is a set of objects that accidentally are S-s; (S) is a set of objects that essentially are non-S-s; (S) is a set of objects that accidentally are non-S-s. Furthermore, an auxiliary function V was adopted as V(S)=Ve(S)∪Va(S), that is V(S) is a set of all S-s. Therefore, our D, d, and d are Johnson’s W, V, and Ve ←192 | 193→respectively. Moreover, our function d can be defined with formula d(S) ∶= W(S); set of all those objects that are not essentially non-S-s, i.e. can be S-s.3

Our interpretation of proposition SaP corresponds to the interpretation of Johnson: V(S)⊆Ve(P); and for SeP we have: d(S)∩d(P)=∅, i.e. V(S)∩(W(P)) = ∅ iff V(S) ⊆ (P). For the other propositions [16] adopted different interpretation that ours, in order to reproduce the modal syllogistic of Aristotle.4

In [26] Thomason used a semantics based on the ordered quadruples in form ⟨W,Ext,Ext+,Ext⟩, where W is a set of objects and Ext, Ext+, and Ext are functions that assign subsets of set W to name letters and meet the following conditions: ∅ ≠ Ext+(x) ⊆ Ext(x) and Ext(x) ∩ Ext(x) ≠ ∅, for each letter x. Thomason’s W, Ext and Ext+ correspond to our D, d and d. Furthermore, his Ext(S) is a set of objects that cannot be S-s. We can express that set through our Dd(S). We have Ext(S) ⊆ (W ∖ Ext(S)), that is d(S) ⊆ d(S). Obviously, Ext, Ext+ and Ext correspond to functions V, Ve, and from [16].

Denotation 6.7. Let ●∈ {◻,◇}. Let us adopt denotation: if ●=◻, then ● =◇, and if ●=◇, then ● =◻.

Now, we will define a function that assigns a contradictory formula to each formula.

Definition 6.8 (Contradictory formulas). Let ○∶ForMTL → ForMTL be a function specified for any P, QLn and ●∈ {◻,◇} with the following conditions:

  1. ○(PaQ) = PoQ
  2. ○(PiQ) = PeQ
  3. ○(PeQ) = PiQ
  4. ○(PoQ) = PaQ
  5. ○(PaQ) = Po●'Q
  6. ○(PiQ) = Pe●'Q
  7. ○(PeQ) = Pi●'Q
  8. ○(PoQ) = Pa●'Q.

Directly from definition of truth in model 6.5 and definition of function ○ 6.8 we get a conclusion.

Corollary 6.9. For any model 𝔐MTL and any formula A, 𝔐MTLA iff 𝔐MTL ⊭ ○(A)

←193 | 194→

Note that each model 𝔐MTL can be identified with interpretation ℑ — in accordance with definition of general interpretation of formulas 5.8. Take any model 𝔐MTL and define set of formulasFunction○ is injective and for any formula B, , by conclusion 6.9.

We define conventionally the relation of semantic consequence.

Definition 6.10 (Semantic consequence relation). Let set X ⊆ ForMTL and A ∈ ForMTL. We shall state that formula A follows from set of formulas X (for short: XA) iff for any model 𝔐MTL, if 𝔐MTLX, then 𝔐MTLA. We shall state that from set of formulas X does not follow formula A (for short: XA) iff it is not the case that XA.

Pair ⟨ForMTL,⊧⟩ is a semantically defined logic, in accordance with general definition 5.11.This implies that relation of semantic consequence ⊧ both is unambiguously determined by set of all models 𝔐MTL for ForMTL of set of formulas MTL, and unambiguously determines set of all models 𝔐MTL for ForMTL of set of formulas MTL, by fact 5.12.

6.2.3Tableau expression

Before we move on to the definition of Te — set of tableau expression for MTL in accordance with general definition of tableau expression 5.15 — let us define several auxiliary concepts.

Definition 6.11 (Expressions). Set of expressions Ex is the union of the following sets.

  • {AiA ∈ ForMTL,i ∈ℕ}
  • {P+iP ∈ Ln,i ∈ ℕ}
  • {PiP ∈ Ln,i ∈ ℕ}
  • {P ∈ Ln,i ∈ ℕ}, where ●∈ {◻,◇}
  • {P ∈ Ln,i ∈ ℕ}, where ●∈ {◻,◇}.

By virtue of definition 6.11, the following conclusion occurs

Corollary 6.12. There exists function gForMTLP(Ex), defined with condition: for any formula AForMTL, g(A) = {A1, A2, A3, . . .}, where {A1,A2,A3, . . .} ⊆ Ex.

Remark 6.13. Practically, in the case of MTL, each Aig(A) will be simply identified with formula A, since in the tableau proof each formula will be self-represented.

←194 | 195→

Next, based on set Ex we define the concept of inconsistent set of expressions that ultimately will correspond to the concept of tableau inconsistent set of expressions.

Definition 6.14 (Inconsistent set of expressions). Let X ⊆ Ex. We shall state that set X is an inconsistent set of expressions iff X meets one of the following conditions:

  1. AX and ○(A) ∈ X, for some A ∈ ForMTL
  2. P+iX and PiX, for some P ∈ Ln and some i ∈ ℕ
  3. for some P ∈ Ln, some i ∈ ℕ and ● ∈ {◇,◻}.

We shall state that set X is a consistent set of expressions iff X is not an inconsistent set of expressions.

Based on definition of model 6.3, conclusion 6.9 and definition 6.14, we get another conclusion.

Corollary 6.15. Let XForMTL and i ∈ ℕ. If there exists model 𝔐MTL such that 𝔐MTLX, then set {xixg(A),AX} is a consistent set of expressions.

Based on definition of set of expressions 6.11, conclusion 6.12, definition of inconsistent set of expressions 6.14 and conclusion 6.15 we get the following fact.

Proposition 6.16. Set of expressions Ex meets the conditions of general definition of tableau expressions 5.15.

Due to the above fact, set Ex will be denoted as TeMTL, while its elements will be called expressions or tableau expressions. In turn, the inconsistent sets of expressions will be called tableau inconsistent (t-inconsistent), while the consistent sets of expressions will be called tableau consistent (t-consistent).

Now, we define the function selecting indices.

Definition 6.17 (Function selecting indices). Let ∗∶ TeMTL →ℕ be such function that for any name letter P ∈ Ln, any i ∈ ℕ, any ● ∈ {◻,◇} and any formula A ∈ ForMTL:

  1. ∗(Ai) = i
  2. ∗(P+i) = i
  3. ∗(Pi) = i

Denotation 6.18. Let x ∈ TeMTL and ∗(x) = i. We adopt denotation xi.

←195 | 196→

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

Definition 6.19. Let X, Y ⊆ TeMTL. We define relation ≡ with condition: XY iff there exists bijection h ∶ ∗(X)→∗(Y) such that for any expression xi ∈ TeMTL: xiX iff xh(i)Y.

From definition 6.19 results the following conclusion.

Corollary 6.20. Let X, YTeMTL. If XY, then:

  • X is t-consistent iff Y is t-consistent
  • sets X and Y have the same cardinality.

By conclusion 6.20 and definition of relation ≡ 6.19, we claim that relation ≡ meets the conditions of general definition of similarity of sets of expressions 5.23.

Proposition 6.21. Relationis the relation of similarity of sets in accordance with the general definition of similarity of sets of expressions 5.23.

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

Definition 6.22. Let X be a set of expressions, while 𝔐MTL = ⟨D,d, d, d⟩ be a model. We shall state that 𝔐MTL is appropriate for set X iff the below conditions are met:

  1. 𝔐MTLX ∩ForMTL
  2. there exists function γ ∶ ℕ → D such that for each name letter P ∈ Ln, each i ∈ ℕ and for any ●∈ {◻,◇}:

a. if P+iX, then γ(i) ∈ d(P)

b. if PiX, then γ(j) ∉ d(P)

c. if X, then γ(i) ∈ d(P)

d. if X, then γ(j) ∉ d(P).

From definition of inconsistent set of expressions 6.14 and definition of model appropriate for the set of expressions 6.22 follows a condition concerning the relationship between the inconsistent sets of expressions and the appropriateness of models.

Corollary 6.23. For any XTeMTL, if X is t-inconsistent, then there exists no model 𝔐MTL appropriate for X.

←196 | 197→

Next, note that relation ⊧ for MTL meets the conditions of relation ⊩ (definition 5.25).Thus, by conclusion 6.23 and definition of appropriate model 6.22 we have the fact.

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

Thus, we have demonstrated that the presented concepts for the tableau system for MTL are special cases of the general concepts described in the previous chapter.

6.2.4Rules for the tableau system for logic MTL

We can proceed to the rules. On each rule, we conventionally assume that each of its input sets is t-consistent and that each input set is basically contained in the output set.

Definition 6.25 (Tableau rules for MTL). Tableau rules for system MTL are the following rules:

Classical rules

where:

  1. j ∉ ∗(X ∖ForMTL)
  2. for any k ∈ ℕ, {P+k,Q+k} ⊈ X.

where:

1. j ∉ ∗(X ∖ForMTL)

2. for any k ∈ ℕ, {P+k,Qk} ⊈ X.

Rules for

←197 | 198→

where:

1. j ∉ ∗(X ∖ForMTL)

2. for any k ∈ ℕ, } ⊈ X.

Ro, where:

1. j ∉ ∗(X ∖ForMTL)

2. for any k ∈ ℕ, {P+k,} ⊈ X.

Rules for

where:

1. j ∉ ∗(X ∖ForMTL)

2. for any k ∈ ℕ, {P+k,X.

where:

1. j ∉ ∗(X ∖ForMTL)

2. for any k ∈ ℕ, {P+k,} ⊈ X.

Bridging rules

←198 | 199→

Set of rules for MTL will be denoted as RMTL.

Note that set RMTL meets both the general conditions of rule (definition 5.29), and the general conditions of set of tableau rules 5.33 — the cores of each rule from RMTL (definition 6.25) are any ordered pairs in which set X is empty.

6.2.5Branches and tableaux for MTL

We accept 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 dependent on set of tableau rules RMTL.

6.2.6Theorem on the completeness of the tableau system for MTL

In order to demonstrate that for the tableau system for MTL the theorem on completeness holds, we must show that the assumptions of general theorem 5.62 are met. So, we must demonstrate that:

  • set of models for language of MTL is good for set of tableau rules RMTL (according to general definition 5.55)
  • set of tableau rules RMTL is good for model for language of MTL (according to general definition 5.59).

Let us first define the concept of model defined by a branch.

Definition 6.26 (Model generated by branch). Let ϕ be any branch. We define the following function AT(ϕ) =⋃ϕ∩(TeMTL ∖ForMTL).

We shall state that model 𝔐MTL = ⟨D,d,d,d⟩ is generated by branch ϕ iff:

  1. D = {x ∈ℕ ∶ x ∈ ∗(At(ϕ))}
  2. for any name letter P ∈ Ln:
←199 | 200→

a. xd(P) iff P+xAt(ϕ)

b. for any ●∈ {◻,◇}, xd(P) iff At(ϕ).

From this definition, we get the following conclusion.

Corollary 6.27. Let ϕ be an open and maximal branch. Then, there exists a model generated by ϕ.

Proof. Take any open and maximal branch ϕ. From definition of open branch 5.39 and definition of model generated by branch 6.26 we get ordered quadruple ⟨D,d,d,d⟩.

We must investigate if for any name letter P ∈ Ln occurs d (P)⊆d(P)⊆d(P). Since branch ϕ is maximal and open, so by virtue of bridging rules from definition of tableau rules RMTL (definition 6.25), for any i ∈ℕ and for any name letter P ∈ Ln:

  • if id(P), then id(P), due to rule
  • if id(P), then id(P), due to rule .

Thus, from definition of model 6.3 we get a conclusion that ⟨D, d, d, d⟩ is a model.

As we can see, the general definition of branch generating model 5.53 gains content in the context of the tableau system of MTL. We might define a function assigning models to open and maximal branches, but we will refrain from doing so and instead directly use conclusion 6.27.While on model 𝔐MTL generated by branch ϕ we shall state that branch ϕ generates model 𝔐MTL.

We will now show that set of models of MTL is good for tableau rules RMTL (according to general definition 5.55). The following lemma will be useful for that.

Lemma 6.28. Let ϕ be an open and maximal branch. Let X i ⊆ ⋃ϕ, for some XForMTL and i ∈ ℕ. Then branch ϕ generates such model 𝔐MTL that 𝔐MTLX.

Proof. Take any open and maximal branch ϕ. Take any set X i ⊆ ⋃ϕ, for some X ⊆ ForMTL and i ∈ ℕ. Note that in the case of MTL set X i is simply a set of formulas (remark 6.13).

Since branch ϕ is open and maximal, so by virtue of the previous conclusion 6.27 there exists model 𝔐MTL = ⟨d, d, d⟩ generated by ϕ.

We will now show that for any formula A contained in ⋃ϕ, it is the case that 𝔐MTLA, i.e.𝔐MTL ⊧⋃ϕ ∩ForMTL. This implies that 𝔐MTLX.

The proof will be carried out by consideration of all the possible cases of construction of formula A. Assume that A ∈ ⋃ϕ. By definition of formula, for some name letters P, Q ∈ Ln, there must occur one of the following cases.

  1. ←200 | 201→ A = PaQ. Take any object iD such that id(P). By definition of generated model 6.26, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ra+, ⋃ϕ also contains tableau expression Q+i. By definition of model generated 6.26, id(Q).Hence, d(P)⊆ d(Q), and by definition of truth in model 6.5, we thus get that 𝔐MTLPaQ. In turn, if there exists no such iD that id(P), then ∅=d(P) ⊆ d(Q), so by definition of truth in model 6.5, we get 𝔐MTLPaQ.
  2. A = PiQ. Since ϕ is a maximal and open branch, so by tableau rule Ri, set ⋃ϕ also contains tableau expressions P+i, Q+i, for some i ∈ ℕ. By definition of model generated 6.26, id(P) and id(Q). Since d(P)∩d(Q) ≠∅, so by definition of truth in model 6.5, we get that 𝔐MTLPiQ.
  3. A = PeQ. Take any object iD such that id(P). By definition of model generated 6.26, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule Re, ⋃ϕ also contains tableau expression Qi. Since branch ϕ is open, so expression Q+i ∉ ⋃ϕ, and consequently, by definition of model generated 6.26, id(Q). Thus, d(P)∩d(Q)=∅ and by definition of truth in model 6.5, we get 𝔐MTLPeQ. In turn, if there exists no object iD such that id(P), then d(P)∩d(Q)=∅, so by definition of truth in model 6.5, we get that 𝔐MTLPeQ.
  4. A = PoQ. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ro, set ⋃ϕ also contains tableau expressions P+i, Qi, for some i ∈ ℕ. By definition of model generated 6.26, id(P) and — since branch ϕ is open and, consequently, expression Q+i ∉⋃ϕid(Q), so d(P) ⊈ d(Q). Thus, by definition of truth in model 6.5, we get 𝔐MTLPoQ.

The remaining eight cases of the possible construction of formula A will be reduced to four cases as both rules that we apply to them and conditions of truth that define their truth are analogous. So, take ●∈ {◻,◇}. We have four cases.

  1. A = PaQ. Take any object iD such that id(P). By definition of model generated 6.26, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule , ⋃ϕ also contains tableau expression . By definition of model generated 6.26, id(Q). Hence, d(P) ⊆ d(Q), and by definition of truth in model 6.5, we thus get that 𝔐MTLPaQ. In turn, if there exists no such iD that id(P), then ∅ = d(P) ⊆ d(Q), so by definition of truth in model 6.5, we get 𝔐MTLPaQ.
  2. ←201 | 202→ A = PiQ. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ri, set ⋃ϕ also contains tableau expressions P+i, , for some i ∈ℕ. By definition of model generated 6.26, id(P) and id(Q). Since d(P)∩d( Q) ≠∅, so by definition of truth in model 6.5, we get that 𝔐MTLPiQ.
  3. A = PeQ. Take any object iD such that id(P). By definition of model generated 6.26, set ⋃ϕ contains tableau expression P+i. Since ϕ is a maximal and open branch, so by virtue of tableau rule , ⋃ϕ also contains tableau expression . Since branch ϕ is open, so expression ∉⋃ϕ, and consequently, by definition of model generated 6.26, id(Q)●'. Thus, d(P)∩ d●'(Q) = ∅ and by definition of truth in model 6.5, we get 𝔐MTLPeQ. In turn, if there exists no object iD such that id(P), then d(P)∩d●'(Q)=∅, so by definition of truth in model 6.5, we get that 𝔐MTLPeQ.
  4. A = PoQ. Since ϕ is a maximal and open branch, so by virtue of tableau rule Ro, set ⋃ϕ also contains tableau expressions P+i, , for some i ∈ ℕ. By definition of model generated 6.26, id(P) and — since branch ϕ is open and, consequently, expression∉⋃ϕid●'(Q), so d(P) ⊈ d●'(Q). Thus, by definition of truth in model 6.5, we get 𝔐MTLPoQ.

From lemma 6.28 and definition 5.55 applied to the set of models for the language of MTL we get a conclusion.

Corollary 6.29. Set of models for language of MTL is good for set of tableau rules RMTL.

We will now proceed to the demonstration of an opposite dependence between rules and models.

Lemma 6.30. Let 𝔐MTL be any model, X, YTeMTL, and let RRMTL. Then, ifX,Y⟩ ∈ R and 𝔐MTL is appropriate for set of expressions X, then 𝔐MTL is appropriate for Y.

Proof. In the proof, wewillmake use of definition of model appropriate for the set of expressions 6.22. Let 𝔐MTL = ⟨D,d,d,d⟩ be any model and X, Y ⊆ TeMTL. We will consider all cases of rules RRMTL, assuming that ⟨X,Y⟩∈ R and 𝔐MTL is appropriate for set of expressions X, and showing that then 𝔐MTL is appropriate for Y.

We have four cases of rules for the classical functors.

  1. Let R = Ra+, then ⟨X,Y⟩ = ⟨Z∪{PaQ,P+i}, Z∪{PaQ,P+i, Q+i}⟩, for some Z ⊆ TeMTL, P,Q∈ Ln and i ∈ ℕ; since 𝔐MTL is appropriate for set of expressions X, ←202 | 203→so by definition 6.22,𝔐MTLPaQ and there exists function γ ∶ℕ→ D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); due to the fact that P+iX, also γ(i) ∈ d(P), while since 𝔐MTLPaQ, 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∪{PaQ,P+i,Q+i}.
  2. Let R =Ri, then ⟨X,Y⟩=⟨Z∪{PiQ},Z∪{PiQ,P+i,Q+i}⟩, for some Z ⊆ TeMTL, P, Q ∈ Ln and i ∈ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22,𝔐MTLPiQ and there exists function γ ∶ ℕ → D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j)∈ d(S) and if SjX, then γ(j) ∉ d(S); however, rule Ri enriches set X with expressions P+i,Q+i and index i is new, it has not occurred in any expression from set X, while since 𝔐MTLPiQ, so by definition of truth in model 6.5, in the domain there exists certain object x such that xd(P)∩d(Q);we define function γ′ ∶ℕ→ Dsuch that for any k ∈ ℕ, if ki, 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∪{PiQ,P+i,Q+i}.
  3. Let R = Re, then ⟨X,Y⟩ = ⟨Z∪{PeQ,P+i},Z∪{PeQ,P+i, Qi}⟩, for some Z ⊆ TeMTL, P,Q∈ Ln and i ∈ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22,𝔐MTLPeQ and there exists function γ ∶ℕ→ D such that for each name letter S ∈ Ln and each j ∈ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); due to the fact that P+iX, also γ(i) ∈ d(P), while since 𝔐MTLPeQ, 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∪{PeQ,P+i,Qi}.
  4. Let R = Ro, then ⟨X,Y⟩ = ⟨Z ∪ {PoQ},Z ∪ {PoQ,P+i, Qi}⟩, for some Z ⊆ TeMTL, P, Q ∈ Ln and i ∈ ℕ; since 𝔐MTL is appropriate for set of expressions X, so by definition 6.22, 𝔐MTLPoQ and there exists function γ ∶ ℕ → D such that for each name letter S ∈ Ln and each j ∈ ℕ: if S+jX, then γ(j) ∈ d(S) and if SjX, then γ(j) ∉ d(S); however, rule Ro enriches set X with expressions P+i,Qi and index i is new, it has not occurred in any expression from set X, while since 𝔐MTLPoQ, so by definition of truth in model 6.5, in the domain there exists certain object x such that xd(P), but xd(Q); we define function γ′ ∶ℕ→ D such that for any k ∈ℕ, if ki, 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∪{PoQ,P+i,Qi}.