Absoluteness of wellfoundedness and Shoenfield absoluteness are two absoluteness results in set theory that are both used incredibly often. But what if we want to apply the result to absoluteness between arbitrary models and , rather than absoluteness between and ? It turns out that our models have to satisfy dependent choice in both absoluteness results, and in Shoenfield absoluteness we have to ensure that the models are of “similar height”.

We start with the absoluteness of wellfoundedness, where the following standard proof turns out to *not* require power set, but *do* require DC.

Theorem (Absoluteness of wellfoundedness).Let be a binary relation on some set . Then wellfoundedness of is absolute between transitive models of .

**Proof.** It suffices to show that wellfoundedness of a binary relation can be described in a fashion.

Firstly wellfoundedness of is equivalent (over ) to there being no function such that for all , which is clearly a statement. Secondly, wellfoundedness of is also equivalent (over ) to there existing a *ranking function* ; i.e., that , which is a statement. **QED**

In the above proof we only needed DC to show the part, meaning that wellfoundedness is always downwards absolute between transitive models of . The next few lemmas lead up to Shoenfield absoluteness, where they treat sets and sets, respectively.

Lemma (ZF+DC).Let . Then for every set there’s a tree on such that .

**Proof.** For notational ease let’s assume that . Let for a formula, and define

.

Note that and clearly , so let . Then for all , so that implies that there’s a sequence of such that , which implies that holds for all , making . **QED**

Lemma (ZF+DC).Let . Then every set is the projection of a tree on .

**Proof.** Assume for notational simplicity that . Let be , so that for some set . By the above lemma there’s a tree such that , so that , meaning that iff is wellfounded.

Note that, using replacement, is wellfounded iff it can be ranked by a function , meaning that implies that for all . We can pick such a ranking function with codomain since wellfoundedness of implies that .

Now define a tree on as follows. Fix a bijection such that, for every , implies that . For define

and then define as iff and that

.

Note that since . For we set iff and . Then iff is illfounded iff . **QED**

Theorem (Shoenfield absoluteness).Let . Then every sentence is absolute between transitive models of such that .

**Proof.** Let be a formula, so that for a -formula . If then trivially by upwards absoluteness of -formulas, so assume instead that . Define

,

so that by assumption. As is a set in , the above lemma implies that we get that for a tree on , so that iff is illfounded in .

Pick some . Then , and in particular also , is illfounded in . Since we get that as well, so that absoluteness of wellfoundedness yields some , concluding . **QED**

We see that the only thing we needed for was to ensure that the resulting tree was in indeed in , to make sure that we could use absoluteness of wellfoundedness.