Last week at the CUNY set theory seminar I presented a proof of an old theorem of Bukovský, which characterises those pairs of models which are set-generic extensions. It turns out that these are precisely those pairs which satisfy a familiar covering property. This result, which seems to have been forgotten for a while, has gathered attention recently, particularly (as far as many of the people at CUNY are concerned) due to its use by Usuba in his work on set-theoretic geology and proving the downward directed grounds hypothesis. In my presentation I didn’t quite get to lay out everything as neatly as I would have liked, so I am writing this post in the hope of giving a fuller account.
As mentioned, the key property that Bukovský isolated is a kind of covering property between a pair of models. We may focus on the case of the relationship between the universe and an inner model ; for us an inner model will be a transitive proper class model of ZFC. We work throughout in GBC (we can even dispense with class choice), so, in particular, there is no need for inner models to be definable.
Definition 1 Let be an inner model and let be regular in . We say that uniformly -covers if for any function with an ordinal and there is another function in such that and for all .
That is to say, covers the function , giving fewer than many guesses at each coordinate. This property is well-known to all students of forcing and all the introductory texts that I know present the following key fact.
Proof: Fix a function in and a name for it. There is some so that it is forced that maps into . We can thus find, for each , a maximal antichain deciding the values of . Now we just let be the set of the possible values given by the conditions in .
Bukovský’s remarkable result is that the uniform covering property precisely characterises the set-forcing extensions.
Theorem 3 (Bukovský, 1973) Let \(M\subseteq V\) be an inner model and let be regular in . The following are equivalent:
- is a -cc generic extension of ; that is, there are a poset and a filter such that is -cc in and is generic over and .
- uniformly -covers .
We already saw the forward implication as theorem 2. The majority of the work, not surprisingly, goes into proving the converse. Starting from the hypothesis that uniformly -covers , the argument can be divided into three fairly self-contained steps:
- If is a set of ordinals (or even ) then is a -cc generic extension of . Here is the least transitive model of ZFC extending and containing .
- There is a set of ordinals such that is a terminal -cc generic extension of ; that is, there is no inner model such that and is a -cc generic extension.
- If is the terminal extension from the previous step, then .
As it turns out, step 1 is the hardest to prove. Therefore we shall make the steps in reverse, starting from 3 and working our way back to 1.
Step 3 follows quite easily from the other two. Specifically, assume that . Since all of our models satisfy choice, there must be a set of ordinals . If we knew that was -cc generic over , this would contradict our assumption on the maximality of .
Proof: Fix a function in . There is an ordinal such that the range of is contained in . Let us pick an injection in . Since uniformly -covers we can find a covering function for in . But then the function is a covering function for in .
Returning to the argument from before, we can now apply step 1 to the pair to conclude that really is -cc generic over , giving us the contradiction and completing step 3.
The key realisation for step 2 is the following lemma:
Proof: It shall suffice to prove that is not -distributive. This is because, if adds a function , then the range of can be covered by a set of size in , by theorem 2. Modulo some coding, the function is then determined by a subset of this covering set.
So now assume toward a contradiction that is -distributive. This means that any family of at most many maximal antichains in has a common refinement. This allows us to build a tree in as follows:
- the root of is the top condition of ;
- every node in has at least two immediate successors;
- every level of is a maximal antichain in .
We can build inductively; the successor steps are easy and we use distributivity to pass through limit steps. Specifically, -distributivity allows us to build the tree up to height (at least) . But now take any condition from the -th level of and consider the branch it determines through . Since every node on the branch is splitting, any one-off-the-branch antichain determined by this branch will have size . But this of course contradicts the -cc.
Seen differently, the proof basically shows that a -cc poset cannot be -distributive.
Let be a set of ordinals coding , so that . We claim that is the required terminal -cc extension of . The set is definitely -cc generic over by step 1. On the other hand, if were not terminal, there would be a further -cc generic extension and, by lemma 5, there must be a new subset of in . But contains all the subsets of in by construction. This completes step 2.
In order to deal with step 1 with some elegance we need to introduce some terminology.
Definition 6 Let be cardinals. We shall denote by the free -complete Boolean algebra on the generators for .
By -complete we mean that suprema of sets of size less than exist. Freeness can be interpreted in two ways. We can think of it in terms of a universal property: any map of the generators into a -complete Boolean algebra extends to a -complete homomorphism on the whole . Alternatively, we can think of as being built in stages, starting from the generators and at each stage taking complements and size suprema of what we had constructed before, and modding out by the minimal obvious relations. This latter viewpoint suggest yet another one. We can also view the generators for as representing the propositional formulas , where is a predicate, and being the Lindenbaum algebra of infinitary formulas built from these atomic formulas via negations and size disjunctions. In my talk I suggested that could, for intuitive purposes, be replaced by , but this is misleading, as I will discuss after theorem 7.
Note that, if , then embeds as a -complete subalgebra into . We will henceforth see these algebras as nested. There is also another kind of nesting.
Theorem 7 Let be an inner model. Then embeds into as an –-complete subalgebra; that is, there is a homomorphism such that for any set in of size we have . In fact, can be taken to extend the identity map on the generators.
In particular, the theorem implies that maps small maximal antichains of into maximal antichains in . I will not give a proof of this result, but I want to point out a subtlety in the statement, which caused a lot of issues in my talk. It may seem that one can give a simple counterexample to the theorem. The one brought up in my talk was as follows: supposing that and were sufficiently large, let , for some real , be the conjunction of the generators or their complements according to . Then it should be the case that in . But if has more reals than , then in , contradicting the theorem. The subtlety arises in the claim that in . This would be the case if were -distributive, since then , but in general this will fail. In fact, by freeness, there is a which is compatible with every and their complements but incompatible with every .
We now know that is essentially a –-complete subalgebra of . This will allow us to pull down information from the algebra in to the algebra in . The foremost is the following lemma.
Proof: Given an ultrafilter , we can simply assign to it the set . Conversely, given a set in there is, by freeness, a unique -complete ultrafilter on which contains or omits the generators according to . But then is an –-complete ultrafilter on , since the latter is an –-complete subalgebra of . It is easy to check that these two assignments are inverse to each other.
Given we will denote by the corresponding ultrafilter on . Clearly , but there is no reason to believe that is in any way generic over . In fact, will not be -cc, so we have not quite finished with step 1 of theorem 2. We will use the uniform covering property to thin out to a -cc poset which the residue of will be generic for.
Let be the function that, given a maximal antichain in , gives the element of the intersection , if such an element exists, and gives some arbitrary element of if not. This function will, in general, only exist in . But since uniformly -covers , we can find a covering function for in ; we may also assume that for all . Essentially, the function represents trying to guess where the potential generic filter coding will meet the antichains of . We will use this guess to remove the inessential parts of the antichain .
We work for a while in . Let be a sufficiently large cardinal (much larger than ). Define a subset of by
It should be noted that, while in , it need not be the case that in .
We wish to see that in . This will follow if we can show that for all , by the –-completeness of . So assume that . By the completeness of , we can find a . But note that also , so . Therefore .
We are ready to define the poset which will add the set over the model . Let
In the Lindenbaum algebra view of , the poset is essentially the Lindenbaum algebra where we add the infinitary inference rules coming from ; that is, from we are allowed to infer .
Proof: Work in and let be a maximal antichain. Then is a subset of of size . We shall show that any element of is compatible with some element of . It will follow that has size .
So pick and fix some -complete ultrafilter on with . Then also , so, in particular, . Since we also have and, by -completeness, there is some . But then , meaning that is compatible with in .
Lemma 10 The filter is -generic over .
Proof: Let be a maximal antichain in . Then , so the join exists in and agrees with the join in . It follows that and, since was maximal, must be the top condition of . Then , so we can use the -completeness of to find a .
Since and are interdefinable over (we have just constructed from and and it is easy to read off from ), this ultimately shows that is a -cc generic extension of , finishing the proof of step 1.