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 = {φ_{1}(x), φ_{2}(x), φ_{3}(x), …} be any countable set of formulas with countably many parameters.

Suppose S is finitely realizable in 𝔐.

Then for each n, 𝔐 ⊨ ∃x (φ_{1}(x)∧…∧φ_{n}(x)).

So by Łoś’s theorem, for each n, the set of models that realize φ_{1}(x)∧…∧φ_{n}(x) is U-large.

So for each n, { k | 𝔐_{k} ⊨ ∃x (φ_{1}(x)∧…∧φ_{n}(x)) } ∈ U.

Here’s a visualization:

In this image, 𝔐_{1} realizes φ_{1}(x)∧…∧φ_{5}(x), 𝔐_{3} realizes all of S, and 𝔐_{5} doesn’t realize φ_{1}(x).

The finite realizability of S tells us that {1, 2, 3, 4, 6, 7, …} (the indices of models realizing φ_{1}) 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 (φ_{1}(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 φ_{1} 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 φ_{1}? 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 φ_{1}(x)∧…∧φ_{n}(x) in 𝔐_{k} if and only if 𝔐_{k} ⊨ ∃x (φ_{1}(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_{1}, a_{2}, a_{3}, …].

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 φ_{1}(x)∧…∧φ_{n}(x) in 𝔐_{k} } = { k | 𝔐_{k} ⊨ ∃x (φ_{1}(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_{1}, a_{2}, a_{3}, …] realizes φ_{n}.

Since φ_{n} was an arbitrary formula in S, [a_{1}, a_{2}, a_{3}, …] realizes all of S.

And we’re done! Since [a_{1}, a_{2}, a_{3}, …] 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.