3.1 The proofs

This section documents some forcing-and-absoluteness proofs of ZFC theorems about concrete objects. Others are collected in Appendix A. Since my foremost purpose is to show that the method has something to tell us about the relevance of the generic multiverse to the foundations of set theory, and to foreground ensuing discussions in §4 and §5, I have opted to give diverse examples accompanied by remarks about their individuating features. The nonexpert reader can skim this section. The key takeaway is that there are forcing-and-absoluteness proofs such that

• • bespoke forcing extensions are used (Theorems 18, 19, 22, 23)

• • bespoke generic absoluteness theorems are invoked (Theorems 11, 21, A.8)

• • generic absoluteness is invoked multiple times (Theorems 18, A.8)

• • distinct forms of generic absoluteness are invoked (Theorem 15)

• • successive forcing extensions are taken (Theorem 22)

• • a forcing extension satisfying ${\mathrm {ZFC}}$ is appealed to in proving a ${\mathrm {ZF}} +{\mathrm {DC}} +{\mathrm {AD}}$ theorem (Theorem 8)

• • mutual genericity is used to pull a fact into the ground universe from two forcing extensions (Theorem 20)

• • the language of forcing arguably allows the result proved to be stated in its full generality, and in a readily applicable way (Theorem 20)

• • ${\mathrm {CH}}$ is not a source of counterexamples but of useful structure (Theorems 8, 11, A.2, A.10)

• • $\neg {\mathrm {CH}}$ is essential to the argument, perhaps in the form of $\mathrm {MA}+\neg {\mathrm {CH}}$ (Theorems 22, A.8, 16, A.4)

• • the argument adapts mutatis mutandis to prove stronger theorems in an extension of ${\mathrm {ZFC}}$ (Theorems 5, 14, 18, A.5)

• • an object is constructed generically and shown, by absoluteness, to exist in an inner model of the ground universe (Theorem A.1)

• • a finite object is generically constructed (Theorem 24)

• • large cardinals are used (Theorem A.6)

• • the result established shows that forcing-and-absoluteness may suffice to solve a further problem (Theorem A.1)

• • their pure or classical counterparts predated them (Theorems 4, 5, Theorems 20, 21, 22, 23)

• • their pure counterparts postdated them (Theorems 6, A.8, 18, A.10)

• • no pure proof is currently known/published (Theorems A.1, 8, 11, A.4, A.5, A.6, 24)

• • they are preferred to their pure counterparts by experts for epistemic or methodological reasons (Theorems 5, 6, 18, 19, 20, 21, 22, 23)

The quotable forms of generic absoluteness appealed to include Shoenfield absoluteness, Martin–Solovay’s $\Sigma ^1_3$ -absoluteness, and Stern’s absoluteness. The theorems come from computability theory, definable equivalence relations, the partition calculus, number theory,Footnote ¹⁵ analysis, graph theory, and functional analysis.

3.1.1 Harrington’s proof of the Halpern–Läuchli theorem

The first example is not quite a forcing-and-absoluteness proof, but it has implications for the study of purity. Halpern and Läuchli wanted to produce a model of ${\mathrm {ZF}}+\neg \mathrm {AC}$ + “every Boolean algebra contains a prime ideal.” At the time, it was known that the statement “every Boolean algebra contains a prime ideal” cannot be proved in ${\mathrm {ZF}}$ alone, but is provable with $\mathrm {AC}$ . The goal was to show that the theory is of intermediate strength between ${\mathrm {ZF}}$ and ${\mathrm {ZFC}}$ . The Halpern–Läuchli theorem, a Ramsey-like theorem for finite products of finitely branching infinite trees without terminal nodes, is a step toward that goal. It was proved with metamathematical methods in the 1966 paper [Reference Halpern and Läuchli37], where the authors characterized their proof as “dissatisfying” due to its indirectness. In 1978, Harrington gave a proof which, despite the current variety of alternative proofs, “is regarded as providing the most insight” by Ramsey theorists [Reference Dobrinen20, p. 2], for whom the theorem is a widely applicable tool. It was Harrington’s argument that was generalized by Shelah to establish a version of Halpern–Läuchli for higher cardinals [Reference Shelah66] and which motivates a research program on variations of Halpern–Läuchli by Dobrinen and Hathaway and others (see [Reference Dobrinen and Hathaway21, Reference Dobrinen and Hathaway22]).

Let $T(n)$ be the nth level of T, i.e., the set of sequences in T of length n. We refer the reader to [Reference Dobrinen20] for the definition of strong subtree.

Theorem 5 (Halpern–Läuchli [Reference Halpern and Läuchli37]; Harrington (see [Reference Dobrinen20],[Reference Farah and Todorčević24]))

Let $T_i \subseteq \omega ^{<\omega }$ , for each $i < d<\omega $ , be a finitely branching tree, and let

$$\begin{align*}c = \bigcup_{n<\omega} \prod_{i<d} T_i(n)\rightarrow k,\end{align*}$$

for some $k<\omega $ , be a coloring. Then there are an infinite set of levels $L\subseteq \omega $ and strong subtrees $S_i\subseteq T_i$ , each with nodes exactly at the levels of L, such that c is monochromatic on

$$\begin{align*}\bigcup_{n\in L} \prod_{i<d} S_i(n).\end{align*}$$

Harrington’s proof uses the Cohen forcing adding $d\times \kappa $ -many Cohen reals to add $\kappa $ -many infinite paths through the trees $T_i$ , where $\kappa = \beth _{2d}$ . It uses the forcing and the forcing language to inductively search for the next monochromatic levels of the strong subtrees.

The reason that Harrington’s proof does not fit the forcing-and-absoluteness proof template exactly is that it neither uses absoluteness (although part of the proof is an argument about what is preserved in c.c.c. forcing) nor requires actually working in a forcing extension. It only requires combinatorially analyzing the forcing. Yet it is highly impure.

3.1.4 Stern’s absoluteness

Stern [Reference Stern76] showed that if $\omega _1$ is inaccessible to reals, then there is no thin $\Sigma ^1_1$ equivalence relation having $\aleph _1$ -many equivalence classes with bounded Borel rank. To do so, he proved a form of generic absoluteness for Borel sets which says that if a Borel set of rank $\alpha $ can be created by forcing (such a set is described by a virtual Borel set), then it can be approximated in the ground model by $\beth _{\alpha }$ -Borel sets.

Theorem 12 (Stern; [Reference Hjorth43, corollary 1.8])

Let $M,N\models {\mathrm {ZFC}}$ be well-founded and suppose that $M\subseteq N$ and $\beth ^M_{-1+\alpha } <\omega _1^N$ . Suppose $(\mathbb {P},p,\tau )\in M$ is a virtual Borel set, $\alpha <\omega _1$ , and

$$\begin{align*}p\Vdash_{\mathbb{P}} "\tau \text{is a Borel code of rank} \alpha," \text{and}\end{align*}$$

$$\begin{align*}(p,p)\Vdash_{\mathbb{P}\times\mathbb{P}} "\tau[g_1] \text{codes the same Borel set as} \tau[g]."\end{align*}$$

Then there is aFootnote ²³ Borel code $(\dot {T},\dot {f})\in N$ of rank $\alpha $ such that

$$\begin{align*}p\Vdash_{\mathbb{P}} "B(\varnothing,\dot{T},\dot{f}) \text{is the Borel set coded by} \tau[g]."\end{align*}$$

Hjorth, describing Stern’s absoluteness and his own use of it, writes

Unlike, say, Shoenfield absoluteness, Stern’s absoluteness can only be made understood in the terminology of forcing. Since forcing is typically associated with the pursuit of independence results, we could easily assume that Stern’s work has little relevance in proving positive theorems about the Borel hierarchy.

However, this would be untrue. Using abstract and indirect metamathematical arguments, and availing ourselves of Stern’s absoluteness principle, we will prove a string of ${\mathrm {ZFC}}$ theorems for which no direct proof is known. [Reference Hjorth43, p. 663]

Among the items in this string are

Theorem 13 (Kanovei; [Reference Hjorth43, theorem 2.2])

If A is a non-Borel $\Sigma ^1_1$ set, then the constituents of A do not have bounded Borel rank.

Hjorth’s proof appeals to $\Pi ^1_2$ -absoluteness and derives a contradiction with Stern’s absoluteness Theorem 12. The proof of the next theorem appeals to Shoenfield absoluteness.

Theorem 14 ([Reference Hjorth43, corollary 4.5])

For $\alpha <\beta <\omega _1$ , there is no injection $f:\Pi ^0_{\beta }\to \Pi ^0_{\alpha }$ which is Borel (in the codes).

In fact this generalizes to the nonexistence of such an injection in $L(\mathbb {R})$ assuming $\mathsf {AD}^{L(\mathbb {R})}$ using essentially the same argument [Reference Hjorth43, theorem 4.7].

Theorem 15 (Harrington; [Reference Hjorth43, theorem 5.5])

The continuous actions of $S_{\infty }$ on Polish spaces induce a $\leq _B$ -unbounded, length $\omega _1$ sequence of Borel equivalence relations.

Both Shoenfield and Stern absoluteness are appealed to in the proof.

Theorem 16 ([Reference Hjorth43, theorem 5.19])

Isomorphism on countable sets of reals is not Borel reducible to the orbit equivalence relation induced by continuous actions of a Polish abelian group on any Polish space.

The proof passes to an extension of $\mathrm {MA}_{\omega _1}$ to utilize the fact that $\Sigma ^1_2$ sets have the Baire property.Footnote ²⁴

A result going beyond ${\mathrm {ZFC}}$ but still about the concrete is also shown and justified by Hjorth as follows:

I should stress that this does not mean that the argument has no relevance assuming the axiom of choice. In fact, Harrington’s argument directly implies that in the presence of large cardinals there is no simply definable uncountable sequence of Borel sets with bounded rank. The method of proof is also fertile, in the sense that it produces useful theorems just in ${\mathrm {ZFC}}$ .Footnote ²⁵

Theorem 17 (Harrington; [Reference Hjorth43, theorem 3.1])

Assume $\mathsf {AD}^{L(\mathbb {R})}$ . Then there is no injection $f:\omega _1\to \Pi ^0_{\alpha }$ , for $\alpha <\omega _1$ , in $L(\mathbb {R})$ .

4.1 Absoluteness theorems and other multiverse conceptions

There are more inclusive superstructures than the generic multiverse in the literature. Hamkins describes some possibilities:

Just as the generic multiverse formalizes an intrinsic feature of the ground universe—namely what can be forced over it with set-sized forcings—these other multiverse conceptions strive to articulate e.g., what can be class-forced over the ground universe. A class-forcing and absoluteness proof of a ${\mathrm {ZFC}}$ theorem about concrete mathematics would be of great interest. Perhaps there will be such a proof using coding into the continuum function, or making use of the Ground Axiom.Footnote ³⁰ Theories of class forcing extensions could conceivably contribute to our understanding of V similarly to those of set forcing extensions.Footnote ³¹ So developing these broader multiverse conceptions may be similarly important for multiverse proponents and nonpluralists alike.

To get such proofs as those just speculated—and further generic multiverse proofs—to work, generic absoluteness theorems tailored to particular extensions, like in the proofs of Lemma 10 and Theorem 21, will presumably be required. Generic absoluteness is intrinsically interesting, but the potential for forcing-and-absoluteness proofs provides practical impetus for studying aspects of it that would likely otherwise go unresearched.

4.2 Extent

Of course, most of the theorems surveyed were proved prior to the generic multiverse being formalized in [Reference Steel74], so saying that the generic multiverse is brought to bear in the proofs is admittedly a charitable construal. Likewise, the extent to which the multiverse proofs show that the whole generic multiverse is not going away is a matter of perspective. It seems enough to know that some forcing extensions are useful in proving theorems in concrete mathematics, a significant part of mathematics accepted by the weak relativist, the weak absolutist, and the strong absolutist. We cannot predict exactly which extensions will prove useful in future proofs, and it seems arbitrary to argue that multiverse proofs only show the utility of a mere “submultiverse” consisting of the specific generic extensions used in §3.1, or e.g., the c.c.c. multiverse.

There is a lacuna: The amalgamability asserted in condition (4) of Definition 2 has not factored into the proofs surveyed. A multiverse proof using amalgamation would be of great interest, as Woodin’s generic multiverse does not satisfy amalgamability and [Reference Maddy and Meadows53] questions whether there is a principled reason to accept it.Footnote ³³

4.3 The content of the Absolutist–Relativist debate

The generic multiverse must be kept distinct from the views about it like Weak Relativism or the Generic Multiverse conception of truth.Footnote ³⁴ The former is an object, the object given by the multiverse language and axioms. It is a category mistake to assent to or argue against an object as opposed to a claim.Footnote ³⁵ The Absolutist is committed to the generic multiverse just as the Relativist is, since the first order theory of the forcing extensions of V is part of what holds in V, and this theory is what the generic multiverse theory captures. Forcing-and-absoluteness proofs indicate that there is practical benefit to studying this theory: One can use worlds in the generic multiverse to prove ${\mathrm {ZFC}}$ theorems about concrete objects relevant to wider mathematics, like definable equivalence relations.

The proofs embody the idea that, for proving ${\mathrm {ZFC}}$ theorems, any universe will do. This is a practical maxim in the neighborhood of the Weak Relativist’s idea that all worlds in the multiverse are on equal footing, although it is weaker. The proofs do not substantiate other tenets of Weak Relativism or Generic Multiversism, namely that forcing extensions “actually” exist as full-blooded universes (whatever that is taken to mean), or that the only meaningful sentence in the language of set theory are those that hold in all universes. (This is part of why they are proofs. Their validity does not depend on metaphysics. Forcing allows the simulation of the universe’s forcing extensions within the universe, and its legitimacy as a proof technique turns on being able to treat forcing extensions entirely virtually.) In these “best case” uses of the generic multiverse conception, the Absolutist is not compelled to see the generic multiverse as anything more than the behavior of the forcing relation, and the Absolutist sees the auxiliary theories used, which are indeterminate for the Weak Relativist, as meaningful.

So Weak Relativist and Strong Absolutist alike are committed to the object, but they disagree about its significance. On my reading, Steel put forth the Weak Absolutist Thesis as a way of making this disagreement mathematically tractable in such a way that a confirmation of it would bring the parties closer together. (A perhaps silly way of putting this reading is that if the Weak Absolutist Thesis is true, then we should all just be Weak Absolutists because the content of Strong Absolutism and Weak Relativism that goes beyond the Weak Absolutist Thesis does not seem to have strictly mathematical content or justification.) Usuba’s theorem confirms the Thesis, assuming an extendible cardinal. This is satisfying to the Absolutist in inverse proportion to how disappointing it would have been for there to provably not be a core. The Strong Absolutist may believe the core is V. But the theorem by itself does not refute the rival philosophical position. Weak Relativism is not the negation of Weak Absolutism.

Usuba’s theorem does, however, put the Weak Relativist on their back foot. They have to give a philosophically coherent answer to (something like) Question 26.

For the Weak Relativist, the core is at minimum a universe with an interesting metamathematical property. Simply saying that that’s all there is to it, that all universes nonetheless remain on an equal footing, seems unsatisfactory as a response to Question 26. That large cardinals imply exactly one world in the multiverse enjoys a property—let alone the property of being the world from which all others arise by generic extension and refinement—cannot be hand waved away. A complete response has to make explicit what it means when the Weak Relativist claims all universes are on an equal footing and how that equal footing is compatible with there being a uniquely definable universe in the multiverse.Footnote ³⁶

Apart from Question 26, or the significance of the core generally, what is there to give traction to the disagreement between the Weak Relativist and the Strong Absolutist? Each view can interpret all of the relevant mathematics, at least if Question 26 has an answer. So insofar as Absolutism and Relativism countenance the same proof techniques (like forcing-and-absoluteness) and are committed to the generic multiverse, and assuming the Weak Relativist has a plausible answer to Question 26, is there content to the Relativist–Absolutist debate? If so, can that content be made mathematically tractable? If either of these questions has a negative answer, it seems to me that Weak Absolutism represents the limits of what can be said with mathematical justification on the topic.

Miller’s program

Bolzano’s efforts to remove geometric intuition from proofs in analysis constituted a research program explicitly aimed at achieving topical purity. There is an analogous program to find elementally pure proofs of some of the theorems in §3: B. Miller [Reference Miller59] pursues classical, forcing-free proofs of classical descriptive set theoretic dichotomies like Silver’s and Burgess’ theorems using chromatic numbers. Miller’s stated motivation is that techniques like Gandy–Harrington forcing—and certainly forcing-and-absoluteness—should be unnecessary to establish these dichotomies. After all, Cantor, Hausdorff, and Suslin proved the perfect set property for closed, Borel, and analytic sets with elementary techniques. Whether Silver’s Theorem is true could have been asked in Cantor’s time, whereas forcing constituted a paradigm shift in set theory and emerged over half a century later. Neither Silver’s nor Harrington’s proof is “classical” in the sense that it is a proof that Cantor could have arrived at. While Harrington’s eliminates passing to a forcing extension and does not need ${\mathrm {GCH}}$ , there’s a sense that any forcing should be unnecessary for establishing ${\mathrm {ZFC}}$ theorems about concrete sets of reals. Miller describes the situation:

The epistemic payoffs of Miller’s program corroborate those which are thought to be associated with purity: “In addition to eliminating the need for sophisticated machinery from mathematical logic, this approach illuminates new connections between seemingly unrelated theorems, leads to a global view of dichotomy theorems from which new results emerge, and readily generalizes to broader classes of definable sets” [Reference Miller59, p. 555].

The objection

The objection to our main claim draws on two facts. First, theorems like Platek’s Theorem 3 tell us that if forcing-and-absoluteness can be used to prove a theorem of a certain logical complexity from ${\mathrm {GCH}}$ , then there is a proof of that theorem which does not use ${\mathrm {GCH}}$ . ${\mathrm {GCH}}$ is provably extraneous to the theorem. Interpolation theorems suggest that there should be proofs which avoid forcing extensions. Second, the mathematical community esteems pure proofs, even when they are not the first proof of a theorem. Finding a pure or explanatory proof, or one that eliminates extraneous or controversial hypotheses, is one of the primary reasons that mathematicians re-prove theorems [Reference Dawson17, Reference Dawson18]. Forcing-and-absoluteness proofs could not be more prime candidates for re-proof.

Together, these facts suggest that the generic multiverse is eliminable because set theorists will seek direct ${\mathrm {ZFC}}$ proofs which use resources local to the theorems they establish. Miller’s program §5 exemplifies this tendency.

5.1 Explanation

While hops in the generic multiverse are ultimately unnecessary to prove some of these results, one wonders whether and when the “pure” proofs would have been discovered without their impure counterparts to guide them. Todorčević, in regards to his theorems in §3.1.7, describes his use of forcing as “the guiding force behind the discovery of these results” [Reference Todorčević78, p. 1183]. These proofs show that extreme impurity can be fruitful in the context of discovery. That Harrington and Shelah have employed the technique so many times attests to this.

Aristotle’s distinction between deduction and demonstration—and the distinctions of Leibniz between sequences of discoveries and orderings of truths and of Bolzano between Gewissmachung and objektive Begründung—track the contexts of discovery and justification. For Aristotle, a deduction is simply a valid argument, whereas a demonstration is a deduction which is in addition explanatory in the sense that it reveals the true grounds for a claim. More broadly, an explanatory proof of a theorem is an argument that gives the reason why the theorem is true as opposed to merely showing that the theorem is true. Deductions—which include impure proofs—are permissible, for Aristotle, in the context of discovery, but demonstrations are required in the context of justification. The proofs discussed in §3 seem to fall in the former category, as one might wonder why the result is true even after digesting its proof, and the subsequent forcing-free proofs function as demonstrations.

Harrington’s proof of the Halpern–Läuchli theorem clashes with the Aristotelian account in a strong sense. It is impure and metamathematical. It was not the first proof of the result. Yet practitioners report that Harrington’s proof provides the true grounds of the theorem. It is the proof that allows the generalization of the theorem to higher cardinals. Todorčević’s proofs give, at least to him, a proper understanding of the results they establish. Similar for Gao et al.’s proofs. The Larson–Zapletal proof of Hjorth’s turbulence theorem arguably give the proper understanding of what the theorem is “really” saying, what its topic is. These are examples of impure proofs which function in the context of justification better than their pure counterparts—the impure proof is the demonstration, the pure proof a deduction.

There is a philosophical literature on explanatory proof (see e.g., [Reference Steiner75, Reference Baron, Colyvan and Ripley7, Reference Baron, Colyvan and Ripley8, Reference Pincock62, Reference Lange48]), and how purity of method and explanation relate [Reference Lange48, Reference Arana4, Reference Ryan64], much of which seeks to identify just what it is that makes a proof explanatory. To be clear, I am not sure of the significance of the distinction between explanatory proofs and those which are supposedly not. A proof is why a theorem is true. Even the most unwieldy, computer-assisted enumerative proof contains why the claim is shows is true. It is immaterial if all of its cases cannot be grasped all at once by a human mathematician. Dissatisfaction with a particular proof need not reflect epistemic virtues inherent to the proof but rather one’s understanding of it. Explanations are answers to “Why?” questions, after all, and the kinds of “Why?” questions one can ask after being presented a proof reflect a lack of comprehension, not shortcomings of the proof. Whether one gains understanding from this proof or that proof is too autobiographical, too much a matter of an individual’s psychology, to be about the proofs themselves.

By saying that some forcing and absoluteness proofs are explanatory, I do not mean that they fall under any of the philosophical rubrics of explanatory proof. (I think they do not, and I think no analysis of proofs will be successful in characterizing explanatory proofs.) I just mean that among mathematicians in the relevant research area, the proofs seem to be the “right” ones, probably by virtue of exhibiting informative connections with other areas of mathematics or casting the problem in a domain familiar to those mathematicians and in which their methods are applicable. There is nothing wrong with the non-forcing and absoluteness proofs, nor anything philosophically deep about the judgments that the forcing and absoluteness proofs are “right.”

5.2 Essential uses

I read Gao et al’s inclusion of the purely topological proof of Theorem 18 as a confirmation of the theorem justifying further use of the forcing-and-absoluteness method in their paper. Together with their observation that from the forcing-and-absoluteness proof of Theorem 18 further corollaries can be drawn, this suggests that the authors see their proofs as being the “right” ones of their theorems. Another reason is that the limitations of measure techniques for establishing Borel nonreducibilities and the fruitfulness of forcing-and-absoluteness suggest to Gao et al. that the latter method may become essential:

They predict that forcing proofs will be crucial to progress in definable equivalence relations theory:

Similarly, Larson and Zapletal’s forcing formulation of turbulence provides methodological advantages over Hjorth’s original. Their proof of Hjorth’s turbulence theorem is an example of a proof which arguably gives insight into the content of the theorem that is not revealed by the original proof. Forcing-and-absoluteness may be a necessary tool in practice.

At least for human mathematicians. These forcing and absoluteness proofs are natural for set theorists to find. They cast the problems in language the set theorist is at home in, and human mathematicians—as opposed to computers—need heuristics, intuitions, and creative insight to guide their proof searches. If carried out by human mathematicians, then, developing theories requires forcing and absoluteness proofs. But if the task of completing theories were left to computers programmed to find the proofs guaranteed to exist by e.g., Platek’s theorem and interpolation theorems, and if human understanding were no longer as central a goal of the pursuit of mathematics, forcing and absoluteness could disappear from deductive mathematical activity.Footnote ⁴⁴ What about non-deductive mathematical activity? If forcing and absoluteness, as a technique, does not lead set theorists to useful new axioms, will it remain a useful tool?

5.3 An inversion

Arana and Detlefsen sought to formally characterize “a widespread, persistent tendency to think that there are ways in which the resources used in a proof/solution can match or fail to match the theorem proved/problem solved, and that when proper match is achieved it in some way(s) adds to the value of the proof/solution produced” [Reference Arana and Detlefsen5, p. 1]. Kreisel was suspicious of the value of this tendency.

With regards to forcing-and-absoluteness proofs, the rigor of the method and the fact that many of the theorems in §3 have not been purely reproved bear out (i). The potential Gao et al. see (§5.2) for the method to establish Borel nonreducibilities would bear out (ii). Through the proofs we gain knowledge of how the structure of V and the structure of its forcing extensions relate and bear on the concrete. These relations are variegated and informative, and they give us confirmation of the coherence of set theory in a sense reminiscent of the following passage by Dawson:

That we can bring forcing extensions to bear on concrete problems in number theory, analysis, or computability theory shouldn’t be possible, the thought goes, unless the generic multiverse and set theory itself are coherent.Footnote ⁴⁵

Confirmations of set theory’s coherence are ultimately why the generic multiverse will not go away. Pure reproofs of the theorems in §3 will not have the same confidence-bolstering effects. They will not reveal far-reaching connections between generic extensions. Miller’s program has mathematical benefits that justify its pursuit—any directive that leads to finding more proofs is worthwhile—but confirmations of the coherence of set theory are not among them. Following Kreisel, if an ideal of purity precludes gaining knowledge of how generic extensions bear on one another in productive ways, so much for that ideal—which is not to say that seeking pure proofs should be discouraged. There are many different values a proof can have. The variety of proofs of a theorem, with all the different values they enjoy—like elemental purity or coherence-confirmation—collectively contribute to our understanding of set theory.Footnote ⁴⁶

5.4 Conclusion

The generic multiverse is not going away, then, because—through the forcing-and-absoluteness method—it aids in proof discovery; some of the impure proofs discovered are the explanatory or “right” proofs of the theorem they establish; and the method may be essential for certain purposes, like proving Borel nonreducibilities. (Should the method somehow lead to new axioms, so much the better.) Forcing-and-absoluteness proofs give a non-local kind of knowledge about—a confirmation of—the coherence of set theory, knowledge which cannot be gotten from pure, direct proofs of the same theorems. Bringing such machinery to bear on theorems about concrete mathematics shouldn’t be possible unless we are onto something.

The proofs put a weak version of the central claim of generic multiversism—that every extension of set theory is as good as any other—to work in a way which is relevant and useful to Absolutists. The proofs have to be rigorously accounted for, and a rigorous setting for studying what forcing extensions V has is needed. The generic multiverse theory does this. Jettisoning the generic multiverse is too strong a reaction to Usuba’s theorem.