3.1 Inner model richness

Extensions of V are useful for postulating the existence of many inner models. The Inner Model Hypothesis does exactly this, using extensions of a model $\mathfrak {M}$ in order to make claims about the inner models of $\mathfrak {M}$ :

The $\mathfrak {M}$ - $\mathsf {IMH}$ thus states that $\mathfrak {M}$ has many inner models, in the sense that any sentence $\phi $ true in an inner model of an outer model of $\mathfrak {M}$ is already true in an inner model of $\mathfrak {M}$ . In this way, $\mathfrak {M}$ has been maximized with respect to internal consistency (see Figure 1 for visual representation of an application of the $\mathfrak {M}$ - $\mathsf {IMH}$ ).

Fig. 1 A visual representation of an application of the $\mathfrak {M}$ - $\mathsf {IMH.}$

There are a number of reasons to find the $\mathfrak {M}$ - $\mathsf {IMH}$ interesting, not least because it maximizes the satisfaction of consistent sentences within structures internal to some $\mathfrak {M}$ . If we could formulate the $\mathsf {IMH}$ as about V, it would thus be foundationally significant: The $\mathsf {IMH}$ gives us an inner model for any sentence model-theoretically compatible with the initial structure of V, and thus serves to ensure the existence of well-founded, proper-class-sized structures in which we can do mathematics. It also has a similarity to Absolute- $\mathsf {MA}$ ; the $\mathsf {IMH}$ is just more general in that it permits the consideration of arbitrary extensions instead of merely set forcing extensions. The $\mathfrak {M}$ - $\mathsf {IMH}$ also has substantial large cardinal strength; it implies the existence of inner models (of $\mathfrak {M}$ ) with measurable cardinals of arbitrarily large Mitchell order, and is consistent relative to the existence of a Woodin cardinal with an inaccessible above.Footnote ²⁵ However, it is also interesting in that it has various anti-large cardinal properties, the $\mathfrak {M}$ - $\mathsf {IMH}$ implies that there are no inaccessibles in $\mathfrak {M}$ .Footnote ²⁶

Whence the problem then for the Universist? If the Universist wishes to use the $\mathsf {IMH}$ as a new axiom about V, she has to examine issues concerning extensions of V. If they ascribe no meaning to claims concerning extensions, then the $\mathsf {IMH}$ is utterly trivial (when viewed as a principle true of the universe, rather than some substructure thereof). Under this analysis, everything true in an inner model of an outer model of V is also true in an inner model of V, as either (i) the outer model is proper, does not exist, and hence nothing is true in an inner model of that proper outer model of V, or (ii) the outer model is V itself, and obviously anything true in an inner model of V is true in an inner model of V. Thus, if the Universist ascribes no meaning to the term ‘outer model of V’ the inner model hypothesis fails to capture what it was designed to state (i.e., a richness of inner models).

However, even supposing that the Universist allows some interpretation of extension talk, the content that the $\mathsf {IMH}$ has is going to vary according to the resources one allows. We begin by making the following definitions:

We then have the following simple fact for the Set-Generic Inner Model Hypothesis:

However, though this restricted version of the $\mathsf {IMH}$ is sufficient to get us a certain richness of inner models (enough to break $V=L$ ) we get more if we allow class forcings. This is brought out in the following:

Thus, we see how inner model hypotheses are dependent for their content and implications upon what we allow as extensions. Indeed, the difference between set forcing and class forcing is brought out by the following:

The theorem highlights that being a set-forcing extension is a relatively restricted kind of extending construction in comparison to others: If one model is a set forcing extension of another (by some $\kappa $ -c.c. forcing), then every function in the extension is already $\kappa $ -covered by some function in the ground model. There is no such requirement for class forcing. For example, consider an $x \subseteq \kappa $ that is $\kappa $ -Cohen generic over $\mathcal {V}$ , and let f be the increasing enumeration of x. Then, f is not $\kappa $ -covered by a function in $\mathcal {V}$ . Thus, the class forcing that adds a single $\kappa $ -Cohen at every regular $\kappa $ violates global $\kappa $ -covering at every $\kappa $ . The question of whether or not there could be an analogue of Bukovský’s Theorem for class forcing is currently unresolved, however any such result would have to transcend the notion of $\kappa $ -global covering.

Suppose then that we do wish to assert that the $\mathsf {IMH}$ is true of V for arbitrary extensions. Then we need to give meaning (in whatever appropriate codification) to the claim that V has various kinds of extension. The intra-V (i.e., internal to V) consequences provable from the $\mathsf {IMH}$ may then vary depending on the kinds of extension we can interpret.

How does this play out with respect to the countable transitive model strategy? Here, there is a prima facie limitation. As it stands, a $\mathfrak {V}$ elementarily equivalent to V is only accurate for first-order statements about V. Because of the inherent incompleteness in second-order properties over V, there is no guarantee that $\mathfrak {V}$ perfectly mirrors V’s higher-order properties. This difficulty is especially interesting given that a large part of set theory comprises examining the structural relationships between models. Simply because an axiom is not first-order is not a reason (without significant further argument) to establish that it is not of independent interest.

The situation can be brought into sharper focus by initially considering the behavior of arbitrary higher-order properties. Letting $\mathcal {C}^{\mathfrak {M}}$ denote a collection of classes for a model $\mathfrak {M}$ (i.e., to serve as interpretation of the second-order variables), and $(M, \in , \mathcal {C}^{\mathfrak {M}})$ be the resulting model of second-order set theory, then it is clear that we can have a $\mathfrak {V}$ elementarily equivalent to V for parameter-free first-order truth, but diverging in the higher-order realm. To see this, consider the following set-sized case. Let some universe $\mathcal {V}$ be of the form $(V_\kappa , \in , V_{\kappa + 1})$ , where $\kappa $ is inaccessible. Now use $\mathsf {AC}$ to obtain a countable elementary (in the language of $\mathbf {MK}$ ) submodel, and collapse to obtain some countable and transitive $\mathfrak {U}=(U, \in , \mathcal {C}^{\mathfrak {U}})$ (note here that both U and $\mathcal {C}^{\mathfrak {U}}$ are countable). Letting $Def(M)$ denote the set of classes of a model $\mathfrak {M}$ definable with first-order parameters, we then have that $(U, \in , \mathcal {C}^{\mathfrak {U}})$ and $(V_\kappa , \in , V_{\kappa + 1})$ satisfy $\mathbf {MK}$ class theory, whereas $(U, \in , Def(U))$ and $(V_\kappa , \in , Def(V_\kappa ))$ each satisfy the weaker $\mathbf {NBG}$ class theory, despite all four models having the same first-order theory. This shows that though we might have a $\mathfrak {V}$ elementary equivalent to V for first-order truth, it may radically diverge from V in its higher-order properties, possibly even (dependent on the class theory we accept for V, and the classes we choose for $\mathfrak {V}$ ) having ‘more’ classes (in the sense of sentences of class theory satisfied) than V.

While we see that $\mathfrak {V}$ need not resemble V with respect to arbitrary higher-order truth, there is the question of whether or not it need resemble V with respect to the higher-order truth relevant for satisfaction of the $\mathsf {IMH}$ . We will show how to code outer models of V later, in order to give meaning to this question concerning the $\mathsf {IMH}$ . However, even in the case of countable transitive models, the question does not have an obvious answer:

The mathematics surrounding this question seems difficult, yielding a potentially philosophically and mathematically interesting line of inquiry. For now, we merely point out that it is at least an open (epistemic) possibility that a $\mathfrak {V}$ equivalent to V for first-order truth might fail to resemble V with respect to the $\mathsf {IMH}$ when we admit some conception of classes for each (assuming that the $\mathsf {IMH}$ can be given a reasonable interpretation over V). Later, we will see that if we allow impredicative class comprehension, this difficulty can be circumvented. A small amount of impredicative similarity between V and $\mathfrak {V}$ is sufficient to yield enough resemblance for the satisfaction of the $\mathsf {IMH}$ to covary between V and $\mathfrak {V}$ .

3.2 $\sharp $ -generation

Interestingly, width extensions (i.e., universes containing the same ordinals but more subsets) allow us to encapsulate many large cardinal consequences of reflection properties. It is here that the notion of a sharp becomes useful. Before we give the definition, we will require a notion of iteration in class theory. We therefore need a preliminary:

We make the following definition (and provide a visual representation in Figure 2):

Fig. 2 A visual representation of the initial ultrapowers corresponding to a sharp $(N,U).$

Using the existence of the maps $\pi _{i,j}: N_i \longrightarrow N_j$ , we can then provide the following definition:

In other words, a model is class iterably sharp generated iff it arises through collecting together the $V^{N_i}_{\kappa _i}$ (i.e., each level indexed by the largest cardinal of the model with index i) resulting from the iteration of a class-iterable sharp through the ordinal height of $\mathfrak {M}$ . Note than in producing the model, we only require that the sharp is iterated $Ord^{\mathfrak {M}}$ -many times, despite the fact that it can be iterated far further.Footnote ³³

A model’s being class iterably sharp generated engenders some pleasant features. In particular, it implies that any satisfaction (possibly with parameters drawn from $\mathfrak {M}$ ) obtainable in height extensions of $\mathfrak {M}$ adding ordinals (through the well-orders in the class theory of the ambient universe) is already reflected to an initial segment of $\mathfrak {M}$ .Footnote ³⁴ In this way, we are able to coalesce many reflection principles into a single property of a model. For example a model $\mathfrak {M}$ being class iterably sharp generated already entails reflection from $\mathfrak {M}$ to initial segments of nth-order logic for any n.Footnote ³⁵ One might then suggest the following kind of axiom in attempting to capture reflection properties:

which would allow us to assert in one fell swoop that V satisfies many reflection axioms (rather than having to assert them in a piecemeal fashion). However, such an axiom is also clearly problematic from the Universist perspective; claiming that V is class iterably sharp generated depends upon the existence of an iterable class sharp for V, which cannot be in V. If it were, one could obtain a class club resulting from iterating the sharp (namely the class of $\kappa _i$ ), which in turn forms a club of regular V-cardinals. The $\omega $ th element of any club of ordinals with proper initial segments in V must be singular with cofinality $\omega $ , and so we would obtain a contradiction at $\kappa _\omega $ ; it would have to be both regular and singular.

Thus, the claim that V is class iterably sharp generated comes out as trivially false; there simply is no such sharp. Moreover, sharps are especially problematic as they cannot be reached by known forcing constructions, so many of our usual simulations of satisfaction for extensions (such as the use of a forcing relation or Boolean-valued model) will not help in their discussion.Footnote ³⁷ Moreover, whilst the first-order consequences of $\mathfrak {V}$ being class iterably sharp generated will be mirrored in V, there is not yet any interpretation of the embeddings yielding the sharp (these being higher-order objects). As we’ll see in §§4–6, we can develop an interpretation of these objects. For now, we look at some other possible uses of extensions.

3.3 Set-theoretic geology

A final kind of higher-order axiom that uses extensions emerges from set-theoretic geology.Footnote ³⁸ The study of the geological properties of a model concerns how different models could have arisen by some variety of extension construction (the metaphor of geology indicates tunneling down into the ground models of a particular starting model). In the original paper of Fuchs et al. (Reference Fuchs, Hamkins and Reitz2015), the authors are almost exclusively concerned with set-generic forcing extensions. We might examine, however, how this can be extended to arbitrary extensions. We now repeat some definitions of Fuchs et al. (Reference Fuchs, Hamkins and Reitz2015) to show how this can be done:

Fuchs et al. (Reference Fuchs, Hamkins and Reitz2015) then go on to prove several facts about the geological properties models may possess. In particular, the paper shows that many of these statements, which appear second-order (given their reference to structural interrelations of proper class models), can actually be rendered in first-order terms. For example they discuss the following:

Theorem 22 ( $\mathbf {ZFC}$ ) (Laver, Reference Laver2007)

(The Ground Model Definability Theorem). Every ground model W of V is definable in V using a parameter from W. Moreover, there is a specific formula $\phi (y,x)$ such that if W is a ground of V, then there exists an $r \in W$ such that:

$$ \begin{align*}W= \{ x | \phi(r, x) \}.\end{align*} $$

This theorem facilitates the study of the geological structure of set-generic multiverses from within a given model in first-order terms. However, we might consider generalizations of the idea of geology to other extensions. Fuchs et al. (Reference Fuchs, Hamkins and Reitz2015) goes some way towards this, considering the structure present when we allow pseudo-grounds into the picture: models that have certain covering and approximation properties that facilitate the definability of the ground model in the (possibly class) forcing extension.

Despite this, the ground-model definability theorem can fail badly when we fully admit class forcing extensions into the picture, as shown by the following:

The theorem shows that for many class forcings, the definability of the ground model in the extension can fail. Thus, by insisting that we examine any geological structure only in cases where we do have definability, we lose a possible route for discovering facts about V. Moreover, insisting on the use of set forcing obscures other possible routes of inquiry. For example, instead of looking at forcing extensions, one could examine arbitrary extensions which preserve cardinals. This is a deep and challenging form of set-theoretic geology. Or, one can look at inner models obtained by iterating the $HOD$ -operation (i.e., looking at the $HOD$ of the $HOD$ , the $HOD$ of the $HOD$ of the $HOD$ etc.).

How might the use of geology be useful in formulating axioms for V? A natural thought for a Universist is that V cannot be ‘reached’ by particular kinds of construction. In the case of the set-generic multiverse, we might then postulate that the following is true:

In the present case, we might consider the following sort of axiom:

Axioms of this form would provide a formalisation of the idea that V is ‘unreachable’ in some sense: it cannot be obtained from an inner model by certain kinds of extension. As it stands, we do not need to talk about extensions in order to talk about the geological structure of V; most of the discussion here concerns how V can be obtained by extending inner models. However, often geological structure is elucidated by considering how particular grounds (possibly satisfying some $\Phi $ -ground axiom) behave within a wider multiverse context. A salient concept here is the following:

In the case of set forcing, this class will be definable, owing to the Laver definability of the ground model of an extension. In fact, by recent results of Usuba,Footnote ⁴⁰ the mantle (the intersection of all grounds of V) and set-generic mantle coincide. However, the loosening of the requirement on set forcing in the definition of the mantle (say to cardinal preserving arbitrary extensions), and the use of this (possibly nondefinable) higher-order entity in postulating an axiom to hold of V (for example that the ‘arbitrary’ mantle is a proper subclass of V), requires some interpretation of arbitrary outer models of V.

4.1 Exposition of V-logic

That infinitary logics relate to talk concerning extensions was known since Barwise (Reference Barwise1975), and utilized by Antos et al. (Reference Antos, Friedman, Honzik and Ternullo2015) in providing an interpretation of extension talk in a framework where any universe could be extended to another with more ordinals. We provide a more technically detailed exposition of the system of V-logic than has been hitherto provided, and show how it can be captured using impredicative class theories, facilitating a possible line of response on behalf of the Universist. Since we will be showing how to code the logic later, we will leave the theory in which the definitions are formulated for §§5–6.

We first set up the language:

We can then define V-logic:

Proof codes in V-logic are thus (possibly infinite) well-founded trees with root the conclusion of the proof. Whenever there is an application of the V-rule, we get proper-class-many branches extending from a single node. More formally, we define the notion of a proof code in V-logic (an example of which is visually represented in Figure 3) as follows:

Fig. 3 Visual representation of a proof of $\chi $ in V-logic.

With the mechanisms of V-logic set up, we now describe how its use is relevant for interpreting extensions of universes.

4.2 Interpreting extensions in V-logic

We have provided explanation of a logic that rigidifies the structure of V; adding constants and axioms to fix V’s properties within the syntax of V-logic. How might this allow us to interpret satisfaction in outer models of V? As we shall argue, consistency in V-logic of theories in $\mathscr {L}^V_\in $ serves that purpose.Footnote ⁴⁴ For the moment, we will work with V-logic as a system in its own right, and show how it can be coded in a manner acceptable to the Universist in §5.

We first introduce a constant $\bar {W}$ to our language. Letting $\Phi $ be a condition in any particular formal language on universes we wish to simulate in an extension, we then introduce the following ‘axioms’ into our theory of V-logic:

1. (i) $\bar {W}$ -Width Axiom. $\bar {W}$ is a universe satisfying $\mathbf {ZFC}$ with the same ordinals as $\bar {V}$ and containing $\bar {V}$ as a proper subclass.

2. (ii) $\bar {W}$ - $\Phi $ -Width Axiom. $\bar {W}$ is such that $\Phi $ .

We can then have the following axiom to give meaning to the notion of an extension such that $\Phi $ , and hence yield intra-V consequences of said extension:

• ${\Phi ^{\vdash _V}}$ -Axiom. The theory in V-logic with the $\bar {W}$ -Width Axiom and $\bar {W}$ - $\Phi $ -Width Axiom is consistent under $\vdash _V$ .Footnote ⁴⁵

We can use this axiom to give meaning to the notion of an intra-V consequence of the axiom mentioning extensions. Any syntactic consequence concerning either some $\bar {x}$ or $\bar {V}$ derived from the axioms mentioning $\bar {W}$ will hold of the respective actual structures: we simply trace the consequences to the relevant constant.

To see this in concrete contexts, let us examine V-logic in action with respect to some of the examples outlined earlier (we’ll show how to code V-logic in §5, but proceed intuitively for now). In the case of a set forcing we could have the following:

If the resulting V-logic theory is consistent, then any syntactic consequence of the existence of $\bar {W}$ concerning $\bar {V}$ will then be true in V.

The situation with class forcing is similar, but with a small twist. For, in the case of class forcing using some class poset $\mathbb {P}^C$ , the existence of a V- $\mathbb {P}^C$ generic $G^C$ is not a first-order property of $\bar {W}$ . Despite this, in V-logic we have the ability to add predicates (as we did with $\bar {V}$ and $\bar {W}$ ). Thus, we can add additional predicates $\bar {\mathbb {P}^C}$ and $\bar {G^C}$ for $\mathbb {P}^C$ and $G^C$ into the usual syntax of V-logic, and state the following axiom:

and then examine whether the resulting theory is consistent in V-logic. Any intra-V consequence of such a (consistent) theory would, for exactly the same reasons as in the case of set forcing, naturally transfer to truths concerning V.

This liberation of methods via syntactic means also allows us to formulate axioms that capture non-forcing extensions. For example:

This then allows us to express the claim that V is sharp generated:

Again, anything provable about V using this theory will be represented by the relevant constants in the theory of V-logic, allowing us to give meaning to the claim that V is class iterably sharp generated. Later (§6) we will see that this corresponds in a neat way to the actual existence of sharps over certain (countable) models of set theory.

We noted earlier (§2) that much extension talk could be interpreted by conducting the construction over a countable transitive model $\mathfrak {V}$ that satisfied exactly the same parameter-free first-order sentences as V. It was noted there, however, that the production of such a model provided no guarantee that the model would respect greater than first-order features of V, in particular the existence of many inner models provided by the $\mathsf {IMH}$ . The key fact here is that now we have the notion of interpreting extensions via consistency in V-logic, we are able to simulate statements about the existence of arbitrary models and their interrelations.

Again, we add a constant $\bar {W}$ to our language and formulate axioms concerning width extensions represented syntactically by the relevant $\bar {W}$ . We can then express the intended content of the $\mathsf {IMH}$ as follows:

Thus, by interpreting the existence of outer models through the consistency of theories, we can now make claims concerning consequences (about V) of the existence of outer models. In particular, we can say that if $\phi $ is satisfiable in an extension of V (syntactically formulated as $\bar {W}$ ) then it is satisfied in an inner model of V. So, the $\mathsf {IMH}^{\vdash _V}$ holds iff whenever the mathematical structure of V does not preclude the V-logic consistency of an outer model satisfying $\phi $ , there is an inner model of V satisfying $\phi $ . In this way, we make claims concerning greater than first-order properties of V needed to express the $\mathsf {IMH}$ in its maximal sense.

Moreover, we can use this to talk about V’s place within a set-theoretically geological structure. Satisfaction in the relevant kinds of extension can be formulated as the consistency of some particular V-logic theory or theories, and V’s geological properties can thereby be studied. Thus V-logic also allows us to talk about V within a higher-order multiverse structure. In fact:

Thus, if we allow the use of V-logic, we are able to syntactically code satisfaction in arbitrary extensions of V in which V appears standard, and hence the effects of extensions of V on V.

There are two slight wrinkles here, however. First, while we have defined the system, we have yet to show that it can be formulated in a theory acceptable to the Universist. Second, while we have ‘given meaning’ to the idea of an outer model via the use of V-logic, we have yet to show that the idea actually does the job we want it to; namely mimicking the existence of extensions. These issues can be brought into sharper focus by contrasting our current situation with the use of forcing relations in interpreting set forcing, possibly in conjunction with a countable transitive elementary submodel $\mathfrak {V}$ of V. There, we know (1) We have the resources in V to talk about the relevant forcing relations (via the use of the forcing language), and (2) Whenever $\mathfrak {V}$ has an extension by some $\mathbb {P}$ - $\mathfrak {V}$ -generic G to $\mathfrak {V}[G] \models \phi $ , there will be a corresponding partial order $\mathbb {P}'$ in V, forcing relation $\Vdash _{\mathbb {P}'}$ , and $p \in \mathbb {P}'$ such that $p \Vdash _{\mathbb {P}'} \phi $ . In this way, the forcing relation is certified as an acceptable interpretation of forcing over V; as it is mirrored in the countable (in line with the Methodological Constraint). In the next two sections we will show that, given an impredicative class theory, we can be in a similar position but with arbitrary extensions (and thus adequately formalize the axioms discussed in §3).

5.1 Admissibility

First, we need to explain the structure we will be coding. We first recall the system of Kripke-Platek set theory $\mathbf {KP}$ :

We make a further pair of definitions:

Our interest will be in $Hyp(V)$ ; the least admissible structure containing V as an element. Of course this structure does not really exist. However, we will show that something isomorphic to $Hyp(V)$ can be coded in an impredicative class theory.

5.2 Class theory

We now provide a short explanation of the impredicative class theory that we will be using (a variant of $\mathbf {MK}$ ). Later, we will show that full $\mathbf {MK}$ (with a certain extra axiom on the existence of isomorphisms) is far more than is required. While a philosophical and mathematical analysis of greater than first-order set theory is merited, considerations of space prevent a full examination. A couple of remarks, however, are in order regarding Universism and impredicative class theory.

There are several options available for the Universist in interpreting proper class discourse over V. While one method is to simply regard class talk as shorthand for the satisfaction of a first-order formula (a method which yields no impredicative comprehension), this is not the only possibility. We might, for example, interpret the class quantifiers nominalistically through the use of plural resources (as in Boolos, Reference Boolos1984 and Uzquiano, Reference Uzquiano2003). Another approach is to interpret classes through some variety of property theory as in Linnebo (Reference Linnebo2006) (or with a little massaging to the set-theoretic context Hale, Reference Hale2013). Still further, we might interpret the class quantifiers using mereology (as in Welch & Horsten, Reference Welch and Horsten2016).

Key to each is that there is at least the possibility for motivating some impredicative class comprehension. For example, the plural interpretation is often taken to motivate full impredicative comprehension for classes.Footnote ⁴⁷ Many views of property theory suggest that impredicatively defined properties are acceptable.Footnote ⁴⁸ Again, for mereological views the amount of class comprehension licensed will depend on one’s views and axioms concerning mereology, however the possibility is open to allow some impredicativity.

For simplicity, we will simply adopt full Morse-Kelly class theory (henceforth ‘ $\mathbf {MK}$ ’), and discuss how much is required for our purposes later (for most applications, we will require $\Sigma ^1_1$ -Comprehension for classes). We thus might view the present work as not only providing an interpretation of extension arguments over V, but also informing what is possible on various class-theoretic approaches. We start by defining our class theory:

Before we delve into the details, we provide a sketch of our strategy. Some of the work and basic ideas occur in Antos & Friedman (Reference Antos and Friedman2017) and Antos (Reference Antos, Friedman, Honzik and Ternullo2015). There, however, additional axioms were required for certain applicationsFootnote ⁵¹ of the coding. We will show that within a variant of $\mathbf {MK}$ , $Hyp(V)$ can be coded by a single class. We then provide some arguments as to how the theory of $Hyp(V)$ might be reduced to the countable.

5.3 Coding $Hyp(V)$ in impredicative class theory

We first need to code the notion of an ordered pair of classes. Initially, this seems problematic; normal pairing functions on sets are type-raising in the sense that they have the things they pair as members. We will assume that this is not available on the current interpretation; most Universist interpretations of proper classes do not permit proper classes being members and so constructions that are necessarily type-raising are impermissible. Despite this, we can use the abundance of sets within V (in particular the closure of V under pairing) to code pairs using a standard trick:

Effectively, we talk about coding an ordered pair of classes by tagging all the members of X with $1$ and all the members of Y with $2$ , and referring to the resulting class. Moreover, short reflection on the above coding shows that it is easy to generalize this to $\alpha $ -tuples by letting $\alpha $ tag $\alpha $ -many copies of V. We are now able to make use of the following definition (with visual representation of some examples provided in Figures 4 and 5):

Fig. 4 An example of a tree corresponding to a coding pair showing membership.

Fig. 5 More complicated coding pair tree structures.

These coding pairs shall be essential in coding the structure of ideal sets that would have to be ‘above’ V were they to exist. One can think of the coding pair as a tree $\mathbb {T}$ which has as its nodes the elements of $M_0$ , a as top node, and R the extension relation of $\mathbb {T}$ . For each tree there are only countably many levels, but each level can have proper-class-many nodes.

Next, we code the ideal objects using coding pairs. For any particular ideal set x, we will code the transitive closure of $\{x\}$ . A fact of the above coding is that any tree will have many isomorphic subtrees, and hence will not be isomorphic to $TC(\{x\})$ .Footnote ⁵² We therefore need to form quotient pairs that provide a coding of ideal sets (we provide a visual representation of an example in Figure 6).

Fig. 6 The quotient process for a coding pair of $3.$

We now have a quotient structure for the coding pairs. Next, we mention some useful properties of these coding pairs for the purposes of showing that they code ideal sets:

Let us take stock. We have quotient structures of coding pairs that behave extensionally and in a well-founded manner, and are coded by individual classes. We are now ready to establish a useful theorem, showing that these quotient coding pairs obey certain operations, and thus we have a code for $Hyp(V)$ . We first, however, explain how we will state what we wish to say.

We will be interested in the theory of these quotient coding pairs, and what codes they can produce. For ease of proof, we will speak as though they are first-order objects, despite the fact that we are using this as an abbreviation for class-theoretic language. We therefore need to make the following:

We are now in a position to establish a theorem that will prove to be very useful in relating class theory and V-logic. Much of the work is putting together results in Antos (Reference Antos, Friedman, Honzik and Ternullo2015) and Antos & Friedman (Reference Antos and Friedman2017). However, the following (somewhat lengthy) remark is required to situate the current discussion:

Remark 53. In Antos (Reference Antos, Friedman, Honzik and Ternullo2015) and Antos & Friedman (Reference Antos and Friedman2017), the first and third author used an axiomatisation $\mathbf {MK}^*$ that also includes the following Class Bounding Axiom:

Definition 54 ( $\mathbf {MK}$ Class Bounding).

$$ \begin{align*}\forall x \exists A \phi(x,A) \rightarrow \exists B \forall x \exists y \phi (x, (B)_y),\end{align*} $$

where $(B)_y$ is defined as follows:

$$ \begin{align*}(B)_y = \{ z | \langle y, z \rangle \in B \}.\end{align*} $$

They also show that, when working over a countable transitive model $\mathfrak {M} = (M, \in , \mathcal {C} )$ such that $\mathfrak {M} \models \mathbf {MK}^*$ , the model $(M^+, \in )$ , where $M^+$ is defined as follows:

$$ \begin{align*}M^+ = \{ x |\text{``There is a coding pair } \langle M_x , R_x \rangle \text{ for } x \text{ in } \mathcal{C}\text{''}\}\end{align*} $$

satisfies $\mathbf {SetMK}^*$ ; a version of $\mathbf {ZFC} -$ Power Set with a Set Bounding Axiom and some constraints on the cardinal structure of $M^+$ . We indicate how the proofs we require are (a) amenable to the current context, (b) realisable using an impredicative class theory, and (c) can be accomplished avoiding the use of Bounding (but with an assumption on the existence of isomorphisms). For the purposes of the proof, it will be much easier to speak of the tree structures $\mathbb {T}_x$ , $\mathbb {T}_y$ , and $\mathbb {T}_z$ , rather than constantly paraphrasing in terms of classes representing the quotient coding structures.

The proofs in Antos (Reference Antos, Friedman, Honzik and Ternullo2015) and Antos & Friedman (Reference Antos and Friedman2017) rely on the following two lemmas:

Lemma 55 ( $\mathbf {MK}^*$ ) (Antos, Reference Antos, Friedman, Honzik and Ternullo2015 ; Antos & Friedman, Reference Antos and Friedman2017)

First Coding Lemma. Let $\mathfrak {M} = (M, \mathcal {C})$ be a transitive $\beta $ -model (i.e., it computes well-founded relations correctly) of $\mathbf {MK}^*$ . Let $\langle N_1 , R_1 \rangle $ and $\langle N_2 , R_2 \rangle $ be coding pairs in $\mathcal {C}$ . Then if there is an isomorphism between $\langle N_1 , R_1 \rangle $ and $\langle N_2, R_2 \rangle $ then there is such an isomorphism in $\mathcal {C}$ .

Lemma 56 ( $\mathbf {MK}^*$ ) (Antos, Reference Antos, Friedman, Honzik and Ternullo2015 ; Antos & Friedman, Reference Antos and Friedman2017)

Second Coding Lemma. For all $x \in M^{+}$ there is a one-to-one function $f \in M^+$ such that $f: x \longrightarrow M_x$ , where $\langle M_x, R_x \rangle $ is a coding pair for x.

Antos (Reference Antos, Friedman, Honzik and Ternullo2015) and Antos & Friedman (Reference Antos and Friedman2017) are concerned with higher-order forcing (i.e., using forcing posets that have some proper classes of a model as conditions) over models of $\mathbf {MK}^*$ . In order to deal with the obvious metamathematical difficulties, they explicitly define the construction over models satisfying $\mathbf {MK}^*$ that are countable, transitive, and are $\beta $ -models. Their strategy is to code a model $(\mathfrak {M})^+$ of $\mathbf {SetMK}^*$ in the original model of $\mathbf {MK}^*$ , and perform a definable class forcing over $(\mathfrak {M})^+$ . This then corresponds to a hyperclass forcing over $\mathfrak {M}$ . The current work shows that the coding outlined is not dependent upon the countability of the models, nor the extra assumption of Class Bounding (though we will motivate the acceptance of the First Coding Lemma). Instead, we can take the coding over V using the interpretation of $\mathbf {MK}$ through class theory, and show how to code the theory of $(V)^+$ using these resources. For the above lemmas then, a few remarks are in order.

(I) The assumption that the model over which we code is a $\beta $ -model is philosophically trivial in the present setting; we are working over the Universist’s V, with some conception of its classes $\mathcal {C}^V$ . For the Universist, $(V, \mathcal {C}^V)$ sets the standard for what a $\beta $ -model is, and so is trivially a $\beta $ -model.

(II) Similar remarks apply to the First Coding Lemma, which is a nontrivial result when we are concerned with a countable transitive model $\mathfrak {M} \models \mathbf {MK}^*$ . Since $\mathfrak {M}$ has an impoverished view of what classes there are, in that setting one needed to establish that $\mathbf {MK}^*$ satisfaction alone ensures that there is a class of the relevant kind in $\mathcal {C}$ . For the purposes at hand, however, the result is again philosophically trivial; the relevant classes $\mathcal {C}^V$ over V set the standard for when two trees representing classes are isomorphic, and so we cannot have isomorphic trees $\mathbb {T}_x$ and $\mathbb {T}_y$ for which there is not a class coding an isomorphism. If there are no things coding an isomorphism between $\mathbb {T}_x$ and $\mathbb {T}_y$ then they are simply not isomorphic. To be absolutely technically explicit about this fact, we will add the First Coding Lemma as an extra axiom, and denote the theory we work in by $\mathbf {MK}^+$ .

(III) Use of the Second Coding Lemma is circumnavigated by the proofs below, and so we will say nothing more about it.

Proof. The proofs of (1.)–(4.) do not require the use of Class Bounding, and so we refer the reader to Antos (Reference Antos, Friedman, Honzik and Ternullo2015) and Antos & Friedman (Reference Antos and Friedman2017). We thus begin with:

(5.) $\Delta _n$ -Separation ${}^+$ . This is slightly more difficult in that it is not clear how to code a first-order formula within $(V)^+$ . This is dealt with by the following:

Proof. By induction on the complexity of $\phi $ . Suppose $\phi $ is of the form $y \widehat {\in } x$ , and let $\mathbb {T}_y$ and $\mathbb {T}_x$ be the associated trees. As $y \widehat {\in } x$ , there is a tree $\mathbb {T}_{y'}$ with top node $a_{y'}$ in the level below the top node of $\mathbb {T}_x$ , such that $\mathbb {T}_y$ is isomorphic to $\mathbb {T}_{y'}$ . By the First Coding Lemma (trivial in the current setting), $\psi $ is then “Y is a class coding a tree $\mathbb {T}_y$ , and X is a class coding a tree $\mathbb {T}_x$ such that $\mathbb {T}_y$ is isomorphic to a class $Y'$ coding a direct subtree $\mathbb {T}_{y'}$ of $\mathbb {T}_x$ .” Suppose then that $\phi $ is of the form $y \widehat {=} x$ . Then $\psi $ is simply “The class that codes $\mathbb {T}_y$ is isomorphic to the class that codes $\mathbb {T}_x$ ,” which is again dealt with by the First Coding Lemma.

For the inductive steps where $\phi $ is of the form $\neg \chi _0$ orFootnote ⁵⁴ $\chi _1 \wedge \chi _2$ , the result is immediate, we just either negate or conjoin the class-theoretic correlate of the $\chi _m$ provided by the induction step.

Suppose then that $\phi $ is of the form $\forall x \chi $ , where $\chi $ is translatable in our class theory by $\chi '$ . Then $\psi $ is “For any class X coding some tree $\mathbb {T}_x$ , $\chi '(X).$ ”□

We now can proceed with the proof of $\Delta _n$ -Separation ${}^+$ . Let $a, x_1,..,x_n$ be first-order names in the theory of $(V)^+$ and $\phi (x, x_1,\ldots ,x_n, a)$ be any $\Delta _n$ -formula in the language of $(V)^+$ . We need to show that:

$$ \begin{align*}b= \{x \widehat{\in} a | \phi(x, x_1,..,x_n,a)\} \widehat{\in} (V)^+\end{align*} $$

and hence that there is a class B representing a coding pair for b with a corresponding tree $\mathbb {T}_b$ .

Let $\mathbb {T}_{x_1}$ ,…, $\mathbb {T}_{x_n}$ and $\mathbb {T}_a$ be codes, that we will refer to using $x_1,\ldots ,x_n$ and a in the language of $(V)^+$ . Further let $\psi $ be the class-theoretic correlate of $\phi $ . If b is empty the result is immediate as there is a coding pair for the empty set. Assume then that b is nonempty and $(V)^+$ thinks that b contains some $c_0$ with coding pair tree $\mathbb {T}_{c_0}$ . Let $\mathbb {T}_{a(c)}$ be a class variable over trees, with the condition that each $\mathbb {T}_{a(c)}$ corresponds to a direct subtree of $\mathbb {T}_a$ (i.e., $a(c)$ is a member of a in $(V)^+$ ). By Class Comprehension, there is a class Z such that if $\psi (\mathbb {T}_{a(c)}, \mathbb {T}_{x_1}, \ldots , \mathbb {T}_{x_n}, \mathbb {T}_a)$ holds then $\{ z | \langle c, z \rangle \in Z \}$ is the direct subtree $\mathbb {T}_{a(c)}$ of $\mathbb {T}_a$ , and if $\psi (\mathbb {T}_{a(c)}, \mathbb {T}_{x_1}, \ldots , \mathbb {T}_{x_n}, \mathbb {T}_a)$ does not hold then $\{ z | \langle c, z \rangle \in Z \} = \mathbb {T}_{c_0}$ .

We then let $\mathbb {T}_b$ be a tree with top node $b_0$ that has as all its direct subtrees the various $\{ z | \langle c, z \rangle \in Z \}$ . The tree $\mathbb {T}_b$ then codes the existence of the necessary $b = \{x \widehat {\in } a | \phi (x, x_1,\ldots ,x_n, a) \} \widehat {\in } (V)^+$ .□

With these properties in place, we proceed to find a code of $Hyp(V)$ in $(V)^+$ :

Proof. We begin with the following definition concerning coding pairs:

By Theorem 57 we can build versions of the L-hierarchy in $(V)^+$ . Moreover, since Global Choice holds in the class theory, $(V)^+$ contains a class well-order $<_V$ of V. Let $L^{(V)^+}(V, <_V)$ then be the substructure of $(V)^+$ obtained by constructing $(V)^+$ ’s version of the L-hierarchy over $(V, <_R)$ through every meta-ordinal $\vartheta $ . Then $L^{(V)^+}(V, <_V)$ validates $\Delta _n$ -Separation ${}^+$ , since any instance of Separation for $L^{(V)^+}(V, <_V)$ translates into an instance of Separation for $(V)^+$ (this is a more specific instance of the fact that $L^{\mathfrak {M}}$ satisfies Separation whenever $\mathfrak {M}$ is a transitive model of Separation). So, pick the least $\varsigma $ such that $L_\varsigma (V, <_V)$ satisfies $\Delta _n$ -Separation ${}^+$ . We claim that $L_\varsigma (V, <_V)$ also satisfies $\Sigma _n$ -Collection ${}^+$ .

Assume for contradiction that $\Sigma _n$ -Collection fails in $L_\varsigma (V, <_V)$ . Working from the perspective of $L_\varsigma (V, <_V)$ , we then have a $\Sigma _n$ -definable function $\phi (x,y)$ from $Ord(V)$ unbounded in $L_\varsigma (V, <_V)$ . We then note that V can be well-ordered in $L_\varsigma (V, <_V)$ and therefore every element of $L_\varsigma (V, <_V)$ can be mapped into $Ord(V)$ (i.e., $Ord(V)$ is the largest cardinal of $L_\varsigma (V)$ ) since $\varsigma $ was chosen to be least. We can then extend $\phi (x,y)$ to a $\Sigma _n$ -definable bijection between $Ord(V)$ and $L_\varsigma (V, <_V)$ , to obtain a $\Sigma _n$ -definable well-order $<_R$ on the subsets of $Ord(V)$ in $L_\varsigma (V, <_V)$ . For $i \widehat {\in } I$ indexing $<_R$ on subsets $x_0, x_1, \ldots , x_i,\ldots $ of $Ord(V)$ we then diagonalise to produce the following $X \subseteq Ord(V)$ :

$$ \begin{align*}X= \{ \alpha \in On | \neg \alpha \widehat{\in} x_\alpha \}.\end{align*} $$

This X is $\Sigma _n$ -definable over $Ord(V)$ by the properties of $<_R$ and the fact that $Ord(V) \widehat {\in } L_\varsigma (V, <_V)$ but cannot be in $L_\varsigma (V, <_V)$ . Since $Ord(V) \widehat {\in } L_\varsigma (V, <_V)$ , this violates $\Delta _n$ -Separation ${}^+$ , $\bot $ .

Thus $L_\varsigma (V, <_V)$ satisfies $\Sigma _n$ -Collection ${}^+$ . We then know that since any instance of $\Sigma _n$ -Collection ${}^+$ in $L_\varsigma (V)$ is expressible in $L_\varsigma (V, <_V)$ , $L_\varsigma (V)$ also satisfies $\Sigma _n$ -Collection ${}^+$ . Thus, there is some $L_\varpi (V)$ satisfying $\Delta _0$ -Separation and $\Sigma _1$ -Collection, with $\varpi $ the least such.

We can now note the following:

and thus observe that $L_\varpi (V) \widehat {=} Hyp(V)$ . Moving back to the coding, this implies the existence of a class H coding a tree $\mathbb {T}_{Hyp(V)}$ for $Hyp(V)$ . □

The above machinery then provides the resources to code $Hyp(V)$ by referring to classes. One natural question concerns how much comprehension is required to code proofs in V-logic. This is approximately answered by the following:

In sum, we have seen thus far that $Hyp(V)$ can be coded within the class theory licensed by an interpretation of proper classes that admits a small amount of impredicativity (namely: $\mathbf {NBG}$ + $\Sigma ^1_1$ -Comprehension + The First Coding Lemma). We now turn to the issue of coding V-logic within $Hyp(V)$ (as rendered in class theory).

5.4 Coding V-logic in $Hyp(V)$

We will show that if $\phi $ is a consequence of a V-logic theory $\mathbf {T}$ , then a proof of $\phi $ appears in $Hyp(V)$ (i.e., the (code of the) least admissible structure containing V), completing the rendering of V-logic for the Universist. Much of this goes through as in Barwise (Reference Barwise1975), but we have used a slightly different definition of proof code, and so this remains to be checked.

We wish to show that if there is a proof of $\phi $ in V-logic, then there is a proof code of $\phi $ in $Hyp(V)$ . First, however, we must be precise about how we interpret the extended syntax of V-logic. Since we have shown already how to code $Hyp(V)$ , we work directly in the language of $Hyp(V)$ and drop the class-theoretic locutions:

We can now state the following:

Proof. We credit this to Barwise, since the proof is not very difficult, but since we have a different notion of proof-code we need to make sure that V-logic is still representable in $Hyp(V)$ .

We proceed by induction on the complexity of our proof P. Suppose that there is a proof P of $\phi $ in V-logic. Then either:

1. (a) P is one line.

2. (b) P is more than one line.

We deal with (a) first. Suppose that P is one line. Then either (i) $\phi $ is of the form $\bar {x} \in \bar {V}$ , (ii) $\phi $ is an atomic or negated atomic sentence of $\mathscr {L}_\in \cup \{\bar {x}| x \in V \}$ , (iii) $\phi $ is an axiom of first-order logic in $\mathscr {L}^V_\in $ , or (iv) $\phi $ is an additional axiom containing some extra predicate (such as $\bar {W}$ , $\bar {\mathbb {P}^C}$ , or $\bar {G^C}$ ).

For (i), suppose $\phi $ is of the form $\bar {x} \in \bar {V}$ for $x \in V$ . Then, the result is immediate: the required sentence is in $Hyp(V)$ by Pairing, and hence so is the tree coding its proof (i.e., $\{ \{\phi \} , \emptyset \}$ ). In the case of (ii), $\phi $ appears in V, and so it is immediate that $\phi $ is in $Hyp(V)$ , with the relevant proof tree. For (iii), we note that all constructions of first-order axioms from simpler formulas $\psi $ and $\chi $ (that are assumed, for induction, to be in $Hyp(V)$ ) can be chained together through Pairing. For (iv), since we represent the various extra predicates by objects that are not pieces of syntax in other parts of V-logic but are in $Hyp(V)$ , any axiom of the form “ $\bar {W}$ is such that $\Phi $ ” is simply a finite sequence of sets already present in $Hyp(V)$ (and similarly when $\bar {\mathbb {P}^C}$ or $\bar {G^C}$ are present). Again, repeated application of Pairing ensures that $\phi $ is in $Hyp(V)$ , as well as the relevant proof tree.

(b) Suppose then that P is more than one line. Assume for induction that all prior steps to the final inference to $\phi $ have proofs in $Hyp(V)$ . Then either (i) $\phi $ is an axiom, or (ii) $\phi $ follows from $\psi $ , $(\psi \rightarrow \phi )$ via modus ponens, or (iii) $\phi $ is of the form $\forall x \in \bar {a} \psi (x)$ and follows from $\psi (\bar {b})$ for all $b \in a$ by the Set-rule, or (iv) $\phi $ is of the form $\forall x \in \bar {V} \psi (x)$ and follows from $\psi (\bar {x})$ for all $x \in V$ by the V-rule.

For each of the steps we need to construct, from the given proof trees, a new proof tree coding a proof of $\phi $ . We already know that the relevant pieces of syntax exist (by part (a)) and so the challenge is simply in the construction of the trees in $Hyp(V)$ .

(i) has already been dealt with in part (a). (ii) Suppose for induction that $\psi $ and $(\psi \rightarrow \phi )$ have proofs coded in $Hyp(V)$ by $\mathbb {T}_\psi = \langle T_\psi , <_\psi \rangle $ and $\mathbb {T}_{(\psi \rightarrow \phi )} = \langle T_{(\psi \rightarrow \phi )}, <_{(\psi \rightarrow \phi )} \rangle $ . Since we know that $Hyp(V)$ satisfies finite iterations of Pairing, we only need to construct $T_\phi $ and $<_\phi $ . We can easily construct $T_\phi = T_\psi \cup T_{(\psi \rightarrow \phi )} \cup \{ \phi \}$ . Next, we define $<_\phi $ as follows:

• $x <_\phi y$ iff:

  1. (i) $x <_\psi y$ , or

  2. (ii) $x <_{(\psi \rightarrow \phi )} y$ , or

  3. (iii) $y = \phi $ .

Since we have $<_\psi $ and $<_{(\psi \rightarrow \phi )}$ already ( $Hyp(V)$ is transitive), we just need to construct $\{ \langle x, \phi \rangle | x \in T_\psi \vee x \in T_{(\psi \rightarrow \phi )} \}$ . We have that $\phi \in Hyp(V)$ , and also for any object $y \in Hyp(V)$ , $\langle y , \phi \rangle \in Hyp(V)$ . We then (working with $Hyp(V)$ ) define the following formula:

$$ \begin{align*}\chi(x, y) =_{df} x \in T_\psi \cup T_{(\psi \rightarrow \phi)} \wedge y= \langle x,\phi \rangle\end{align*} $$

$\chi (x, y)$ is clearly a $\Delta _0$ formula defining a function that maps any particular $x \in T_\psi \cup T_{(\psi \rightarrow \phi )}$ to $\langle x , \phi \rangle $ . We also have the following lemma:

Lemma 66 ( $\mathbf {MK}^+$ ) (Barwise, Reference Barwise1975).Footnote ⁵⁷

$\Sigma _1$ -Replacement. $Hyp(V)$ satisfies Replacement for $\Sigma _1$ formulas. □

We thus have $\{ \langle x, \phi \rangle | x \in T_\psi \wedge x \in T_{(\psi \rightarrow \phi )} \} \in Hyp(V)$ as desired. $\langle T_\phi , <_\phi \rangle $ clearly codes a proof of $\phi $ from $\psi $ and $(\psi \rightarrow \phi )$ , the proof steps are inherited from the previous trees, and each proof step prior to $\phi $ is $<_\phi $ -related to $\phi $ .

We deal with (iii) and (iv) in tandem. As the strategy is the same for both, we give only the proof of (iv). Suppose then that $\phi $ is of the form $\forall x \in \bar {V} \psi (x)$ and follows from $\psi (\bar {b})$ for all $b \in V$ by the V-rule. Assume for induction that every $\psi (\bar {b})$ has a proof code $\mathbb {T}_{\psi (\bar {b})} = \langle T_{\psi (\bar {b})}, <_{\psi (\bar {b})} \rangle \in Hyp(V)$ . We then identify:

Lemma 67 ( $\mathbf {MK}^+$ ) (Barwise, Reference Barwise1975).Footnote ⁵⁸

$\Sigma _1$ -Collection. $Hyp(V)$ satisfies Collection for $\Sigma _1$ formulas.

Using $\Sigma _1$ -Collection, we have a nonempty set X which contains proofs of $\psi (\bar {b})$ for each b, and a nonempty set Y containing the relations of each of the $\mathbb {T}_{\psi (\bar {b})}$ . Separating out from X and Y, yields a set $X'$ containing just the domains of proof trees of V-logic proofs in X, and a set $Y'$ containing just the relations of V-logic proof trees in Y. The argument for the full tree of $\mathbb {T}_\phi $ is then exactly the same as in (ii). □

We now are in a position where:

1. (1) Extensions of V can be coded syntactically using V-logic.

2. (2) $Hyp(V)$ can be coded in $\mathbf {MK}^+$ (in fact, $\mathbf {NBG}$ + $\Sigma ^1_1$ -Comprehension + The First Coding Lemma suffices).

3. (3) If $\phi $ is provable in V-logic, then $\phi $ has a proof code in $Hyp(V)$ .

Thus consistency and the axioms we have discussed can be coded using $\mathbf {MK}^+$ class theory. We could stop here, having shown how the Hilbertian Challenge can be met for higher-order properties of V, so long as some impredicative class theory is accepted.Footnote ⁵⁹ However, we still need to satisfy the Methodological Constraint, and it is to this issue that we now turn.