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 Mk 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 Mk that realizes φ1 through φn. Let’s call this object ak.
In other words, ak is an element of Mk 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 ak ∈ Mk that realizes all of S.
And if 𝔐k doesn’t realize φ1? Then in 𝔐k, c will refer to any arbitrary element of Mk.
One important consequence of this way of defining the “ak“s is that for any k and n, ak 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 [a1, a2, a3, …].
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 | ak realizes φn in 𝔐k } ⊇ { k | ak realizes φ1(x)∧…∧φn(x) in 𝔐k } = { k | 𝔐k ⊨ ∃x (φ1(x)∧…∧φn(x)) } ∈ U.
Since ultrafilters are closed under supersets, { k | ak realizes φn(x) in 𝔐k } ∈ U
Since c refers to ak in 𝔐k, { k | 𝔐k ⊨ φn(c) } ∈ U.
So by Łoś’s theorem, 𝔐 ⊨ φn(c).
So in 𝔐, [a1, a2, a3, …] realizes φn.
Since φn was an arbitrary formula in S, [a1, a2, a3, …] realizes all of S.
And we’re done! Since [a1, a2, a3, …] 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.