Three old pieces

Kees Doets

May 31, 1999

Abstract

This contribution consists of three pieces that are independent of each other. The first one recalls an expedition into Swedish Lapland undertaken by Johan and myself 25 year ago and is mainly picturesque, the second one is a remark to Johan’s 1972 Master’s Thesis centering around a new equivalent of the Prime Ideal Theorem, and the final one is a short proof of the Boundedness Theorem that is fundamental for the paper of Johan and Jon Barwise on pebble games.

Contents

1  2
2  2
3  5

At the time when Johan was exactly half the age he is now, we departed for the North in order to make an extended hike in Lapland. The undertaking must have been less agreeable to Johan for several reasons. Scientifically, he cannot have found much inspiration with me during the many hours that we shared company in our cramped bivouac: it was in this period that he was laying the foundations for what now is well-known as modal correspondence theory, and modal logic wasn’t exactly my favorite subject. However, a far greater problem was looming over our expedition. Only one week earlier, Johan had fallen deeply and irrevocably for the charms of a girl by the name of Lida, and, instead of looking forward to romantic hours in sunny Amsterdam, he had to face sub-arctic swarms of ruthless mosquitoes.

We left early august for the 3000 kms drive taking us beyond the Polar Circle. In Malmö we purchased the lightest tent possible, not withstanding the fact that it by necessity also was the smallest one. In Härnösand, Johan had to visit a dentist for the first time. Far north in Vietas, we changed from car to backpack in a nasty drizzle. That night, a few hours prior to our take-off, we witnessed on tv Nixon’s fall from presidency. At the end of our second day’s hike into vacuum lapponia, it turned out that Härnösand’s dentistry wasn’t as unfallible as we’d hoped for. We walked back to civilisation, Johan in pains all the way. This time, a Malmberget dentist took care of Johan, sending him away equipped with both a new filling in his tooth and a do-it-yourself emergency kit in his pack.

There remained sufficiently many days for a somewhat smaller venture through the heart of Sarek, which was completed without further problems. In particular, I was thankful I never had to melt the do-it-yourself kit into Johan’s molar.

Some late august evening, I delivered Johan, at the Weteringplantsoen, to the arms of Lida.

2

Exactly two years prior to the events related above, Johan finished a Master’s Thesis [Ben72] on weakenings of the Axiom of Choice, to which the following is a footnote.

Call a set S a selector for a collection A of sets if every intersection a ∩ S (where a ∈ A) is a singleton. The following is one of the standard applications of Compactness.

On Selectors. Suppose that every finite subcollection of a certain collection of finite sets has a selector. Then the collection itself has a selector as well.

This is generalized in [Ben72] to the following (Johan’s) Proposition, in which the target-class of singleton-subsets of the previous proposition can be just any class K of subsets:

JP. Suppose that A is a collection of finite sets and K ⊂ ⋃_{a∈A} ℘(a) is such that [⋆] for every finite B ⊂ A there exists S ⊂ ⋃ B such that ∀a ∈ B(a∩S ∈ K). Then S ⊂ ⋃ A exists such that ∀a ∈ A(a ∩ S ∈ K).

Johan proves JP using the Tychonov Theorem for T2-spaces and shows that it implies the Boolean Prime Ideal Theorem, settling JP as an equivalent of the latter.

Looking for illustrations of the use of clauses in a text on resolution (where clauses are all-important), it occurred to me that JP allows a proof that is amusing in its simplicity.

Recall that a (propositional) clause is a finite set of literals (propositional variables and their negations) mimicking the disjunction of its elements. Thus, a clause is satisfied by a truth assignment if at least one of its elements takes the value true.

Proof of JP. Consider the elements of ⋃ A as propositional variables. Σ is the set of all clauses of the form (a−b)∪\overline{b} where a ∈ A, b ⊂ a, and b ∉ K (I use the notation \overline{b} = \{\overline{x} | x ∈ b\}, where \overline{x} denotes the negation of a variable x). Any truth assignment γ : ⋃ A → {true, false} is associated with a set S^{γ} = {x ∈ ⋃ A | γ(x) = true}. JP is now (almost) immediate from Clausal Compactness (a set of clauses is satisfiable whenever everyone of its finite subsets is) and the following

Claim. γ satisfies Σ iff ∀a ∈ A(a ∩ S^{γ} ∈ K).

The proof of this is straightforward but omitted, since a similar claim follows below. □

Reflecting on this proof, the following modification eventually presented itself. First, note that, instead of requiring [⋆] for arbitrary finite B ⊂ A, it suffices to require this only for subcollections {a ∈ A | a ⊂ Y } where Y ⊂ ⋃ A is finite, since these subcollections are “dense” among the finite ones: every finite B ⊂ A is contained in the collection {a ∈ A | a ⊂ ⋃ B} of this form. This explains the somewhat different wording of the following, where collections of finite sets appear to have vanished.

JP^{+}. Suppose that X is a set and L is a collection of pairs (Y, S) —where Y ⊂ X is finite and S ⊂ Y — that satisfies

[⇓] if (Y, S) ∈ L and Y′ ⊂ Y, then (Y′, S ∩ Y′) ∈ L.

If for every finite Y ⊂ X there exists S ⊂ Y with (Y, S) ∈ L, then S ⊂ X exists such that for every finite Y ⊂ X, (Y, S ∩ Y) ∈ L.

This is reminiscent of the fact that a structure can be expanded into a model of a universal first-order theory whenever all its finite substrucures can be so expanded — cf. [Doe71].

The versatility of JP^{+} (much greater than that of either JP or the former model-theoretic principle) is witnessed by the following examples. In 1–4 and 8, the objects to be constructed are plain sets; however, in 5 it is a relation and in 6 a sequence of sets: note how this circumstance affects the choice of X in each case.

1. JP^{+} immediately implies JP. As indicated above, put X = ⋃ A and let (Y, S) ∈ L iff ∀a ∈ A(a ⊂ Y ⇒ a ∩ S ∈ K).

2. Also, the Boolean Prime Ideal Theorem is a straightforward consequence of JP^{+}. (X is the boolean algebra; (Y, S) ∈ L iff S ∩ Y′ is a prime ideal for every subalgebra Y′ included in Y.)

3. By coincidence, JP^{+} also easily implies another equivalent of the Boolean Prime Ideal Theorem considered by Johan: the fact that an inverse limit of a system of non-empty finite sets is non-empty. To see this, let A be the system of non-empty finite sets, put X = ⋃ A, and let (Y, S) ∈ L iff S is a selector for {a ∈ A | a ⊂ Y } that respects the morphisms of the system.

4. JP^{+} implies König’s Lemma, also discussed in [Ben72]. For, suppose given an infinite, finitely-splitting tree. For an integer n, let T_{n} be the (finite) set of nodes of height n, let X = ⋃_{n} T_{n} be the set of nodes of the tree, and let (Y, S) ∈ L iff S is a selector of {T_{n} | T_{n} ⊂ Y } that consists of pairwise comparable nodes.

5. JP^{+} readily implies the Order Extension Principle: every partial ordering can be extended to a linear one. If P is the partially ordered set, let X = P^{2}, and let (Y, S) ∈ L iff S is a linear ordering of Dom(Y) = {x ∈ P | ∃y((x, y) ∈ Y ∨ (y, x) ∈ Y)} that extends the given partial ordering on Dom(Y).

6. JP^{+} also implies another classic in this area: the fact that a graph G is k-colorable whenever everyone of its finite subgraphs is. This time, put X = {(x, i) | x ∈ G ∧ 1 ⩽ i ⩽ k}; let (Y, S) ∈ L iff the k sets C_{i} = {x ∈ G | (x, i) ∈ S} (i = 1, …, k) form a coloring of the subgraph {x ∈ G | ∃i[(x, i) ∈ Y]}.

7. The following problem comes from [Mil95] (a text that introduces mathematical logic using the “Moore-method”, via exercises that one often won’t find elsewhere); the reader may like to answer it using JP^{+}: “Given a set of students and a set of classes, suppose each student wants one of a finite set of classes, and each class has a finite enrollment limit. Show that if each finite set of students can be accommodated, they all can be accommodated.”

Proof of JP^{+}. Again, the elements of X are taken as propositional variables. For finite Y ⊂ X, Σ_{Y} is the set of all clauses (Y − S) ∪ \overline{S}, where S ⊂ Y and (Y, S) ∉ L. As above, \overline{S} = \{\overline{x} | x ∈ S\}, where \overline{x} is the negation of the variable x; and, for a truth assignment γ : X → {true, false}, S^{γ} is the associated set {x ∈ X | γ(x) = true}.

Claim. γ ⊧ Σ_{Y} iff (Y, S^{γ} ∩ Y) ∈ L.

Proof. First, note that, if S ⊂ Y, then:

γ ⊧ (Y − S) ∪ \overline{S} ⟺ S^{γ} ∩ Y ≠ S.

For: γ ⊧ x ∈ Y − S, iff x ∈ (S^{γ} ∩ Y) − S; and γ ⊧ \overline{x} ∈ \overline{S}, iff x ∈ S − (S^{γ} ∩ Y).

It follows that:

γ ⊧ Σ_{Y} ⟺ ∀S ⊂ Y [(Y, S) ∉ L ⇒ γ ⊧ (Y − S) ∪ \overline{S}]
⟺ ∀S ⊂ Y [(Y, S) ∉ L ⇒ S^{γ} ∩ Y ≠ S]
⟺ ∀S[S^{γ} ∩ Y = S ⇒ (Y, S) ∈ L]
⟺ (Y, S^{γ} ∩ Y) ∈ L.

Now assume the hypotheses of JP^{+}. Let Σ be the union of all Σ_{Y} where Y ⊂ X is finite. By the Claim, it suffices to satisfy Σ. By Clausal Compactness, it suffices to satisfy all finite subsets of Σ. Thus, suppose that Δ ⊂ Σ is finite. Let Y ⊂ X be the union of the finitely many finite Y′ ⊂ X such that for some S, (Y′ − S) ∪ \overline{S} ∈ Δ. By the Claim and by hypothesis, Σ_{Y} is satisfiable. By [⇓], every Σ_{Y′} with Y′ ⊂ Y will be satisfied as well. A fortiori, Δ is satisfied. □

Remark. Observe that the collections K of JP and L of JP^{+} don’t need to be definable in any way — a condition that one would expect necessary for a proof using Compactness. Related to this, the sets of clauses Σ_{Y} used in the proof are very much different from those used in standard compactness arguments for the proposition on selectors and the above-mentioned examples 2, 4–6. E.g., in the case of 6, one would use, for every finite G′ ⊂ G, the clauses {(x, 1), …, (x, k)} (x ∈ G′), \{\overline{(x, i)}, \overline{(x, j)}\} (x ∈ G′, i ≠ j), and \{\overline{(x, i)}, \overline{(y, i)}\} (for vertices x, y ∈ G′ connected by an edge). The set of these clauses is computable from G′ in time quadratic in the size of G′, a fact that is essential in the complexity reduction of graph colorability to clausal satisfiability. On the other hand, Σ_{Y} is exponential in the size of Y.

Now note that JP^{+} has brought us almost back to our starting point Clausal Compactness.

8. To see how easily Compactness is implied, let A be a set of clauses that is finitely satisfiable. Note that any S ⊂ ⋃ A that is consistent, that is: does not contain a pair of opposite literals, can be thought of as a truth assignment that assigns true to the variables in S and false to the variables of which the negation is in S. Obviously, a clause is satisfied by this truth assignment iff it is intersected by S. Thus, in order to apply JP^{+} to the problem of satisfying A, put X = ⋃ A and define, for finite Y ⊂ X, (Y, S) ∈ L iff S is consistent and intersects every clause in A which is included in Y.

In view of 1–8, JP^{+} might well be considered as a purely set-theoretic form of Clausal Compactness.

3

At the time, logic was very much dominated by set theory, thanks to the invention of forcing some ten years earlier. Therefore, it was remarkable that Barwise became prominent with his admissible fragments of infinitary languages. Until then, infinitary compactness hypotheses strictly belonged to the realm of large cardinals, but the Barwise Compactness Theorem turned out to be an instrument of great versatility at a more modest level.

One year after Johan and I forced our way through the Lapland wastes, Barwise published the final word [Bar75] on the subject. From the present perspective, [BvB96] seems therefore but an afterthought: it could have been written some twenty years earlier. The paper presents a most elegant view on interpolation and preservation. One of its cornerstones is the following ([BvB96] Theorem 3, p.5):

Boundedness Theorem. If Σ = Σ(<, …) is a set of L_{∞ω}-sentences that only has well-ordered (or well-founded) models, then the order types (or ranks) of these models are bounded.

In [Bar75], this is Theorem 3.1, p.270. The proof as given there is difficult to digest, due to the use of rather exotic supervalidity properties and the Weak Completeness Theorem. As an aid to readers of [BvB96], here follows a proof from which these ingredients have been eliminated.

Proof of the Boundedness Theorem. Assume that Σ is as in the hypothesis. For every existentially quantified subformula ∃x_{k}φ(x_{0}, …, x_{k}) of a sentence in Σ, choose a new k-ary (Skolem) function symbol f = f_{∃x_{k}φ}. SK is the set of all sentences (Skolem axioms) (avoiding clashes of variables)

∀x_{0} ⋯ ∀x_{k−1}(∃x_{k}φ → φ(x_{0}, …, x_{k−1}, f_{∃x_{k}φ}(x_{0}, …, x_{k−1}))).

Lemma 1. Every model for the vocabulary of Σ can be expanded into a model of SK.

In what follows, the notation

A ≺ B

is used to indicate that (i) the model A is a submodel of the model B, and (ii) every subformula of a Σ-sentence is satisfied by a sequence from A iff it is satisfied by this sequence in B.

Lemma 2. If A ⊂ B ⊧ SK, then A ≺ B.

Proof. Standard induction on subformulas of Σ-sentences. The only interesting case is for quantifications. Suppose that B ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}), and let f^{B} be the function that B associates with the Skolem-function symbol f_{∃x_{k}φ}. Since B ⊧ SK, we have that B ⊧ φ(a_{0}, …, a_{k−1}, f^{B}(a_{0}, …, a_{k−1})). Since A ⊂ B, we have f^{B}(a_{0}, …, a_{k−1}) ∈ A. Thus, by IH, A ⊧ φ(a_{0}, …, a_{k−1}, f^{B}(a_{0}, …, a_{k−1})), and A ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}). □

Lemma 3. If A_{0} ⊂ A_{1} ⊂ A_{2} ⊂ ⋯ is a chain of models of Σ + SK, then ⋃_{n} A_{n} ⊧ Σ.

Proof. By Lemma 2, A_{0} ≺ A_{1} ≺ A_{2} ≺ ⋯; and it follows that al these models are ≺ ⋃_{n} A_{n}: another standard induction on subformulas of Σ-sentences.

Here follows the quantifier-case. Suppose that ⋃_{n} A_{n} ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}), where a_{0}, …, a_{k−1} ∈ A_{m}. We need to show that A_{m} ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}). Let a_{k} ∈ ⋃_{n} A_{n} be such that ⋃_{n} A_{n} ⊧ φ(a_{0}, …, a_{k−1}, a_{k}). Choose m′ > m such that a_{0}, …, a_{k−1}, a_{k} ∈ A_{m′}. By IH, A_{m′} ⊧ φ(a_{0}, …, a_{k−1}, a_{k}). Thus, A_{m′} ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}). However, A_{m} ≺ A_{m′}. Hence, A_{m} ⊧ ∃x_{k}φ(a_{0}, …, a_{k−1}).

□

Next, let M_{n} consist of all models (A, a_{i})_{i<n} where A ⊧ Σ + SK, in which a_{n−1} < ⋯ < a_{0}, and which is Skolem-generated from a_{0}, …, a_{n−1}.

We can assume that the universe of such a model is a quotient of the set of terms generated from new constant symbols c_{0}, …, c_{n−1} for the latter elements. Consequently, we can assume that each M_{n} is a set; and hence, ⋃_{n} M_{n} is a set as well.

For models (A, a_{i})_{i<m} and (B, b_{i})_{i<k} in ⋃_{n} M_{n}, define

(A, a_{i})_{i<m} ≪ (B, b_{i})_{i<k} iff, m > k and (B, b_{i})_{i<k} ⊂ (A, a_{i})_{i<k}.

Claim 1. ≪ is well-founded.

Proof. By Lemma 3, the union of a ≪-descending sequence of models is again a model of Σ; but in such a union there is a <-descending sequence of elements, contrary to the assumption that all models of Σ are well-founded. □

Thus, every model in ⋃_{n} M_{n} has a ≪-rank.

Let (A, a_{i})_{i<n} be an arbitrary model of Σ + SK such that a_{n−1} < ⋯ < a_{0}. Then S(A, a_{i})_{i<n}, the submodel of (A, a_{i})_{i<n} that is Skolem-generated from a_{0}, …, a_{n−1}, can be assumed to be in M_{n}.

Claim 2. The <-rank of a_{n−1} in (A, a_{i})_{i<n} is bounded by the ≪-rank of the model S(A, a_{i})_{i<n}.

Proof. Induction w.r.t. the ≪-rank of S(A, a_{i})_{i<n}, as in Barwise’s proof. Let a_{n} ∈ A be an arbitrary element such that a_{n} < a_{n−1}. Then S(A, a_{i})_{i⩽n} ≪ S(A, a_{i})_{i<n}. Thus, the ≪-rank of S(A, a_{i})_{i⩽n} is smaller than the ≪-rank of S(A, a_{i})_{i<n}; and, by IH, the <-rank of a_{n} in (A, a_{i})_{i⩽n} is ⩽ the ≪-rank of S(A, a_{i})_{i⩽n}. Consequently, the <-rank of a_{n} in (A, a_{i})_{i⩽n} is < the ≪-rank of S(A, a_{i})_{i<n}; and since a_{n} was arbitrary, Claim 2 is follows. □

Finally, suppose that A is any model of Σ. By Lemma 1, we may w.l.o.g. assume that A has been expanded into a model of SK. The Boundedness Theorem now follows from the fact that the <-rank of A is bounded by the ≪-rank of S(A). To see this, let a be an arbitrary element of A. Then the <-rank of a in A is (by Claim 2) ⩽ the ≪-rank of S(A, a), which is (since S(A, a) ≪ S(A)) < the ≪-rank of S(A). □

References

[Bar75] J. Barwise: Admissible Sets and Structures. Springer, Berlin etc. 1975.

[Ben72] J. van Benthem: Weakenings of the axiom of choice (in dutch: “Verzwakkingen van het keuze-axioma”). Masters thesis, Dept. of Mathematics, University of Amsterdam 1972.

[BvB96] J. Barwise and J. van Benthem: Interpolation, preservation, and pebble games. Report ML-1996-12, ILLC 1996.

[Doe71] K. Doets: A theorem on the existence of expansions, Bull. de l’Ac.Pol. des Sci., Vol. XIX Nr. 1 1971 pp.1–3.

[Mil95] A.W. Miller: Introduction to mathematical logic. Dept. of Math., Univ. of Wisconsin 1995.