# Non-tightness in class theory and second-order arithmetic

Alfredo Roque Freire  University of Aveiro
Center for Research & Development in Mathematics and Applications - CIDMA
Campus Universitário de Santiago 3810-193 Aveiro
Portugal<EMAIL_ADDRESS>and  Kameryn J. Williams  Sam Houston State
University
Department of Mathematics and Statistics
Box 2206
Huntsville, TX 77341-2206
USA<EMAIL_ADDRESS>http://kamerynjw.net

###### Abstract.

A theory $T$ is tight if different deductively closed extensions of $T$ (in
the same language) cannot be bi-interpretable. Many well-studied foundational
theories are tight, including $\mathsf{PA}$ [Vis06], $\mathsf{ZF}$,
$\mathsf{Z}_{2}$, and $\mathsf{KM}$ [Ena16]. In this article we extend
Enayat’s investigations to subsystems of these latter two theories. We prove
that restricting the Comprehension schema of $\mathsf{Z}_{2}$ and
$\mathsf{KM}$ gives non-tight theories. Specifically, we show that
$\mathsf{GB}$ and $\mathsf{ACA}_{0}$ each admit different bi-interpretable
extensions, and the same holds for their extensions by adding
$\Sigma^{1}_{k}$-Comprehension, for $k\geq 1$. These results provide evidence
that tightness characterizes $\mathsf{Z}_{2}$ and $\mathsf{KM}$ in a minimal
way.

We thank the anonymous referee for their comments. This research was supported
by FCT through CIDMA and projects UIDB/04106/2020 and UIDP/04106/2020.

##  1\. Introduction

It is well known that set theories like $\mathsf{ZF}$ and class theories like
$\mathsf{GB}$ or $\mathsf{KM}$ are capable of interpreting many of their
extensions as theories. For instance, $\mathsf{ZF}$ interprets
$\mathsf{ZFC}+\mathsf{CH}$ via the constructible universe, or one may use the
Boolean ultrapower construction over the notion of forcing
$\mathrm{Add}(\omega,\omega_{2})$ to produce an interpretation of
$\mathsf{ZF}+\lnot\mathsf{CH}$ in $\mathsf{ZF}$ (see. [HS06]). Accordingly,
$\mathsf{ZF}+\mathsf{CH}$ and $\mathsf{ZF}+\lnot\mathsf{CH}$ are mutually
interpretable. Mutual interpretability yields equiconsistency results but for
many set-theoretical purposes it is a coarse notion of equivalence. The issue
is that we may lose information. For an example where this loss is severe,
consider a model of $\mathsf{ZFC}+\neg\mathsf{CH}$ with a measurable cardinal.
Carry out the constructible universe interpretation of
$\mathsf{ZF}+\mathsf{CH}$ in this model followed by the Boolean ultrapower
interpretation. This produces a model of $\mathsf{ZFC}+\neg\mathsf{CH}$ again,
but the model cannot have a measurable cardinal. (Because as a forcing
extension of $\mathrm{L}$ it will miss, for example, $0^{\sharp}$.) Even in
less severe cases information is lost—the boolean ultrapower interpretation
produces ill-founded models, so this two-step interpretation destroys
information about well-foundedness.

interpreted modelsinterpreted modelsModels of $\mathsf{ZF}+\mathsf{CH}$Models
of $\displaystyle\mathsf{ZF}+\neg\mathsf{CH}$ Figure 1. The $\mathrm{L}$ and
Boolean ultrapower interpretations

To avoid this limitation and properly establish an equivalence between
theories, we need a bi-interpretation.111 Interpretations were formally
introduced by Tarski in [Tar53] to deal with undecidable theories. Arguably,
we can say that interpretations were introduced informally in the study of the
consistency of alternative axioms of geometry in the second half of the XIX
century (see [Hod93, p. 260]). Feferman studied interpretations themselves as
mathematical objects in [Fef60, Fef62]. Finally, bi-interpretations appear as
faithful interpretations in [FKO62] even though their definition still do not
encompass the full extent of what we now call bi-interpretations. Precisely, a
_bi-interpretation_ between two theories $T_{1}$ and $T_{2}$ are
interpretations $\mathcal{I}$ and $\mathcal{J}$, respectively of $T_{1}$ in
$T_{2}$ and of $T_{2}$ in $T_{1}$, so that there are definable functions $f$
and $g$ in $T_{1}$ and $T_{2}$ such that for all $\varphi$ and $\psi$

$T_{1}\vdash\varphi(x_{1},x_{2},\ldots,x_{n})\leftrightarrow\varphi^{\mathcal{I}^{\mathcal{J}}}(f(x_{1}),f(x_{2}),\ldots,f(x_{n}))$

And

$T_{2}\vdash\psi(x_{1},x_{2},\ldots,x_{k})\leftrightarrow\psi^{\mathcal{J}^{\mathcal{I}}}(g(x_{1}),g(x_{2}),\ldots,g(x_{k})).$

One can also view bi-interpretations on the level of individual models, saying
that models $M_{1}$ and $M_{2}$ are bi-interpretable. One should view the
theory definition as a uniform version of the model definition, saying that
every model of the theory $T_{1}$ is bi-interpretable with a model of the
theory $T_{2}$, and vice versa, always using the same choice of
interpretations.

Notably, theories such as PA and ZF cannot fix one model up to isomorphism,
i.e. they are not categorical. We can however say that the second order
versions of PA and ZF are respectively categorical (Dedekind in [Ded65]) and
quasi-categorical (Zermelo in [Zer30]). These categoricity results assume that
second order quantifiers indeed range over all subsets of a given domain. Thus
it requires us to attribute to the mathematician a not substantiated ability
to fix the meaning of second order concepts.222See [BW16, Put80] for a
detailed philosophical analysis of the categoricity results.. In this context,
the semantic notion of bi-interpretation can be understood as a weak form of
‘sameness’ allowing for a weaker form of categoricity that do not rely on an
arbitrary reference to the fullness of second order
quantifiers.333Alternatively to considering bi-interpretations, one may
consider a single model with two versions of the same theory (e.g. two
separate symbols for $\in$). Proving that the two versions are always
isomorphic amounts to what is call Internal Categoricity. This concept is
nonetheless limited in scope as it uses the axiom-schemes of the theory to
allow for the two models to be related (e.g. separation satisfied by each
model should include formulas with the alternative symbol for membership).
This concept was introduced by Parson [Par90] with respect to arithmetic.
Väänänen and Wang in [Vää12, VW15, Vää20] studied the internal categoricity in
set theory and further advanced the topic in recent years. Instead of
asserting that two models have isomorphic ontologies, a bi-interpretation
equates the expressible ontology of possibly different models.

In pursuing this form of categority for set and class theories, one should
examine which theories do not admit bi-interpretable models. Indeed, the
interpretations of $\mathsf{ZF}+\mathsf{CH}$ and $\mathsf{ZF}+\neg\mathsf{CH}$
given above lose information. But, are there different interpretations that do
not have this problem, and instead give a bi-interpretation? As demonstrated
by Enayat [Ena16], any two bi-interpreted models of $\mathsf{ZF}$ are
isomorphic. Consequently, no two different extensions of $\mathsf{ZF}$ are bi-
interpretable, and so the answer is negative. While a theory like
$\mathsf{ZF}$ has many models due to the incompleteness phenomenon, in a sense
we cannot have “too many”. This property of $\mathsf{ZF}$ was first
investigated by Visser in [Vis06] with respect to arithmetic and later named
by Enayat as tightness.444Philosophically, as bi-interpretation deals with
expressible ontology, the fact that different models of ZF are never bi-
interpretable suggests that universalist set theorists ‘living’ in different
universes can only assert to fully understand each other if both believe the
other is wrong about their own intuitions. Not only the other is wrong about
the statement that their model is the model of set theory, but also that their
own intuitions about the structure of their models are wrong. A detailed
analysis of this dynamic can be found in [Fre21].

######  Definition.

A theory $T$ is _tight_ if every two bi-interpretable extensions of $T$ in the
same language as $T$ have the same deductive closure.

######  Definition.

A theory $T$ is _semantically tight_ if every two bi-interpretable models of
$T$ are isomorphic.555 Enayat works with a stronger notion he calls solid.
Consider $N$ is a $M$-definable model and that $N$ has a definable copy
$\overline{M}$ of $M$. Using the same interpretation, $\overline{M}$ obtains a
definable copy $\overline{N}$ of $N$. Saying that $M$ and $N$ are bi-
interpretable amounts to (i) there is a $M$-definable isomorphism from $M$ to
$\overline{M}$ and (ii) there is a $N$-definable isomorphism from $N$ to
$\overline{N}$. If we can prove that models $M$ and $N$ of a theory $T$ are
isomorphic without assuming (ii), we can say that $T$ is not only semantically
tight but also solid.

It is evident that every semantically tight theory is also tight.

######  Theorem (Enayat).

$\mathsf{ZF}$, $\mathsf{KM}$, $\mathsf{Z}_{2}$ are tight and semantically
tight.666Enayat proved that $\mathsf{ZF}$, $\mathsf{KM}$, $\mathsf{Z}_{2}$ are
tight [Ena16]; Visser proved that $\mathsf{PA}$ is tight [Vis06]. Visser and
Friedman also proved the $\mathsf{ZF}$ case in an unpublished work (see note 1
of [Ena16]). Indeed, Enayat shows the stronger result that all these theories
are solid. Note, however, that the results in this paper concern non-tightness
and hence will trivially imply non-solidity. For a brief exposition on this,
we recommend Hamkins’s blog post [Ham18].

A natural followup question is whether there are tight subsystems of these
theories. This was proposed in [Ena16, p. 14] and partially addressed with
respect to $\mathsf{ZF}$ by Freire and Hamkins in [FH20]. They show that there
are bi-interpretable models of $\mathsf{Z}$ and
$\mathsf{ZFC}^{-}$.777$\mathsf{Z}$ refers to the first order version of
Zermelo set theory composed of $\mathsf{ZF}$ without the Replacement schema;
$\mathsf{ZFC}^{-}$ stands for $\mathsf{ZFC}$ without the Powerset axiom. Note
that $\mathsf{ZFC}^{-}$ should be axiomatized with Collection schema, not
Replacement, and the well-ordering theorem instead of Zermelo’s formulation of
choice, as these are not equivalent in the absence of Powerset [Zar96].
Moreover, since these model constructions were uniformly produced, they
obtained different bi-interpretable extensions of $\mathsf{Z}$ and
$\mathsf{ZFC}^{-}$. A full answer to this question amounts to a profound
characterization of $\mathsf{ZF}$ and it should be done by obtaining bi-
interpretable models of the theory $\mathsf{Z}$ with fragments of the axiom
scheme of replacement.

In a similar light, this article investigates tightness for subsystems of
$\mathsf{KM}$, obtained by restricting the Comprehension axiom. The weakest
subsytem in this hierarchy is Gödel–Bernays class theory $\mathsf{GB}$, where
Comprehension is only allowed for first-order formulae. Strengthening upward
adding Comprehension for $\Sigma^{1}_{k}$ formulae gives theories we will call
$\mathsf{KM}_{k}$.

Our first main results are that $\mathsf{GB}$ and $\mathsf{KM}_{k}$ are not
semantically tight.

######  Main Theorem 1.0.1.

Let $\kappa$ be an inaccessible cardinal and suppose
$\mathrm{V}_{\kappa}\models\mathrm{V}=\mathrm{HOD}$.

  * •

The minimum model of $\mathsf{GB}$ over $\mathrm{V}_{\kappa}$ is bi-
interpretable with a certain extension adding a Cohen-generic class of
ordinals. Thus, $\mathsf{GB}$ is not semantically tight.

  * •

Let $k\geq 1$. The minimum model of $\mathsf{KM}_{k}$ over
$\mathrm{V}_{\kappa}$ is bi-interpretable with a certain extension adding a
Cohen-generic class of ordinals. Thus, $\mathsf{KM}_{k}$ is not semantically
tight.

We then build on these to show that, indeed, these theories are not tight, and
that the same is true for subsystems of $\mathsf{Z}_{2}$. The failure of
tightness should be seen as a uniform version of the failure of semantic
tightness.

######  Main Theorem 1.0.2.

The following theories are not tight.

  * •

$\mathsf{GB}$;

  * •

$\mathsf{KM}_{k}$ for $k\geq 1$; and

  * •

$\mathsf{KM}_{k}+\Sigma^{1}_{k}$-Class Collection, for $k\geq 1$; and

  * •

Any of the above theories plus the schema of Replacement for all second-order
formulae.

While our primary interest is in class theories, our methods are flexible
enough to also apply to subsystems of second-order arithmetic.

######  Main Theorem 1.0.3.

The following theories are not tight.

  * •

$\mathsf{ACA}_{0}$;

  * •

$\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$ for $k\geq 1$;

  * •

$\Sigma_{k}^{1}\text{-}\mathsf{AC}_{0}$ for $k\geq 1$; and

  * •

Any of the above theories plus the full Induction schema, i.e. the theories
$\mathsf{ACA}$, $\Pi_{k}^{1}\text{-}\mathsf{CA}$, and
$\Sigma_{k}^{1}\text{-}\mathsf{AC}$.

In forthcoming work, Ali Enayat [Ena] independently investigated the
nontightness of fragments of $\mathsf{KM}$ and $\mathsf{Z}_{2}$. He showed
that finitely axiomatizable subtheories of these are not tight. That gives an
alternate proof of the nontightness of $\mathsf{GB}$, $\mathsf{KM}_{k}$,
$\mathsf{ACA}_{0}$, and $\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$, as well as the
versions with Class Collection or $\mathsf{AC}$. But the second-order
Replacement schema and the full Induction schema are not finitely
axiomatizable, so his methods don’t apply to the theories with those schemata.

We present the semantic non-tightness (Section 3) and non-tightness (Section
4) results for class theory separately. The constructions for non-tightness
amounts to more difficult variants of the constructions for semantic non-
tightness, generalized to apply to a wider class of models, including
nonstandard models, so we present the easier constructions first.
Additionally, the constructions over $\mathrm{V}_{\kappa}$ may be of interest
to the set theorist with no interest in nonstandard models, and we wish to be
accommodating to any such reader. In Section 5, we explore how to apply the
same technique to subsystems of second-order arithmetic. And in Section 6 we
briefly discuss the extent to which our constructions generalize and what
questions remain open.

Before these sections we recall some definitions and basic facts about class
theory.

##  2\. Review of class theories and class forcing

In this paper we look at class theories, also called second-order set
theories, those set theories that have proper classes as objects in their
domains of discourse. We will use a two-sorted approach, writing a model as
e.g. $(M,\mathcal{X})$ with $M$ being the sets of the model and $\mathcal{X}$
being the classes of the model. Following standard convention, when writing
formulae in the language of class theory we will use lowercase variables for
sets and uppercase variables for classes. For example, $\forall x\exists
Y\forall z\ (z\in x\Leftrightarrow z\in Y)$ asserts that every set is co-
extensional with some class, a trivial consequence of First-Order
Comprehension.

If a formula only quantifies over sets—but possibly has class parameters—we
call it _first-order_. The class of first-order formulae is denoted with any
of $\Sigma^{1}_{0}$, $\Pi^{1}_{0}$, or $\Delta^{1}_{0}$. From the first-order
formulae we build up the hierarchy of $\Sigma^{1}_{k}$ and $\Pi^{1}_{k}$
formulae by adding class quantifiers in the way familiar to any logician.
Namely, a $\Sigma^{1}_{k}$ formula is of the form
$\exists\bar{X}_{1}\cdots\forall\bar{X}_{k}\varphi(\bar{X}_{1},\ldots\bar{X}_{k})$,
where $\varphi$ is first-order and there are $k$ many blocks of alternating
class quantifiers, while a $\Pi^{1}_{k}$ formula is of the form
$\forall\bar{X}_{1}\cdots\exists\bar{X}_{k}\varphi(\bar{X}_{1},\ldots\bar{X}_{k})$,
again with first-order $\varphi$ and $k$ many blocks of alternating class
quantifiers.

######  Definition 2.0.1.

_Gödel–Bernays_ class theory $\mathsf{GB}$ is axiomatized by the following.

  * •

$\mathsf{ZFC}$ for classes;888The models we consider in this paper will all
satisfy $\mathrm{V}=\mathrm{HOD}$ and hence satisfy the axiom of choice. So
for our purposes we do not want to use merely $\mathsf{ZF}$ for the sets. For
this same reason our models will for free satisfy Global Choice.

  * •

Class Extensionality, asserting that two classes are equal if and only if they
have the same elements;

  * •

Class Replacement, asserting that the image of a set under a class function is
always a set; and

  * •

First-Order Comprehension, asserting that classes can be defined using
comprehension for first-order formulae. More precisely, this axiom schema has
as instances the universal closure of

$\exists X\ X=\\{y:\varphi(y,\bar{P})\\}$

for each first-order formula $\varphi$.

If we add to $\mathsf{GB}$ Full Comprehension, viz. the instances of
Comprehension for any formula in the language of class theory, we get
_Kelley–Morse_ class theory $\mathsf{KM}$. For finite $k\geq 1$, adding
$\Sigma^{1}_{k}$-Comprehension—Comprehension for $\Sigma^{1}_{k}$
formulae—gives the theory we will call $\mathsf{KM}_{k}$.

For some purposes $\mathsf{KM}$ is insufficient, and needs to be extended by a
version of Collection for classes.999For example, $\mathsf{KM}$ does not
suffice to prove a class version of Fodor’s lemma [GHK21], but adding Class
Collection enables the proof of class Fodor’s lemma. It will be convenient in
this paper to work with this stronger variant (but not stronger in consistency
strength). Using a stronger version will not harm our results since tightness
is preserved by extension in the same language.

A _hyperclass_ is a collection of classes. Formally these do not exist in our
models similar to how classes formally do not exist as objects in
$\mathsf{ZFC}$. However, some hyperclasses we can code with an individual
class.

######  Definition 2.0.2.

A _code_ for a hyperclass is a class of ordered pairs. We say that a
hyperclass $\mathcal{A}$ is coded if there is a code $A$ so that

$\mathcal{A}=\big{\\{}(A)_{i}:i\in\mathrm{V}\big{\\}},$

where $(A)_{i}=\\{x:(i,x)\in A\\}$ is the _$i$ -th slice_ of $A$.

######  Definition 2.0.3.

The _Class Collection_ ($\mathsf{CC}$) axiom schema asserts that if for each
set there is a class satisfying some property, then we can collect witnesses
classes into a single coded hyperclass.101010In the context of second-order
arithmetic, the analogous axiom schema is referred to as $\mathsf{AC}$; cf.
Definition 5.0.2. Formally, instances of this schema are the universal closure
of

$\forall x\exists Y\ \varphi(x,Y,\bar{P})\Rightarrow\exists B\ \forall
x\exists i\ \varphi(x,(B)_{i},\bar{P}),$

where $\varphi$ ranges across all formulae in the language of class theory. If
we restrict this schema to $\Sigma^{1}_{k}$ formulae we get _$\Sigma^{1}_{k}$
-Class Collection_ ($\Sigma_{k}^{1}\text{-}\mathsf{CC}$).

Marek and Mostowski [MM75, Theorem 2.5] showed that given any model of
$\mathsf{KM}$ you can thin down the classes to get a model of
$\mathsf{KMCC}=\mathsf{KM}+\mathsf{CC}$ with the same sets. Ratajczyk [Rat79]
built on their work to show that given any model of $\mathsf{KM}_{k}$ you can
thin down the classes to get a model of
$\mathsf{KMCC}_{k}=\mathsf{KM}_{k}+\Sigma_{k}^{1}\text{-}\mathsf{CC}$ with the
same sets, where $k>0$.

Just as Collection yields that every formula in the language of set theory is
equivalent to one in the Lévy hierarchy, $\mathsf{CC}$ yields that every
formula in the language of class theory is equivalent to a $\Sigma^{1}_{k}$
formula for some $k$. So the theories $\mathsf{KMCC}_{k}$ give a hierarchy of
stronger and stronger theories which in the union give the full theory
$\mathsf{KMCC}$.

###  2.1. Bi-interpretability with first-order set theory

For some of our results it will be convenient to work with first-order set
theories rather than class theories. The construction behind the more
difficult direction of these bi-interpretations goes back to Scott [Sco60].
The key observation is that the Foundation axiom implies that every set $x$ is
determined by the isomorphism type of $(\operatorname{TC}(\\{x\\}),\in)$. As
such, sets can be represented with isomorphism classes of well-founded,
extensional directed graphs with a maximum element. In this way a model of
$\mathsf{GB}$ can represent sets of rank $\mathord{>}\mathrm{Ord}$. To have a
name, call this construction the _unrolling construction_ and refer to the
model of first-order set theory obtained as the _unrolled model_.

######  Theorem 2.1.1 ([MM75]).

$\mathsf{KMCC}$ and $\mathsf{ZFC}^{-}$ plus “there is a largest cardinal, and
it is inaccessible” are bi-interpretable.111111See [AF17] for a modern
treatment of this result.

Denote this latter theory by $\mathsf{ZFC}^{-}_{\mathrm{I}}$. Working in
$\mathsf{ZFC}^{-}_{\mathrm{I}}$ let $\kappa$ denote the largest cardinal. For
these bi-interpretability results, $\mathrm{V}$ of the model of class theory
is isomorphic to $\mathrm{V}_{\kappa}$ of the unrolled model of
$\mathsf{ZFC}^{-}_{\mathrm{I}}$. That is, the sets are fixed and the bi-
interpretation is entirely about what happens in the classes.

Doing the construction more carefully you can get versions of this result for
restricted amounts of Comprehension. Here, let
$\mathsf{ZFC}^{-}_{\mathrm{I},k}$ denote the theory obtained from
$\mathsf{ZFC}^{-}_{\mathrm{I}}$ by restricting the Collection and Separation
schemata to $\Sigma_{k}$ formulae.

######  Theorem 2.1.2 ([Rat79]).

The following pair of theories are bi-interpretable, for $k\geq 1$.

  * •

$\mathsf{KMCC}_{k}$ and $\mathsf{ZFC}^{-}_{\mathrm{I},k}$.

The reader who desires to read through the construction in detail is referred
to the second author’s dissertation [Wil18].

The main utility of these bi-interpretation results is that they allow us to
use known facts about models of first-order set theory to draw conclusions
about models of class theory. Additionally, some arguments become easier to
formulate in that context, since we have access to von Neumann ordinals, the
Mostowski collapse theorem, and so on, whereas with classes we don’t have
direct access to these powerful tools.

###  2.2. Class forcing

We will use class forcing over models of $\mathsf{KMCC}_{k}$. Because the
theory of this is less well-known than over models of $\mathsf{KM}$ or
$\mathsf{GB}$, we recall the important facts here. Let’s begin by addressing
nonstandard models.

With a transitive model of set theory, given a generic $G$ you can interpret
all $\mathbb{P}$-names via an induction external to the model. If a model of
set theory is ill-founded, we cannot do that. Instead we need an approach
similar to the Boolean ultrapower approach. The atomic forcing relations
$p\Vdash\sigma=\tau$ and $p\Vdash\sigma\in\tau$ yield the equivalence relation
$=_{G}$ defined as $\sigma=_{G}\tau$ if and only if $p\Vdash\sigma=\tau$ for
some $p\in G$ and a similarly defined congruence $\in_{G}$ modulo $=_{G}$.
Quotienting the $\mathbb{P}$-names by $=_{G}$ and using $\in_{G}$ as the
membership relation gives the forcing extension. Identifying the ground model
with the collection of $\check{x}/\mathord{=_{G}}$ for check names
$\check{x}$, we get the forcing extension as a genuine extension. It is
straightforward to check that in case you start with a transitive model, this
produces a model isomorphic to the one obtained by the external induction. The
usual lemmata about forcing can be proved in this context.121212For a recent
exposition of these details, with a focus on how it makes sense for ill-
founded models, we recommend [Git+20].

######  Theorem 2.2.1 (Stanley, S.D. Friedman [Sta84, Fri00]).

$\mathsf{GB}$ proves that pretame class forcings satisfy the forcing theorem
for first-order formulae, viz. that the relations
$p\Vdash\varphi(\sigma,\ldots)$ are classes for each first-order formula
$\varphi$.

######  Corollary 2.2.2.

Forcing with a tame class forcing preserves all axioms of $\mathsf{GB}$ or
$\mathsf{KM}$.

We elide the technicalities of tameness and pretameness, and point the reader
to [Fri00] or [AG]. What is needed for our purposes is that
$\mathrm{Add}(\mathrm{Ord},1)$, the forcing to add a Cohen-generic class of
ordinals, is tame.

######  Theorem 2.2.3.

Let $k\geq 1$. Forcing with a tame class forcing preserves all axioms of
$\mathsf{KMCC}_{k}$.

###### Proof Sketch.

One way to prove this goes through the bi-interpretability with first-order
set theory. Knowing that set forcing preserves $\mathsf{ZFC}^{-}_{k}$, with a
little work one concludes tame class forcing preserves $\mathsf{KMCC}_{k}$.

Alternatively, one can prove this directly within class theory. To prove
$\Sigma^{1}_{k}$-Comprehension and Class Collection, first you need to prove
that the forcing relations for $\Sigma^{1}_{k}$-formulae are classes. Note
that this uses $\Sigma_{k}^{1}\text{-}\mathsf{CC}$ to be able to pull the set
quantifiers expressing “densely many conditions force such and such” inside
class quantifiers, so you get a $\Sigma^{1}_{k}$-definition for the forcing
relations. (Compare to, in the $\mathsf{ZF}$ context, how replacement is used
to pull bounded quantifiers inside to get that the forcing relation for a
$\Sigma_{k}$ formula is $\Sigma_{k}$.) Once you know these forcing relations
are classes, you then prove the preservation of the axioms in the usual way. ∎

######  Definition 2.2.4.

Suppose $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are two models of class theory
with the same sets $M$. Say that $(M,\mathcal{Y})$ is a _width-extension_ of
$(M,\mathcal{X})$ if $\mathcal{X}\subseteq\mathcal{Y}$ and for every well-
order $\Gamma\in\mathcal{Y}$ there is $\Gamma^{\prime}\in\mathcal{X}$ so that
$(M,\mathcal{Y})$ has an isomorphism $\Gamma\cong\Gamma^{\prime}$.

This notion is a class theoretic cousin of the familiar notion in first-order
set theory of an extension which does not contain any new ordinals. As in the
$\mathsf{ZF}$ context, forcing gives a width-extension (assuming strong enough
axioms in the ground model).

######  Theorem 2.2.5.

Let $k\geq 1$. Forcing over a model of $\mathsf{KMCC}_{k}$ with a pretame
forcing produces a width extension.

###### Proof.

Hamkins and Woodin [HW18] proved that pretame forcing over a model of Open
Class Determinancy cannot add new ordertypes for well-orders. Since
$\Sigma^{1}_{1}$-Comprehension is enough to prove determinancy for open class
games [GH17], this gives the result.

Alternatively, one can prove this via the bi-interpretability with first-order
set theory, using that forcing over a model of $\mathsf{ZFC}^{-}_{1}$ cannot
add new ordinals. ∎

As an aside, we remark that it is open whether $\mathsf{KMCC}_{1}$ is
necessary for this result.

######  Question 2.2.6.

Does $\mathsf{GB}$ prove that every pretame forcing extension is a width
extension?

##  3\. Semantic non-tightness in class theory

In this section we show that certain fragments of $\mathsf{KM}$ fail to be
semantically tight. All models considered will have the same sets. Namely,
they will be $\mathrm{V}_{\kappa}$ for a fixed inaccessible cardinal $\kappa$,
and we will assume that $\mathrm{V}_{\kappa}\models\mathrm{V}=\mathrm{HOD}$.
(It is easy to arrange such by forcing, if necessary. Alternatively, this can
be obtained by restricting down to an inner model.)

It is well known that satisfying $\mathrm{V}=\mathrm{HOD}$ is equivalent to
having a definable (without parameters) global well-order. We will use the
slightly stronger fact that there is a uniform definition which works for any
model of $\mathrm{V}=\mathrm{HOD}$. Namely, $\mathrm{V}=\mathrm{HOD}$ asserts
that every set is definable in some $\mathrm{V}_{\beta}$ using some ordinal
parameter $\alpha$. So if we order the sets $x$ by the least $\beta$, then the
least formula $\varphi(v_{1},v_{2})$, then the least parameter $\alpha$ so
that $x$ is defined by $\varphi$ in $\mathrm{V}_{\beta}$ using parameter
$\alpha$, this gives a global well-order of the universe in ordertype
$\mathrm{Ord}$. We will call this the _$\mathrm{HOD}$ -order_, refer to
_$\mathrm{HOD}$ -least_ choices, and so on.

###  3.1. Semantic non-tightness of $\mathsf{GB}$

The strategy for establishing the semantic non-tightness of $\mathsf{GB}$ is
this. Using $\mathrm{V}_{\kappa}$ as the sets there is a minimum model of
$\mathsf{GB}$, namely
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$ where we
append the first-order definable subsets of $\mathrm{V}_{\kappa}$ to be the
classes. By Tarski’s theorem on the undefinability of truth, being in
$\operatorname{Def}(\mathrm{V}_{\kappa})$ cannot be first-order definable over
$\mathrm{V}_{\kappa}$. But it is second-order definable and indeed absolutely
so. Moreover, we will produce a carefully defined $\mathrm{C}\subseteq\kappa$
which is also absolutely second-order definable over $\mathrm{V}_{\kappa}$.
Our two bi-interpretable models of $\mathsf{GB}$ will then be
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$ and
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C}))$
where $\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$ denotes the
hyperclass of subsets of $\mathrm{V}_{\kappa}$ definable using $\mathrm{C}$ as
a parameter.

######  Observation 3.1.1.

The satisfaction predicate $\mathrm{T}$ for $\mathrm{V}_{\kappa}$ is both
$\Sigma^{1}_{1}$ and $\Pi^{1}_{1}$ definable over $\mathrm{V}_{\kappa}$. If
$\mathcal{X}\subseteq\mathcal{P}(\mathrm{V}_{\kappa})$ is any possible
collection of classes which give a model of $\mathsf{GB}$ then $\mathcal{X}$
will correctly define $\mathrm{T}$.

The content of this observation can be traced back to Mostowski [Mos51].

###### Proof.

To define $\mathrm{T}$ in a $\Sigma^{1}_{1}$ way, we observe that it is the
union of the $\Sigma_{k}$-satisfaction predicates, and these all agree on
their common domains. While the first-order definitions of these are
progressively more complex as $k$ increases, whether a class is a
$\Sigma_{k}$-satisfaction class is uniformly recognizable in $k$. Namely, $S$
is the $\Sigma_{k}$-satisfaction class if it satisfies the Tarskian recursion
on its domain and it judges the truth of all and only the $\Sigma_{k}$
formulae. To define $\mathrm{T}$ in a $\Pi^{1}_{1}$ way,
$\varphi[\vec{a}]\in\mathrm{T}$ iff for any class $S$ if $S$ is a
$\Sigma_{k}$-satisfaction class and $\varphi[\vec{a}]$ is in its domain, then
$S$ judges $\varphi[\vec{a}]$ to be true.

Observe that $\mathsf{GB}$ suffices to prove the $\Sigma_{k}$-satisfaction
classes exist. So these definitions work for any model of $\mathsf{GB}$ with
$\mathrm{V}_{\kappa}$ as its sets. (Here we use that we are working over a
transitive model and so there are only standard $k$ to worry about.) ∎

While $\operatorname{Def}(\mathrm{V}_{\kappa})$ is a hyperclass and thus
cannot be a class in any model of class theory with $\mathrm{V}_{\kappa}$ as
its sets, it can be coded by a single class.

######  Observation 3.1.2.

After a minor reshuffling of coordinates, $\mathrm{T}$ is a code for
$\operatorname{Def}(\mathrm{V}_{\kappa})$.

###### Proof.

A class $X$ is definable if and only if
$X=\\{x:\varphi[x,\vec{a}]\in\mathrm{T}\\}$ for some formula $\varphi$ with
parameters $\vec{a}$. So by reshuffling coordinates in $\mathrm{T}$ to consist
of ordered pairs $((\varphi,\vec{a}),x)$ we get a code for
$\operatorname{Def}(\mathrm{V}_{\kappa})$. ∎

We will slightly abuse notation and use $\mathrm{T}$ to refer both to the
satisfaction class and to this code for
$\operatorname{Def}(\mathrm{V}_{\kappa})$. We will write $(\mathrm{T})_{\xi}$
to refer to the slice of $\mathrm{T}$ corresponding to the $\xi$-th pair
$(\varphi,\vec{a})$ in the $\mathrm{HOD}$-order.

If $\mathrm{C}$ is a second-order definable generic for a forcing
$\mathbb{P}\in\operatorname{Def}(\mathrm{V}_{\kappa})$ then similar results
hold for $\mathrm{T}(\mathrm{C})$, the satisfaction class relative to
$\mathrm{C}$ as a parameter, and
$\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$, the hyperclass of
classes definable using $\mathrm{C}$ as a parameter.

######  Lemma 3.1.3.

Suppose $\mathrm{C}$ is a generic over
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$ for a forcing
$\mathbb{P}\in\operatorname{Def}(\mathrm{V}_{\kappa})$, and $\mathrm{C}$ is
second-order definable. Then, $\mathrm{T}(\mathrm{C})$ is definable, indeed
definable in a uniform manner across all
$(\mathrm{V}_{\kappa},\mathcal{X})\models\mathsf{GB}$ which define
$\mathrm{C}$ the same. Moreover, after a minor reshuffling of coordinates
$\mathrm{T}(\mathrm{C})$ is a code for
$\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$.

###### Proof.

The reason this isn’t completely trivial is that partial satisfaction classes
relative to $\mathrm{C}$ will not be (first-order) definable unless
$\mathbb{P}$ is trivial, and so we cannot just relativize the definition of
$\mathrm{T}$. Instead, we use the forcing theorem:
$\varphi[\vec{a}]\in\mathrm{T}(\mathrm{C})$ if and only if there is
$p\in\mathrm{C}$ so that
“$p\Vdash\varphi(\vec{a},\check{C})\text{''}\in\mathrm{T}$. By the assumption
that $\mathrm{C}$ is second-order definable we can express “there is
$p\in\mathrm{C}$ so that…”. This definition works across any
$(\mathrm{V}_{\kappa},\mathcal{X})\models\mathsf{GB}$ which defines
$\mathrm{C}$ the same because $\mathrm{T}$ is absolute. Finally, the same
argument as with $\mathrm{T}$ gives a code for the hyperclass
$\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$. ∎

In particular, this lemma implies that “every class is definable from
$\mathrm{C}$” is a second-order definable property. We will write
$\mathrm{Class}=\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$ as an
abbreviation for the second-order formula asserting this.

It remains to determine how to give an absolute definition for a generic
$\mathrm{C}$. In brief, we will define $\mathrm{C}$ to be a carefully chosen
Cohen generic subclass of $\kappa$, using the $\mathrm{HOD}$-order to ensure
canonicity of any choices.

######  Lemma 3.1.4.

There is a second-order definition for $\mathrm{C}\subseteq\kappa$ which is
Cohen-generic over
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$ so that any
$\mathsf{GB}$ model over $\mathrm{V}_{\kappa}$ defines $\mathrm{C}$ the same.
Consequently, there is a second-order definition for $\mathrm{T}(\mathrm{C})$
so that all $\mathsf{GB}$ models over $\mathrm{V}_{\kappa}$ define
$\mathrm{T}(\mathrm{C})$ the same.

The idea behind this lemma is originally due to Feferman [Fef65], who did the
same construction in the context of arithmetic. See [Odi83, Odi83a, Odi83b]
for an exposition of Feferman’s work.

###### Proof.

Recall that the forcing $\mathrm{Add}(\kappa,1)$ is $\mathord{<}\kappa$-closed
and is first-order definable over $\mathrm{V}_{\kappa}$. There are $\kappa$
many dense subsets of $\mathrm{Add}(\kappa,1)$ which appear in
$\operatorname{Def}(\mathrm{V}_{\kappa})$, so we can meet them one at a time,
using closure at limit stages. From $\mathrm{T}$ define a sequence
$\vec{D}={\left\langle D_{\xi}:\xi\in\kappa\right\rangle}$ of all the dense
classes in $\operatorname{Def}(\mathrm{V}_{\kappa})$ by ordering them by the
$\mathrm{HOD}$-least pair $(\varphi,\vec{a})$ which gives a dense class. Note
that $\vec{D}$ is first-order definable from $\mathrm{T}$. Since $\mathrm{T}$
is absolutely definable this means that all models of $\mathsf{GB}$ over
$\mathrm{V}_{\kappa}$ compute $\vec{D}$ the same.

The construction is done in $\kappa$ many steps. Start with $p_{0}=\emptyset$.
Having built $p_{\xi}$ define $p_{\xi+1}$ to be the $\mathrm{HOD}$-least
condition $<p_{\xi}$ which meets $D_{\xi}$. And if $\eta$ is limit then define
$p_{\eta}=\bigcup_{\xi<\eta}p_{\xi}$. Because $\kappa$ is inaccessible we have
that $p_{\eta}\in\mathrm{V}_{\kappa}$ and thus we can continue the induction.
Finally, set $\mathrm{C}=\bigcup_{\xi\in\kappa}p_{\xi}$. Because any model of
$\mathsf{GB}$ over $\mathrm{V}_{\kappa}$ computes $\vec{D}$ the same,
inductively we can see that they all compute each $p_{\xi}$ the same, whence
they compute $\mathrm{C}$ the same. ∎

We are now in a position to exhibit that $\mathsf{GB}$ is not semantically
tight.

######  Theorem 3.1.5.

The two models $(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$
and $(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C}))$
of $\mathsf{GB}$, where $\kappa$ is inaccessible,
$\mathrm{V}_{\kappa}\models\mathrm{V}=\mathrm{HOD}$, and $\mathrm{C}$ is the
generic defined as above, are bi-interpretable.131313Indeed, as remarked by
the referee, one can alternatively establish the bi-interpretation of
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa}))$ and
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C}))$
with $(\mathrm{V}_{\kappa},\mathrm{T})$. The interpretation of
$(\mathrm{V}_{\kappa},\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C}))$ in
$(\mathrm{V}_{\kappa},\mathrm{T})$ is obtained by representing
$\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C}))$ with the
$\mathrm{HOD}$-least codes of $\mathrm{T}$ with the additional symbol for $C$;
the other direction is obtained directly by the Observation 3.1.1.

######  Corollary 3.1.6.

$\mathsf{GB}$ is not semantically tight. ∎

###### Proof of Theorem.

Let $\mathcal{X}=\operatorname{Def}(\mathrm{V}_{\kappa})$ and
$\mathcal{Y}=\operatorname{Def}(\mathrm{V}_{\kappa};\mathrm{C})$. Interpreting
$(\mathrm{V}_{\kappa},\mathcal{X})$ inside $(\mathrm{V}_{\kappa},\mathcal{Y})$
is simple. The interpretation, call it $\mathcal{I}$, is the identity on its
domain, and $\in^{\mathcal{I}}$ is simply $\in$. The domain includes all of
$\mathrm{V}_{\kappa}$ to be the sets of the interpreted model, but restricts
the classes to only include those which are first-order definable. This domain
is second-order definable because $\mathrm{T}$ is second-order definable.

The interpretation in the other direction, call it $\mathcal{J}$, takes more
care, since we need to refer to classes which are not actually in
$\mathcal{X}$. For the sets of the interpreted model we will take all of
$\\{0\\}\times\mathrm{V}_{\kappa}$ and for the classes we will take a subset
of $\\{1\\}\times\kappa$. Specifically, $(1,\xi)$ is in the domain of
$\mathcal{J}$ just in case
$(\mathrm{T}(\mathrm{C}))_{\xi}\neq(\mathrm{T}(\mathrm{C}))_{\eta}$ for all
$\eta<\xi$, where the subscripts refer to the rank of the indices in the
$\mathrm{HOD}$-order. For sets, $(0,x)\in^{\mathcal{J}}(0,y)$ if and only if
$x\in y$. For set-class membership, $(0,x)\in^{\mathcal{J}}(1,\eta)$ if and
only if $x\in(\mathrm{T}(\mathrm{C}))_{\eta}$. In effect, the interpretation
is that each class in the extension is interpreted as (the index of) the first
formula which defines it.

It is clear from the constructions that
$\mathcal{I}(\mathrm{V}_{\kappa},\mathcal{Y})=(\mathrm{V}_{\kappa},\mathcal{X})$
and
$\mathcal{J}(\mathrm{V}_{\kappa},\mathcal{X})\cong(\mathrm{V}_{\kappa},\mathcal{Y})$.
For one composition, work inside $(\mathrm{V}_{\kappa},\mathcal{X})$. It is
easy that $\mathcal{I}(\mathcal{J}(\mathrm{V}_{\kappa}))$ is isomorphic to
$\mathrm{V}_{\kappa}$—just strip off the $0$ in the first coordinate. For the
classes, to define an isomorphism
$\mathcal{X}\cong\mathcal{I}(\mathcal{J}(\mathcal{X}))$, given a class $X$
first query $\mathrm{T}(\mathrm{C})$ to find the $\mathrm{HOD}$-least formula
which defines $X$. Call the index of this formula $\xi$. Then send $X$ to
$(1,\xi)$. This isomorphism is first-order definable from
$\mathrm{T}(\mathrm{C})$, so it is second-order definable over
$(\mathrm{V}_{\kappa},\mathcal{X})$, which correctly computes it. For the
other composition, it is again easy that the sets of
$\mathcal{J}\circ\mathcal{I}$ are isomorphic to the sets in the ground model.
For the classes, again do the same trick of looking for the
$\mathrm{HOD}$-least slice of $\mathrm{T}(\mathrm{C})$ which gives $X$. ∎

###  3.2. Semantic non-tightness of $\mathsf{KM}_{k}$

Fix for the entirety of this section finite $k\geq 1$.

It will be convenient to work with the stronger theory $\mathsf{KMCC}_{k}$.
This gives a slight improvement to the conclusion that $\mathsf{KM}_{k}$ is
not semantically tight, so that is no cost to pay. To show that
$\mathsf{KMCC}_{k}$ is semantically non-tight we will follow the same strategy
as in the previous subsection. One model of $\mathsf{KMCC}_{k}$ will be the
minimum model of $\mathsf{KMCC}_{k}$ over $\kappa$ and the other will be an
extension of the minimum model by a canonically chosen Cohen generic.

Fix finite $k\geq 1$. Let $\alpha>\kappa$ be the smallest ordinal so that
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ satisfies $\Sigma_{k}$-Collection
and $\Sigma_{k}$-Separation. By the assumption that
$\mathrm{V}_{\kappa}\models\mathrm{V}=\mathrm{HOD}$, we have a definable
global well-order in $\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$, call it the
_$\mathrm{L}(\mathrm{V}_{\kappa})$ -order_. Set $\mathcal{M}$ to consist of
all subsets of $\mathrm{V}_{\kappa}$ which appear as elements of
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$. This
$(\mathrm{V}_{\kappa},\mathcal{M})$ will be our minimum model of
$\mathsf{KMCC}_{k}$.

######  Lemma 3.2.1.

The minimum model $(\mathrm{V}_{\kappa},\mathcal{M})\models\mathsf{KMCC}_{k}$.

###### Proof.

It is immediate that the model satisfies Class Extensionality and Class
Replacement. Consider a $\Sigma^{1}_{k}$-formula $\varphi(x)$, possibly with
parameters from $\mathcal{M}$. Inside
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$, the set
$\\{x\in\mathrm{V}_{\kappa}:\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})\models\varphi(x)^{\mathcal{M}}\\}$
exists by $\Sigma_{k}$-Separation. But then this set is in $\mathcal{M}$,
establishing the instance of Comprehension for $\varphi$. Now consider a
$\Sigma^{1}_{k}$-formula $\varphi(x,Y)$, possibly with parameters from
$\mathcal{M}$, and assume that for each $x\in\mathrm{V}$ there is
$Y\in\mathcal{M}$ so that
$(\mathrm{V}_{\kappa},\mathcal{M})\models\varphi(x,Y)$. By
$\Sigma_{k}$-Collection in $\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ we find
therein a set $b\subseteq\mathcal{P}(\mathrm{V}_{\kappa})$ so that for each
$x\in\mathrm{V}_{\kappa}$ there is $Y\in b$ so that
$\varphi(x,Y)^{\mathcal{M}}$. Because
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ has an injection $f:b\to\kappa$ we
can build the set $B=\\{(f(Y),y):y\in Y\in b\\}$, which is in $\mathcal{M}$.
This $B$ witnesses the instance of Class Collection for $\varphi$, completing
the proof. ∎

While this is not necessary to produce non-isomorphic but bi-interpretable
models of $\mathsf{KMCC}_{k}$, we remark as an aside that this $\mathcal{M}$
really does give a minimum model.

######  Theorem 3.2.2 (Ratajcyk).

If $(\mathrm{V}_{\kappa},\mathcal{X})\models\mathsf{KM}_{k}$ then
$\mathcal{M}\subseteq\mathcal{X}$.

###### Proof.

By work of Ratajcyk [Rat79], every model of $\mathsf{KM}_{k}$ contains a
submodel with the same sets which satisfies $\mathsf{KMCC}_{k}$. So we may
assume that $(\mathrm{V}_{\kappa},\mathcal{X})\models\mathsf{KMCC}_{k}$. Let
$M\models\mathsf{ZFC}^{-}_{\mathrm{I},k}$ be the unrolled model, obtained as
discussed in Subsection 2.1. Because $\kappa$ has uncountable cofinality,
$(\mathrm{V}_{\kappa},\mathcal{X})$ is correct about which of its classes are
well-founded. Thus, $M$ is well-founded, and we assume without loss that $M$
is transitive. By the leastness of $\alpha$, we have
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})\subseteq M$ and thus
$\mathcal{M}\subseteq\mathcal{X}$. ∎

Next we need to see that we can define a code for $\mathcal{M}$ in such a way
that different models of $\mathsf{KMCC}_{k}$ over $\mathrm{V}_{\kappa}$ will
define the same code. First, let us work with
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$. We begin by highlighting an easy
but useful fact.

######  Lemma 3.2.3.

Over $\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ there is a definable
increasing cofinal map $\alpha\to\kappa$. Consequently, any outer model of
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ can define this map, with the same
definition working uniformly across all outer models.

###### Proof Sketch.

The argument combines two facts. First, because
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ doesn’t satisfy
$\Sigma_{k+1}$-Replacement, there is a definable cofinal map from some
$\xi<\alpha$ to $\alpha$. Second, because
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ satisfies that every set injects
into $\kappa$ we may take $\xi=\kappa$. And it’s easy to get the map to be
increasing. ∎

Once we have an increasing cofinal map $f:\kappa\to\alpha$ it is
straightforward to define a bijection
$\kappa\to\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$. For each $f(i)$ pick the
$\mathrm{L}(\mathrm{V}_{\kappa})$-least bijection
$b_{i}:\kappa\to\mathrm{L}_{f(i)}$. Combining these together we get a map
$\kappa\times\kappa\to\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$, and via a
pairing function we may take the domain to be $\kappa$. To get a bijection we
need to ensure everything in the codomain is hit only once, but this is easily
done by only picking the least index. Writing down an explicit definition is
tedious, but it is clear that this produces a definable map. One can think of
this bijection as giving us uniform access to all of
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$.

But we want to work over $(\mathrm{V}_{\kappa},\mathcal{M})$ to get a uniform
access to all of $\mathcal{M}$, which requires some small adjustments.

######  Corollary 3.2.4.

Over $(\mathrm{V}_{\kappa},\mathcal{M})$ we can define, via a second-order
formula, a code $\mathrm{T}_{\mathcal{M}}$ for $\mathcal{M}$. Moreover, we can
do this in such a way that any
$(\mathrm{V}_{\kappa},\mathcal{Y})\models\mathsf{KMCC}_{k}$ which is a width-
extension of $\mathcal{M}$ will define the same code
$\mathrm{T}_{\mathcal{M}}$.

###### Proof.

Let $f:\kappa\to\alpha$ denote the definable, cofinal map defined above. The
point is, we can mimic the definition of $f$ inside
$(\mathrm{V}_{\kappa},\mathcal{M})$. In some detail: There is an isomorphic
copy of
$(\operatorname{TC}(\\{x\\}),\mathord{\in}\upharpoonright\operatorname{TC}(\\{x\\}))$
in $\mathcal{M}$ for each $x\in\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$.
More, by Mostowski’s collapse lemma any extensional, well-founded relation
with a maximum element in $\mathcal{M}$ is isomorphic to the restriction of
$\in$ to $\operatorname{TC}(\\{x\\})$ for some
$x\in\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$.141414Note that Mostowski’s
lemma is provable in $\mathsf{KP}+\Sigma_{1}$-Separation, so it holds in
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$. In sum,
$(\mathrm{V}_{\kappa},\mathcal{M})$ can mimic quantification over
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ by quantifying over extensional,
well-founded relations with a maximum element, and thus
$(\mathrm{V}_{\kappa},\mathcal{M})$ can mimic the definition of $f$.

We then define a code
$\mathrm{T}_{\mathcal{M}}\subseteq\kappa\times\kappa\times\mathrm{V}_{\kappa}$
for $\mathcal{M}$ by putting $(i,j,x)$ in $\mathrm{T}_{\mathcal{M}}$ if $x$ is
in the $j$-th element of $\mathrm{L}_{f(i)}(\mathrm{V}_{\kappa})$ according to
the $\mathrm{L}(\mathrm{V}_{\kappa})$-least enumeration of
$\mathrm{L}_{f(i)}(\mathrm{V}_{\kappa})$. And this definition is absolute to
width-extensions because width-extensions will define
$\mathrm{L}(\mathrm{V}_{\kappa})$ the same and so define $F$ the same. ∎

Note that this definition for the code $\mathrm{T}_{\mathcal{M}}$ is not
$\Sigma^{1}_{k}$ because the definition of $f$ is logically too complex. Of
course we cannot hope to find a $\Sigma^{1}_{k}$ definition. For if
$\mathrm{T}_{\mathcal{M}}$ were $\Sigma^{1}_{k}$ definable then it would be an
element of $\mathcal{M}$ by $\Sigma^{1}_{k}$-Comprehension, but then
$\mathrm{T}_{\mathcal{M}}$ would be an element of
$\mathrm{L}_{\xi}(\mathrm{V}_{\kappa})$ for some $\xi<\alpha$ and so all of
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa})$ would occur by stage $\xi$. That
would be absurd.

Similar machinery works for relative constructibility. Given a class
$\mathrm{C}$ over $\mathrm{V}_{\kappa}$, let $\mathcal{M}(\mathrm{C})$ denote
the subsets of $\mathrm{V}_{\kappa}$ which appear in
$\mathrm{L}_{\alpha}(\mathrm{V}_{\kappa},\mathrm{C})$. As in the $\mathsf{GB}$
case, if $\mathrm{C}$ is a generic for a forcing in $\mathcal{M}$ then we can
define a canonical choice of a code $\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ for
$\mathcal{M}(\mathrm{C})$.

######  Lemma 3.2.5.

Suppose $\mathrm{C}\subseteq\mathrm{V}_{\kappa}$ is generic over
$(\mathrm{V}_{\kappa},\mathcal{M})$ for a the forcing $\mathrm{Add}(\kappa,1)$
and $\mathrm{C}$ is uniformly second-order definable in every model of
$\mathsf{KMCC}_{k}$ which width-extends $\mathcal{M}$. Then we can define, via
a second-order formula, a code $\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ for
$\mathcal{M}(\mathrm{C})$in such a way that any model of $\mathsf{KMCC}_{k}$
which width-extends $\mathcal{M}$ will define
$\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ the same.

###### Proof Sketch.

Again we use a definable cofinal map $f:\kappa\to\alpha$ to define
$\mathrm{T}_{\mathcal{M}}(\mathrm{C})$. The difference is, rather than ask
about elements of levels of $\mathrm{L}(\mathrm{V}_{\kappa})$ we ask about
what conditions in $\mathrm{C}$ force. Here’s one way you could implement
this. Put $(i,j,x)$ in $\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ if there is a
condition $p\in\mathrm{C}$ which forces that $x$ is an element of the $j$-th
element of $\mathrm{L}_{f(i)}(\mathrm{V}_{\kappa},\mathrm{C})$ according to
the $\mathrm{L}(\mathrm{V}_{\kappa},\mathrm{C})$-least enumeration. Again the
forcing lemma lets us do this definition inside $\mathcal{M}$. This definition
is uniform across width-extensions because they have the same class well-
orders and thus compute $\mathrm{L}(\mathrm{V}_{\kappa})$ the same. ∎

It remains to give the definition for $\mathrm{C}$. We use the same strategy
as before to get a definition absolute for width-extensions of
$(\mathrm{V}_{\kappa},\mathcal{M})$. From the code $\mathrm{T}_{\mathcal{M}}$
we canonically extract a $\kappa$-sequence of dense subclasses of
$\mathrm{Add}(\kappa,1)$ in $\mathcal{M}$ and meet them one at a time. We use
the $\mathrm{HOD}$-order in $\mathrm{V}_{\kappa}$ to ensure a canonical choice
at each step.

######  Lemma 3.2.6.

There is a second-order definition for $\mathrm{C}\subseteq\kappa$ which is
Cohen-generic over $(\mathrm{V}_{\kappa},\mathcal{M})$ so that any model of
$\mathsf{KMCC}_{k}$ which width-extends $(\mathrm{V}_{\kappa},\mathcal{M})$
defines $\mathrm{C}$ the same. Consequently, there is a second-order
definition for $\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ so that all width
extensions of $(\mathrm{V}_{\kappa},\mathcal{M})$ which satisfy
$\mathsf{KMCC}_{k}$ will define $\mathrm{T}(\mathrm{C})$ the same. ∎

Recall Theorem 2.2.3 that tame class forcing, such as adding a Cohen-generic
class of ordinals, preserves $\mathsf{KMCC}_{k}$. Also recall Theorem 2.2.5
that tame class forcing produces width-extensions. So
$(\mathrm{V}_{\kappa},\mathcal{M}[\mathrm{C}])$ is among the width-extensions
of $(\mathrm{V}_{\kappa},\mathcal{M})$ subject to the conclusion of the lemma.

We are now in a position to exhibit that $\Sigma_{k}^{1}\text{-}\mathsf{CA}$
is not semantically tight. This is analogous to the $\mathsf{GB}$ proof, so we
omit most the details.

######  Theorem 3.2.7.

Let $k\geq 1$, let $\kappa$ be inaccessible, and let $\mathcal{M}$ and
$\mathrm{C}$ be defined as above, where we assume
$\mathrm{V}_{\kappa}\models\mathrm{V}=\mathrm{HOD}$. The two models
$(\mathrm{V}_{\kappa},\mathcal{M})$ and
$(\mathrm{V}_{\kappa},\mathcal{M}(\mathrm{C}))$ of $\mathsf{KMCC}_{k}$ are bi-
interpretable.

######  Corollary 3.2.8.

$\mathsf{KM}_{k}$ and $\mathsf{KMCC}_{k}$ are not semantically tight. ∎

###### Proof Sketch of Theorem.

Interpreting $(\mathrm{V}_{\kappa},\mathcal{M})$ inside the larger model
$(\mathrm{V}_{\kappa},\mathcal{M}[\mathrm{C}])$ is easy, because $\mathcal{M}$
is a definable hyperclass in the larger model. For the other direction, use
the code $\mathrm{T}_{\mathcal{M}}[\mathrm{C}]$, which is second-order
definable over $(\mathrm{V}_{\kappa},\mathcal{M})$ to give an interpretation,
as in the similar direction in the proof of Theorem 3.1.5, interpreting
classes in the larger model by the ($\mathrm{HOD}$-least) index of their slice
in $\mathrm{T}_{\mathcal{M}}$.

As remarked after the lemmata, $(\mathrm{V}_{\kappa},\mathcal{M}[\mathrm{C}])$
and $(\mathrm{V}_{\kappa},\mathcal{M}[\mathrm{C}])$ compute
$\mathrm{T}_{\mathcal{M}}$ and $\mathrm{T}_{\mathcal{M}}[\mathrm{C}]$ the
same. This ensures that composing one interpretation with the other gives back
(an isomorphic copy of) the model we started out with. ∎

##  4\. Non-tightness in class theory

To obtain the nontightness of the class theories we consider we need a uniform
construction, one which applies to any model of a fixed first-order theory. We
will strengthen the theories we used to ensure an appropriately modified
version of the construction from Section 3 goes through in a more general
setting. Two key facts about $\mathrm{V}_{\kappa}$ we used were its well-
foundedness, ensuring uniqueness of certain constructions, and the regularity
of $\kappa$, ensuring that when we constructed a Cohen generic in $\kappa$
many steps that the partial constructions were sets in $\mathrm{V}_{\kappa}$.
For our purposes we can replace these non-first-order axiomatizable properties
with a strong form of the Replacement schema.

######  Definition 4.0.1.

Let $\Phi$ be a collection of formulae in the language of set or class theory.
The axiom schema of _$\Phi$ -Replacement_ consists of the instances of
Replacement for all functional $\varphi\in\Phi$, i.e. the axioms

$\forall a\ \big{(}(\forall x\in a\exists y\ \varphi(x,y))\Rightarrow(\exists
b\forall x\in a\exists y\in b\ \varphi(x,y))\big{)},$

allowing parameters, which we suppressed here. Let $\mathsf{SOR}$ denote
_Second-Order Replacement_ , namely $\Phi$-Replacement where $\Phi$ is the
collection of all second-order formulae in the language of class theory,
allowing class parameters.

It is not difficult to see that $\mathsf{SOR}$ is consistent, given mild large
cardinals. If $\kappa$ is inaccessible then
$(\mathrm{V}_{\kappa},\mathcal{X})\models\mathsf{SOR}$ for any collection
$\mathcal{X}\subseteq\mathcal{P}(\mathrm{V}_{\kappa})$ of classes over
$\mathrm{V}_{\kappa}$, by the regularity of $\kappa$.

Let’s collect some consequences of $\mathsf{SOR}$. These are proved using the
same arguments for the first-order versions of the axiom/theorem schemata.

######  Lemma 4.0.2 (Second-order separation).

Fix $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. If $x\in M$ and
$\varphi(y)$ is any second-order formula, possibly with parameters, then
$\\{y\in^{M}x:(M,\mathcal{X})\models\varphi(y)\\}$ is an element of
$M$.151515There is a small abuse of notation here. It could be $M$ isn’t a
transitive set and $\in^{M}$ isn’t the true $\in$. In such a case it doesn’t
make sense to talk about $\\{y\in^{M}x:(M,\mathcal{X})\models\varphi(y)\\}$
being an element of $M$. What we mean is that $M$ has an element $z$ so that
$(M,\mathcal{X})\models z=\\{y\in x:\varphi(y)\\}$. We use this sort of talk
rather than more precise circumlocutions because we think it clearer to stick
close to how we talk about transitive models. ∎

######  Lemma 4.0.3 (Second-order recursion along $\mathrm{Ord}$).

Fix $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Let $G\subseteq M$ be a
second-order definable class function. Then there is a unique definable
function $F$ over $(M,\mathcal{X})$ such that
$F(\alpha)=G(F\upharpoonright\alpha)$ for every $\alpha\in\mathrm{Ord}^{M}$. ∎

######  Lemma 4.0.4 (Second-order recursion along set-like, well-founded
relations).

Fix $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Let $G\subseteq M$ be a
second-order definable class function and $R\subseteq M$ be a second-order
definable, set-like, well-founded relation.161616We of course mean that
$(M,\mathcal{X})$ thinks that $R$ is set-like and well-founded. In the sequel
we will use similar phrasing with similar intent, and trust the reader to
understand. If we wish to speak of what is seen externally to the model we
will be explicit. Then there is a unique definable function $F$ over
$(M,\mathcal{X})$ such that
$F(x)=G(F\upharpoonright\operatorname{Ext}_{R}(x))$ for every
$x\in\operatorname{dom}R$. ∎

We highlight an immediate corollary we will make repeated use of.

######  Corollary 4.0.5.

Fix $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Suppose $F\subseteq M$
is defined by second-order recursion. Then for any $x\in M$ we have that
$F(x)\in M$.

###### Proof.

Because $F(x)$ is definable by second-order Separation. ∎

######  Lemma 4.0.6 (Second-order induction).

Fix $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Let $R\subseteq M$ be a
second-order definable, set-like, well-founded relation. Suppose $X$ is a
second-order definable, inductive subset of the domain of $R$. Then
$X=\operatorname{dom}R$. ∎

An instance of this is especially relevant to our purposes.

######  Corollary 4.0.7.

Over $\mathsf{GB}$, $\mathsf{SOR}$ proves the single sentence that asserts for
every $k\in\omega$ there is a $\Sigma_{k}$ satisfaction predicate.

###### Proof.

It is easy to see that the subset of $\omega$ consisting of the $k$ for which
a $\Sigma_{k}$ satisfaction predicate exists is inductive. ∎

Just $\mathsf{GB}$ alone proves the existence of the $\Sigma_{k}$ satisfaction
predicate for every standard $k$, by an induction in the metatheory. The point
is, with $\mathsf{SOR}$ the quantification over $k$ is not in the metatheory
and we get $\Sigma_{k}$ satisfaction predicates even for nonstandard $k$. The
connoisseur of nonstandard models knows that $\omega$-nonstandard models may
fail to admit any $\Sigma_{k}$ satisfaction predicate for nonstandard
$k$.171717For the non-connoisseur: Let $M$ be an $\omega$-nonstandard model of
$\mathsf{ZF}$, and let $\mathcal{X}$ consist of its definable classes. Then
$(M,\mathcal{X})\models\mathsf{GB}$. But $\mathcal{X}$ cannot have a
$\Sigma_{k}$ satisfaction predicate for nonstandard $k$ by Tarski’s theorem on
the undefinability of truth. Second-Order Replacement rules these models out
from consideration.

As an aside, we remark that $\mathsf{GB}+\mathsf{SOR}$ exceeds $\mathsf{GB}$
in consistency strength.

######  Proposition 4.0.8.

$\mathsf{GB}+\mathsf{SOR}$ proves the consistency of $\mathsf{GB}$.

###### Proof Sketch.

Work internally to a model of $\mathsf{GB}+\mathsf{SOR}$. By second-order
Separation form the set of (parameter-free) first-order truths of the universe
of sets. By induction this truth set contains every instance of Replacement
and Separation. And it must be consistent, so we have constructed a consistent
extension of $\mathsf{ZFC}$, whence we get the consistency of $\mathsf{GB}$. ∎

On the other hand, $\mathsf{SOR}$ says very little about what classes exist.

######  Lemma 4.0.9.

Let $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Suppose
$\mathcal{Y}\subseteq\mathcal{X}$ is definable over $(M,\mathcal{X})$ by a
second-order formula, possibly using parameters. Then
$(M,\mathcal{Y})\models\mathsf{SOR}$.

###### Proof.

Consider an instance $\psi$ of $\mathsf{SOR}$. Let $\psi^{\mathcal{Y}}$ be the
relativization of $\psi$ so that class quantifiers only quantify over elements
of $\mathcal{Y}$, using that $\mathcal{Y}$ is definable. (Set quantifiers are
unchanged.) By $\mathsf{SOR}$ we get that
$(M,\mathcal{X})\models\psi^{\mathcal{Y}}$. Hence
$(M,\mathcal{Y})\models\psi$. ∎

In particular, by similar logic as to how we defined
$\operatorname{Def}(\mathrm{V}_{\kappa})$ in the previous section, we will get
that any model of $\mathsf{GB}$ can define what internally looks like the
definable classes. This gives a model of $\mathsf{GB}+\mathsf{SOR}$ with a
weak second-order theory, not even able to prove the existence of a
satisfaction predicate which measures all first-order formulae. Such a model
will fail to satisfy even $\Pi_{1}^{1}\text{-}\mathsf{CA}$.

We close this section with the fact that forcing preserves $\mathsf{SOR}$.

######  Lemma 4.0.10.

Suppose $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}$. Then, any forcing
extension of $(M,\mathcal{X})$ by a tame, $\mathord{<}\mathrm{Ord}$-closed
forcing in $\mathcal{X}$ will satisfy $\mathsf{SOR}$.

###### Proof.

Let $(M,\mathcal{X}[G])$ denote the forcing extension—the sets are the same by
$\mathord{<}\mathrm{Ord}$-closure—and suppose toward a contradiction that it
fails to satisfy $\mathsf{SOR}$. Let $\varphi(x,y)$ be an instance of
$\mathsf{SOR}$ which fails in this extension; that is, $(M,\mathcal{X}[G])$
has a set $a$ so that for all $x\in a$ there is unique $y$ so that
$\varphi(x,y)$ but there is no set containing all such $y$. This is forced by
some condition $p\in G$. By $\mathord{<}\mathrm{Ord}$-closure we may moreover
assume that $p$ decides the identity of each of these witnesses; there are
$\left\lvert a\right\rvert<\mathrm{Ord}$ many names to decide, so by closure
we have enough space to continually extend to decide each of them. And they
are decided to be equal to some check name $\check{y}$, since no sets are
added. But then $(M,\mathcal{X})$ satisfies that there is a set $a$ so that
for all $x\in a$ there is a unique set $y$ so that
$p\Vdash\varphi(\check{x},\check{y})$, with no set $b$ containing all such
$y$. This is a failure of $\mathsf{SOR}$ in the ground model, contrary to the
assumptions of the lemma. ∎

###  4.1. Non-tightness of $\mathsf{GB}$

All results in this section concern models of
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$, and the reader is warned
we will not make this assumption explicit in every single definition and
lemma. Many results do not need the full strength of this assumption, but we
leave it to the interested reader to identify the minimal assumptions for each
result.

We start this section by considering truth and definability. We take some care
to make it clear everything works in the $\omega$-nonstandard case. All
definitions that follow take place in the context of a fixed model of
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$.

######  Definition 4.1.1.

A _partial satisfaction predicate_ is a class $S$ of (first-order) formulae
$\varphi[\vec{a}]$ equipped with set parameters assigned to all free variables
so that the domain of $S$ is closed under subformulae and $S$ satisfies the
Tarskian recursion on its domain. If the domain of $S$ is all $\Sigma_{k}$
formulae, for $k\in\omega$, we call $S$ the _$\Sigma_{k}$ satisfaction
predicate_.

Our use of the definite article in that last sentence is justified by the
following observation.

######  Proposition 4.1.2.

Any two partial satisfaction classes agree on their common domain.

###### Proof.

By Elementary Comprehension form the class of locations where they disagree.
If nonempty there must be a minimal location $\varphi[\vec{a}]$ of
disagreement. But since they agree on subformulae of $\varphi[\vec{a}]$ and
they both satisfy the Tarskian recursion they must agree on the truth of
$\varphi[\vec{a}]$. ∎

######  Definition 4.1.3.

Define $\mathrm{T}$ to be the union of all partial satisfaction predicate.
Write $\mathrm{T}_{k}$ for the $\Sigma_{k}$ satisfaction predicate.

It follows from earlier remarks that $\mathsf{SOR}$ implies $\mathrm{T}$ is
the full satisfaction predicate, the unique satisfaction predicate that
measures the truth of all formulae.181818Uniqueness here is only inside the
model of $\mathsf{GB}$. From the external perspective we may see multiple
subsets of $M$ which satisfy the Tarskian recursion and measure the truth of
all formulae in $M$. But only one of these can be a class in our model.

A notion of satisfaction carries a notion of definability. Let $\mathcal{D}$
be the (second-order definable) hyperclass of all $\mathrm{T}$-definable
classes. That is, $X\in\mathcal{D}$ if and only if there is
$\varphi[x,\vec{a}]$ so that $X=\\{x:\varphi[x,\vec{a}]\in\mathrm{T}\\}$. As
in the $\mathrm{V}_{\kappa}$ case, with minor reshuffling of indexing
$\mathrm{T}$ gives a code for $\mathcal{D}$.

######  Definition 4.1.4.

We write $\mathrm{Class}=\operatorname{Def}(V)$ to denote the axiom asserting
that every class is in $\mathcal{D}$.

######  Lemma 4.1.5.

Consider a model $(M,\mathcal{X})$ of
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$. Then
$\mathcal{D}^{\mathcal{X}}\subseteq\mathcal{X}$ and
$(M,\mathcal{D}^{\mathcal{X}})\models\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$.

###### Proof.

For the first part, we note that $X$ is $\mathrm{T}$-definable if, and only
if, $X$ is $\Sigma_{k}$-definable for some $k\in\omega^{M}$. By
$\mathsf{SOR}$, for each $k$ the $\Sigma_{k}$ satisfaction predicate is in
$\mathcal{X}$. So from First-Order Comprehension we obtain $X\in\mathcal{X}$.

For the second part: Extensionality is trivially obtained and Replacement
holds because it holds in the larger $\mathcal{X}$. For First-Order
Comprehension, fix $A\in\mathcal{D}^{\mathcal{X}}$ and assume $B$ is
externally definable from $A$ via a $\Sigma_{\ell}$-formula with set
parameters, i.e. for standard $\ell$. Because $A$ is $\mathrm{T}$-definable
that means that $A$ is $\Sigma_{k}$-definable for some level $k$ in
$\omega^{M}$. But then $B$ is $\Sigma_{k+\ell}$-definable, whence $B$ is
$\mathrm{T}$-definable. Finally, that $(M,\mathcal{D}^{\mathcal{X}})$
satisfies $\mathsf{SOR}$ is Lemma 4.0.9 and that it satisfies
$\mathrm{V}=\mathrm{HOD}$ is because $\mathrm{V}=\mathrm{HOD}$ only quantifies
over sets. ∎

######  Lemma 4.1.6.

The definition of $\mathcal{D}$ is absolute between models with the same sets
and same $\mathrm{T}$. That is, if $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are
models where $\mathrm{T}^{\mathcal{X}}=\mathrm{T}^{\mathcal{Y}}$ then
$\mathcal{D}^{\mathcal{X}}=\mathcal{D}^{\mathcal{Y}}$.

###### Proof.

Just observe that the definition of $\mathcal{D}$ from the parameter
$\mathrm{T}$ only quantifies over sets. ∎

######  Lemma 4.1.7.

Moving to $\mathcal{D}$ preserves the satisfaction predicate. In symbols:
$\mathrm{T}^{\mathcal{D}}=\mathrm{T}$.

###### Proof.

Because the $\Sigma_{k}$ satisfaction predicate is $\Sigma_{k+1}$-definable. ∎

Altogether, we have that $\mathcal{D}$ thinks it is the minimum model of
$\mathsf{GB}$.

######  Corollary 4.1.8.

The $\mathcal{D}$ operator is idempotent. That is, for any
$(M,\mathcal{X})\models\mathsf{GB}$ we have that
$\mathcal{D}^{\mathcal{D}^{\mathcal{X}}}=\mathcal{D}^{\mathcal{X}}$.
Consequently, $(M,\mathcal{D}^{\mathcal{X}})$ satisfies
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}+\mathrm{Class}=\operatorname{Def}(V)$.
∎

######  Corollary 4.1.9.

If
$(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}+\mathrm{Class}=\operatorname{Def}(V)$,
then $\mathcal{X}=\mathcal{D}^{\mathcal{X}}$. ∎

These definitions and results about satisfaction/definability can be
relativized to a class parameter. If this parameter is an element of
$\mathcal{X}$ then the proofs are near identical. If the parameter is a
second-order definable Cohen generic then we need a slight change. As in the
proof of Lemma 3.1.3, the change is to ask about what is forced. We state the
relativized results only for the Cohen generic case, and omit any proofs as
they are the same modulo this small change.

######  Lemma 4.1.10.

Fix $(M,\mathcal{X})\models\mathsf{GB}$ and suppose $\mathrm{C}\subseteq M$ is
generic over $\mathcal{D}^{\mathcal{X}}$ for the forcing
$\mathrm{Add}(\mathrm{Ord},1)$. Then
$\mathrm{C}\in\mathcal{D}(\mathrm{C})^{\mathcal{X}}$ and
$(M,\mathcal{D}(\mathrm{C})^{\mathcal{X}})\models\mathsf{GB}$. Moreover, if
$\mathrm{C}$ is uniformly definable over models with the same sets and the
same $\mathrm{T}$, then the definitions of $\mathrm{T}(\mathrm{C})$ and
$\mathcal{D}(\mathrm{C})$ are absolute between these models. ∎

######  Lemma 4.1.11.

For any $(M,\mathcal{X})\models\mathsf{GB}$ and any Cohen-generic
$\mathrm{C}$, we have that
$\mathcal{D}(\mathrm{C})^{\mathcal{D}(\mathrm{C})^{\mathcal{X}}}=\mathcal{D}(\mathrm{C})^{\mathcal{X}}$.
∎

######  Corollary 4.1.12.

Fix $(M,\mathcal{X})\models\mathsf{GB}$ and fix a Cohen-generic $\mathrm{C}$.
Then
$(M,\mathcal{D}(\mathrm{C})^{\mathcal{X}})\models\mathsf{GB}+\mathrm{Class}=\operatorname{Def}(V;\mathrm{C})$.
Note that this can be expressed as a single second-order assertion, using the
parameter $\mathrm{C}$. ∎

######  Corollary 4.1.13.

If $(M,\mathcal{X})\models\mathsf{GB}+Class=\operatorname{Def}(V;\mathrm{C})$
where $\mathrm{C}$ is a Cohen-generic over $(M,\mathcal{D}^{\mathcal{X}})$,
then $\mathcal{X}=\mathcal{D}(\mathrm{C})^{\mathcal{X}}$. ∎

Now we turn our attention to the definition of the Cohen generic $\mathrm{C}$
we use in our construction.

######  Lemma 4.1.14.

Work over
$(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$. Over
this model there is second-order definable $\mathrm{C}\subseteq M$ which is
generic for $\mathrm{Add}(\mathrm{Ord},1)^{M}$ over
$(M,\mathcal{D}^{\mathcal{X}})$. Moreover, $\mathrm{C}$ and
$\mathrm{T}(\mathrm{C})$ are absolute to any
$(M,\mathcal{Y})\models\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$ for
which $\mathrm{T}^{\mathcal{Y}}=\mathrm{T}^{\mathcal{X}}$.

###### Proof.

As in Lemma 3.1.4, we define the class
$D\subset\mathrm{Ord}\times\mathrm{Add}(\mathrm{Ord},1)$ such that the slices
$(D)_{i}$ are all the $\mathrm{T}$-definable dense subclass of
$\mathrm{Add}(\mathrm{Ord},1)$. The order in $D$ is obtained from the
$\mathrm{HOD}$-order in $M$. We also use the $\mathrm{HOD}$-order to
recursively build the sequence of increasingly stronger forcing condition
${\left\langle p_{\xi}:\xi\in\mathrm{Ord}\right\rangle}$ such that
$p_{\xi}\in(D)_{\xi}$. This is where we use $\mathsf{SOR}$: This sequence is
defined by transfinite recursion using a second-order definition (because we
need a second-order definition to define $\mathrm{T}$ to thereby define $D$).
By Lemma 4.0.3 this recursion succeeds and the initial segments of the
sequences are sets in $M$.

What remains in the proof is precisely the same as in the proof of Lemma
3.1.4. We omit repeating it. ∎

A consequence of Lemma 4.0.10 is that the extension by $\mathrm{C}$ will
satisfy $\mathsf{SOR}$. To check that the lemma we just proved includes this
extension itself we simply need to check that it defines $\mathrm{T}$ the same
as its ground model. Fortunately this is easy.

######  Lemma 4.1.15.

Let $(M,\mathcal{X})\models\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}$.
Then any extension of $(M,\mathcal{X})$ by a tame forcing in $\mathcal{X}$
which does not add sets will define $\mathrm{T}$ the same as $\mathcal{X}$.

###### Proof.

Let $(M,\mathcal{X}[G])$ denote the forcing extension. It satisfies
$\mathsf{GB}$, so it thinks that $\Sigma_{k}$ satisfaction predicates are
unique. Since $\mathcal{X}[G]$ contains all of $\mathcal{X}$, it thus agrees
with $\mathcal{X}$ as to what class is the $\Sigma_{k}$ satisfaction predicate
for all $k$, even nonstandard. So they define $\mathrm{T}$ the same. ∎

Finally we are in a position to prove that $\mathsf{GB}$ is not tight.

######  Theorem 4.1.16.

Consider the following two theories.

  * •

$D$ is the theory consisting of
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}+\mathrm{Class}=\operatorname{Def}(V)$.

  * •

$U$ is the theory consisting of
$\mathsf{GB}+\mathsf{SOR}+\mathrm{V}=\mathrm{HOD}+\mathrm{Class}=\operatorname{Def}(V;\mathrm{C})$
where $\mathrm{C}$ is the Cohen generic over $\mathcal{D}$ built up according
to Lemma 4.1.14.

The theories $D$ and $U$ are bi-interpretable, via interpretations that fix
the sets of the models.

######  Corollary 4.1.17.

$\mathsf{GB}$ and $\mathsf{GB}+\mathsf{SOR}$ are not tight. ∎

###### Proof Sketch of Theorem.

We use the same interpretations $\mathcal{I}$ and $\mathcal{J}$ from Theorem
3.1.5.

First we interpret $D$ in $U$ via $\mathcal{I}$, whose domain is
$\mathcal{D}$. This is expressible beacuse $\mathcal{D}$ is a definable
hyperclass. As before, $\mathcal{I}$ is the identity on its domain and
$\in^{\mathcal{I}}$ is $\in$. The lemmata about $\mathcal{D}$ then give that
this is an interpretation of $D$ in $U$.

For the other direction let us work in an arbitrary model
$(M,\mathcal{X})\models D$. For the sets of the interpreted model we will take
all of $\\{0\\}\times M$ and for the classes we will take a subset of
$\\{1\\}\times\mathrm{Ord}.$Specifically, $(1,\xi)$ is in the domain of
$\mathcal{M}$ just in case
$(\mathrm{T}(\mathrm{C}))_{\xi}\neq(\mathrm{T}(\mathrm{C}))_{\eta}$ for all
$\eta<\xi$, where the subscripts refer to the rank of the indices in the
canonical global well-order. For sets, $(0,x)\in^{\mathcal{M}}(0,y)$ if and
only if $x\in y$. For set-class membership, $(0,x)\in^{\mathcal{M}}(1,\eta)$
if and only if $x\in(\mathrm{T}(\mathrm{C}))_{\eta}$. In effect, the
interpretation is that each class in the extension is interpreted as (the
index of) the first formula which defines it. The lemmata about $\mathrm{C}$
imply that this is an interpretation of $U$ in $D$. In particular.

That these interpretations compose to give definable bijections is the same
argument as in Theorem 3.1.5. ∎

###  4.2. Non-tightness of $\mathsf{KMCC}_{k}$

Our work here is to show that the construction in Section 3.2 can be made to
work uniformly, instead of working only over a fixed transitive model. As
before, it will be convenient to work with the unrolled model of
$\mathsf{ZFC}^{-}_{\mathrm{I},k}$ as described in Section 2.1. We will use
$\mathrm{Class}=\mathrm{L}$ to mean that every class is (second-order)
constructible. More precisely, $\mathrm{Class}=\mathrm{L}$ expresses the
translation of $\mathrm{V}=\mathrm{L}$ in the unrolled model. Note that
$\mathrm{Class}=\mathrm{L}$ implies $\mathrm{V}=\mathrm{L}$.191919Earlier we
only assumed $\mathrm{V}=\mathrm{HOD}$. We think that the results in this
section would go through in that more general context. But since we needed to
make use of some nontrivial fine structure theory for this section we found it
easier to work in this section with models where everything is constructible,
rather than work with relative constructability. This is a cost, since it
means our results as written cannot apply to models with large enough large
cardinals. We leave it to the reader who wishes to avoid this cost to check
the details for the relative constructibility context.

Before we describe our construction, let us recall the construction in the
transitive context. A transitive model of
$\mathsf{ZFC}^{-}_{\mathrm{I},k}+\mathrm{V}=\mathrm{L}$ is of the form
$\mathrm{L}_{\alpha}$ and thinks there is a largest cardinal, call it
$\kappa$, and it is inaccessible. This $\mathrm{L}_{\alpha}$ is bi-
interpetable with a model of the form
$(\mathrm{L}_{\kappa},\mathcal{M})\models\mathsf{KMCC}_{k}$. There is a least
$\alpha$ which gives such a model of $\mathsf{KMCC}_{k}$ with
$\mathrm{L}_{\kappa}$ as the sets. It can be characterized as the smallest
$\alpha>\kappa$ which satisfies $\Sigma_{k}$-Replacement.

In the transitive setting, we used that such $\alpha$ must admit some
$\Sigma_{k+1}$-definable cofinal map $\kappa\to\alpha$. But if we are to have
a uniform construction then we must have a single definition for a cofinal map
across all models, and it must be sufficiently absolute to achieve the
nontightness of $\mathsf{KMCC}_{k}$. The basic idea is, we successively close
off under taking witnesses for instances of $\Sigma_{k}$-Replacement for more
and more inputs. For this we will make use of some fine structural tools.

Briefly: Jensen—e.g. in [Jen72]—gave a precise analysis of the structure of
$\mathrm{L}$ as built up using rudimentary functions. He considers an
alternate hierarchy, the $\mathrm{J}$ hierarchy, to build up $\mathrm{L}$. But
the $\mathrm{J}$ and $\mathrm{L}$ hierarchies agree on limit levels, so the
distinction will not be relevant for our purposes. A key theorem he proves is
that levels of the $\mathrm{J}$ hierarchy have $\Sigma_{k}$ Skolem functions
for all $k$, uniformly so. Let us give a version of this appropriate to our
context.

######  Definition 4.2.1.

Consider a model $U$ of a strong enough fragment of $\mathsf{ZFC}$ and fix
finite $k$. We say that _$U$ has a $\Sigma_{k}$ Skolem function_ when there is
a $\Sigma_{k}$ definition for the function $h:\omega^{U}\times U\to U$ such
that, for every $\Sigma_{k}$ formula $\varphi$,

$U\models\exists y\
\varphi(y,x)\Rightarrow\varphi(h(\ulcorner\varphi\urcorner,x),x).$

######  Theorem 4.2.2 (Jensen’s $\Sigma_{\ell}$ uniformization theorem).

Fix $1\leq k\leq\ell$. There is a $\Sigma_{k}$ formula $\psi$ such that
$\mathsf{ZFC}^{-}_{\ell}+\mathrm{V}=\mathrm{L}$ proves that $\psi$ defines a
$\Sigma_{k}$ Skolem function. That is, if
$U\models\mathsf{ZFC}^{-}_{\ell}+\mathrm{V}=\mathrm{L}$ then the function
$h=\psi^{U}$ defined by $\psi$ in $U$ is a $\Sigma_{k}$ Skolem function for
$U$.

This is a combination of some results in [Jen72], mainly Lemma 2.9. and Lemma
3.4.(i) together with the technique of standard codes developed in Section 4.
A recent version of these can be found in the recent [Jen21] where Jensen
develops the fine structure theory in more detail, mentioning more precisely
where and how uniformization applies absolutely. Jensen presents his work in
the context of transitive models with $\mathsf{ZFC}$ as the background theory.
A careful read-through of his arguments makes clear that this background
theory is overkill. One does not need the Powerset axiom to carry out the
inductive construction, and the amount of Collection and Separation needed
does not exceed the complexity of the desired Skolem function. Rather than
multiply this paper’s length by giving a reconstruction of Jensen’s arguments
with a careful accounting of the axioms used, we point the reader to the
above-cited works. We also point to [Dod82] for an analysis of the minimal
axioms—less than even $\mathsf{KP}$—needed to carry out the basic
constructions of the rudimentary functions.

######  Lemma 4.2.3.

Fix $k\geq 1$. Work over
$\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{Class}=\mathrm{L}$ Consider the
unrolled model
$U\models\mathsf{ZFC}^{-}_{\mathrm{I},k}+\mathrm{V}=\mathrm{L}$, and let
$\kappa$ denote the largest cardinal in this model. Then there is a definition
for a sequence ${\left\langle\alpha_{i}:i\in\omega\right\rangle}$ so that
$\bigcup_{i}\mathrm{L}_{\alpha_{i}}\models\mathsf{ZFC}^{-}_{\mathrm{I},k}$,
with the same largest cardinal $\kappa$. Consequently the property “the
sequence ${\left\langle\alpha_{i}\right\rangle}$ is cofinal in the ordinals”
is expressible.

Before the proof let’s clear up a potential misunderstanding. The union
$\bigcup_{i}\mathrm{L}_{\alpha_{i}}$ refers to the direct limit of the system
of models $\mathrm{L}_{\alpha_{i}}$, each equipped with the membership
relation from the unrolled model. If we’re working over a transitive, model
then this union is itself a level of the $\mathrm{L}$ hierarchy. But in a
nonstandard model there might be a cut and the sequence $\alpha_{i}$ doesn’t
have a supremum in the model. (Indeed, that is exactly what happens when the
sequence is cofinal, which it will be in the models we are interested in.)
After all, while the sequence is definable, its definition is too complex for
the weak theory satisfied by the model to guarantee its supremum exists as an
element of the model. Nonetheless, the direct system is definable and hence
its direct limit is also definable.

###### Proof.

Consider a model
$(M,\mathcal{M})\models\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{Class}=\mathrm{L}$
and work in its unrolled model $U\models\mathsf{ZFC}^{-}_{\mathrm{I},k}$. From
Theorem 4.2.2, we have a $\Sigma_{k}$ Skolem function $h$ for $U$. Define the
$\omega$-sequence ${\left\langle\alpha_{i}\right\rangle}$ as follows: Start
with $\alpha_{0}=\kappa$ and at successors we will pick $\alpha_{i+1}$ to be
give a level of the $\mathrm{L}$ hierarchy which is closed under $h$ for
inputs from $\mathrm{L}_{\alpha_{i}}$. To this purpose, define the class
function

$W(\alpha)=\\{\xi\in\mathrm{Ord}:\xi=h(\ulcorner\varphi\urcorner,x)\text{
where }x\in\mathrm{L}_{\alpha}\textrm{ and }\varphi\text{ is }\Sigma_{k}\\}.$

The function $h$ is $\Sigma_{k}$ and being $\mathrm{L}_{\alpha}$ is a
$\Sigma_{1}$ property of $\alpha$. So in all $W$ is $\Sigma_{k}$, and so
$W(\alpha)$ is a set in $U$. Then, set

$\alpha_{i+1}=\bigcup W(\alpha_{i}).$

If $\psi(y,x)$ is $\Sigma_{k}$ then the property “$\mathrm{L}_{\xi}$ contains
$h(\ulcorner\psi\urcorner,x)$” is also $\Sigma_{k}$ in parameters $\xi$ and
$x$. So this definition really does give that $\mathrm{L}_{\alpha_{i+1}}$ is
closed under $h$ for inputs from $\mathrm{L}_{\alpha_{i}}$.

We can always continue the construction one more step, and so the set of $i$
for which $\alpha_{i}$ is defined forms an inductive subset of $\omega$. So by
$\mathsf{SOR}$ it must be all of $\omega$.

To show that
$N=\bigcup_{i}\mathrm{L}_{\alpha_{i}}\models\mathsf{ZFC}^{-}_{\mathrm{I},k}$
we first show that any $\Sigma_{k}$ formula $\theta(y,x)$ with a parameter $x$
in one of the $\mathrm{L}_{\alpha_{i}}$ reflects. To this end fix such
$\theta(y,x)$ and $x\in\mathrm{L}_{\alpha_{i}}$. Suppose that $U\models\exists
y\ \theta(y,x)$. Then $U\models\theta(h(\ulcorner\theta\urcorner,x))$. But
$h(\ulcorner\theta\urcorner,x)\in\mathrm{L}_{\alpha_{i+1}}$. By Tarski–Vaught
we get that $N$ is a $\Sigma_{k}$ elementary submodel of $U$. Now by a
standard argument we get that $N\models\Sigma_{k}$-Replacement. Namely,
suppose there is $a\in N$ so that for each $x\in a$ there’s a unique $y$ so
that $\varphi(x,y)$, where $\varphi$ is a $\Sigma_{k}$ formula, possibly with
parameters. Then there’s $i$ so that $a$ and all parameters are in
$\mathrm{L}_{\alpha_{i}}$. Using that $N$ is $\Sigma_{k}$-elementary in $U$,
we get that the witnesses $y$ must all be in $\mathrm{L}_{\alpha_{i+1}}$,
witnessing that instance of Replacement. This immediately implies that
$N\models\Sigma_{k}$-Separation and Collection, where for the second fact we
use that $N$ has a definable global well-order. That
$N\models\mathrm{V}=\mathrm{L}$ is immediate. And $N$ has the same $\kappa$ as
its largest cardinal by an inductive argument. Trivially
$\mathrm{L}_{\alpha_{0}}=\mathrm{L}_{\kappa}$ has cardinality $\kappa$. And
then inductively $\mathrm{L}_{\alpha_{i+1}}$ is a union of $\kappa$ many sets
of size $\kappa$ whence it’s also of cardinality $\kappa$. ∎

This theorem allows us a characterization of models of class theory which
think they are the minimum model of $\mathsf{KMCC}_{k}$. Namely, let
$\mathrm{Class}=\mathrm{MinMod}_{k}$ be the conjunction of
$\mathrm{Class}=\mathrm{L}$ and “in the unrolling the sequence
${\left\langle\alpha_{i}\right\rangle}$ is cofinal in the ordinals”. Moreover,
we can express whether a model is a width-extension of a model of
$\mathrm{Class}=\mathrm{MinMod}_{k}$, by expressing that the second-order
constructible classes of that model satisfy
$\mathrm{Class}=\mathrm{MinMod}_{k}$.

As in the transitive case, having a definable cofinal sequence in the ordinals
of the unrolled model allows us to define a code for the hyperclass of all
classes.

######  Lemma 4.2.4.

Fix $k\geq 1$. Let
$(M,\mathcal{M})\models\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{MinMod}_{k}$.
Then over $(M,\mathcal{M})$ there is a definition for a code
$\mathrm{T}_{\mathcal{M}}$ for $\mathcal{M}$. Moreover, this definition can be
chosen to be absolute across all width-extensions of $(M,\mathcal{M})$.

###### Proof Sketch.

As in Corollary 3.2.4, but since our cofinal sequence has length $\omega$ we
define the code to consist of triples $(i,j,x)$ where $i\in\omega$,
$j\in\mathrm{Ord}$, and $x$ is a set. To make the definition absolute across
width-extensions, relativize it to second-order $\mathrm{L}$. ∎

We can also do this for Cohen generics over a model of $\mathrm{MinMod}_{k}$,
as in Lemma 3.2.5.

######  Lemma 4.2.5.

Fix $k\geq 1$. Let
$(M,\mathcal{M})\models\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{MinMod}_{k}$ and
suppose $\mathrm{C}\subseteq M$ is a generic over $(M,\mathcal{M})$ for
$\mathrm{Add}(\mathrm{Ord},1)$ which is second-order definable over
$(M,\mathcal{M})$. Then there is a definition for a code
$\mathrm{T}_{\mathcal{M}}(\mathrm{C})$ which is absolute across all width-
extensions of $(M,\mathcal{M})$. ∎

The extension by $\mathrm{C}$ is a width-extension, so it is among those
extensions for which the definition of $\mathrm{T}_{\mathcal{M}}(\mathrm{C})$
is absolute.

Finally, we must say how to define $\mathrm{C}$. But there is no new content
here. Work in a model of $\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{MinMod}_{k}$.
Using the code $\mathrm{T}_{\mathcal{M}}$ we extract a canonical
$\mathrm{Ord}$-sequence of the dense subclasses of
$\mathrm{Add}(\mathrm{Ord},1)$ in the model. We extend to meet these
subclasses one at a time, always using the $\mathrm{L}$-order to make choices
of how to extend. Here $\mathsf{SOR}$ comes into play to ensure this
construction never takes us outside the model. So in $\mathrm{Ord}$ many steps
we produce $\mathrm{C}$. And any extension which defines
$\mathrm{T}_{\mathcal{M}}$ the same will define $\mathrm{C}$ the same.

Let $\mathrm{Class}=\mathrm{MinMod}_{k}[\mathrm{C}]$ be the second-order
formula which expresses that the classes are precisely those which appear in
the code $\mathrm{T}_{\mathcal{M}}[\mathrm{C}]$. Intuitive, this formula
expresses that the model is the forcing extension of the minimum model of
$\mathsf{KMCC}_{k}$ by the canonical choice of a Cohen generic.

Following the same interpretation strategy as before, we get that any model of
$\mathrm{Class}=\mathrm{MinMod}_{k}$ is bi-interpretable with its extension by
$\mathrm{C}$.

######  Theorem 4.2.6.

Fix $k\geq 1$. The following two theories are bi-interpertable.

  1. (1)

$D_{k}=\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{Class}=\mathrm{MinMod}_{k}$.

  2. (2)

$U_{k}=\mathsf{KMCC}_{k}+\mathsf{SOR}+\mathrm{Class}=\mathrm{MinMod}_{k}[\mathrm{C}]$.
∎

######  Corollary 4.2.7.

Fix $k\geq 1$. The theories $\mathsf{KMCC}_{k}$ and
$\mathsf{KMCC}_{k}+\mathsf{SOR}$ are not tight. ∎

##  5\. Non-tightness in second-order arithmetic

The constructions used in the previous section also work in the context of
second-order arithmetic. However, there are enough subtleties and notational
differences in arithmetic context that for ease of exposition we discuss it
separately in this section. Most proofs carry over mutatis mutandis from the
class theory context, and we leave it to the interested reader to rewrite the
proofs with the changed details. We state some facts about models of second-
order arithmetic without proof, and we point the reader to Simpson’s book on
the subject [Sim09], especially Chapter VII, for proofs and detailed
references.

In the class theory context, to get the failure of tightness we added the full
second-order Replacement schema to our theories. In the arithmetic context,
the analogue is the full Induction schema, i.e. the instances of Induction for
every second-order formula, and we will include it in our theories to ensure
constructions go through the model’s full $\omega$.

The strategy is the same as in class theory. For fragments of second-order
arithmetic we can write down a theory which characterizes a minimum model. We
can define a canonical code for this minimum model, and thereby define a
canonical Cohen extension of the minimum model. These two models are bi-
interpretable. Of course, with the nonstandardness phenomenon there is no hope
for an notion of minimum absolute between all models of the theory. But we can
get a sufficiently absolute notion to enable the bi-interpretation, so we get
the fragment of $\mathsf{Z}_{2}$ cannot be tight.

First we discuss the analogue of $\mathsf{GB}$. The theory $\mathsf{ACA}_{0}$
has as its principle axioms Induction and Comprehension for arithmetical
formulae. If you strengthen Induction to the full schema, over all second-
order formulae, you get the theory $\mathsf{ACA}$. Every $\omega$-model of
$\mathsf{ACA}_{0}$—viz. a model whose numbers are isomorphic to
$\omega$—automatically satisfies full $\mathsf{ACA}$. But for nonstandard
models the theories diverge. For instance, analogous to the situation with
$\mathsf{GB}$ and $\mathsf{SOR}$, over $\mathsf{ACA}$ you can prove that the
$\Sigma_{k}$-satisfaction class exists for all $k$, even nonstandard. Whereas
with just $\mathsf{ACA}_{0}$ you are only guaranteed to have such for standard
$k$. The reason, of course, is that $(M,\operatorname{Def}(M))$ is always a
model of $\mathsf{ACA}_{0}$ for any $M\models\mathsf{PA}$, and no nonstandard
$\Sigma_{k}$-satisfaction class can be definable.

Following the $\mathsf{GB}$ context, we can write down a theory which
identifies the minimum $\omega$-model, namely the arithmetical reals, among
all $\omega$-models. Using full Induction, this will allow a definition
sufficiently absolute among nonstandard models to enable two distinct but bi-
interpretable extensions of $\mathsf{ACA}$.

There is a second-order definition for the (first-order) satisfaction
predicate, call it $\mathrm{T}$. Indeed, the same definition as before—viz.
the union of the $\Sigma_{k}$-satisfaction classes—will do, modulo the details
of Gödel coding. Note that full Induction is used to ensure there is a
$\Sigma_{k}$-satisfaction predicate for every $k$ in the model. This makes
possible a theory $D$ expressing $\mathsf{ACA}$ $+$ “every set is
arithmetical” and a theory $U$ expressing $\mathsf{ACA}$ $+$ “there is a
canonical Cohen-generic $\mathrm{C}$ over the arithmetical sets and every set
is arithmetical in $\mathrm{C}$”. These two theories are then bi-
interpretable, with two key points—proved much the same as the class theoretic
case—being that forcing preserves full and induction and the definition of
$\mathrm{T}$.

All in all, we get the following result.

######  Theorem 5.0.1.

The theory $\mathsf{ACA}$ is not tight. Consequently, any weakening of
$\mathsf{ACA}$ in the language of second-order arithmetic, such as
$\mathsf{ACA}_{0}$, is also not tight. ∎

For stronger fragments of $\mathsf{Z}_{2}$ the same basic strategy works, but
producing the code for the minimum model is more difficult than defining a
satisfaction predicate. We start by recalling some definitions and facts.

######  Definition 5.0.2.

Fix $k\geq 1$.

  * •

The theory $\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$ is obtained from
$\mathsf{ACA}_{0}$ by adding Comprehension for $\Pi^{1}_{k}$ formulae.

  * •

The theory $\Pi_{k}^{1}\text{-}\mathsf{CA}$ is obtained from
$\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$ by adding full Induction.

  * •

The theory $\Sigma_{k}^{1}\text{-}\mathsf{AC}_{0}$ is obtained from
$\Pi_{k}^{1}\text{-}\mathsf{CA}$ by adding the $\Sigma^{1}_{k}$-Choice schema.
This schema is the arithmetic counterpart to the $\Sigma^{1}_{k}$-Class
Collection schema; cf. Definition 2.0.3.

  * •

The theory $\Sigma_{k}^{1}\text{-}\mathsf{AC}$ is obtained from
$\Sigma_{k}^{1}\text{-}\mathsf{AC}_{0}$ by adding full Induction.

The theory $\mathsf{ATR}_{0}$, a strict subtheory of
$\Pi_{1}^{1}\text{-}\mathsf{CA}_{0}$, is strong enough to carry out the
unrolling construction. As such, theories of arithmetic which extend
$\mathsf{ATR}_{0}$ are bi-interpretable with certain set theories. These
theories are strong enough to carry out the construction of $\mathrm{L}$.
Restricting to the constructible sets gives fragments of the AC schema, so
$\Sigma_{k}^{1}\text{-}\mathsf{AC}$ does not exceed
$\Pi_{k}^{1}\text{-}\mathsf{CA}$ in consistency strength. Unlike in class
theory, however, weak enough fragments of the $\mathsf{AC}$ schema are
outright provable, without any assumption of every set being constructible.

######  Theorem 5.0.3.

The $\Sigma^{1}_{1}$-Choice schema is a consequence of $\mathsf{ATR}_{0}$, and
over $\mathsf{ATR}_{0}$ the $\Sigma^{1}_{2}$-Choice schema is equivalent to
$\Delta^{1}_{2}$-Comprehension. For $k>2$, the $\Sigma^{1}_{k}$-Choice schema
is a consequence of $\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$ $+$ “there is a real
from which every real is constructible”.

For our purposes we are looking at models which satisfy that every real is
constructible, or Cohen-extensions thereof. So we will only be looking at
models of $\Sigma_{k}^{1}\text{-}\mathsf{AC}$. (This will include
$\Sigma_{1}^{1}\text{-}\mathsf{AC}=\Pi_{1}^{1}\text{-}\mathsf{CA}$ and
$\Sigma_{2}^{1}\text{-}\mathsf{AC}=\Pi_{2}^{1}\text{-}\mathsf{CA}$, but for
the sake of uniform notation we will use the former names.) Here are bi-
interpretation results for these theories.

######  Theorem 5.0.4.

The following pairs of theories are bi-interpretable.

  * •

$\mathsf{Z}_{2}$ $+$ $\Sigma^{1}_{\infty}$-$\mathsf{CA}$ and
$\mathsf{ZFC}^{-}$ plus “every set is countable”.

  * •

For $k\geq 1$, $\Pi_{k+1}^{1}\text{-}\mathsf{CA}_{0}$ and
$\mathsf{ZFC}^{-}_{k}$ plus “every set is countable”.

In the class theoretic case, the indexing was the same. Here they are off by
one. The culprit is well-foundedness. In class theory this is a first-order
property, whereas in arithmetic it is $\Pi^{1}_{1}$-universal. Because of this
misaligned indexing, the situation with $\Sigma_{1}^{1}\text{-}\mathsf{AC}$ is
different from the stronger theories. We discuss it first.

######  Theorem 5.0.5.

The minimum $\beta$-model of $\Sigma_{1}^{1}\text{-}\mathsf{AC}$ consists of
the reals in $\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$, where
$\omega_{\omega}^{\mathrm{CK}}$ is the supremum of the first $\omega$ many
admissible ordinals.

Note that the inclusion of full Induction means that any model of
$\Sigma_{1}^{1}\text{-}\mathsf{AC}$ thinks the $n$-th admissible ordinal
$\omega_{n}^{\mathrm{CK}}$ exists even for nonstandard $n$. This is because
$\Sigma_{1}^{1}\text{-}\mathsf{AC}_{0}$ is strong enough to prove that the
admissible ordinals are unbounded and so the set of such $n$ is inductive. And
over $\Sigma_{1}^{1}\text{-}\mathsf{AC}$ we can define the sequence of the
$\omega_{n}^{\mathrm{CK}}$. From this sequence we can extract a canonical code
of all the reals in $\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$, as in the
similar argument for strong fragments of $\mathsf{KM}$. From this code we can
define, via a second-order formula, a canonical choice for a Cohen real
$\mathrm{C}$ which is generic over
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$.

It is straightforward to formulate an axiom asserting over
$\Sigma_{1}^{1}\text{-}\mathsf{AC}$ that every set is in
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$. Namely, this axiom asserts that
for every set $X$ there is an integer $n$ so that there is a length $n$
sequence of well-orders $\gamma_{i}$ so that each $\gamma_{i}$ is admissible,
$\gamma_{0}=\omega$, there are no admissibles between $\gamma_{i}$ and
$\gamma_{i+1}$, and $X$ is in $\mathrm{L}_{\gamma_{n}}$. Call this axiom
$\mathrm{Class}=\mathrm{Adm}_{\omega}$. Similarly, we can formulate an axiom
$\mathrm{Class}=\mathrm{Adm}_{\omega}[\mathrm{C}]$ which asserts that
$\mathrm{C}$ exists and every set is in
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}[\mathrm{C}]$, where $\mathrm{C}$
is definable Cohen generic over the reals in
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$. We follow the same strategy as
before to define $\mathrm{C}$, using the canonical code of
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$.

Putting this all together, we get that the theories
$\Sigma_{1}^{1}\text{-}\mathsf{AC}+\mathrm{Class}=\mathrm{Adm}_{\omega}$ and
$\Sigma_{1}^{1}\text{-}\mathsf{AC}+\mathrm{Class}=\mathrm{Adm}_{\omega}[\mathrm{C}]$
are bi-interpretable. A key point is, a model of
$\Sigma_{1}^{1}\text{-}\mathsf{AC}$ and any Cohen-extension thereof will have
the same well-orders and agree on which well-orders give admissible ordinals.
So they will define the canonical code for the reals in
$\mathrm{L}_{\omega_{\omega}^{\mathrm{CK}}}$ the same, and thereby define
$\mathrm{C}$ the same.

######  Theorem 5.0.6.

The theory $\Sigma_{1}^{1}\text{-}\mathsf{AC}$
($=\Pi_{1}^{1}\text{-}\mathsf{CA}$) is not tight. Consequently, any weakening
of $\Sigma_{1}^{1}\text{-}\mathsf{AC}$ in the language of second-order
arithmetic, such as $\Pi_{1}^{1}\text{-}\mathsf{CA}_{0}$, is also not tight. ∎

We turn at last to $\Sigma_{k}^{1}\text{-}\mathsf{AC}$ for $k\geq 2$. For
these the characterization of the least $\beta$-model is more complex.

######  Theorem 5.0.7.

For $k>1$, the minimum $\beta$-model of $\Sigma_{k}^{1}\text{-}\mathsf{AC}$
consists of the reals in $\mathrm{L}_{\alpha}$ where $\alpha$ is the least
ordinal so that $\mathrm{L}_{\alpha}$ satisfies $\Pi_{k-1}$-Separation.
Equivalently, $\alpha$ is the least ordinal so that $\mathrm{L}_{\alpha}$
satisfies $\Sigma_{k-1}$-Replacement. Equivalently, $\alpha$ is the least
ordinal whose $k$-th projectum $\rho^{\alpha}_{k}$ is itself.

Yet again, the sticking point is defining a cofinal $\omega$-sequence in
$\alpha$. Here we can use the same fine structural facts as in Section 4.2. If
$(M,\mathcal{X})\models\Sigma_{k}^{1}\text{-}\mathsf{AC}$ $+$ “every set is
constructible” then it is bi-interpretable with its unrolling
$U\models\mathsf{ZFC}^{-}_{k-1}+\mathrm{V}=\mathrm{L}$. By Theorem 4.2.2 $U$
has a $\Sigma_{n}$ Skolem function. Using this Skolem function and full
Induction we can define an $\omega$-sequence of ordinals $\alpha_{n}$ which
are cofinal in what $U$ thinks is the minimum model of
$\mathsf{ZFC}^{-}_{k-1}$, as in the proof of Lemma 4.2.3. We can thus
formulate an axiom expressing that $U$ is itself this minimum model, namely by
asserting that every set is in $\mathrm{L}_{\alpha_{n}}$ for some $n$.

All this can be translated over to the model $(M,\mathcal{X})$ of second-order
arithmetic. Let $\mathrm{Class}=\mathrm{MinMod}_{k}$ denote the formula in the
language of second-order arithmetic asserting that every set is in this
minimum model. Then any model of
$\Sigma_{k}^{1}\text{-}\mathsf{AC}+\mathrm{Class}=\mathrm{MinMod}_{k}$ can
define a canonical code for itself, using the definable $\omega$-sequence
${\left\langle\alpha_{n}\right\rangle}$ of ordinals cofinal in the height of
its unrolling. This code will be absolute between this model and its Cohen-
extensions, because they will have the same well-orders and hence the same
$\mathrm{L}$. From this code we can define a canonical choice for a Cohen real
$\mathrm{C}$ which is generic over the minimum model. And so we can formulate
an axiom $\mathrm{Class}=\mathrm{MinMod}_{k}[\mathrm{C}]$ which asserts over
$\Sigma_{k}^{1}\text{-}\mathsf{AC}$ that $\mathrm{C}$ exists and every real is
in the extension of the minumum model by $\mathrm{C}$.

Following the same interpretations as used in the previous theorems, we then
conclude that
$\Sigma_{k}^{1}\text{-}\mathsf{AC}+\mathrm{Class}=\mathrm{MinMod}_{k}$ and
$\Sigma_{k}^{1}\text{-}\mathsf{AC}+\mathrm{Class}=\mathrm{MinMod}_{k}[\mathrm{C}]$
are bi-interpretable.

######  Theorem 5.0.8.

Fix $k\geq 2$. Then, $\Sigma_{k}^{1}\text{-}\mathsf{AC}$ is not tight.
Consequently, any theory weaker than $\Sigma_{k}^{1}\text{-}\mathsf{AC}$ in
the language of arithmetic, such as $\Pi_{k}^{1}\text{-}\mathsf{CA}$ and
$\Pi_{k}^{1}\text{-}\mathsf{CA}_{0}$, are also not tight. ∎

##  6\. Final remarks

The reader who thoroughly read the previous sections will have noticed that
this article is about essentially one construction done over and over in
different settings. We remark that it may be carried out in yet more settings.
For example, [Wil19] proves that there is a minimum $\beta$-model of
$\mathsf{ETR}$, where _Elementary Transfinite Recursion_ $\mathsf{ETR}$ is the
class theoretic analogue of $\mathsf{ATR}_{0}$. One can take their
construction of the minimum $\beta$-model of $\mathsf{ETR}$ and put the
construction of this article in that setting, thereby showing that the minimum
$\beta$-model of $\mathsf{ETR}$ is bi-interpretable with its extension by a
canonical choice of Cohen generic.

In [Ena16], Enayat conjectures that no (proper) subsystem of the tight
theories $\mathsf{PA}$, $\mathsf{Z}_{2}$, $\mathsf{ZF}$, $\mathsf{KM}$ can be
tight. In this article, we demonstrated the non-tightness of
$\mathsf{KM}_{k}+\mathsf{SOR}$ for all natural numbers $k$. These results
yield a natural and comprehensive collection of non-tight subtheories
approximating $\mathsf{KM}$. Indeed, it shows that full comprehension is the
minimal level of comprehension that produces a tight theory from
$\mathsf{GB}$.

As we were writing this article, we learned from Ali Enayat that in
forthcoming work [Ena] he had independently proved that all finitely
axiomatizable fragments of $\mathsf{PA}$, $\mathsf{Z}_{2}$, $\mathsf{ZF}$,
$\mathsf{KM}$ are not tight. His proof provides an alternate proof of the
nontightness of $\mathsf{GB}$ and $\mathsf{KM}_{k}$, along with their
arithmetical counterparts. But his argument does not apply to
$\mathsf{GB}+\mathsf{SOR}$, $\mathsf{KM}_{k}+\mathsf{SOR}$ and their
arithmetical counterparts, as the second-order Replacement schema
(respectively, the second-order Induction schema) is not finitely
axiomatizable. Thus, putting together Enayat’s results, our results in this
aritcle, and those of Freire and Hamkins [FH20], we have a substantial basis
for Enayat’s conjecture. And while there still are other theories to consider
in order to assert that all subtheories of KM are not tight, these would be
quite unnatural subtheories.

What is missing to get the full result? With respect to class theories, we
should consider proper subtheories of $\mathsf{KM}$ that have instances of
Comprehension of ever growing formula complexity, but in such a way that full
$\mathsf{KM}$ isn’t provable from those instances. This type of subsystem is
hardly considered in the literature and for this reason it may require some
novel treatment. The status of same kind of the fragment of arithmetic and
first-order set theory is also unknown. Additionally, while one may consider
levels of formula complexity in the single scheme (induction) in arithmetic
and (comprehension) in class theory, the same do not apply to $\mathsf{ZF}$ as
one should also consider fragments of Replacement together with the full
scheme of Separation, or other natural systems like Zermelo set theory plus
the assertion that every set is in a $\mathrm{V}_{\alpha}$. Therefore, while
the picture may be said to be nearly complete for $\mathsf{KM}$, $\mathsf{PA}$
and $\mathsf{Z}_{2}$, there is still a lot to be discovered with respect to
$\mathsf{ZF}$.

## References

  * [AF17] Carolin Antos and Sy-David Friedman  “Hyperclass Forcing in Morse-Kelley Class Theory”  In _The Journal of Symbolic Logic_ 82.2, 2017, pp. 549–575
  * [AG] Carolin Antos and Victoria Gitman  “Modern Class Forcing” (Forthcoming)  In _Research Trends in Contemporary Logic_ College Publications  URL: https://philarchive.org/archive/ANTMCFv1
  * [BW16] Tim Button and Sean Walsh  “Structure and categoricity: Determinacy of reference and truth value in the philosophy of mathematics”  In _Philosophia Mathematica_ 24.3 OUP, 2016, pp. 283–307
  * [Ded65] Richard Dedekind  “Was sind und was sollen die Zahlen?”  In _Was sind und was sollen die Zahlen?. Stetigkeit und Irrationale Zahlen_ Wiesbaden: Vieweg+Teubner Verlag, 1965, pp. 1–47  DOI: 10.1007/978-3-663-19573-3˙1
  * [Dod82] A. Dodd  “The Core Model”, Lecture note series / London mathematical society  Cambridge University Press, 1982
  * [Ena] Ali Enayat  “Tightness, solidity, and internal categoricity” In preparation
  * [Ena16] Ali Enayat  “Variations on a Visserian theme”  In _Liber Amicorum Alberti : a tribute to Albert Visser_ London: College Publications, 2016, pp. 99–110  arXiv:1702.07093 [math.LO]
  * [Fef60] Solomon Feferman  “Arithmetization of metamathematics in a general setting”  In _Fundamenta mathematicae_ 49.1, 1960, pp. 35–92
  * [Fef62] Solomon Feferman  “Transfinite recursive progressions of axiomatic theories”  In _The Journal of symbolic logic_ 27.3 Cambridge University Press, 1962, pp. 259–316
  * [Fef65] Solomon Feferman  “Some applications of forcing and generic sets”  In _Fundamenta Mathematica_ 56, 1965, pp. 325–345
  * [FH20] Alfredo Roque Freire and Joel David Hamkins  “Bi-interpretation in weak set theories”  In _Journal of Symbolic Logic_ , 2020  DOI: 10.1017/jsl.2020.72
  * [FKO62] Solomon Feferman, Georg Kreisel and Steven Orey  “1—Consistency and faithful interpretations”  In _Archiv für mathematische Logik und Grundlagenforschung_ 6.1 Springer, 1962, pp. 52–63
  * [Fre21] Alfredo Roque Freire  “Irreducible features of set theories” In review, 2021  DOI: 10.13140/RG.2.2.20667.44322/1
  * [Fri00] Sy D. Friedman  “Fine Structure and Class Forcing”, De Gruyter Series in Logic and Its Applications, 3  De Gruyter, 2000
  * [GH17] Victoria Gitman and Joel David Hamkins  “Open determinacy for class games”  In _Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin’s 60th Birthday_ , Contemporary Mathematics  American Mathematical Society, 2017  arXiv: http://jdh.hamkins.org/open-determinacy-for-class-games
  * [GHK21] Victoria Gitman, Joel David Hamkins and Asaf Karagila  “Kelley-Morse set theory does not prove the class Fodor theorem”  In _Fundamenta Mathematicae_ 254.2, 2021, pp. 133–154  DOI: 10.4064/fm725-9-2020
  * [Git+20] Victoria Gitman, Joel David Hamkins, Peter Holy, Philipp Schlicht and Kameryn J. Williams  “The exact strength of the class forcing theorem”  In _The Journal of Symbolic Logic_ 85.3 Cambridge University Press, 2020, pp. 869–905  DOI: 10.1017/jsl.2019.89
  * [Ham18] Joel David Hamkins  “Different set theories are never bi-interpretable”, 2018  URL: http://jdh.hamkins.org/different-set-theories-are-never-bi-interpretable/
  * [Hod93] Wilfrid Hodges  “Model theory”  Cambridge University Press, 1993
  * [HS06] Joel David Hamkins and Daniel Seabold  “Well-founded Boolean ultrapowers as large cardinal embeddings”, 2006, pp. 1–40  arXiv: http://jdh.hamkins.org/boolean-ultrapowers/
  * [HW18] Joel David Hamkins and W. Hugh Woodin  “Open class determinacy is preserved by forcing” Under review  In _Mathematics ArXiv_ , 2018, pp. 1–14  arXiv: http://wp.me/p5M0LV-1KF
  * [Jen21] R Björn Jensen  “Manuscript on fine structure, inner model theory, and the core model below one Woodin cardinal” Unpublished, 2021  URL: https://ivv5hpp.uni-muenster.de/u/rds/skript-2021-07-07.pdf
  * [Jen72] R Björn Jensen  “The fine structure of the constructible hierarchy”  In _Annals of mathematical logic_ 4.3 North-Holland, 1972, pp. 229–308
  * [MM75] W. Marek and A. Mostowski  “On extendability of models of ZF set theory to the models of Kelley-Morse theory of classes”  In _ISILC Logic Conference: Proceedings of the International Summer Institute and Logic Colloquium, Kiel 1974_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1975, pp. 460–542  DOI: 10.1007/BFb0079429
  * [Mos51] Andrzej Mostowski  “Some impredicative definitions in set theory”  In _Fundamenta Mathematica_ 37, 1951, pp. 111–124
  * [Odi83] Piergiorgio Odifreddi  “Forcing and reducibilities”  In _The Journal of Symbolic Logic_ 48.2 Cambridge University Press, 1983, pp. 288–310
  * [Odi83a] Piergiorgio Odifreddi  “Forcing and Reducibilities. II. Forcing in Fragments of Analysis”  In _The Journal of Symbolic Logic_ 48.3 Association for Symbolic Logic, 1983, pp. 724–743
  * [Odi83b] Piergiorgio Odifreddi  “Forcing and Reducibilities. III. Forcing in Fragments of Set Theory”  In _The Journal of Symbolic Logic_ 48.4 Association for Symbolic Logic, 1983, pp. 1013–1034
  * [Par90] Charles Parsons  “The structuralist view of mathematical objects”  In _Synthese_ 84.3 Springer, 1990, pp. 303–346
  * [Put80] Hilary Putnam  “Models and reality”  In _The journal of symbolic logic_ 45.3 Cambridge University Press, 1980, pp. 464–482
  * [Rat79] Zygmunt Ratajczyk  “On sentences provable in impredicative extensions of theories” 40 pp.  In _Dissertationes Mathematicae_ 178, 1979
  * [Sco60] Dana Scott  “A different kind of model for set theory” Unpublished paper, talk given at the 1960 Stanford Congress of Logic, Methodology, and Philosophy of Science, 1960
  * [Sim09] Stephen George Simpson  “Subsystems of second order arithmetic”, Perspectives in Logic  New York: Association for Symbolic Logic, 2009
  * [Sta84] Maurice C. Stanley  “A unique generic real”, 1984
  * [Tar53] Alfred Tarski  “A general method in proofs of undecidability”  In _Undecidable theories_ 13 Elsevier, 1953, pp. 1–30
  * [Vää12] Jouko Väänänen  “Second order logic or set theory?”  In _Bulletin of Symbolic Logic_ 18.1 Cambridge University Press, 2012, pp. 91–121
  * [Vää20] Jouko Väänänen  “Tracing internal categoricity”  In _Theoria_ 87.4 Wiley Online Library, 2020, pp. 986–1000
  * [Vis06] Albert Visser  “Categories of theories and interpretations”  In _Logic in Tehran_ 26, Lect. Notes Log.  Assoc. Symbol. Logic, La Jolla, CA, 2006, pp. 284–341
  * [VW15] Jouko Väänänen and Tong Wang  “Internal categoricity in arithmetic and set theory”  In _Notre Dame Journal of Formal Logic_ 56.1 Duke University Press, 2015, pp. 121–134
  * [Wil18] Kameryn J. Williams  “The structure of models of second-order set theory”, 2018
  * [Wil19] Kameryn J. Williams  “Minimum models of second-order set theories”  In _The Journal of Symbolic Logic_ 84.2 Cambridge University Press, 2019, pp. 589–620  DOI: 10.1017/jsl.2019.27
  * [Zar96] Andrzej M. Zarach  “Replacement $\nrightarrow$ collection”  In _Gödel ’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, proceedings_ 6, Lecture Notes in Logic  Berlin: Springer-Verlag, 1996, pp. 307–322  URL: http://projecteuclid.org/euclid.lnl/1235417032
  * [Zer30] Ernst Zermelo  “Über grenzzahlen und mengenbereiche: Neue untersuchungen über die grundlagen der mengenlehre”  In _Fundamenta mathematicae_ 16, 1930