Previous: All About Countable Saturation

After I had finished writing up and illustrating the proof of countable saturation in the last post, I came up with a significantly simpler proof. Darn! I don’t want to erase all those pretty pictures I already made, so I’ll just include this proof as a separate little bonus.

I’m also going to be a little more careful with notation that I have been thus far, by distinguishing structures from their universes. The fancy 𝔐 will refer to a structure, which has both a universe as well as an interpretation of all the constant, function, and relation symbols. The universe of 𝔐 will be written with a non-fancy M.

The Proof

Let 𝔐 be the ultraproduct ∏(𝔐_k)_k∈ℕ/U.
Let S = {φ₁(x), φ₂(x), φ₃(x), …} be any countable set of formulas with countably many parameters.

Suppose S is finitely realizable in 𝔐.
Then for each n, 𝔐 ⊨ ∃x (φ₁(x)∧…∧φ_n(x)).
So by Łoś’s theorem, for each n, the set of models that realize φ₁(x)∧…∧φ_n(x) is U-large.
So for each n, { k | 𝔐_k ⊨ ∃x (φ₁(x)∧…∧φ_n(x)) } ∈ U.

Here’s a visualization:

In this image, 𝔐₁ realizes φ₁(x)∧…∧φ₅(x), 𝔐₃ realizes all of S, and 𝔐₅ doesn’t realize φ₁(x).
The finite realizability of S tells us that {1, 2, 3, 4, 6, 7, …} (the indices of models realizing φ₁) is U-large. So are {1, 2, 3, 4, 7, …}, {1, 3, 4, 7, …}, {3, 4, 7, …}, and so on.

Now we add a new constant c to L.
We want to define c on each 𝔐_k in such a way that in 𝔐, c refers to an element of M that realizes all of S.
We do this by saying that in 𝔐_k, c refers to an element of M_k that realizes as large an initial segment of S as possible. More precisely:

For each finite k, consider the largest n for which 𝔐_k ⊨ ∃x (φ₁(x)∧…∧φ_n(x)). (In the above example, for k = 1 we’d have n = 5. For k = 2 we’d have n = 2. And so on.)
In 𝔐_k, c will refer to any object in M_k that realizes φ₁ through φ_n. Let’s call this object a_k.
In other words, a_k is an element of M_k that realizes as large of an initial segment of S as possible, and c refers to this element.

Two special cases:
What if 𝔐_k realizes all of S? Then in 𝔐_k, c will refer to any a_k ∈ M_k that realizes all of S.
And if 𝔐_k doesn’t realize φ₁? Then in 𝔐_k, c will refer to any arbitrary element of M_k.

One important consequence of this way of defining the “a_k“s is that for any k and n, a_k realizes φ₁(x)∧…∧φ_n(x) in 𝔐_k if and only if 𝔐_k ⊨ ∃x (φ₁(x)∧…∧φ_n(x)). This’ll be used in a few lines, marked by a blue =.

The ultraproduct construction now tells us exactly what c refers to in 𝔐: the equivalence class [a₁, a₂, a₃, …].
All that’s left to do is to prove that this element of 𝔐 realizes all of S. Here’s the argument:

Let φ_n(x) be any arbitrary formula in S.
{ k | a_k realizes φ_n in 𝔐_k } ⊇ { k | a_k realizes φ₁(x)∧…∧φ_n(x) in 𝔐_k } = { k | 𝔐_k ⊨ ∃x (φ₁(x)∧…∧φ_n(x)) } ∈ U.
Since ultrafilters are closed under supersets, { k | a_k realizes φ_n(x) in 𝔐_k } ∈ U
Since c refers to a_k in 𝔐_k, { k | 𝔐_k ⊨ φ_n(c) } ∈ U.
So by Łoś’s theorem, 𝔐 ⊨ φ_n(c).
So in 𝔐, [a₁, a₂, a₃, …] realizes φ_n.
Since φ_n was an arbitrary formula in S, [a₁, a₂, a₃, …] realizes all of S.

And we’re done! Since [a₁, a₂, a₃, …] realizes all of S, S is realizable!

Concluding thoughts

This proof is pretty similar to the one in the last post, but with some unnecessary bells and whistles removed. Unlike the last one, this one was designed by me personally, so it’s possible there’s something important missing. But I doubt it!

It has a similar “constructive” character to the last proof, in that it doesn’t just say that S is realizable in M, it also tells you exactly what the element of M that realizes S is. I’ve noticed that this “constructiveness” is a common feature of proofs in this area of logic. Look back at our proofs of the compactness theorem. They didn’t just tell us that our starting set of sentences was satisfiable; they actually gave us a recipe for constructing a model of that set of sentences.

Now, why am I putting constructive in quotation marks? The thing is, on the traditional notion of constructiveness, none of these proofs are really constructive, because free ultrafilters can’t be shown to exist for arbitrary infinite sets without the axiom of choice. (Remember our usage of Zorn’s lemma in Part 3 of the series?) The axiom of choice is a big no-no for the constructivist, and there is a sense in which you can’t super concretely “get your hands on” a free ultrafilter. There’s no nice general procedure for specifying what’s in the ultrafilter and what’s not; if there was we wouldn’t need choice, we’d just define the ultrafilter with this procedure!

Nonetheless, I think there’s a nice notion of “conditional constructiveness”, where you say “assuming that you somehow get your hands on an ultrafilter, then what can you construct with it”. And in this sense, you can construct all the things I gave examples of earlier. 

Not all nonconstructive objects are equally scary or hard-to-comprehend in my eyes, so it’s nice to be able to say something like “these are both nonconstructive in the absolute sense, but the first is constructive conditional on the existence of a free ultrafilter on the naturals, and the second is constructive conditional on the ZFC-independent existence of a large cardinal.” An approach like this frees you up to care about constructiveness without having to ascribe to the full strict Brouwerian philosophy.