PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 93–97 DOI 102298/PIM0796093K

ANALYTIC TABLEAUX AND INTERPOLATION

Miodrag Kapetanović

Dedicated to Saša Kron, friend and techer.

Abstract. A tableau system for the predicate logic with countable conjunctions and disjunctions is presented and the completeness of the set of rules proved. These tableaux are used to prove a slightly more general form of the Malitz interpolation theorem.

1. Introduction

The logic L_{ω_{1}ω}, obtained from first order logic by allowing countable conjunctions and disjunctions, has been extensively studied and used in model theory ([3] is a standard reference). Although Gentzen systems for this logic also exist (see [4] but also [1] for a more recent treatment), the corresponding tableau system(s) do not seem to be used in practice. For that reason a tableau system for L_{ω_{1}ω} is presented in some detail, followed by a completeness proof. Included are minor novelties in the inductive definition of tableau with possible technical advantages.

In order to simplify exposition all structures are assumed to have at least one constant. L_{ω_{1}ω}-formulas are defined as in the first order logic with the additional clause: if Φ = {ϕ_{i} | i < ω} is at most countable set of formulas, then both ⋀ Φ and ⋁ Φ are formulas written also as ⋀_{i<ω} ϕ_{i}, ⋁_{i<ω} ϕ_{i} respectively. Hereafter a formula (sentence) will always mean an L_{ω_{1}ω}-formula (sentence). Writing φ as φcy we emphasize that all constants in φ are among c = {c_{0}, c_{1}, …} and that all free variables in φ are among y = {y_{0}, y_{1}, …} and similarly for sets of formulas.

2. A tableau system for L_{ω_{1}ω}

Since L_{ω_{1}ω} is an extension of first order logic we could simply make use of the well known uniform notation of Smullyan [6], treating ⋀ Φ as α, ⋁ Φ as β, etc. Another approach is used instead, that seems simple and illustrative enough: only sentences in negation normal form, i.e., those which are built up from atomic formulas and their negations using ∧, ∨, ∀ and ∃ are treated. There is no loss of generality since every formula is equivalent to a formula in such form, and φ ∧ ψ, φ ∨ ψ and φ → ψ are defined as ⋀{φ, ψ}, ⋁{φ, ψ} and ⋁{¬φ, ψ} respectively. Hence the following rules are needed:

2000 Mathematics Subject Classification: 03C40, 03C75, 03F99.

(∧) \frac{⋀ Φ}{Φ}  (∨) \frac{⋁_{i<ω} φ_{i}}{φ_{0} | φ_{1} | … | φ_{i} | …}  (∀) \frac{∀xφ}{φ_{x}t}  (∃) \frac{∃xφ}{φ_{x}c}

Here t is any ground term and c is a new constant, which should be understood in the following sense. The set L(φ) of all relational and functional symbols (including symbols of constants) occurring in φ is the language of φ, and L_{C}(φ) is the expansion of L(φ) by a countable set C of new constants, i.e., L(φ) and C are disjoint, whereas by φ-term we mean any ground term generated by the constants from L_{C}(φ). More explicitly, if f is an n-ary functional symbol from L_{C}(φ) and t_{0}, …, t_{n−1} a sequence of φ-terms, then ft_{0} … t_{n−1} is a φ-term.

Tableaux are defined as rooted trees whose nodes have at most countably many immediate successors and each node is labelled with a set of sentences. Nodes are denoted by σ, τ, … and τ0, τ1, … are immediate successors of τ. In the following definition T denotes a tableau for a given sentence φ^{1} and l_{σ}^{T} is the label of the node σ from the underlying tree of T.

Definition 2.1. (1) A tree whose only node is labelled by {φ} is a

tableau for φ.

(2) If ⋀ Φ ∈ l_{σ}^{T}, then T′ obtained from T by setting l_{σ}^{T′} = l_{σ}^{T} ∪ Φ is a tableau for φ.

(3) If ∀xψ ∈ l_{σ}^{T}, t is a φ-term and if T′ is obtained from T by setting l_{σ}^{T′} = l_{σ}^{T} ∪ {ψ_{x}(t)}, then T′ is a tableau for φ.

(4) If ∃yψ ∈ l_{σ}^{T} and c ∈ C is new for T, then T′ is obtained from T by setting l_{σ}^{T′} = l_{σ}^{T} ∪ {ψ_{y}c} is a tableau for φ.

(5) Let τ be a leaf of a branch containing σ. If ⋁_{i<ω} φ_{i} ∈ l_{σ}^{T} and T′ stems from T by expanding the domain of T by {τi | i < ω} and by setting l_{τi}^{T′} = {φ_{i}} for all i < ω then T′ (based on the new domain) is a tableau for φ.

For every leaf τ of the domain of T the set B = ⋃{l_{σ}^{T} | σ is a predecessor of τ} is a branch of T. A branch is closed if it contains a pair of complementary closed literals and a tableau is closed if all its branches are closed. It is easily checked that the rules are correct: if a tableau for φ closes, then φ has no model.

Since Hintikka sets play the central role in completeness proofs we recall the definition and sketch the proof of the main lemma.

Definition 2.2. A set H of sentences is a Hintikka set if it satisfies the following conditions:

(H0) for all atomic sentences ϕ from L(H), {ϕ, ¬ϕ} ⊈ H; (H∧) if ⋀ Φ ∈ H, then Φ ⊆ H; (H∨) if ⋁ Φ ∈ H, then Φ ∩ H ≠ ∅; (H∀) if ∀xφ ∈ H, then φ_{x}t ∈ H for all ground terms from L(H); (H∃) if ∃xφ ∈ H, then φ_{x}t for some ground term t from L(H).

1There is no harm in speaking about tableaux for (at most) countable sets of sentences since any such set Φ can be replaced by ⋀ Φ, or even about a tableau for a set of sets of sentences, where the intended meaning for {Φ_{i} | i < ω} is ⋁{⋀ Φ_{i} | i < ω}.

The connection is established by calling a closed non-literal used up on a branch if it satisfies the appropriate condition from the above definition. For instance ⋀ Φ is used up on B if Φ ⊆ B etc.

Lemma 2.1 (Hintikka’s Lemma). Every Hintikka set possesses a term model.

Proof. Let A = (A, …, f^{A}, …, …, R^{A}, …), where A = {t | t is a ground term of L(H)} and f^{A}(t_{0}, …, t_{n−1}) =^{def} ft_{0} … t_{n−1} for all n-ary function symbols from L(H), n ∈ ω. We stipulate A ⊨ ϕ ⇔ ϕ ∈ H for all atomic sentences from L(H) and the proof of A ⊨ H by induction on the complexity of sentences from H is straightforward. For instance if ϕ ∈ H is atomic then A ⊨ ϕ by definition of A and if ¬ϕ ∈ H, then ϕ ∉ H by (H0), so A ⊭ ϕ again by the definition of A. Further if ⋀ Φ ∈ H, then Φ ⊆ H, so A ⊨ Φ by induction hypothesis, hence A ⊨ ⋀ Φ and similarly for ⋁ Φ ∈ H, where A ⊨ Φ ∩ H, again using induction hypothesis. If ∃yψ ∈ H, then ψ_{y}t ∈ H for some ground t. By induction hypothesis A ⊨ ψ_{y}t, so A ⊨ ∃yψ. Finally if ∀xψ ∈ H, then ψ_{x}t ∈ H for all ground terms t, so A satisfies each of ψ_{x}t by induction hypothesis and we may conclude A ⊨ ∀xψ since A is a term structure. □

A set Γ of sentences is consistent if there is no closed tableau for ⋀ Γ.

Lemma 2.2. If {φ} is consistent, then there is a Hintikka set containing φ.

Proof. We shall define a sequence T_{0}, T_{1}, … of tableaux for φ together with the sequence B_{0} ⊆ B_{1} ⊆ … of respective consistent branches. Notice first that L(φ) is countable for every sentence φ and so is the set of all φ-terms as well as the set of all subsentences of φ and only these occur in a tableau for φ. This altogether guarantees the countability of all sets of sentences appearing in the tableau construction. With this in mind we can easily devise a particular enumeration of all L_{C}(φ)-sentences which ensures that the rule (∀) is applied to every (occurrence of a) sentence of the form ∀xψ unboundedly many times^{2}. Starting with B_{0} = {φ} and using the fact that the rules are correct, we can show that, given consistent B_{i} from T_{i}, any application of a rule must result in a T_{i+1} with at least one consistent branch B_{i+1} ⊇ B_{i}. As an illustration let ∃yψ ∈ B_{i} and let B_{i+1} = B_{i} ∪{ψ_{y}c} (c new for T_{i}). If B_{i+1} was inconsistent, then (by correctness) it would have no model, in other words B_{i} ⊨ ¬ψ_{y}c and, since c is new, B_{i} ⊨ ∀y¬ψ, a contradiction since ∃yψ ∈ B_{i}. Other cases are similar so there are two possibilities: we either stop at some stage i since all of B_{i} is used up or proceed generating a sequence {B_{i} | i < ω}. In the first case B_{i} is obviously a Hintikka set,otherwise let B = ⋃_{i<ω} B_{i}. Notice first that {ϕ, ¬ϕ} ⊈ B, since it would be included in some B_{i} which is impossible. Next, all sentences in B are obviously used up at some stage except universal ones. But given any such ∀xψ and any ground t, ψ_{x}t must appear in some B_{i}, since we kept visiting ∀xψ thus ensuring that all terms are attended to. □

2It is understood that each time ψ is instantiated by a term not used before for that occurrence of ψ.

Reformulating the statement we get the main theorem.

Theorem 2.1 (Completeness Theorem). If ⊨ φ, then there is a closed tableau for φ.

3. Interpolation

By A_{A} we mean the structure A enriched with all elements of A as constants and its signature is denoted by L_{a}(A), where a is the list of names of all elements of A. Recall that diag(A) = {θa | θa is a closed literal and A_{A} ⊨ θa} is the diagram of A.

Theorem 3.1. Given a sentence σ and a formula φz, suppose that for all A, B ⊨ σ and all a ⊆ A, if A ⊆ B and B ⊨ φa, then A ⊨ φa. Then there is a universal formula ψz such that σ ⊨ ∀z(φz ↔ ψz)^{3}.

Proof. Enrich L with a set c = {c_{0}, c_{1}, …} of new constants in 1–1 correspondence with z. If ψ_{z}c ≡ ⋀{χ_{z}c | χz is an L(φ)-formula of the form ∀x ⋁ Φxz, where Φ is a set of literals and σ, φc ⊨ χc}, then we shall prove that ψz is the desired universal formula. Obviously σ ⊨ φc → ψc and if the reverse is true we get σ ⊨ φc ↔ ψc, hence σ ⊨ ∀z(φz ↔ ψz) with ψ universal q.e.d.

Given A ⊨ σ ∧ ψc, it suffices to find B ⊇ A such that B ⊨ σ ∧ φc, since by the theorem assumption A ⊨ φc. By the downward Löwenheim–Skolem theorem we may assume A countable, so enrich L_{c}(φ) with (the list of the names of) all elements of A and let ϕ^{−} = ¬ϕ and (¬ϕ)^{−} = ϕ, for all atomic sentences ϕ of the expanded language. We claim that any tableau T for σ ∧ φc (in this language) has a branch on which there is no literal ϕac such that a ⊂ A and ϕ^{−}ac ∈ diag(A). Suppose not and let Φac = {ϕ_{B}ac | B is a branch of T, ϕ_{B}ac ∈ B and ϕ_{B}^{−}ac ∈ diag(A)}. Then a tableau for σ ∧ φc ∧ ⋀{ϕ^{−}ac | ϕac ∈ Φac} closes. This implies σ ∧ φc ⊨ ¬ ⋀{ϕ^{−}ac | ϕ ∈ Φ}, i.e., σ ∧ φc ⊨ ⋁ Φac. Notice that a is finite and constants from a are new for σ ∧ φc, so σ ∧ φc ⊨ ∀x ⋁ Φxc. Since A ⊨ σ ∧ ψc, it follows that A ⊨ ∀x ⋁ Φxc, hence A ⊨ ⋁ Φac, so A ⊨ ϕac for some ϕac ∈ Φac, contradiction since ϕ^{−}ac ∈ diag(A). Together this implies that σ ∧ φc ∧ ⋀ diag(A) is consistent, therefore has a model B. As B ⊨ diag(A) we are done. □

The above result is presented relative to a given sentence σ in order to gain some generality. If we drop that condition we get the well known preservation theorem of Malitz [5], although he had it for universal sentences only. In fact somewhat more general result holds as well, one that resembles so called Malitz interpolation theorem, also proved in [5] (and again for sentences only).

Theorem 3.2. Given a sentence σ and formulas φz, θz suppose that for all A, B ⊨ σ and all a ⊆ A, if A ⊆ B and B ⊨ φa, then A ⊨ θa. Then there is a universal formula ψz such that σ ⊨ ∀z(φz → ψz) ∧ ∀z(ψz → θz).

Proof. Define ψ as above and repeat the whole argument, only that this time we conclude A ⊨ θc, so that σ ⊨ ψc → θc and we are done. □

3It is fairly obvious that the condition is necessary as well.

4. Conclusion and future prospects

We have presented a tableau system for the predicate logic L_{ω_{1}ω} resembling Gentzen systems and applicable in model theory. Beside completeness proof a kind of interpolation theorem is proved that generalizes a result of Malitz using only a simple notion of diagram. It seems that a refined version of the infinitary case of the omitting types theorem can be obtained in the same manner. On the effective side, we can go back to the first order case and look for more effective constructions, leading possibly to automated treatment, since the form of the main results is retained.

References

[1] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic, Springer-Verlag, New York, 1984

[2] W. Hodges, Model Theory, Cambridge University Press, 1993

[3] H. J. Keisler, Model Theory for Infinitary Logic, North-Holland, Amsterdam, 1971

[4] E. G. K. Lopez-Escobar, An interpolation theorem for denumerably long formulas, Fund. Math. 57 (1965), 254–272

[5] J. Malitz, Universal classes in infinitary languages, Duke Math. J. 36 (1969), 621–630

[6] R. Smullyan, First-Order Logic, Dover, New York, 1995

Matematički institut Kneza Mihaila 36 11000 Beograd, p.p. 367 Serbia

    kapi@mi.sanu.ac.yu