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

# 3.5.1 Estimation of cardinality of model for TL

We will now proceed to the main theorem which synthesizes all so far covered facts and lemmas, stating the dependencies between the semantic consequence relation, branch consequence relation and the existence of closed tableau.

Theorem 3.56 (Theorem on the completeness of tableau system for TL). For any X ⊆ ForTL, A ∈ ForTL, the below statements are equivalent.

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

Proof. Take any X ⊆ ForTL and A ∈ For. We will prove three implications.

(a) X ⊧ A ⇒X ⊳ A

Assume that X ⋫ A. We must show that X⊭A. From the assumption and definition ⊳ 3.33, we know that for each finite set Y ⊆X, there exists a branch beginning with set Y ∪{○(A)} which is maximal and open. Take any finite subset Y′ ⊆ X. Thus, there exists branch ϕ beginning with set Y′∪{○(A)} which is maximal and open. Since branch ϕ is maximal and open, so by lemma on generation of model 3.54, there exists model 𝔐TL such that 𝔐TL ⊧ Y′ ∪{○(A)}.

Due to the fact that set Y′ is arbitrary, so for any Y, finite subset of X, there exists model 𝔐TL such that 𝔐TL ⊧ Y ∪{○(A)}. Thus, for any Y, finite subset of X, Y ⊭ A, due to the fact 3.13.While by fact 3.9, relation ⊧ is compact, so X ⊭ A.

(b) X ⊳ A ⇒there exists finite Y ⊆ X and closed tableau ⟨Y,A,Φ⟩

Assume that for any finite subset Y ⊆ X, each tableau ⟨Y,A,Φ⟩ is open. Take any finite subset Y ⊆ X. By the assumption, each tableau ⟨Y,A,Φ⟩ is open. By definition of tableau 3.36, each set Φ contains one branch beginning with set ←96 | 97→Y ∪{○(A)}. Consequently, by definition of open tableau 3.48, each branch beginning with set Y ∪○(A) is open. However, from fact 3.32, we know that since set Y ∪{○(A)} is finite, then there exists branch beginning with Y ∪{○(A)} that is maximal. Since that branch is open and set Y is a finite subset of X, by definition of relation of branch consequence 3.33 X ⋫ A,

(c) there exists finite Y ⊆ X and closed tableau ⟨Y,A,Φ⟩ ⇒X ⊧ A

Assume that there exists finite subset Y ⊆ X and closed tableau ⟨Y,A,Φ⟩. Indirectly assume that X ⊭ A, thus, by definition of relation of semantic consequence 3.5, there exists such model 𝔐TL that 𝔐TL ⊧ X, but 𝔐TL ⊭ A. From fact 3.13, we know that 𝔐TL ⊧○(A). Consequently, 𝔐TL ⊧ X∪{○(A)}, and thus 𝔐TL ⊧ Y ∪{○(A)}. Since tableau ⟨Y,A,Φ⟩ is closed, then by definition 3.48, Φ contains branch ψ beginning with set Y ∪{○(A)} which is closed. So, branch ψ is maximal by conclusion 3.30 and has lengths n, for certain n ∈ℕ. What is more, by conclusion 3.29, set ψ(n) is t-inconsistent.

Since 𝔐TL ⊧ Y ∪{○(A)}, so model 𝔐TL is appropriate for set Y ∪{○(A)}. Now, applying lemma 3.55, n −1-times we get conclusion that 𝔐TL is appropriate for set ψ(n). However, due to the fact that ψ(n) is t-inconsistent and conclusion 3.17, there exists no model appropriate for ψ(n).

### 3.5.1Estimation of cardinality of model for TL

When applying tableau methods for TL another issue appears. With the tableau proof, we can estimate the upper limit of the cardinality of models that we only need to check in order to establish whether a given inference is correct7.While, in the study we do not take up this issue in general (as it is related to the issue of decidaility), but this outcome for TL we can virtually get directly from the theorem on completeness of tableau system for TL 3.56.8

By existential formula, we mean any formula in form PiQ or PoQ, where P, Q, ∈ Ln.

Now, we shall 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 formulas, function λ “selects” all existential formulas that belong to a given set.

←97 | 98→Now, in turn, we shall define 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.

We have the theorem.

Theorem 3.57. Let X be a finite set of formulas and let A ∈ ForTL. Then:

Proof. Take any finite set of formulas X and any formula A.

The implication “from the right to the left” follows from the definition of relation of semantic consequence 3.5. Because if X ⊧ A, then for any model 𝔐TL, if 𝔐TL ⊧ X, then 𝔐TL ⊧ A. Particularly, for such models 𝔐TL = ⟨D,d⟩ that ∣D∣ = σ(X ∪{○(A)}).

Now, assume that X ⊭A. From the theorem on completeness of tableau system of TL 3.56, we get that X ⋫ A. By definition of relation of branch consequence 3.33, for any finite Y ⊆ X, there exists maximal and open branch beginning with set Y ∪{○(A)}. Since X is a finite set, so there exists maximal and open branch ϕ beginning with set X ∪ {○(A)}. So, by lemma on generation of model 3.54, there exists such model 𝔐TL = ⟨D,d⟩ that 𝔐TL ⊧ X∪{○(A)}, thus 𝔐TL ⊧ X and 𝔐TL ⊭ A, by fact 3.14.

By definition 3.52, domain D = {i ∈ ℕ ∶ i ∈ ∗(At(ϕ))}, and each object i ∈ D emerged in some expression in ⋃ϕ ∩(TeTL ∖ For) by the application of rule Ri or Ro to some existential formula. As for each existential formula, we can only one time apply rule Ri or Ro, thus ∣D∣ ≤ σ(X ∪{○(A)}).

Model 𝔐TL was generated by an open and maximal branch, so rule Ri or Ro was applied to each existential formula. Thus, for any existential formula, there exists at least one object i ∈ D, due to the fact that rules Ri and Ro introduce expressions with new indices. Hence, ∣D∣ ≥ σ(X ∪{○(A)}).

So, consequently, there exists such model 𝔐TL = ⟨D,d⟩ that ∣D∣ = σ(X ∪ {○(A)}),𝔐TL ⊧ X and 𝔐TL ⊭ A.

1 Because we are going to name systems of various types of reasoning about the relationships between names, we will use rather term ‘Term Logic’ than ‘Syllogistic logic’.

2 The considerations contained in this chapter are based on the English language study [9]. In that paper, we presented an outline of the tableau system for TL without a thorough analysis of details. Since the production of this article, we have also generalized the concept of tableau rules and modified other tableau concepts which has affected other concepts and the very nature of the tableau system. Some other variants of tableaux for syllogistic are presented in [15], [22].

3 We write about classic categorical propositions because categorical propositions can also take non-classical forms. They can be e.g. any numerical propositions: At least five P are Q, or e.g. modal propositions de re: Each P is by necessity Q. Besides, in the last chapter we will construct a tableau system for the logic of categorical modal propositions de re. In addition, there are many other possibilities to enrich classical categorical propositions.

4 We write among other things since this definition above all differs in the set on which we define rules. Nevertheless, all the other conditions are nearly identical to those of the concept of rule for CPL.

5 Note that we are considering a pattern of inference rather than a specific inference as we use metavariables and letters instead of indices. It is obvious, however, that further considerations would be identical if we used name letters and digits.

6 Of course, we might define equivalents of rules Ri and Ro in such a way that the introduced expressions as indices only had for instance the least number that does not appear in the set to which we apply the rule. Then, the number of branches would amount to one. There are many ways to define these rules similarly, but from the formal point of view each time we would then examine a different axiomatization than the assumed set of rules RTL.

7 Estimations of cardinality of model for syllogistic, for languages richer than the language of TL, have been examined in the studies by: A. Pietruszczak [20], [21], P. Kulicki [17], [18].

8 This outcome was originally described in article [9]. However, when defining the tableau system for TL, in that study, we applied another set of rules and non-formalised tableau concepts.