2 The basic setup

We want to verify our results for models of the base theory that is Gödel–Bernays set theory $\mathrm {GB}$ , and also for some of its variants. In Section 9, we will also consider the stronger theory $\mathrm {KM}$ , and we will consider yet another strengthening of it in Section 10. These theories are usually presented as theories in a two-sorted language, with variables for sets and for classes, and their models will be of the form $\mathcal {M}=\langle M,\mathcal {C}\rangle $ , where M denotes the domain of sets, and $\mathcal {C}$ denotes the domain of classes of $\mathcal {M}$ .

Let $\mathcal L(\in )$ denote the collection of first order formulas in the language with the $\in $ -predicate in which we additionally allow for second order variables, and atomic formulas of the form $x\in X$ , where x is a first order variable and X is a second order variable. We consider equality between first or second order elements to abbreviate the statement that they have the same elements. The axioms of $\mathrm {GB}$ are given by the axioms of $\mathrm {ZF}$ for sets, allowing class parameters in the axiom schemes of separation and replacement (that is, allowing for formulas from $\mathcal L(\in )$ in which second order variables are replaced by second order parameters from $\mathcal {C}$ ), together with the class axiom of first order class comprehension, that is comprehension for classes using $\mathcal L(\in )$ -formulas with second order parameters from $\mathcal {C}$ . If $\mathcal {M}\models \mathrm {GB}$ (or any of its variants), we usually use lowercase letters to denote first order elements of $\mathcal {M}$ , that is elements of M, and uppercase letters to denote second order elements of $\mathcal {M}$ , that is elements of $\mathcal {C}$ . Note that by the separation axiom, we have $M\subseteq \mathcal {C}$ .

We will also consider the strengthenings of $\mathrm {GB}$ that are obtained by adding the axiom of choice ( $\mathrm {GBc}$ ) in the form of the statement that every set can be well-ordered, or ( $\mathrm {GBC}$ ) the axiom that there is a well-order of all sets in order-type $\operatorname {\mathrm {Ord}}$ (or equivalently, a set-like global well-order), as well as the axiom systems $\mathrm {GB}^-$ , $\mathrm {GBc}^-$ , and $\mathrm {GBC}^-$ , which are obtained from $\mathrm {GB}$ , $\mathrm {GBc}$ , or $\mathrm {GBC}$ respectively by removing the powerset axiom and using the axiom scheme of collection rather than replacement. We fix a base theory T to be one of the above theories.

We next provide the definition of a class forcing generic framework, which will be the basic formal concept in our approach. As in [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7], we will use the more general notion of preorders rather than (the perhaps more common restriction to) partial orders, dropping the requirement of antisymmetry. If $\vec A$ is a finite sequence, we will use the statement $\vec A\in \mathcal {C}$ to abbreviate the property that all sequents of $\vec A$ are elements of $\mathcal {C}$ .

Definition 2.1. A class forcing generic framework is a tuple of the form

$$ \begin{align*}\left\langle\mathcal{M},\mathbb{P},R,\left(\operatorname{\mathrm{\Vdash}}_\varphi^{\vec A}\right)_{\varphi\in\mathcal L(\in),\vec A\in\mathcal{C}},\mathfrak G\right\rangle\textrm{ with the following properties}.\end{align*} $$

• • $\mathcal {M}$ is a transitive set-size model of $T: M$ is transitive, $\bigcup \mathcal {C}\subseteq M$ , and $\mathcal {M}$ is a set such that $\mathcal {M}\models T$ .

• • $\mathbb {P}=\langle P,\le \rangle $ is a preorder with weakest element $\operatorname {\mathrm {\mathsf {1}}}_P$ (that is $p\le \operatorname {\mathrm {\mathsf {1}}}_P$ for every $p\in P$ ) such that both P and $\le $ are in $\mathcal {C}$ .

• • The $\mathbb {P}$ -membership relation R is a relation on $P\times M\times \mathcal {C}$ that is definable over $\mathcal {M}$ by an $\mathcal L(\in )$ -formula $\varphi (p,a,B)$ with first order variables p and a, and a second order variable B, so that for $p\in P$ , $a\in M$ , and $B\in \mathcal {C}$ we have $R(p,a,B)$ if and only if $\varphi (p,a,B)$ .Footnote ³ We denote the property $R(p,a,B)$ as $a\in _p B$ .Footnote ⁴

• • $\mathfrak G$ is a second order unary predicate on P, i.e., a unary predicate on $\mathcal P(P)$ , and we require that $\mathfrak G(G)$ implies that $G\subseteq P$ is a filter. If $\mathfrak G(G)$ holds, we say that G is a generic filter, or a $\mathbb {P}$ -generic filter on M. Whenever we quantify over G in the following, we assume that we quantify over G’s such that $\mathfrak G(G)$ holds.

• • For every $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L(\in )$ for which the number of second order variables corresponds to the length of $\vec A$ , $\operatorname {\mathrm {\Vdash }}_\varphi ^{\vec A}\in \mathcal {C}$ is a predicate (which we also call a forcing relation for $\varphi $ ) on $P\times M^m$ , where m denotes the number of free first order variables of $\varphi $ . If $\langle q,a_0,\ldots ,a_{m-1}\rangle \in \operatorname {\mathrm {\Vdash }}_\varphi ^{\vec A}$ , we also write $q\operatorname {\mathrm {\Vdash }}\varphi (a_0,\ldots ,a_{m-1},\vec A)$ .

3 The basic axioms

In this section, we present our basic axioms for class forcing generic frameworks.

1. (1) Existence of generic filters: $\forall p\in P\,\exists G\ p\in G$ .Footnote ⁵

2. (2) Well-Foundedness: The binary relation $\exists p\in P\ a\in _p b$ on M is well-founded.

3. (3) Growth of Information: For all $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L(\in )$ , for all $\vec a\in M$ , and $p,q\in P$ , if $p\operatorname {\mathrm {\Vdash }}\varphi (\vec a,\vec A)$ and $q\le p$ , then $q\operatorname {\mathrm {\Vdash }}\varphi (\vec a,\vec A)$ .

Assume that G is such that $\mathfrak G(G)$ holds. Define a relation $\in _G$ on $\mathcal {C}$ by letting $a\in _G B$ if $\exists p\in G\ a\in _p B$ . Using axiom (2), this relation on $\mathcal {C}$ is well-founded, and since $\mathcal {M}\in V$ , it is clearly set-like in V. We may thus recursively define our evaluation function $F_G$ along the relation $\in _G$ , letting $F_G(B)=\{F_G(a)\mid a\in _G B\}$ for each $B\in \mathcal {C}$ .Footnote ⁶ Let $\mathcal {M}[G]$ denote the $\in $ -structure on the transitive set $F_G[\mathcal {C}]$ :Footnote ⁷ That is, let $\mathcal {M}[G]=\langle M[G],\mathcal {C}[G]\rangle $ , where $M[G]=F_G[M]$ , and $\mathcal {C}[G]=F_G[\mathcal {C}]$ .

The next two axioms state that a natural form of the forcing theorem holds, that is based on our forcing relations. Given a finite tuple $\vec A=\langle A_i\mid i<n\rangle \in \mathcal {C}$ , let $F_G(\vec A)=\langle F_G(A_i)\mid i<n\rangle $ .

1. (4) Truth Lemma: For all $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L(\in )$ for which the number of second order variables corresponds to the length of $\vec A$ , all $\vec a\in M$ , and all G,

   $$ \begin{align*}\mathcal{M}[G]\models\varphi(F_G(\vec a),F_G(\vec A))\textrm{ iff }\exists p\in G\ p\operatorname{\mathrm{\Vdash}}\varphi(\vec a,\vec A).\end{align*} $$

2. (5) Definability Lemma: For all $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L(\in )$ for which the number of second order variables corresponds to the length of $\vec A$ , all $\vec a\in M$ , and $p\in P$ ,

   $$ \begin{align*}p\operatorname{\mathrm{\Vdash}}\varphi(\vec a,\vec A)\textrm{ iff }\forall G\ni p\ \mathcal{M}[G]\models\varphi(F_G(\vec a),F_G(\vec A)).\end{align*} $$
   Footnote ⁸

Our next axiom ( $\bar 6$ ) states that within M, a weak form of set-likeness holds for the $\mathbb {P}$ -membership relation. We will later replace it by the stronger axiom (6).Footnote ⁹

1. ( $\bar 6$ ) Weak Set-Likeness: If $b\in M$ , then $\{a\mid \exists p\in P\ a\in _p b\}\in M$ .

We will also introduce two additional axioms, axioms (7) and (8), later on in our paper. For the moment, we introduce two other additional axioms, stating that all elements of M have a name in M, and that there is a (class) name for our generic filters. They will later be replaced by the stronger axiom (7) which will imply both these axioms. Since those are only temporary axioms, we will not provide them with a number.

• (*) Names for ground model objects:

  • • $\forall a\in M\,\exists \check a\in M\,\forall G\ F_G(\check a)=a$ , and

  • • $\forall A\in \mathcal {C}\,\exists \check A\in \mathcal {C}\,\forall G\ F_G(\check A)=A$ .

• (**) Name for generic filters: $\exists \dot G\in \mathcal {C}\ \forall G\ F_G(\dot G)=G$ .

Given $a\in M$ and $A\in \mathcal {C}$ , we will use $\check a$ and $\check A$ to denote names for a and A as provided by axiom (*) above, and we will use $\dot G$ to denote a (class) name for G as provided by axiom (**) above.

4 Forcing predicates and density

Our axioms (1)–(5) together with the axioms (*) and (**) suffice to verify some of the basic properties of forcing, and in particular to verify that the forcing predicates satisfy their usual defining clauses, by arguments that are similar to the arguments of [Reference Freire3, Section 4]. For the sake of completeness, and for the benefit of our readers, we would nevertheless like to present some of these arguments here. The first step will be to verify an auxiliary result on the forcing of negated statements.

Lemma 4.1. For all $\varphi \in \mathcal L(\in )$ , $p\in P$ , $\vec a\in M$ , and $\vec A\in \mathcal {C}$ , we have that

$$ \begin{align*}p\operatorname{\mathrm{\Vdash}}\lnot\varphi(\vec a,\vec A)\textrm{ iff }\forall q\le p\ q\not\operatorname{\mathrm{\Vdash}}\varphi(\vec a,\vec A).\end{align*} $$

We are now ready to show that our axioms imply generic filters to intersect all dense classes in $\mathcal {C}$ .

Proof Let G be a generic filter and assume for a contradiction that $G\cap D=\emptyset $ . Making use of axioms (*) and (**), it follows that

$$ \begin{align*}\mathcal{M}[G]\models\lnot\exists x\ x\in F_G(\check D)\cap F_G(\dot G).\end{align*} $$

By axiom (4), we may thus find $p\in G$ such that

$$ \begin{align*}p\operatorname{\mathrm{\Vdash}}\lnot\exists x\ x\in\check D\cap\dot G.\end{align*} $$

By Lemma 4.1, equivalently

$$ \begin{align*}\forall q\le p\ q\not\operatorname{\mathrm{\Vdash}}\exists x\ x\in\check D\cap\dot G.\end{align*} $$

Since D is dense, we may fix $q\le p$ in D. But then,

$$ \begin{align*}q\operatorname{\mathrm{\Vdash}}\check q\in\check D\cap\dot G,\end{align*} $$

contradicting the above.

We next need another auxiliary result on open dense sets (which could easily be extended to arbitrary dense sets, but the current version is sufficient for our purposes). We say that a subset A of a preorder P is open if it is downward closed, that is if $p\in A$ and $q\le p$ , then also $q\in A$ .

Lemma 4.3. If $D\subseteq P$ is open, $D\in \mathcal {C}$ , then D is dense below p if and only if

$$ \begin{align*}(\dagger)\ \forall G\ni p\,D\cap G\ne\emptyset.\end{align*} $$

It is now possible to show, as in [Reference Freire3], that the usual defining clauses for the forcing relation can be recovered from our basic axioms. The only additional clause that we need is the one for the elementhood relation with respect to classes. Its proof is very similar to the one for the elementhood relation with respect to sets; however we would like to provide one sample argument here in this paper for the benefit of our readers, and we will refer them to [Reference Freire3] for the other clauses below (note that since $M\subseteq \mathcal {C}$ , the below lemma also covers the case of the elementhood relation with respect to sets). Let $a\operatorname {\mathrm {\overline {\in }}}_p B$ if and only if $\exists q\ge p\ a\in _q B$ .Footnote ¹⁰

In the next lemma, we list the remaining results with respect to the forcing predicates obeying their usual defining clauses, which are shown exactly as in [Reference Freire3, Section 5], simply carrying along additional second order predicates (in case there are any). For the detailed arguments to verify these properties, we refer the interested reader to [Reference Freire3]. We consider the relations $\in $ and $\ne $ as our atomic relations in the below; however $a\ne b$ could be seen as abbreviating $\lnot (a=b)$ , and $a\not \in b$ should be seen as abbreviating $\lnot (a\in b)$ .

The existence of forcing relations for atomic formulas is usually a problematic aspect in the case of class forcing (for a detailed account of this see [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7]). The fundamental difference in our setup is that the definability of forcing predicates is already an integral assumption. In the above, we only show that any single step, reducing forcing statements about atomic formulas to ones for names of lower rank, proceeds as usual. We thus avoid the usual problem of having to obtain the definability of the forcing predicates for atomic formulas by recursion (which a priori is a recursion on classes, and is thus not guaranteed by the axioms of $\mathrm {GBC}$ , see [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7], or also [Reference Gitman, Hamkins, Holy, Schlicht and Williams6]). The existence of such recursions is an axiom of $\mathrm {KM}$ on the other hand, and this is the reason why every notion of class forcing satisfies the forcing theorem in $\mathrm {KM}$ (see [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7], [Reference Gitman, Hamkins, Holy, Schlicht and Williams6], or [Reference Antos-Kuby1]).

5 An axiomatization that assumes the preservation of the axioms of set theory

In this section, we introduce two further temporary axioms.

• (***) Preservation of axioms: $\forall G\ \mathcal {M}[G]\models T$ Footnote ¹¹ and

• (****) Absoluteness of $\mathbb {P}$ -membership: The formula $\varphi $ defining the $\mathbb {P}$ -membership relation R is absolute for transitive models of T containing $\mathcal {C}$ .

Building on the terminology from [Reference Freire3, Section 3], let us say that a class forcing generic extension is a class forcing generic framework together with a particular choice of generic filter G. Our next theorem shows that under a suitable set of axioms, this notion corresponds to the usual notion of a class forcing extension, and in particular it shows that $\mathcal {M}[G]$ is well-defined, in the sense that it only depends on $\mathcal {M}$ and on G.

6 On the notion of tameness

One of the classical results about set forcing is that it preserves the axioms of $\mathrm {ZF}^-$ , $\mathrm {ZF}$ , and $\mathrm {ZFC}$ , and this easily extends to any of the second order theories that we consider in this paper. However the situation is completely different for class forcing, for any of the second order theories that we consider in this paper may easily be destroyed by class forcing. For example, simply consider the notion of forcing which adds a function from $\omega $ to $\operatorname {\mathrm {Ord}}$ using finite conditions. This notion of class forcing will provide us with a class function mapping $\omega $ surjectively onto $\operatorname {\mathrm {Ord}}$ in any of its generic extensions, clearly yielding $\mathrm {GB}^-$ to fail. A key notion in this context is that of pretameness, which was implicit in earlier work of A. Zarach and of M. Stanley, and which was isolated by Friedman in [Reference Friedman5]. In the following, when we talk about sequences of classes, we will assume some suitable coding so that these sequences can themselves be viewed as classes.

M. Stanley showed that pretameness is actually equivalent to the property that forcing with $\mathbb {P}$ preserves the axioms of $\mathrm {GB}^-$ in a standard class forcing setup (see [Reference Holy, Krapf and Schlicht8, Theorem 3.1]), and it is shown in [Reference Holy, Krapf and Schlicht8, Theorem 1.12] that pretameness is equivalent to a large number of desirable niceness features of forcing notions. It therefore seems very natural to restrict ones attention to pretame notions of forcing in the context of class forcing. Pretame notions of forcing also preserve the axiom of choice, and the existence of a global well-order in order type $\operatorname {\mathrm {Ord}}$ : regarding the axiom of choice, if x is a set in a generic extension $\mathcal {M}[G]$ by a pretame forcing notion $\mathbb {P}$ , we pick a $\mathbb {P}$ -name $\dot x$ for x, and a well-order $\prec $ of $X=\{\sigma \mid \exists p\in P\ \langle \sigma ,p\rangle \in \dot x\}$ . We then construct a well-order of x as follows: given two of its elements y and z, we let $y\triangleleft z$ if the $\prec $ -least $\mathbb {P}$ -name for y in X (that is, the $\prec $ -least $\sigma \in X$ so that $\sigma ^G=y$ ) is $\prec $ -below any $\mathbb {P}$ -name for z in X. The argument for the preservation of the existence of a global well-order in order type $\operatorname {\mathrm {Ord}}$ is essentially the same, and presented within [Reference Holy, Krapf and Schlicht8, Theorem 3.1].

However, pretame notions of forcing need not preserve the powerset axiom. This can easily be observed by considering the pretame notion of forcing that adds a proper class of Cohen subsets of $\omega $ . Since in any of its extensions, the powerset of $\omega $ would have to be a proper class, it cannot exist as a set. For the preservation of the powerset axiom, we need the notion of tameness. In his [Reference Friedman4], Friedman introduces tameness of a class forcing notion $\mathbb {P}$ as the axiom requiring that $\mathbb {P}$ is pretame and that the weakest condition of $\mathbb {P}$ forces the powerset axiom to hold (in the generic extension). Since pretameness of $\mathbb {P}$ implies the $\mathbb {P}$ -forcing relation to be definable, forcing the powerset axiom to hold is a first order property of $\mathbb {P}$ . Previously, in his [Reference Friedman5], a more combinatorial definition of tameness was provided, which however seems potentially problematic to us (we do not see how a crucial step in the argument of [Reference Friedman5, Theorem 2.21] proceeds, which is supposed to show that this combinatorial version of tameness implies the preservation of the powerset axiom), but this issue can easily be fixed by slightly strengthening the original property of tameness from [Reference Friedman5] (we will let tameness denote this strengthened property in the below)—we will show that (our version of) tameness is equivalent to the preservation of the powerset axiom under certain additional axioms (which all hold in any standard setup for class forcing) in Section 7.Footnote ¹²

Note that if $\langle D_0,D_1\rangle $ is a predense $\le p$ partition of $\mathbb {P}$ for some $p\in P$ , and $q\le p$ , then $\langle D_0,D_1\rangle $ is also a predense $\le q$ partition of $\mathbb {P}$ . We will tacitly make use of this in the below.

7 An axiomatization that does not assume the preservation of the axioms of set theory

Alternatively, we can replace ( $\bar 6$ ), (*), (**), (***), and (****) by the following axioms, and in particular we can derive the preservation of the axioms of set theory from natural axioms rather than requiring it. Axiom (6) below is a strengthening of axiom ( $\bar 6$ ), which seems to be a natural requirement in the context of class forcing, and could be seen to essentially say that the objects that are our version of names for sets correspond to set-sized objects in a standard class forcing setup. Axiom (7) essentially says that we can freely (from the perspective of $\mathcal {M}$ ) construct our version of names in $\mathcal {M}$ . Axiom (8) is (pre)tameness, and is only required in the case of class forcing (for it is trivial in the case of set forcing).

1. (6) Strong Set-Likeness: If $b\in M$ , then $\{\langle a,p\rangle \mid a\in _p b\}\in M$ .

2. (7) Universality: If $S\in \mathcal {C}$ is a relation on $M\times P$ , then there exists $B\in \mathcal {C}$ such that

   $$ \begin{align*}S(a,p)\textrm{ if and only if }a\in_p B.\end{align*} $$
   Moreover, if $S\in M$ , then we obtain the above B to be in M, and there is a map $\Gamma $ that is first order definable over M which on input $S\in M$ yields one such witnessing $B\in M$ .Footnote ¹⁴
3. (8)

   1. • Pretameness: $\mathbb {P}$ is pretame (for $\mathcal {M}$ ).

   2. • Tameness: If T contains the power set axiom, then we make the stronger requirement that $\mathbb {P}$ is tame (for $\mathcal {M}$ ).

Let us make the important remark that our axioms (1)–(8), as well as the axioms (*), (**), (***), and (****), hold in the standard setup for class forcing, as described for example in [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7]. Given a transitive model $\mathcal {M}=\langle M,\mathcal {C}\rangle $ of T, and a pretame, or tame (in case T contains the powerset axiom) notion of class forcing $\mathbb {P}\in \mathcal {C}$ such that for every condition p from $\mathbb {P}$ , there is a $\mathbb {P}$ -generic filter over $\mathcal {M}$ that contains p as an element (this is the case in particular if $\mathcal {M}$ is countableFootnote ¹⁵ ), interpreting $a\in _p B$ as $\langle a,p\rangle \in B$ , we arrive at such a standard setup, and it is well-known how to verify axioms (1)–(8), (*), (**), (***), and (****) with respect to $\mathcal {M}$ and $\mathbb {P}$ in this context—for the forcing theorem, as described in our axioms (4) and (5), see [Reference Holy, Krapf, Lücke, Njegomir and Schlicht7, Reference Holy, Krapf and Schlicht8].

Making heavy use of axioms (6) and (7), our next lemma shows that standard forcing names and their evaluations essentially coincide with elements of our ground model $\mathcal {M}$ and their images under our evaluation function $F_G$ .

Proof Let us first verify (i). Let $\sigma $ be a $\mathbb {P}$ -name in M. Making use of the map $\Gamma $ that was introduced in axiom (7), we recursively define a translation function h, letting

$$ \begin{align*}h(\tau)=\Gamma(\{\langle h(\nu),p\rangle\mid\langle\nu,p\rangle\in\tau\})\in M.\end{align*} $$

It follows that $F_G(h(\sigma ))=\{F_G(a)\mid \exists p\in G\ a\in _p h(\sigma )\}$

$$ \begin{align*}=\{F_G(a)\mid a=h(\tau)\textrm{ and }\exists p\in G\ \langle\tau,p\rangle\in\sigma\}=\{\tau^G\mid\exists p\in G\ \langle\tau,p\rangle\in\sigma\}=\sigma^G.\end{align*} $$

Now if $\sigma \in \mathcal {C}$ , using axiom (7), we can define $h(\sigma )$ to be such that for all $\mathbb {P}$ -names $\tau \in M$ and $p\in P$ ,

$$ \begin{align*}h(\tau)\in_p h(\sigma)\textrm{ if and only if }\langle\tau,p\rangle\in\sigma.\end{align*} $$

We thus obtain $h(\sigma )\in \mathcal {C}$ , and then the same argument as above shows that $F_G(h(\sigma ))=\sigma ^G$ .

Now let us verify (ii), in a similar way. Let $b\in M$ , and making use of axiom (6), we obtain a map $E\in \mathcal {C}$ with domain M such that for every $a\in M$ , $E(a)=\{\langle x,p\rangle \mid x\in _p a\}\in M$ . Making use of this map, we recursively define another translation function g, letting $g(b)=\{\langle g(a),p\rangle \mid a\in E(b),a\in _p b\}$ for $b\in M$ . Similar to before, it now follows that

$$ \begin{align*}g(b)^G=\{g(a)^G\mid\exists p\in G\ \langle g(a),p\rangle\in g(b)\}=\{F_G(a)\mid\exists p\in G\ a\in_p b\}=F_G(b).\end{align*} $$

If $B\in \mathcal {C}$ , we can define $g(B)=\{\langle g(a),p\rangle \mid a\in _p B\}$ , and then the same argument as above shows that $g(b)^G=F_G(b)$ .

Our next goal is to show that we can derive axiom (***) as well as the consequences of Theorem 5.1 from axioms (1)–(8). There are two somewhat different ways to do this. The first possibility is to make use of Lemma 7.2, and then invoke the relevant standard results about the preservation of the axioms of set theory in standard generic extensions,Footnote ¹⁶ and also about their minimality. The second possibility is to directly verify the individual axioms of set theory in our generic extension $\mathcal {M}[G]$ from our axioms. The advantage of this second option is that we do not make use of any standard results in this case (but of course, the arguments to verify the individual axioms in our generic extension are essentially analogous to the corresponding classical arguments). We can then infer minimality of $\mathcal {M}[G]$ by invoking Theorem 5.1 with respect to the standard setup for class forcing.Footnote ¹⁷ We would like to present both approaches in the below.

Second Proof We directly verify the individual axioms in our generic extension. This argument mostly proceeds similar to the proof of [Reference Holy, Krapf and Schlicht8, Theorem 3.1(1)]. The verification of the powerset axiom in $\mathcal {M}[G]$ proceeds somewhat similar to the proof of [Reference Friedman5, Theorem 2.21], however making use of our modified definition of tameness.

Since $\mathcal {M}[G]$ is a transitive $\in $ -structure, it clearly satisfies Regularity and Extensionality. Using axiom (7), it is easy to see that $M[G]$ satisfies Pairing, and by axiom (*), it satisfies Infinity.

Let us treat the union axiom: Let $a\in M[G]$ be given; we need to show that for some $b\in M[G]$ , $\bigcup a\subseteq b$ . Let $X=\{c\mid \exists p\ c\in _p a\}\in M$ by axiom ( $\bar 6$ ). Let $Y=\{d\mid \exists c\in X\,\exists q\ d\in _q c\}\in M$ by axiom ( $\bar 6$ ). Using axiom (7), let $\dot b\in M$ be such that $d\in _r\dot b$ if and only if $d\in Y$ and $r=1$ . Using the definition of $F_G$ , it is straightforward to check that $b=F_G(\dot b)$ is as desired.

Let us verify first order class comprehension in $\mathcal {M}[G]$ . If $\varphi \in \mathcal L(\in )$ and $B\in \mathcal {C}$ , using axiom (7), let $A\in \mathcal {C}$ be such that $a\in _p A$ if and only if $p\operatorname {\mathrm {\Vdash }}\varphi (a,B)$ . It then follows that $F_G(A)=\{x\in M[G]\mid \mathcal {M}[G]\models \varphi (x,F_G(B))\}$ .

We now show that $\mathcal {M}[G]$ satisfies collection. Let $a\in M$ , $A\in \mathcal {C}$ , and assume that $\mathcal {M}[G]\models \forall x\in F_G(a)\,\exists y\ \langle x,y\rangle \in F_G(A)$ . We need to find $b\in M$ such that $\mathcal {M}[G]\models \forall x\in F_G(a)\,\exists y\in F_G(b)\ \langle x,y\rangle \in F_G(A)$ .

By axiom (4), we may pick some $p\in G$ such that $p\operatorname {\mathrm {\Vdash }}\forall x\in a\,\exists y\ \langle x,y\rangle \in A$ . By axiom (6), $X=\{\langle c,r\rangle \mid c\in _r a\}\in M$ . For each $\langle c,r\rangle \in X$ , let

$$ \begin{align*}D_{\langle c,r\rangle}=\{s\in P\mid [s\le p,r\,\land\,\exists d\in M\ s\operatorname{\mathrm{\Vdash}}\langle c,d\rangle\in A]\,\lor\,s\perp r\}\in\mathcal{C}.\end{align*} $$

By Lemma 4.5, it follows that each $D_{\langle c,r\rangle }$ is dense below p in $\mathbb {P}$ . Using that $\mathbb {P}$ is pretame by axiom (8), there is $q\in G$ below p and there is a sequence $\langle d_{\langle c,r\rangle }\mid \langle c,r\rangle \in X\rangle \in M$ such that $d_{\langle c,r\rangle }\subseteq D_{\langle c,r\rangle }$ and $d_{\langle c,r\rangle }$ is predense below q in $\mathbb {P}$ for each $\langle c,r\rangle \in X$ .

Using collection in M, there is a set $Y\in M$ such that for each $\langle c,r\rangle \in X$ and for each $s\in d_{\langle c,r\rangle }$ that is compatible with r, there is $d\in Y$ such that $s\operatorname {\mathrm {\Vdash }}\varphi (c,d,A)$ . Using axiom (7), let $b\in M$ be such that $d\in _s b$ if and only if $d\in Y$ and there is $\langle c,r\rangle \in X$ such that $s\in d_{\langle c,r\rangle }$ and $s\operatorname {\mathrm {\Vdash }}\varphi (c,d,A)$ . Then, by construction, $\mathcal {M}[G]\models \forall x\in F_G(a)\,\exists y\in F_G(b)\ \langle x,y\rangle \in F_G(A)$ , as desired.

Let us next show that $\mathcal {M}[G]$ satisfies separation. Let $a\in M$ and $A\in \mathcal {C}$ . We need to find $b\in M$ such that $\mathcal {M}[G]\models F_G(b)=F_G(a)\cap F_G(A)$ . By axiom (6), $X=\{\langle c,r\rangle \mid c\in _r a\}\in M$ . For each $\langle c,r\rangle \in X$ , let $D_{\langle c,r\rangle }=\{q\in P\mid q\le r\textrm { decides }c\in A\,\lor \,q\perp r\}\in \mathcal {C}$ . By an easy application of Lemma 4.1, it follows that each $D_{\langle c,r\rangle }$ is dense in $\mathbb {P}$ . Using that $\mathbb {P}$ is pretame by axiom (8), we may pick $p\in G$ and a sequence $\langle d_{\langle c,r\rangle }\mid \langle c,r\rangle \in X\rangle \in M$ such that $d_{\langle c,r\rangle }\subseteq D_{\langle c,r\rangle }$ and $d_{\langle c,r\rangle }$ is predense below p in $\mathbb {P}$ for each $\langle c,r\rangle \in X$ . Using axiom (7), let $b\in M$ be such that $c\in _q b$ if and only if there is $r\in P$ such that $q\le r$ , $\langle c,r\rangle \in X$ , $q\in d_{\langle c,r\rangle }$ , and $q\operatorname {\mathrm {\Vdash }} c\in A$ . It clearly follows that b is as desired.

Let us observe at this point that we have by now verified the axioms of $\mathrm {GB}^-$ in $\mathcal {M}[G]$ . By our absoluteness assumptions on the $\mathbb {P}$ -membership relation, this allows us to perform the relevant recursion to obtain $F_G\in \mathcal {C}[G]$ .

Let us argue that the axiom of choice is preserved. Let $a\in M$ . We have to find a well-order $\triangleleft $ of $F_G(a)$ in $M[G]$ . Using axiom ( $\bar 6$ ), let $X=\{c\mid \exists r\in P\ c\in _r a\}\in M$ , and let $\prec $ be a well-order of X, using the axiom of choice in M. Now given x and y in $F_G(a)$ , making use of our above observation, we simply let $x\triangleleft y$ if and only if there is $\dot x\in X$ such that $x=F_G(\dot x)$ and for all $\dot y\in X$ such that $y=F_G(\dot y)$ , we have $\dot x\prec \dot y$ . Using that separation holds in $\mathcal {M}[G]$ , we thus obtain $\triangleleft \in M[G]$ .

Let’s argue that if $\mathcal {M}$ has a set-like global well-order $\prec \,\in \mathcal {C}$ , then we can find a set-like global well-order $\triangleleft $ of $M[G]$ in $\mathcal {C}[G]$ . Using our above observation, we simply let $x\triangleleft y$ if and only if there is $\dot x\in M$ such that $x=F_G(\dot x)$ and for all $\dot y\in M$ such that $y=F_G(\dot y)$ , we have $\dot x\prec \dot y$ . Using that first order class comprehension holds in $\mathcal {M}[G]$ , we thus obtain $\triangleleft \in \mathcal {C}[G]$ .

Finally, we argue that assuming $\mathbb {P}$ to be tame, the powerset axiom is preserved. Working in $\mathcal {M}[G]$ , it suffices to show that $\mathcal P(a)$ exists in $M[G]$ for every $a\in M$ : If $b\in M[G]$ , $b=F_G(\sigma )$ , using axiom ( $\bar 6$ ), let $X=\{c\mid \exists r\in P\ c\in _r\sigma \}\in M$ . Using that $F_G\in \mathcal {C}[G]$ , and using that replacement holds in $\mathcal {M}[G]$ , there is a surjection from X onto b in $M[G]$ , and this surjection naturally induces a surjection from $\mathcal P(X)$ onto $\mathcal P(b)$ in $\mathcal {C}[G]$ . Using replacement in $\mathcal {M}[G]$ once again, if $\mathcal P(X)\in M[G]$ , it follows that $\mathcal P(b)\in M[G]$ .

Therefore, let $a\in M$ . By Lemma 4.2, we may pick $q\in G$ and $\alpha \in \operatorname {\mathrm {Ord}}(M)$ witnessing the tameness of $\mathbb {P}$ with respect to a. Now for any $\sigma \in M$ such that $q\operatorname {\mathrm {\Vdash }}\sigma \subseteq \check a$ , consider the sequence of classes $\vec D=\langle \langle D_0^i,D_1^i\rangle \mid i\in a\rangle $ defined by letting $D_0^i=\{r\le q\mid r\operatorname {\mathrm {\Vdash }}\check i\not \in \sigma \}$ and $D_1^i=\{r\le q\mid r\operatorname {\mathrm {\Vdash }}\check i\in \sigma \}$ . For every $i\in a$ and $j\in \{0,1\}$ , let $E_j^i$ be the dense set obtained as the downward closure of $D_j^i$ . By pretameness, for every $r\le q$ , we obtain $s\le r$ and a predense $\le s$ partition $\vec d=\langle \langle d_0^i,d_1^i\rangle \mid i\in a\rangle $ such that $d_0^i\subseteq E_0^i$ and $d_1^i\subseteq E_1^i$ for every $i\in a$ . By our choice of q and $\alpha $ , we find $\vec e\in V_\alpha ^M$ and $t\le s$ such that $\vec d$ and $\vec e$ are equivalent $\le s$ .Footnote ¹⁸ Since this yields a dense set of conditions t, we may pick such $t\in G$ . Thus,

$$ \begin{align*}i\in F_G(\sigma)\ \iff\ G\cap e_1^i\ne\emptyset,\end{align*} $$

and therefore using axiom (7), letting $\sigma _0\in M$ be such that $c\in _s\sigma _0$ if and only if $c=\check i$ for some $i\in a$ and $s\in e_1^i$ , it follows that $F_G(\sigma )=F_G(\sigma _0)$ . Making use of the map $\Gamma $ described in axiom (7), we have a definable choice of such $\sigma _0$ ’s in M given a predense $\le r$ partition $\vec e\in V_\alpha ^M$ , and using replacement in M, we thus obtain a set $\Sigma \in M$ containing a suitable $\sigma _0$ for every predense $\le r$ partition $\vec e\in V_\alpha ^M$ . Using axiom (7) once again, let $\pi \in M$ be such that $c\in _s\pi $ if and only if $c\in \Sigma $ and $s=1$ . Using separation in $\mathcal {M}[G]$ , this clearly yields $\{x\in F_G(\pi )\mid x\subseteq a\}\in M[G]$ to be the powerset of a in $\mathcal {M}[G]$ , as desired.

Having verified all axioms of T in $\mathcal {M}[G]$ , there are two ways to end the proof: In case axiom (****) holds, the statement of our theorem is a direct consequence of Theorem 5.1, and we have not made any use of the standard setup for class forcing in this case. Without axiom (****), we use that all of our axioms hold in the standard setup for class forcing with $\mathbb {P}$ over $\mathcal {M}$ , and that $\mathcal {M}[G]$ is just the standard class forcing extension of $\mathcal {M}$ by G by Lemma 7.2, and therefore $\mathcal {M}[G]$ is the $\subseteq $ -smallest model of T that contains $\mathcal {C}\cup \{G\}$ as a subset of its collection of classes by Theorem 5.1 used within the standard setup.

Our next proposition shows in particular that notions of forcing that preserve $\mathrm {GB}$ need to be tame (in the sense of Definition 6.2), thus strengthening [Reference Friedman5, Proposition 2.20]. Its proof is similar to the proof that is provided for [Reference Friedman5, Proposition 2.20].

Proof If $\mathbb {P}$ is not pretame, then there is a sequence $\vec D=\langle D_i\mid i\in I\rangle \in \mathcal {C}$ of dense subclasses of $\mathbb {P}$ with $I\in M$ and a condition $p\in P$ witnessing that pretameness fails with respect to $\vec D$ . Using axiom (1), let G be a $\mathbb {P}$ -generic filter over $\mathcal {M}$ with $p\in G$ . In the extension $\mathcal {M}[G]$ , consider the (class) function $F\colon I\to \operatorname {\mathrm {Ord}}^M$ defined by letting

$$ \begin{align*}F(i)=\min\{\alpha\in\operatorname{\mathrm{Ord}}^M\mid G\cap D_i\cap V_\alpha^M\ne\emptyset\},\end{align*} $$

which is an element of $\mathcal {C}[G]$ by first order class comprehension in $\mathcal {M}[G]$ . Since replacement holds in $\mathcal {M}[G]$ , there is some $x\in M[G]$ with $\operatorname {\mathrm {ran}} F\subseteq x$ . Let $\gamma =\sup x$ . Using axiom (4), let $q\le p$ be a condition in G that forces this property of $\check \gamma $ . Using our assumption on p and on $\vec D$ however,

$$ \begin{align*}\exists i\in I\,\forall r\in D_i\cap V_\gamma^M\ q\perp r,\end{align*} $$

yielding $G\cap D_i\cap V_\gamma ^M=\emptyset $ , a contradiction.

If T contains the powerset axiom however $\mathbb {P}$ is not tame, we may thus choose $a\in M$ and $p\in P$ such that for every $\alpha \in \operatorname {\mathrm {Ord}}(M)$ and $q\le p$ , there is $r\le q$ and a sequence $\vec d\in M$ of predense $\le r$ partitions of $\mathbb {P}$ with domain a such that whenever $s\le r$ , then $\vec d$ is not equivalent $\le s$ to any $\vec e$ in $V_\alpha ^M$ . Using axiom (1), let G be a $\mathbb {P}$ -generic filter over $\mathcal {M}$ with $p\in G$ . Since the above yields a dense set of such conditions r for every $\alpha \in \operatorname {\mathrm {Ord}}(M)$ , by Lemma 4.2, there are $r_\alpha \in G$ and a sequence of predense $\le r_\alpha $ partitions $\vec d_\alpha =\langle \langle d_{\alpha ,0}^i,d_{\alpha ,1}^i\rangle \mid i\in a\rangle \in M$ for every $\alpha \in \operatorname {\mathrm {Ord}}(M)$ , witnessing that $\mathbb {P}$ is not tame.Footnote ¹⁹ Whenever $\vec d=\langle \langle d_0^i,d_1^i\rangle \mid i\in a\rangle \in M$ is a sequence of predense $\le t$ partitions for some $t\in G$ , we use axiom (7) to define $\dot f_{\vec d}\in M$ , letting $x\in _u\dot f_{\vec d}$ if and only if

$$ \begin{align*}\left[x=\check{\langle i,0\rangle}\,\land\,u\in d_0^i\right]\,\lor\,\left[x=\check{\langle i,1\rangle}\,\land\,u\in d_1^i\right].\end{align*} $$

That is, $\dot f_{\vec d}$ can be seen as a canonical name for the function $f_{\vec d}\in M[G]$ , $f_{\vec d}\colon a\to 2$ that is defined by letting $f_{\vec d}(i)=0\,\iff \,G\cap d_0^i\ne \emptyset $ for every $i\in a$ . Note that, using axioms (4) and (5), two sequences $\vec d$ and $\vec d'$ of predense $\le t$ partitions with domain a of $\mathbb {P}$ in $\mathcal {C}$ are equivalent $\le t$ if and only if $t\operatorname {\mathrm {\Vdash }}\dot f_{\vec d}=\dot f_{\vec d'}$ . Thus, for any $\alpha \in \operatorname {\mathrm {Ord}}^M$ , $r_\alpha $ forces that $\dot f_{\vec d_\alpha }\ne \dot f_{\vec e}$ for any predense $\le r_\alpha $ partition $\vec e\in V_\alpha ^M$ with domain a. This implies that in $\mathcal {M}[G]$ , we obtain a cofinal partial function F from $\{f\in M[G]\mid f\colon a\to 2\}$ to $\operatorname {\mathrm {Ord}}$ , by letting $F(f)$ be the least $\alpha $ such that there is a condition $r\in G$ and a predense $\le r$ partition $\vec e\in V_\alpha ^M$ with domain a such that $f=f_{\vec e}$ . By replacement in $\mathcal {M}[G]$ thus, the powerset of a cannot exist as a set in $M[G]$ , and hence $\mathcal {M}[G]$ does not satisfy the powerset axiom.

8 Set forcing

The axioms for set forcing, which are essentially as in [Reference Freire3], can easily be derived from the case of class forcing over models of $\mathrm {GBc}$ that was treated in this paper. In addition, we will also consider the base theories $\mathrm {ZF}^-$ , $\mathrm {ZFC}^-$ , and $\mathrm {ZF}$ , which correspond to the second order theories $\mathrm {GB}^-$ , $\mathrm {GBc}^-$ , and $\mathrm {GB}$ . Let T thus denote our base theory, which will either be $\mathrm {ZF}^-$ , $\mathrm {ZFC}^-$ , $\mathrm {ZF}$ , or $\mathrm {ZFC}$ . Our terminology will be slightly different from that of [Reference Freire3]. In this section, let $\mathcal L(\in )$ denote the collection of first order formulas.

Definition 8.1. A set forcing generic framework is a tuple of the form

$$ \begin{align*}\left\langle M,\mathbb{P},R,\left(\operatorname{\mathrm{\Vdash}}_\varphi\right)_{\varphi\in\mathcal L(\in)},\mathfrak G\right\rangle\textrm{ with the following properties}.\end{align*} $$

• • M is a transitive set-size model of T.

• • $\mathbb {P}=\langle P,\le \rangle \in M$ is a preorder.

• • The $\mathbb {P}$ -membership relation R is a relation on $P\times M^2$ that is definable over M by an $\mathcal L(\in )$ -formula. We denote the property $R(p,a,b)$ as $a\in _p b$ .Footnote ²⁰

• • $\mathfrak G$ is a second order unary predicate on P, i.e., a unary predicate on $\mathcal P(P)$ , and we require that $\mathfrak G(G)$ implies that $G\subseteq \mathbb {P}$ is a filter. If $\mathfrak G(G)$ holds, we say that G is a generic filter, or a $\mathbb {P}$ -generic filter on M. Whenever we quantify over G in the following, we assume that we quantify over G’s such that $\mathfrak G(G)$ holds.

• • For every $\varphi \in \mathcal L(\in )$ , $\operatorname {\mathrm {\Vdash }}_\varphi \in \mathcal {C}$ is a predicate (which we also call a forcing relation for $\varphi $ ) on $P\times M^m$ , where m denotes the number of free variables of $\varphi $ . If $\langle q,a_0,\ldots ,a_{m-1}\rangle \in \operatorname {\mathrm {\Vdash }}_\varphi $ , we also write $q\operatorname {\mathrm {\Vdash }}\varphi (a_0,\ldots ,a_{m-1})$ .

Let us briefly provide the list of corresponding axioms for set forcing.

• (S1) Existence of generic filters: $\forall p\in P\,\exists G\ p\in G$ .

• (S2) Well-Foundedness: The binary relation $\exists p\in \mathbb {P}\ a\in _p b$ on M is well-founded.

• (S3) Growth of Information: For all $\varphi \in \mathcal L(\in )$ , for all $\vec a\in M$ , and $p,q\in P$ , if $p\operatorname {\mathrm {\Vdash }}\varphi (\vec a)$ and $q\le p$ , then $q\operatorname {\mathrm {\Vdash }}\varphi (\vec a)$ .

Define the relation $\in _G$ on M by letting $a\in _G b$ if $\exists p\in G\ a\in _p b$ . Recursively define our evaluation function $F_G$ along the relation $\in _G$ , letting $F_G(a)=\{F_G(b)\mid b\in _G a\}$ for each $a\in M$ . Let $M[G]$ denote the $\in $ -structure on the transitive set $F_G[M]$ .

• (S4) Truth Lemma: For all $\varphi \in \mathcal L(\in )$ , all $\vec a\in M$ , and all G,

  $$ \begin{align*}M[G]\models\varphi(F_G(\vec a))\textrm{ iff }\exists p\in G\ p\operatorname{\mathrm{\Vdash}}\varphi(\vec a).\end{align*} $$

• (S5) Definability Lemma: For all $\varphi \in \mathcal L(\in )$ , all $\vec a\in M$ , and $p\in P$ ,

  $$ \begin{align*}p\operatorname{\mathrm{\Vdash}}\varphi(\vec a)\textrm{ iff }\forall G\ni p\ M[G]\models\varphi(F_G(\vec a)).\end{align*} $$

• (S6) Set-Likeness: If $b\in M$ , then $\{a\mid \exists p\in P\ a\in _p b\}\in M$ .

• (S*) Names for ground model objects: $\forall a\in M\,\exists \check a\in M\,\forall G\ F_G(\check a)\,{=}\,a$ .

• (S**) Name for generic filters: $\exists \dot G\in M\ \forall G\ F_G(\dot G)=G$ .

• (S***) Preservation of axioms: $\forall G\ M[G]\models T$ .

• (S****) Absoluteness of $\mathbb {P}$ -membership: The formula $\varphi $ defining the $\mathbb {P}$ -membership relation R is absolute for transitive models of T containing M.

We can use these axioms to deduce the following version of Theorem 5.1 (by essentially using the same argument). A set forcing generic extension is a set forcing generic framework together with a particular choice of generic filter G.

Proceeding toward a set forcing analogue of the results of Section 7, we introduce one further axiom.

• (S7) Universality: If $s\in M$ is a relation on $M\times P$ , then there exists $b\in \mathcal {M}$ such that

  $$ \begin{align*}s(a,p)\textrm{ if and only if }a\in_p b.\end{align*} $$
  We additionally assume that there is a map $\Gamma $ that is first order definable over M which on input s yields one such witnessing $b\,{\in}\, M$ .Footnote ²¹

The arguments from Section 7 then also yield the following.

Another way of verifying Theorem 8.3 is to observe that a set forcing generic framework satisfying axioms (S1)–(S7) corresponds exactly to a class forcing generic framework over a model $\mathcal {M}=\langle M,\mathcal {C}\rangle $ satisfying axioms (1)–(8) for which $\mathcal {C}$ is just the collection of subsets of M that are first order definable over M, and to then apply Theorem 7.3:Footnote ²²

In one direction, it should be pretty clear that starting from a class forcing generic framework in this setting, when $\mathbb {P}\in M$ however is a set-sized partial order, we can easily isolate a corresponding set forcing generic framework with respect to $\mathbb {P}$ and verify our set forcing axioms for that framework from their class forcing counterparts.

Let us provide a few more details on the other direction, which is relevant for verifying Theorem 8.3. We start with a set forcing generic framework

$$ \begin{align*}\left\langle M,\mathbb{P},R,\left(\operatorname{\mathrm{\Vdash}}_\varphi\right)_{\varphi\in\mathcal L(\in)},\mathfrak G\right\rangle.\end{align*} $$

We first have to extend our $\mathbb {P}$ -membership relation R. Using the same letter R also for its extension, we simply do so by letting $R(p,a,B)$ if and only if $\langle a,p\rangle \in B$ in case $B\in \mathcal {C}\setminus M$ . That is, at the top level, when B is a proper class, we define our $\mathbb {P}$ -membership relation to behave analogous to the relation $\langle a,p\rangle \in B$ from the classical setting. For every nonzero length $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L(\in )$ , we have to define relations $\operatorname {\mathrm {\Vdash }}_\varphi ^{\vec A}$ ; however we simply define them to equal the corresponding first order forcing relations from our set forcing generic framework for the formulas obtained by replacing the elements of $\vec A$ by their defining formulas. Using our extended $\mathbb {P}$ -membership relation, we can now define $a\in _G B$ if $\exists p\in G\ a\in _p B$ in case B is a proper class, and we can thus also define $F_G(B)$ for $B\in \mathcal {C}\setminus M$ , letting $F_G(B)=\{F_G(a)\mid \exists p\in G\langle a,p\rangle \in B\}$ . We then let $\mathcal {M}[G]=\langle F_G[M],F_G[\mathcal {C}]\rangle $ , as we did in Section 3. It is then easy to see that each of axioms (S1)–(S6) implies its corresponding axiom from (1)–(6). In order to verify axiom (7), assume that $S\in \mathcal C\setminus M$ is a relation on $M\times P$ . Let $B\in \mathcal {C}$ be such that $S(a,p)$ holds if and only if $\langle a,p\rangle \in B$ . Then B witnesses the relevant instance of axiom (7). Finally, it is well-known and easy to check that any notion of set forcing is pretame for models of $\mathrm {GB}^-$ , and tame for models of $\mathrm {GB}$ , thus yielding axiom (8).

9 Kelley–Morse set theory

Kelley–Morse set theory $\mathrm {KM}$ extends the axioms of $\mathrm {GBC}$ by the scheme of second order class comprehension. Let $\mathcal L^2(\in )$ denote the collection of all second order formulas in the language with the $\in $ -predicate.

Definition 9.1. A class forcing generic framework for $\mathrm {KM}$ is a tuple of the form

$$ \begin{align*}\left\langle\mathcal{M},\mathbb{P},R,\left(\operatorname{\mathrm{\Vdash}}_\varphi^{\vec A}\right)_{\varphi\in\mathcal L^2(\in),\vec A\in\mathcal{C}}\!,\mathfrak G\right\rangle\end{align*} $$

with the same properties as those of a class forcing generic framework in Definition 2.1, except that the last item from that definition has to be changed to the following.

• • For every $\vec A\in \mathcal {C}$ and $\varphi \in \mathcal L^2(\in )$ for which the number of free second order variables corresponds to the length of $\vec A$ , $\operatorname {\mathrm {\Vdash }}_\varphi ^{\vec A}\in \mathcal {C}$ is a predicate (which we also call a forcing relation for $\varphi $ ) on $P\times M^m$ , where m denotes the number of free first order variables of $\varphi $ .

  If $\langle q,a_0,\ldots ,a_{m-1}\rangle \in \operatorname {\mathrm {\Vdash }}_\varphi ^{\vec A}$ , we also write $q\operatorname {\mathrm {\Vdash }}\varphi (a_0,\ldots ,a_{m-1},\vec A)$ .

Axioms (1)–(5) are the same as in Section 3, except that $\mathcal L(\in )$ has to be replaced by $\mathcal L^2(\in )$ throughout, and that in axioms (4) and (5), we have to refer to the number of free second order variables, rather than just the number of second order variables. Axioms ( $\bar 6$ ), (*), and (**) are exactly as in Section 3.

We can then use the above axioms to show that the forcing predicates obey their usual defining clauses as in Section 4, except that we have to consider additional types of formulas. As in the case of $\mathrm {GBC}$ we can avoid atomic formulas expressing (in)equality for classes, for we may consider those to be defined in terms of the $\in $ -relation. But we need to treat second order quantification, extending Lemma 4.5 by the following clause. It is verified essentially by the same argument as for first order quantification in [Reference Freire3]; however we would like to provide the argument for the benefit of our readers.

We can now let axioms (***) and (****) be as in Section 5, and verify the analogue of Theorem 5.1 when $T=\mathrm {KM}$ exactly as in that section, showing that $\mathcal {M}[G]$ is the least model of $\mathrm {KM}$ that contains $\mathcal {C}\cup \{G\}$ as a subset of its collection of classes.

Let axiom (6) be exactly as in Section 7. Let axiom (7) be exactly as in Section 7, except that we can ignore its additional definability assumption, for the axioms of $\mathrm {KM}$ include the existence of a global well-order. Let axiom (8) be the assumption that $\mathbb {P}$ is tame (for $\mathcal {M}$ ), as in Section 7, noting that the axioms of $\mathrm {KM}$ include the power set axiom.

As in Section 7, we would like to show that our axioms (1)–(8) imply axioms (*), (**), and (***), and that $\mathcal {M}[G]$ is the $\subseteq $ -smallest model of T that contains $\mathcal {C}\cup \{G\}$ as a subset of its collection of classes. For (*) and (**), this is shown exactly as in Lemma 7.1. The verification of (***) and the minimality of $\mathcal {M}[G]$ proceeds exactly as in the proofs of Theorem 7.3; however we have to additionally verify second order class comprehension in $\mathcal {M}[G]$ in the second proof. This is done by essentially the same argument as for first order class comprehension from the second proof of Theorem 7.3.

10 Extensions of $\mathrm {KM}$

The results of the previous section can also be extended to base theories beyond $\mathrm {KM}$ . As a sample result, let us finally investigate the case of the base theory T that is $\mathrm {KM}$ together with the axiom of class choice ( $\operatorname {\mathrm {CC}}$ ), which was first studied by Mostowski and Marek in [Reference Marek and Mostowski9].

Note that in the above, we could equivalently use arbitrary sets rather than just ordinals as indices, for our base theory $\mathrm {KM}$ provides us with a global well-order in order-type $\operatorname {\mathrm {Ord}}$ . We will tacitly make use of this in the below.

It is shown in [Reference Antos-Kuby2] that tame forcing preserves $\mathrm {KM}+\operatorname {\mathrm {CC}}$ . All results from the previous section thus apply to the stronger base theory $T=\mathrm {KM}+\operatorname {\mathrm {CC}}$ as well—we only need to verify that axioms (1)–(8) from Section 9 imply the preservation of $\operatorname {\mathrm {CC}}$ . Our proof of this is based on the argument from [Reference Antos-Kuby2]. Given $x,y\in M$ , let $\check {\{x,y\}}$ be defined by letting $a\in _p\check {\{x,y\}}$ if and only if $a\in \{x,y\}$ and $p=1$ . Let $\check {\langle x,y\rangle }$ be defined by letting $a\in _p\check {\langle x,y\rangle }$ if and only if $a\in \{\check {\{x,x\}},\check {\{x,y\}}\}$ and $p=1$ . Thus, $\check {\langle x,y\rangle }$ is a canonical name for the ordered pair $\langle F_G(x),F_G(y)\rangle $ in our setup.

Proof Let $A\in \mathcal {C}$ . As a first step, we will argue that a strong form of Lemma 9.2 holds, namely whenever $p\operatorname {\mathrm {\Vdash }}\exists X\varphi (X,A)$ , then there is $X\in \mathcal {C}$ such that $p\operatorname {\mathrm {\Vdash }}\varphi (X,A)$ . Using (second order) class comprehension in $\mathcal {M}$ , let $D\in \mathcal {C}$ be the dense class of all $q\le p$ for which there is some $X_q\in \mathcal {C}$ such that $q\operatorname {\mathrm {\Vdash }}\varphi (X_q,A)$ . Let A be a maximal antichain in D. Using $\operatorname {\mathrm {CC}}$ in $\mathcal {M}$ , for every $q\in A$ , we may pick some $X_q\in \mathcal {C}$ such that $q\operatorname {\mathrm {\Vdash }}\varphi (X_q,A)$ . Now we obtain our desired $X\in \mathcal {C}$ making use of axiom (7), letting $a\in _r X$ if and only if

$$ \begin{align*}r\le q\,\land\,a\in\operatorname{\mathrm{dom}}(X_q)\,\land\,r\operatorname{\mathrm{\Vdash}} a\in X_q.\end{align*} $$

Now suppose that $\mathcal {M}[G]\models \forall \alpha \,\exists X\ \varphi (\alpha ,X,F_G(A))$ . By axiom (4), there is $p\in G$ such that $p\operatorname {\mathrm {\Vdash }}\forall \alpha \,\exists X\ \varphi (\alpha ,X,A)$ . For any $\alpha \in \operatorname {\mathrm {Ord}}^{\mathcal {M}}$ , by the above, we find some $X^\alpha \in \mathcal {C}$ such that $p\operatorname {\mathrm {\Vdash }}\varphi (\alpha ,X^\alpha ,A)$ . Using that our forcing relations are in $\mathcal {C}$ , and using $\operatorname {\mathrm {CC}}$ in $\mathcal {M}$ , we may obtain $X\in \mathcal {C}$ such that $\forall \alpha \ p\operatorname {\mathrm {\Vdash }}\varphi (\alpha ,X_\alpha ,A)$ . Making use of axiom (7), define $Y\in \mathcal {C}$ by letting $a\in _r Y$ if and only if for some $\alpha \in \operatorname {\mathrm {Ord}}^{\mathcal {M}}$ , $a=\check {\langle \alpha ,x\rangle }$ and r is such that $x\in _r X_\alpha $ . It follows that for all $\alpha \in \operatorname {\mathrm {Ord}}$ , $\mathcal {M}[G]\models \varphi (\alpha ,F_G(X)_\alpha ,F_G(A))$ , as desired.

11 Open questions and possible future directions

One obvious question is whether our axiom system can be simplified, or whether some of its axioms could be weakened or even omitted. We have already remarked that the definability of the map $\Gamma $ provided by axiom (7) is not necessary in many cases, and it is not hard to see that for any of the axiom systems we consider, it would instead suffice, in the terminology of axiom (7), to have a map $\Gamma $ which provides a set of witnesses for each $S\in M$ . Moreover, axiom (7) could in fact be replaced by the weaker Item (i) from Lemma 7.2, or some equivalent form of that item, which however seems less desirable as an axiom due to its reference to generic filters. All other requirements made by our axioms seem to be necessary as far as we know. Let us remark that Proposition 7.4 shows that axiom (8) cannot be omitted.

In the present paper, we considered base theories containing at least the axioms of $\mathrm {GB}^-$ , or the corresponding first order theory $\mathrm {ZF}^-$ . The following question was posed to us by Ali Enayat.

One such weaker base theory would be Kripke–Platek set theory; however in his [Reference Mathias10], Mathias developed a weaker axiom system of provident set theory, and shows that models of this theory support a smooth theory of set forcing. It seems plausible that a careful adaption of our axioms could make them work in the context of such weaker models of set theory as well.

A topic that is somewhat implicit in our paper is touched by the following.

Another future direction of research would be the following.