Are there interesting examples of theorems proved using ‘height’ extensions?

Question

It's well known that forcing is more than a tool for proving independence: We can prove theorems and formulate axioms in theories like $\mathsf{ZFC}$ by moving to forcing extensions (e.g. $\mathfrak{p}=\mathfrak{t}$, remarkable cardinals, Todorčević and Farah's book "Some applications of the method of forcing"). Are there nice examples of theorems/axioms that use "height" extensions (i.e. where we use "ordinals" longer than $\mathit{Ord}$ or where the resources required are strictly greater than second-order etc.) to prove some result in $\mathsf{ZFC}$ (or an extension thereof) or about the ground model? (From here on, let "height extension of $M$" denote any model $M'$ such that $\mathit{Ord}^M \in M'$).

Some uses that occur to me:

1. Uses of $\mathsf{ETR}$ in class theory (e.g. using iterated truth predicates and the connection to determinacy for class games, cf. Gitman and Hamkins "Open Determinacy for Class Games").

2. #-generation. This is a technical axiom to state, so I won't do so here, the core point is that we capture reflection properties of some model $M$ by taking it to be an initial segment of a model $M'$ generated by an ultrapower construction (this ultrapower, in turn, may be longer than $\mathit{Ord}^M$). See Honzik and Friedman "On Strong Forms of Reflection in Set Theory" for details.

3. There are useful definable well-order longer than $\mathit{Ord}$ (e.g. the ordering on mice).

I am curious as to whether the use of such "height" extensions pops up a lot in set-theoretic practice, and whether its as useful/ubiquitous as the use of forcing in proving theorems and formulating axioms (beyond relative consistency).

Answer 1

Here is another instance, which appears in my recent paper with Bokai Yao on second-order reflection in the context of KMU with abundant urelements.

• Joel David Hamkins and Bokai Yao, Reflection in second-order set theory with abundant urelemets bi-interprets a supercompact cardinal, 2022, arXiv:2204.09766.

The following theorem is an immediate consequence of the main theorem.

Theorem. Assume Kelley-Morse set theory with urelements KMU, with the abundant atom axiom and second-order reflection. Then there is a stationary proper class of measurable cardinals, partially supercompact cardinals, and more.

I mention the theorem because the main proof method is to undertake the unrolling construction, which produces sets at ranks higher than Ord.

Starting at lower right in the model $\langle V(A),\in,\mathcal{V}\rangle$ in which the hypothesis is satisfied, we undertake unrolling to produce the models $W$ and $\bar V$, in which there is a supercompact cardinal. In fact, it is the cardinal $\kappa=\text{Ord}^V$ that becomes supercompact in these taller models. And the supercompactness of $\kappa$ in $\bar V$ and $W$ reflects to diverse consequences in the original universe $V(A)$ and its class of pure sets $V$, such as a stationary proper class of measurable and partially supercompact cardinals, as much supercompactness as desired.

Answer 2

Here is another example.

The maximality principle in forcing is the scheme asserting of every statement $\varphi$ in the language of set theory that if there is forcing extension $V[G]$ of the set-theoretic universe $V$ for which all further forcing extensions $V[G][H]$ satisfy $\varphi$, then $\varphi$ was already true in the original universe $V$.

The principle is naturally expressed in modal terms, using the forcing interpretation of the modal operators, by the S5 axiom $\Diamond\Box\varphi\to\varphi$.

I introduced this forcing modality in my paper:

• Hamkins, Joel David, A simple maximality principle., J. Symb. Log. 68, No. 2, 527-550 (2003). ZBL1056.03028.

And I also gave several consistency proofs of the maximality principle, one of which is relevant for your question. Namely, if there is a fully correct cardinal $\delta$, which means that the scheme $V_\delta\prec V$ holds, then there is a forcing extension of the universe $V[G]$ in which the maximality principle holds. Basically, one lines up all the statements $\varphi_0$, $\varphi_1,\dots$, and then at each stage you ask whether $\varphi_n$ is forceably necessary over $V_\delta$, and if so, you add a forcing factor to achieve this. This defines a finite-support iteration, which will be a forcing extension $V[G]$ in which every instance of the MP is true.

Intuitively, one wants to carry this argument out over $V$, except that it would require us to use a truth predicate since asking whether a given statement is forceable is as hard as asking whether it is true. This is why $V_\delta\prec V$ helps us out, because we need only ask about forcing over $V_\delta$, which is a set, and so we have a truth predicate there.

The hypothesis that $V_\delta\prec V$ cannot be omitted from the proof that MP is forceable, for there are some models of ZFC that have no forcing extensions satisfying MP.

The method accommodates real parameters, if you also assume that $\delta$ is inaccessible, and the assumption $V_\delta\prec V$ is equivalent in consistency strength over ZFC to Ord being definably Mahlo. The result is a model of the boldfact maximality principle $\text{MP}(\mathbb{R})$.

The relevance for your question is that the hypothesis $V_\delta\prec V$ is conservative over ZFC. A simple compactness argument shows by the reflection theorem that every model $W$ of ZFC has an extension with a cardinal $\delta$ for which $W\prec V_\delta\prec V$. Thus, we have extended the model $W$ by adding $\delta$ and a lot of other ordinals on top of $\delta$, in the style of your question. Starting with any model $W$, we can find an elementary extension $V$, with taller ordinals, having a forcing extension $V[G]$ in which the maximality principle holds.

And we get a similar conservativity for $V_\delta\prec V+\delta$ inaccessible over the theory ZFC + Ord is definably Mahlo.

The maximality principle was introduced and studied before my paper (independently) by:

• Stavi, Jonathan; Väänänen, Jouko, Reflection principles for the continuum, Zhang, Yi (ed.), Logic and algebra. Providence, RI: American Mathematical Society (AMS). Contemp. Math. 302, 59-84 (2002). ZBL1013.03059.

Unfortunately, this paper is slightly marred by the oversight that they do not state or use the hypothesis $V_\delta\prec V$, and they suggest that the maximality principle is forceable over every model of ZFC. But this is not true, as I had mentioned. Fortunately, one can correct their arguments simply by incorporating $V_\delta\prec V$ in the style of my arguments.