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

3 Tableau system for Term Logic

←64 | 65→

3Tableau system for Term Logic

3.1Introductory remarks

Now, we will describe the tableau system for Term Logic1 (for short: TL).2 By Term Logic we mean a logic in which both premises and conclusions have the form of classical categorical propositions:3

  • Each P is Q.
  • Some P is Q.
  • No P is Q.
  • Some P is not Q.

Moreover, we do not assume that in Term Logic the names appearing in categorical propositions are not empty. So we consider the most general approach—the simplest language and semantics.

The tableau system we will describe can be treated as a stand-alone system. But, this is not the purpose of its construction. We intend to indicate an example of the use of analogous tableau concepts, such as those we defined for the tableau system for CPL. Although the defined system will also feature the property of a finite branch, there will be new features that will be mentioned soon.

We will redefine the concepts of rule, various types of branches and tableaux in an almost identical way to the tableau concepts defined in the previous chapter. We mean almost identical because, after all, we will face a different language of tableau proof and a different set of tableau rules than in the case of the tableau ←65 | 66→system for CPL. However, these differences will not affect the formal nature of concepts themselves, so although, for example, a branch for TL will be built from different sets of expressions than a branch for CPL, the structure of presentation itself will be identical — because we aim at presenting a general scheme of the tableau system construction, a synthesis consisting in abstracting from tableau concepts those properties that are not specific, and therefore do not depend on the characteristics of exemplary systems which we define in detail in the initial chapters of the book.

The importance of the presented tableau system TL for our considerations consists in the fact that the set of formulas for Term Logic is a proper subset of the set of proof expressions, and moreover, there are no branchings in the tableaux. This case is located between borderline cases because of the relation of the set of logic formulas to the set of tableau expressions. However, in some respects it has a borderline character itself, because the tableaux do not host any branchings, so the tableau proofs boil down to the construction of a single maximal branch. General tableau concepts could be therefore simplified in the tableau system for TL although they still provide more detail on the general concepts that we describe in the book.

3.2Language and semantics

The construction of tableau system for Term Logic requires, as usual, the presentation of basic concepts. Let us start with the alphabet of language of TL.

Definition 3.1 (Alphabet of TL). The alphabet of Term Logic is the sum of the following sets:

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

Although the set of name letters is infinite and includes indexed letters, in practice 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 TL.

Definition 3.2 (Formula of TL). Set of formulas TL is the smallest set containing the following expressions:

  • PaQ
  • PiQ
  • PeQ
  • PoQ
←66 | 67→

where P,Q ∈ Ln.

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

Another basic concept is the concept of model for TL, and then the concept of truth in the model.

Definition 3.3 (Model for language of TL). Model 𝔐TL for language of TL will be called such ordered pair ⟨D,d⟩ that:

  • D is any set
  • d is a function from set Ln in set P(D) of all subsets of set D, i.e. d ∶Ln → P(D).

Definition 3.4 (Truth in model). Let 𝔐TL = ⟨D,d⟩ be a model and A∈ ForTL. We shall state that formula A is true in model 𝔐TL (for short 𝔐TLA) 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).

Formula A is false in model 𝔐TL (for short 𝔐TLA) if for any name letters P, Q ∈ Ln none of the conditions is met.

Let X ⊆ ForTL. Set X is true in model 𝔐TL (for short: 𝔐TLX) iff for any formula AX, 𝔐TLA. Set of formulas X is false in model 𝔐TL (for short: 𝔐TLX) iff it is not the case that for any formula AX,𝔐TLA.

Making use of the concept of model, we can now define the concept of entailment or otherwise semantic consequence relation in TL.

Definition 3.5 (Semantic consequence of TL). Let X ⊆ ForTL and A ∈ ForTL. From set X follows formula A(for short: XA) iff for any model𝔐TL, if𝔐TLX, then 𝔐TLA. Relation ⊧ will be also called semantic consequence relation of Term Logic, or shortly semantic consequence.

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

We will now take up the issue of the compactness of semantic consequence relation. According to definition 2.48 compactness of relation ⊧ is expressed by the following definition.

Definition 3.7 (Compactness of semantic consequence of TL). Relation of semantic consequence ⊧ is compact iff for any set of formulas X and any formula A it is the case that: XA ⇔there exists such finite set YX that YA.

←67 | 68→

Compactness of relation ⊧ seems pretty obvious, so we are just going to outline the proof consisting in embedding TL into Monadic Logic of Predicates of which the relation of consequence is compact.

Before we proceed to the verbalization and proof of the relevant theorem, let us recall a few concepts concerning the Monadic Logic of Predicates (for short MLP):

• the alphabet of MLP contains:

classical, Boolean constants: ¬, ∧, ∨, →,↔, and quantifiers ∃, ∀

unary predicate letters Lp = {p1, q1, r1, p2, q2, r2, . . .} (in practice, we will use a finite number of the following letters: p, q, r, s, treating them as metavariables ranging over set Lp)

set of individual constants Ci and individual variables Vi as well as auxiliary symbols: ), (.

  • MLP formulas will be constructed in a standard way and these are atomic expressions of type p(x), where p ∈ Lp, whereas x ∈ Ci ∪ Vi, and more complex expressions using quantifiers, Boolean constants and brackets; set of formulas MLP we shall denote as ForMLP
  • models for formulas from set ForMLP are ordered triples 𝔐MLP = ⟨D,dLp,dCi⟩, where:

D is a non-empty set of any objects which is called a domain

dLp is a function from the set of predicate letters in the set of all subsets of D, i.e. in P(D)

dCi is a function from the set of individual constants in set D

  • both truth conditions for MLP formulas and relation of semantic consequence ⊧MLP are defined in a standard way
  • relation ⊧MLP is compact.

Since set of name letters Ln set of predicate letters Lp are countable, then there exists bijection: π ∶ Ln → Lp, where π(X) = x, for all letters. Obviously, for π there exists the inverse function π−1.

Next, we define function g from set of formulas ForTL in set of formulas ForMLP with the following conditions, for any name letters P, Q ∈ Ln:

  1. g(PaQ)=∀x(π(P)(x)→π(Q)(x))
  2. g(PiQ) = ∃x(π(P)(x)∧π(Q)(x))
  3. g(PeQ)=∀x(π(P)(x)→¬π(Q)(x))
  4. g(PoQ) = ∃x(π(P)(x)∧¬π(Q)(x)),

where x is any, but fixed variable from set Vi.

←68 | 69→

In turn, having function g, we define transformation Tr: ForTLg(ForTL) in such way that Tr(y) = g(y), for any y ∈ ForTL. Note that function Tr is a bijection because:

(a) for each yg(ForTL) there exists such z ∈ ForTL that TR(z) = y

(b) for any y, z ∈ ForTL, if y and z are various formulas, then Tr(y) ≠ Tr(z), by definition of function g.

Hence, there exists the inverse function to Tr, function Tr−1g(ForTL) → ForTL, so such function that for any y ∈ ForTL, Tr−1(Tr(y)) = y.

Now, we will show that the following fact holds.

Proposition 3.8. For any set of formulas XForTL and any formula A: XATr(X) ⊧MLP Tr(A).

Proof. Take any set of formulas X ⊆ ForTL and formula A.

First, let us consider implication ‘⇒’, assuming that XA. Take any model 𝔐MLP = ⟨D,dLp,dCi⟩ such that 𝔐MLPMLP Tr(X). Based on model 𝔐MLP we will define model 𝔐TL = ⟨D′,d⟩ as follows:

  • D′ = D
  • for any P ∈ Ln, d(P) = dLp(π(P)).

We will show that 𝔐TLX. We will now consider cases of formulas that can belong to set X. Take any name letters P, Q ∈ Ln and assume that some of the cases occurs. We know that for some p,q ∈ Lp, π(P) = p and π(Q) = q.

  1. PaQX, then Tr(PaQ)=∀x(p(x)→ q(x)) and by assumption 𝔐MLPMLPx(p(x) → q(x)), consequently, for each denotation of variable x, if denotation x belongs to set dLp(p), then it belongs to set dLp(q), hence by definition of model 𝔐TL, d(P) ⊆ d(Q), so by definition of truth in model 3.4,𝔐TLPaQ
  2. PiQX, then Tr(PiQ) = ∃x(p(x)∧q(x)) and by assumption 𝔐MLPMLPx(p(x) ∧ q(x)), hence there exists such denotation of variable x that this denotation belongs to set dLp(p) and set dLp(q), thus by definition of model 𝔐TL, d(P)∩d(Q) ≠∅, so by definition of truth in model 3.4,𝔐TLPiQ
  3. PeQX, then Tr(PeQ)=∀x(p(x)→¬q(x)) and by assumption 𝔐MLPMLPx(p(x) → ¬q(x)), hence for each denotation of variable x, if denotation x belongs to set dLp(p), then it does not belong to set dLp(q), thus by definition of model 𝔐TL, d(P)∩d(Q)=∅, so by definition of truth in model 3.4,𝔐TLPeQ
  4. ←69 | 70→ PoQX, then Tr(PoQ)=∃x(p(x)∧¬q(x)) and by assumption 𝔐MLPMLPx(p(x)∧¬q(x)), hence there exists such denotation of variable x that this denotation belongs to set dLp(p) and does not belong to set dLp(q), thus by definition of model 𝔐TL, d(P) ⊈ d(Q), so by definition of truth in model 3.4, 𝔐TLPoQ.

Hence, 𝔐TLX. In turn, from definition of relation ⊧ it follows that 𝔐TLA.

Now, we will show that𝔐MLPMLP Tr(A). We will consider cases of formulas that can be identical to formula A. Take any name letters P, Q ∈ Ln and assume that some of the cases occurs. We know that for some p,q ∈ Lp, π(P) = p and π(Q) = q.

  1. A = PaQ, then 𝔐TLPaQ, so by definition of truth in model 3.4, d(P) ⊆ d(Q), thus by definition of model 𝔐TL, for each denotation of variable x, if denotation x belongs to set dLp(p), then it belongs to set dLp(q), hence 𝔐MLPMLPx(p(x)→ q(x)), thus 𝔐MLPMLP Tr(PaQ)
  2. A =PiQ, then 𝔐TLPiQ, so by definition of truth in model 3.4, d(P)∩d(Q) ≠ ∅, thus by definition of model 𝔐TL, there exists such denotation of variable x that this denotation belongs to set dLp(p) and to set dLp(q), hence 𝔐MLPMLPx(p(x)∧q(x)), thus 𝔐MLPMLP Tr(PiQ)
  3. A = PeQ, then 𝔐TLPeQ, so by definition of truth in model 3.4, d(P) ∩ d(Q) = ∅, thus by definition of model 𝔐TL, for each denotation of variable x, if denotation x belongs to set dLp(p), then it does not belong to set dLp(q), so 𝔐MLPMLPx(p(x)→¬q(x)), thus 𝔐MLPMLP Tr(PeQ)
  4. A = PoQ, then 𝔐TLPoQ, so by definition of truth in model 3.4, d(P) ⊈ d(Q), thus by definition of model 𝔐TL, there exists such denotation of variable x, that this denotation belongs to set dLp(p), but it does not belong to set dLp(q), so 𝔐MLPMLPx(p(x)∧¬q(x)), thus 𝔐MLPMLP Tr(PoQ).

Hence, 𝔐MLPMLP Tr(A). Whereas from the arbitrariness of model 𝔐MLP we have Tr(X) ⊧MLP Tr(A).

Next, let us consider implication ‘⇐’, assuming that Tr(X)⊧MLP Tr(A). Take any model𝔐TL = ⟨D,d⟩ such that 𝔐TLX. Based on model𝔐TL, we will define model 𝔐MLP = ⟨D′,dLp,dCi⟩ as follows:

  • D′ = D, if D ≠∅; otherwise D′ = D′′, for some whichever, fixed D′′ ≠∅
  • for any p ∈ Lp, dLp(p) = d(π−1(p))
  • for any x ∈ Ci, dCi(x) ∈ D′.

We will show that 𝔐MLPMLP Tr(X).We will now consider cases of formulas that can belong to set X, and consequently, their images under function Tr belong ←70 | 71→to Tr(X). Take any name letters P,Q∈ Ln and assume that some of the below cases occurs. We know that for some p,q ∈ Lp, π(P) = p and π(Q) = q.

  1. PaQX, then 𝔐TLPaQ, so by definition of truth in model 3.4, d(P) ⊆ d(Q), thus by definition of model 𝔐MLP, for each denotation of variable x, if denotation x belongs to set dLp(p), then it belongs to set dLp(q), hence 𝔐MLPMLPx(p(x)→ q(x)), thus 𝔐MLPMLP Tr(PaQ)
  2. PiQX, then 𝔐TLPiQ, so by definition of truth in model 3.4, d(P)∩d(Q) ≠ ∅, thus by definition of model 𝔐MLP, there exists such denotation of variable x, that this denotation belongs to set dLp(p) and to set dLp(q), hence 𝔐MLPMLPx(p(x)∧q(x)), thus 𝔐MLPMLP Tr(PiQ)
  3. PeQX, then 𝔐TLPeQ, so by definition of truth in model 3.4, d(P) ∩ d (Q)=∅, thus by definition of model 𝔐MLP, for each denotation of variable x, if denotation x belongs to set dLp(p), then it does not belong to set dLp(q), hence 𝔐MLPMLPx(p(x)→¬q(x)), thus 𝔐MLPMLP Tr(PeQ)
  4. PoQX, then 𝔐TLPoQ, so by definition of truth in model 3.4, d(P) ⊈d(Q), thus by definition of model 𝔐MLP, there exists such denotation of variable x that this denotation belongs to set dLp(p), but it does not belong to set dLp(q), hence 𝔐MLPMLPx(p(x)∧¬q(x)), thus 𝔐MLPMLP Tr(PoQ).

Hence, 𝔐MLPMLP Tr(X). From definition of relation ⊧MLP it follows that 𝔐MLPMLP TR(A).

We will now show that 𝔐TLA. We will consider cases of formulas that can be identical to formula A. Take any name letters P, Q ∈ Ln and assume that some of the below cases occurs. We know that for some p,q ∈ Lp, π(P)=p and π(Q)=q.

  1. A ∶= PaQ, then Tr(PaQ) = ∀x(p(x) → q(x)), and since 𝔐MLPMLPx(p(x) → q(x)), consequently, for each denotation of variable x, if denotation x belongs to set dLp(p), then it belongs to set dLp(q), hence by definition of model 𝔐MLP, d(P) ⊆ d(Q), so by definition of truth in model 3.4,𝔐TLPaQ
  2. A ∶= PiQ, then Tr(PiQ) = ∃x(p(x) ∧ q(x)), and because 𝔐MLPMLPx(p(x) ∧ q(x)), hence there exists such denotation of variable x that this denotation belongs to set dLp(p) and set dLp(q), thus by definition of model 𝔐MLP, d(P)∩d(Q) ≠∅, so by definition of truth in model 3.4,𝔐TLPiQ
  3. A ∶= PeQ, then Tr(PeQ) = ∀x(p(x) → ¬q(x)), and because 𝔐MLPMLPx(p(x) → ¬q(x)), hence for each denotation of variable x, if denotation x belongs to set dLp(p), then it does not belong to set dLp(q), thus by definition of model 𝔐MLP, d(P)∩d(Q)=∅, so by definition of truth in model 3.4, 𝔐TLPeQ
  4. ←71 | 72→ A ∶= PoQ, then Tr(PoQ) = ∃x(p(x) ∧ ¬q(x), and because 𝔐MLPMLPx(p(x)∧¬q(x)), hence there exists such denotation of variable x, that this denotation belongs to set dLp(p) and does not belong to set dLp(q), thus by definition of model 𝔐MLP, d(P) ⊈ d(Q), so by definition of truth in model 3.4,𝔐TLPoQ.

Hence, 𝔐TLA. Whereas from the arbitrariness of model 𝔐TL we have XA.

Let us now proceed to the very fact concerning the compactness of relation ⊧.

Proposition 3.9. Relation of semantic consequenceis compact.

Proof. Now, take any set X ⊆ ForTL and any formula A ∈ ForTL and assume that XA. By virtue of fact 3.8 we know that Tr(X)⊧MLP Tr(A). And since relation ⊧MLP is compact, then there exists such finite subset Y′ ⊆ Tr(X) that Y′ ⊧MLP Tr(A).

Due to definition of function Tr and fact 3.8, there exists such finite subset YX that Tr−1(Y′) = Y and YA.

On the other hand, let us assume there exists such finite subset YX that YA. Then, however, due to definition of relation of semantic consequence of TL 3.5, XA.

Thus, relation of semantic consequence ⊧ of TL is compact.

3.3Basic concepts of the tableau system for TL

Unlike the tableau system for CPL in the case of tableau system for TL the tableau proofs will be carried out in a more rich language than the set of formulas. The elements of expressions of this language will be simply called tableau expressions.

Definition 3.10 (Tableau expressions of TL). Set of tableau expressions is the union of the three following sets:

  • {P+iP ∈ Ln,i ∈ ℕ}
  • {PiP ∈ Ln,i ∈ ℕ}
  • ForTL.

We specify this set as TeTL, and its elements will be called expressions or tableau expressions. Numbers that exist in expressions with + or − sign will be called indices.

Remark 3.11. In case of TL set TeTL, i.e. set of proof expressions of which subsets will be used for construction of tableaux, is composed of formulas of TL and ←72 | 73→additional expressions which play a role worth explaining. We mean expressions P+i, Pi, where P ∈ Ln and i ∈ ℕ. Although our approach to the tableau system is syntactic — we treat tableau proof as a transformation of sets of symbols without reference to their meaning—we can point to the semantic intuitions behind such kind of expressions. The natural numbers appearing in the expressions, in the construction of the model will denote the objects in the universe under consideration, while symbols +/− will mean being or not being the designator of a given name denoted by letter P. According to known literature, it seems that this sort of use of an additional language to describe whether or not given objects belong to the ranges of names in the context of tableau proofs has not yet been fully developed.

We will now define an auxiliary function that is to attribute formulas to formulas that contradict them. This function, among other things, will be used to begin tableau proofs, so it will play a similar role as negation in the tableau system from the previous chapter.

Definition 3.12. Function ○∶ ForTL → ForTL, for any P,Q ∈ Ln, is defined with the following conditions:

  1. ○(PaQ) = PoQ
  2. ○(PiQ) = PeQ
  3. ○(PeQ) = PiQ
  4. ○(PoQ) = PaQ.

Notice that by virtue of definition 3.12 and definition of truth in model 3.4, the following fact occurs.

Proposition 3.13. For any formula A and any model 𝔐TL: 𝔐TLA iff 𝔐TL ⊭ ○(A).

As we wrote, 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. Let it be reminded that in case of the defined system for TL, the proof expressions are the proper superset of the set of formulas, so the concept of t-incosistent set of formulas will also cover additional expressions.

Definition 3.14 (Tableau inconsistent set of expressions). Set X ⊆ TeTL will be calles tableau inconsistent (for short: t-inconsistent) iff one of the below conditions is met:

  1. there exists such formula A ∈ ForTL that AX and ○(A) ∈ X
  2. there exists such name letter P ∈ Ln and such number i ∈ ℕ that P+iX and PiX.
←73 | 74→

Set X will be called t-consistent iff it is not t-inconsistent.

Remark 3.15. From the definition of tableau inconsistent set of expressions 3.14 we might remove the first condition and require the t-inconsistency to emerge in the set of “pure” tableau expressions. However, we will leave this condition to find t-inconsistency faster wherever possible, without the need for further application of tableau rules.

Let us now introduce the concept of model appropriate for the set of expressions. It is a generalisation of the concept of truth in model in the entire set TeTL.

Definition 3.16 (Model appropriate for the set of expressions). Let X be a set of tableau expressions, while 𝔐TL = ⟨D,d⟩ be a model. Model 𝔐TL is appropriate for set X iff the below conditions are met:

  1. 𝔐TLX ∩ForTL
  2. there exists function γ ∶ ℕ → D such that for each name letter P ∈ Ln and each i ∈ ℕ:

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

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

From the two above definitions, an important conclusion for metatheory follows, namely the relationship between the inconsistent sets of expressions and the appropriateness of models.

Corollary 3.17. For any XTeTL, if X is t-inconsistent, then there exists no model 𝔐TL appropriate for X.

Proof. Take any tableau inconsistent set of expressions X and any model 𝔐TL = ⟨D,d⟩. From the definition of tableau inconsistent set of expressions 3.14 it follows that:

1. there exists such formula A ∈ ForTL that AX and ○(A) ∈ X,

or

2. there exists such name letter P ∈ Ln and such number i ∈ ℕ that P+iX and PiX.

If the first case occurs, then from fact 3.13 we know that 𝔐TLA or 𝔐TL ⊭ ○(A). If the second case occurs, then from definition of model 3.3 we know that there exists no such function γ ∶ ℕ → D that for each j ∈ ℕ:

  1. if P+jX, then γ(j) ∈ d(P)
  2. if PjX, then γ(j) ∉ d(P).
←74 | 75→

Since then γ(i) ∈ d(P) and γ(i) ∉ d(P). Hence, from the definition of model appropriate for the set of expressions 3.16 it follows that 𝔐TL is not a model appropriate for set of expressions X. Whereas from the arbitrariness of model 𝔐TL it follows that there does not exist model 𝔐TL appropriate for X.

3.3.1Tableau rules for TL

The starting point for the construction of a tableau system for TL should be a precise definition of the concept of tableau rule. Before we proceed to the general concept of rule, we will introduce a certain auxiliary function∗ ∶TeTL∖ForTL → ℕ such that for any P ∈ Ln and any i ∈ ℕ:

  • ∗(P+i) = i
  • ∗(Pi) = i.

To each expression not being a formula, meaning a name letter with an index, function ∗ attributes an index which is found in it.

Similar to the case of CPL, we will first provide the general concept of rule. Not only because it allows to provide the general conditions that a tableau rule must meet. In the case of TL we will also provide alternative sets of tableau rules that are suitable for construction of a tableau system for TL. This means that within the below general concept of a tableau rule, we can define different sets of tableau rules that define various, however equivalent in terms of scope for correct inferences, tableau systems for TL (see note 3.20).

Definition 3.18 (Rule). Let P(TeTL) be a power set of the set of tableau expressions. Let P(Te)n be n–ry Cartesian product for some

n ∈ℕ.

• By a rule we understand any subset RP(TeTL)n such that if ⟨X1, . . . ,Xn⟩∈ R, then:

1. X1 is t-consistent

2. X1Xi, for each 1 < in.

• If n ≥ 2, then each element R will be called ordered n-tuple (pair, triple, etc., respectively).

• The first element of each n-tuples will be called an input set (set of premises), while its remaining elements output sets (sets of conclusions).

←75 | 76→

Definition of rule for TL differs from the definition of rule for CPL 2.12 among other things4 in having introduced to the definition of rule for TL a condition of t-consistency of the input sets. We will no longer put down the rules in the form of sets, but immediately in the schematic, fractional form. Thus, from the general definition of rule itself, it follows that the input sets of tableau rules will be t-consistent.

A set of tableau rules designed for the defined tableau system for TL shall be introduced by means of the following definition.

Definition 3.19 (Tableau rules for TL). Tableau rules for TL are the following rules:

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

1. j ∉ ∗(X ∖ForTL)

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

Set of tableau rules for TL will be defined as RTL.

According to the general definition of rule 3.18, the input sets of each rule are t-consistent. In addition, in each tableau rule, the input set is basically contained in the output set. The notations provided are schemes of pairs belonging to the rules, so for each of the rules X is any set of expressions, P, Q are any name letters and j is any index such that all these elements satisfy the conditions imposed on the rule. One novelty is that set RTL contains rules that must include at least two premises, e.g. rule Ra+.

←76 | 77→

Another new and important aspect of the tableau rules in this system for TL are conditions in rules Ri, Ro. In both rules, we basically have the same conditions, so through one example we will discuss them collectively.

These conditions must be met if a given set is to be an output set with an assumed input set. So, the notation adopted in both rules says, for example, that if pair ⟨X ∪{PiQ},X ∪{PiQ,P+j,Q+j}⟩ belongs to rule Ri, then:

1. j ∉ ∗(X ∖ForTL) and

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

These conditions are therefore necessary conditions for a given pair to belong to the rule.

Condition 1 requires the index which is entered to be new, meaning not appearing in any expression belonging to the output set. The semantic intuitions behind this procedure require the object denoted by new index to be new as well and not to remain in any positive relationship with the other names that appear in a given proof sequence.

In turn, condition 2 requires the input of a pair of expressions (in this example pair P+j, Q+j) to take place only when a similar pair does not already belong to the output set. In practice, this condition makes it impossible to enter unnecessary expressions in the proof, as is the case in example 3.21.

Analogous conditions will be considered in the next chapter which will be devoted to modal logic. There, we are going to provide an example which will illustrate the problem of infinite branches. In that case, even applying conditions blocking the unnecessary use of rules will not prevent the emergence of infinite branches. It will, however, prevent the creation of infinite branches in situations where this is not a consequence of logic itself, but of the wrong definition of the tableau system.

Remark 3.20. We can consider alternative sets of rules for the construction of a tableau system for TL. The following rule would help.

Rule Re′− allows to proceed from premises PeQ, Q+j to conclusion Pj. The semantic intuition contained in this rule says that if a name from the predicate in a general contradicting proposition has a subject j as the designator, then this object is not the designator of the subject of this proposition.

Making use of rule Re−, we can define the following sets of tableau rules, different from set RTL:

←77 | 78→

(a) RTL ∪{Re}

(b) (RTL ∖{Re})∪{Re′−}.

Likewise, we could consider another rule that says that if we have a proposition PaQ and expression Qj saying—intuitively—that an object denoted by j is not a designator of name Q, then this object is not a designator of name P either.

Making use of rule Ra, we can define the following sets of tableau rules, different from set RTL:

(a) RTL ∪{Ra}

(b) (RTL ∖{Ra+})∪{Ra}.

Furthermore, extending the language of logic of TL to the language which includes expressions denoting statements that a particular object is or is not the designator of a given name, we could consider another rule that allows “reversing” general contradicting propositions:

It is worth noting that the tableau system for TL we are now describing, there are no branching rules (all tableau rules are sets of pairs). So there will be no branchings in the tableaux. However, we might consider such variant of rule Ra+ which would allow branchings:

However, due to the economy of tableau proof, it is better—as far as possible — to introduce the fewest possible number of tableau rules that are not sets of pairs.

Although all these rules and sets of rules seem to be interesting, we will not consider them all — neither for the language of TL, nor for extended languages — for the reasons described in the previous chapter (note 2.19). Instead, we will focus on the tableau system determined by set of rules RTL.

Nonetheless, let us stress once again that the examples provided indicate that the general definition of rule 3.18 makes sense. There may exist many sets of tableau rules that potentially—we mean (potentially) because to determine this it always requires a proof—they define the same logic.

←78 | 79→

Example 3.21. Starting from set X ∪{PiQ} and using rule Ri without condition 2, we could get an infinite sequence in which we enter a new index in each of the elements:

Such a sequence is infinite not because of the properties of the logic itself, but because of the unnecessary acceptance of continuous application to the same elements of the rule already applied once.

The adopted set of tableau rules — in our case set RTL — determines the content of the range of successive concepts of the tableau system. Although the formal concepts that we will describe will be analogous to those from the previous chapter, each of them will depend on set RTL.

3.3.2Branches for TL

With a fixed set of tableau rules, we can proceed to the concept of branch. As we already know, branches are such sequences of sets that each two adjacent elements are in turn: an input set and an output set of some n-tuple that belongs to the set of tableau rules. Branches are therefore setwise objects consisting of sets. Below, we present the formal definition of branch in the tableau system for TL.

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

  1. ϕ(1) = X
  2. for any iK: if i + 1 ∈ K, then there exists such rule RRTL and such pair ⟨Y1,Y2⟩∈ R that ϕ(Xi) = Y1 i ϕ(Xi+1) = Y2.

Having two branches ϕ, ψ such that ϕψ we shall state that:

  • ϕ is a sub-branch of ψ
  • ψ is a super-branch of ϕ.

Denotation 3.23. From now on — when speaking of branches for TL — for convenience, we will use the following notations or designations:

  1. ←79 | 80→ X1, . . . ,Xn, where n ≥ 1
  2. X1, . . . ,Xn⟩, where n ≥ 1
  3. abbreviations: ϕM (where M is a domain ϕ, i.e. ϕMP(TeTL))
  4. or—to denote branches—small Greek letters: ϕ, ψ, etc.