I recently stumbled upon yet another example of how class forcing can be wilder than set forcing. A class forcing can be well-behaved under the assumption that the ground model satisfies the axiom of choice while being destructive if choice fails in the ground model. (Thank you to Joel David Hamkins for a helpful conversation and for noticing the key fact I had missed.)
Proposition: There is a (definable) class forcing so that:
- If then forcing with over preserves .
- If then forcing with over does not preserve Replacement.
Proof: This forcing is the forcing to add a global choice function. Specifically, conditions in are functions whose domains are ordinals. The order is the natural one, namely if extends . (Observe that this definition only depends upon the first-order part of our model of set theory, justifying the use of above instead of .)
An easy density argument shows that for any it is dense to get in the range of a condition. Therefore, forcing with adds a surjection , from which we can easily define a global choice function. Note that this doesn’t require the ground model to satisfy any fragment of choice. While we will see that forcing with over a model without choice kills Replacement, at least we get Global Choice as a consolation prize.
We also have that is -closed, meaning that any set-sized decreasing sequence of conditions has a lower bound. Given a descending sequence of conditions from , they have as a lower bound. Therefore, forcing with does not add any new sets. In particular, if we start with a model of , then choice is preserved.
To finish the argument for (1) of the Proposition we need to see that is preserved. For that, I will be lazy and link to a pair [1, 2] of blog posts by Victoria Gitman who was kind enough to write up the gritty details. Let’s check, however, where Vika’s argument uses that choice holds in the ground model. Consider her argument that Replacement is preserved, i.e. that if is a class (in the forcing extension) and is a set then is a set. Vika does this by contradiction, assuming some in the generic forces . She then finds a stronger condition which decides , leading to the desired contradiction. To do this, she uses a well-order of . Of course, if choice fails, then we can find with no well-order, so her argument won’t work in that context.
Now let’s see (2) of the Proposition. Suppose we have a ground model set which lacks a well-order. Call this set . As we saw above, if is the generic function added by forcing with , then every element of appears in the range of . However, it cannot be that they all appear by some bounded stage. If it were that for some ordinal , then since is a set from the ground model, we would have a well-order of in the ground model, contrary to our assumption.
This gives a failure of Replacement. Namely, consider the function taking to the least so that . By the above paragraph, we get that is not a set. ∎
The following corollary can be extracted from the above argument.
Corollary: In the absence of Replacement, Global Choice does not imply (Set) Choice. In other words, in the absence of Replacement the existence of a (class) function which picks elements from every nonempty set does not imply the existence of a set function which picks elements from every nonempty subset of a set .
I view this corollary as (yet more) evidence of the importance of Replacement. It is necessary to prove the ‘obvious fact’ that Global Choice implies (Set) Choice.