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.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 XForTL, AForTL, the below statements are equivalent.

  • XA
  • XA
  • there exists finite YX and closed tableauY,A,Φ⟩.

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

(a) XAXA

Assume that XA. We must show that XA. From the assumption and definition ⊳ 3.33, we know that for each finite set YX, 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 𝔐TLY′ ∪{○(A)}.

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

(b) XA ⇒there exists finite YX and closed tableau ⟨Y,A,Φ⟩

Assume that for any finite subset YX, each tableau ⟨Y,A,Φ⟩ is open. Take any finite subset YX. 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 XA,

(c) there exists finite YX and closed tableau ⟨Y,A,Φ⟩ ⇒XA

Assume that there exists finite subset YX and closed tableau ⟨Y,A,Φ⟩. Indirectly assume that XA, thus, by definition of relation of semantic consequence 3.5, there exists such model 𝔐TL that 𝔐TLX, but 𝔐TLA. From fact 3.13, we know that 𝔐TL ⊧○(A). Consequently, 𝔐TLX∪{○(A)}, and thus 𝔐TLY ∪{○(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 𝔐TLY ∪{○(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 AForTL. 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 XA, then for any model 𝔐TL, if 𝔐TLX, then 𝔐TLA. Particularly, for such models 𝔐TL = ⟨D,d⟩ that ∣D∣ = σ(X ∪{○(A)}).

Now, assume that XA. From the theorem on completeness of tableau system of TL 3.56, we get that XA. By definition of relation of branch consequence 3.33, for any finite YX, 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 𝔐TLX∪{○(A)}, thus 𝔐TLX and 𝔐TLA, by fact 3.14.

By definition 3.52, domain D = {i ∈ ℕ ∶ i ∈ ∗(At(ϕ))}, and each object iD 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 iD, 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)}),𝔐TLX and 𝔐TLA.


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.