paper-reflection.tex

\documentclass[oneside,reqno]{amsart}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amsthm,mathtools,stmaryrd,amssymb,graphicx}
\usepackage{booktabs}
\usepackage[all]{xy}
\usepackage[protrusion=true,expansion=true]{microtype}
\usepackage{xspace}

\usepackage[natbib=true,style=numeric,maxnames=10]{biblatex}
\usepackage[babel]{csquotes}
\bibliography{paper-reflection.bib}

\graphicspath{{images/}}

\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}

\title[Reflections on reflection for intuitionistic set theories]{Reflections on reflection for \\ intuitionistic set theories}
\author{}
\email{}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{ex}[defn]{Example}

\theoremstyle{plain}
\newtheorem{prop}[defn]{Proposition}
\newtheorem{cor}[defn]{Corollary}
\newtheorem{lemma}[defn]{Lemma}
\newtheorem{thm}[defn]{Theorem}
\newtheorem{scholium}[defn]{Scholium}

\theoremstyle{remark}
\newtheorem{rem}[defn]{Remark}
\newtheorem{question}[defn]{Question}
\newtheorem{speculation}[defn]{Speculation}
\newtheorem{caveat}[defn]{Caveat}
\newtheorem{conjecture}[defn]{Conjecture}

\newenvironment{indentblock}{%
  \list{}{\leftmargin\leftmargin}%
  \item\relax
}{%
  \endlist
}

\newcommand{\xra}[1]{\xrightarrow{#1}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\EE}{\mathbb{E}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\CC}{\mathbb{C}}
\renewcommand{\SS}{\mathbb{S}}
\renewcommand{\P}{\mathcal{P}}
\renewcommand{\O}{\mathcal{O}}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\op}{\mathrm{op}}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Mod}{Mod}
\DeclareMathOperator{\Sh}{Sh}
\DeclareMathOperator{\PSh}{PSh}
\DeclareMathOperator{\rank}{rank}
\DeclareMathOperator{\length}{length}
\DeclareMathOperator{\List}{List}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Eff}{\mathrm{Ef{}f}}
\renewcommand{\_}{\mathpunct{.}\,}
\newcommand{\effective}{ef{}fective\xspace}
\newcommand{\?}{\,{:}\,}
\newcommand{\realizes}{\Vdash}
\newcommand{\notnot}{\emph{not~not}\xspace}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}

\newcommand{\stacksproject}[1]{\cite[{\href{https://stacks.math.columbia.edu/tag/#1}{Tag~#1}}]{stacks-project}}

\renewcommand{\paragraph}[1]{\noindent\textbf{#1.}}

\newcommand{\PRA}{\textsc{pra}}
\newcommand{\ZF}{\textsc{zf}}
\newcommand{\IZF}{\textsc{izf}}
\newcommand{\IZFS}{\textsc{izf/s}}
\newcommand{\CZF}{\textsc{czf}}
\newcommand{\ZFC}{\textsc{zfc}}
\newcommand{\ZFCS}{\textsc{zfc/s}}
\newcommand{\ZFCI}{\textsc{zfc+i}}
\newcommand{\RRS}{\textsc{rrs}}
\newcommand{\RDC}{\textsc{rdc}}
\newcommand{\DC}{\textsc{dc}}
\newcommand{\MDC}{\textsc{mdc}}
\newcommand{\ES}{(\IZF+\RRS_2)/\textsc{s}}

\begin{document}

\begin{abstract}
  We study the well-known reflection principle of Zermelo--Fraenkel set theory
  in the context of intuitionistic Zermelo--Fraenkel set theory~$\IZF$. We show
  that the reflection principle is equivalent to~$\RRS_2$, a strengthened
  version of Aczel's relation reflection scheme. As
  applications, we give a new proof that relativized dependent choice is
  equivalent to the conjunction of the relation reflection scheme and dependent
  choice, and we present an intuitionistic version of Feferman's~$\ZFCS$, a
  conservative extension of~$\ZFC$ which is useful as a foundation for category
  theory.
\end{abstract}

\maketitle
\thispagestyle{empty}

\section{Introduction}

The basic form of the reflection principle for Zermelo--Fraenkel set
theory~$\ZF$ is the following.
\begin{thm}Let~$\varphi(x_1,\ldots,x_n)$ be a formula in the language of set
theory with some of its free variables as indicated (and further free variables
allowed). Then~$\ZF$ proves
\[ \forall M\_
  \exists S \supseteq M\_
  \forall x_1,\ldots,x_n \in S\_
  \varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^S(x_1,\ldots,x_n), \]
where~$\varphi^S$ is the~$S$-relativization of~$\varphi$, obtained by
substituting any occurrence of~``$\forall x$'' and~``$\exists x$'' by~``$\forall
x \in S$'' and~``$\exists x \in S$''.
Furthermore, the resulting set~$S$ may be supposed to be transitive, to be closed
under subsets or even to be a stage~$V_\alpha$ of the cumulative hierarchy;
% XXX: "hence" instead of "or even"?
and given not a single formula~$\varphi$ but a finite
list~$\varphi_1,\ldots,\varphi_s$ of formulas, we may suppose that~$S$ reflects
all of them.
\end{thm}

The reflection principle expresses that truth of any formula can already be
checked in an initial segment of the universe. This observation
is important both for philosophical and for practical
reasons: Philosophically, it tells us that the set-theoretic universe cannot be
distinguished from its initial segments by any set-theoretical property.
Practically, it allows to
transfer results obtained for a restricted class of objects to all such
objects. For instance, if we manage to verify (the $S$-relativization of) some
group-theoretic statement for all groups contained in an arbitrary set~$S$,
then we may deduce that the statement holds
for all groups in the universe. Examples from sheaf cohomology and more
generally category theory abound; an example from set theory is presented in
Proposition~\ref{prop:zf-rrs2}.

The reflection principle has been used by Feferman to construct~$\ZFCS$ (``$\ZFC$ with
smallness''), a conservative extension of~$\ZFC$ which provides a useful
foundation of category theory~\cite{feferman:zfcs}. This system extends~$\ZFC$
by a new constant symbol~$\SS$ together with axioms stating
that~$\SS$ is transitive, closed under subsets and reflective with respect to
every formula~$\varphi(x_1,\ldots,x_n)$ of the original language:
\[ \label{ax:refl}\tag{$\star$}
\forall x_1,\ldots,x_n \in \SS\_ \varphi(x_1,\ldots,x_n) \Leftrightarrow
\varphi^{\SS}(x_1,\ldots,x_n). \]
The system~$\ZFCS$ is conservative over~$\ZFC$ because any given proof in~$\ZFCS$ uses
only a finite number of instances of the axioms~\eqref{ax:refl}, whereby the reflection
principle can be used to yield an honest set~$S$ which validates just the same equivalences
and can hence be used in place of~$\SS$.

Elements of~$\SS$ are deemed ``small'', so that~$\SS$ is the set of all small
sets. The system~$\ZFCS$ is useful as a foundation for category theory because
it supports, without requiring new set-theoretical commitments such as the
existence of Grothendieck universes, a native treatment of large structures.
For instance, the category of all small sets can be formed entirely
within~$\ZFCS$, without resorting to classes. We invite the reader desiring
to learn more about the merits of~$\ZFCS$ to study the survey by
Shulman~\cite[Section~11]{shulman:sets}.

To our naive eyes, the passage from~$\ZFC$ to~$\ZFCS$ looked sufficiently
innocent so that we set out to develop an intuitionistic version of~$\ZFCS$: To
our mind, size issues were entirely different concerns than issues of constructivity, and
we hence opined that they should be dealt with separately. Such a separation
would not only lead to improved mental hygiene and better understanding, but
would also allow us to use the benefits
of~$\ZFCS$ in situations where the law of excluded middle and the axiom of
choice are not available, such as in realizability semantics, sheaf semantics
or quite generally topos semantics.

We expected this modification to be entirely straightforward. However, the
situation turned out to be more subtle, and we failed in our original goal of
verifying the reflection principle in intuitionistic Zermelo--Fraenkel set
theory~$\IZF$. The situation for~$\CZF$, the predicative subsystem of~$\IZF$
commonly heralded as the largest common denominator of all flavors of
constructive set theory, remains even more elusive. (XXX, update: $\CZF$ does
not, and cannot be expected to, verify the reflection principle.)

However, we succeeded in verifying the reflection principle in only a slight
extension of~$\IZF$:

\begin{thm}The reflection principle is equivalent, over~$\IZF$, to the strong
relation reflection scheme~$\RRS_2$.\end{thm}

We also give a weaker version of the reflection principle which is equivalent
to Aczel's original reflection scheme~$\RRS$.
Both~$\RRS$ and~$\RRS_2$ will be reviewed below. They are validated not
only by~$\ZFC$, but also by~$\ZF$, and furthermore by
all known models of~$\IZF$, hence might be regarded as not entirely
% XXX: be more precise in "all known"
unconstructive, even though they are conjectured to be independent of~$\IZF$. As a
result, the question whether the reflection principle holds for~$\IZF$ remains
open (though conjectured to be false), and for the stronger system~$\IZF+\RRS_2$
we can give a variant ``with smallness'' which can serve as a set-theoretic
foundation for category theory.

% Since~$\ZF$ proves~$\RRS_2$, our proof of the reflection principle also serves
% as a new classical proof. However, the standard proof is shorter, XXX
% Hint that we don't need regularity.

This note is organized as follows. Section~\ref{sect:review} reviews the
classical proof of the reflection principle in the context of~$\ZF$ set theory.
Section~\ref{sect:axioms} reviews Aczel's relation reflection scheme and its
variants. Our main result is presented in Section~\ref{sect:constructive-proof}.
We conclude in Section~\ref{sect:appl-rdc} and
Section~\ref{sect:appl-smallness} with two applications.

\textbf{Acknowledgments.} We are grateful to Daniel Albert for his careful
reading of earlier drafts. XXX

% XXX briefly recall the language of IZF/ZF.
% XXX state free variables more precisely


\section{Review of the classical reflection principle}
\label{sect:review}

A basic proof of the reflection principle in~$\ZF$ runs as follows. Our proof
of the reflection principle in~$\IZF+\RRS_2$ will follow the same outline.

\begin{lemma}\label{lemma:zf-smallstep}
Let~$\varphi(u_1,\ldots,u_n,x)$ be a formula in the language of set
theory. Then~$\ZF$ proves
\begin{multline*}
  {\qquad}\forall M\_
  \exists S \supseteq M\_
  \forall u_1,\ldots,u_n \in S\_ \\
  (\exists x\_ \varphi(u_1,\ldots,u_n,x)) \Longrightarrow
  (\exists x \in S\_ \varphi(u_1,\ldots,u_n,x)).{\qquad}
\end{multline*}
Furthermore: (1)~We may suppose that~$S$ is transitive. (2)~We may suppose that~$S$ is
closed under subsets. (3)~Given a finite list~$\varphi_1,\ldots,\varphi_s$
of formulas instead of the single formula~$\varphi$, we may suppose that~$S$
bounds all the formulas~$\varphi_i$.
\end{lemma}

\begin{proof}Given a class~$X$ (as commonly understood as the comprehension of
a formula), we denote by~$X^\sim$ its subclass~$\{ x \in X \,|\, \forall y
\in X\_ \rank(x) \leq \rank(y) \}$, where the rank function refers to the stage
in the cumulative hierarchy. The two fundamental properties of this construction are:
This subclass is equal to a set,\footnote{If~$X$ is empty, then
this claim is trivial; if~$X$ is inhabited by some element~$x_0$, then~$X^\sim$ can
be obtained using separation from~$V_{\rank(x_0)+1}$; and in fact, by an argument
using the set of truth values and unbounded separation, the claim can also be
proven in~$\IZF$.} and it is inhabited if and only if~$X$ is.

Starting with~$S_0 \defeq M$, we construct~$S_{k+1}$ from~$S_k$ as the union
\[ S_{k+1} \defeq S_k \cup \bigcup_{u_1,\ldots,u_n \in S_k} \{ x \,|\,
\varphi(u_1,\ldots,u_n,x) \}^\sim. \]
It is then easy to check that~$S \defeq \bigcup_{k \in \NN} S_k$ is a set with the
required property.

For addendum~(1), we change the definition of~$S_{k+1}$ to be the transitive
closure of what is was before. To further accommodate addendum~(2), we change
this definition again, to be~$P^\omega$ of what is was before,
where~$P^\omega(X) \defeq \bigcup_{\ell \in \NN} P^{(\ell)}(X)$ is the union of
iterated powersets. For addendum~(3), we change the definition of~$S_{k+1}$ to
include one summand for each formula~$\varphi_i$.
\end{proof}

The proof constructed by Lemma~\ref{lemma:zf-smallstep} is mostly constructive; however,
there is one issue with nontrivial ramifications: While~$\IZF$ does show
that the subclass~$X^\sim$ of a given class~$X$ is a set, it does not verify
that~$X^\sim$ is inhabited if~$X$ is. This would amount to the constructive
taboo that any inhabited set contains a rank-minimal element. Moreover, by
a result of Friedman and Scedrov~\cite{XXX}, no definable substitute
for~$X^\sim$ exists. The remedy presented in
Section~\ref{sect:constructive-proof} will construct~$X^\sim$ in a non-unique
fashion and then deal with the resulting fallout that taking the union requires
additional care.

\begin{thm}\label{thm:zf-bigstep}
Let~$\varphi(x_1,\ldots,x_n)$ be a formula in the language of set
theory. Then~$\ZF$ proves
\[ \forall M\_
  \exists S \supseteq M\_
  \forall x_1,\ldots,x_n \in S\_
  \varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^S(x_1,\ldots,x_n). \]
Furthermore, the
resulting set~$S$ may be supposed to be transitive and to be closed under
subsets; and given not a single formula~$\varphi$ but a finite
list~$\varphi_1,\ldots,\varphi_s$ of formulas, we may suppose that~$S$ reflects
all of them.
\end{thm}

\begin{proof}Let a set~$M$ be given. We obtain~$S$ by applying
Lemma~\ref{lemma:zf-smallstep} to the list of all subformulas of~$\varphi$
which start with an existential quantifier. That
the resulting set~$S$ has the required property can then be checked by an induction on the structure
of~$\varphi$. The cases~$\text{``$=$''}, \text{``$\in$''}, \text{``$\top$''},
\text{``$\bot$''}, \text{``$\wedge$''},
\text{``$\vee$''}, \text{``$\Rightarrow$''}$ follow
trivially from the induction hypothesis. The case~``$\forall$'' does
not need to be treated since we may assume without loss of generality that all
universal quantifiers in~$\varphi$ have been rewritten
as~``$\neg\exists\neg$''.

The remaining case is where~$\varphi$ is of the form~$\varphi \equiv (\exists
x\_ \psi(u_1,\ldots,u_m,x))$. In this case the claim is that
\[ \forall u_1,\ldots,u_m \in S\_
  (\exists x\_ \psi(u_1,\ldots,u_m,x)) \Longleftrightarrow
  (\exists x \in S\_ \psi^S(u_1,\ldots,u_m,x)). \]
This claim follows by the property of~$S$ guaranteed by
Lemma~\ref{lemma:zf-smallstep} and by the induction hypothesis concerning the
subformula~$\psi^S(u_1,\ldots,u_m,x)$.
\end{proof}

The proof of Theorem~\ref{thm:zf-bigstep} is constructive with the sole
exception of treating the case of universal quantifiers by appealing to the law
of excluded middle and referring to the unconstructive Lemma~\ref{lemma:zf-smallstep}. For the constructive proof in
Section~\ref{sect:constructive-proof}, we will solve both issues by instead appealing to a strengthened
version of Lemma~\ref{lemma:zf-smallstep}.


\section{Aczel's relation reflection axiom scheme and its variants}
\label{sect:axioms}

We follow the usual convention that~$\IZF$ is the set theory with the following
axioms: extensionality, pair, union, empty set, infinity, unbounded separation,
collection, powerset and~$\in$-induction. We direct the reader wishing for a
survey of~$\IZF$ and other nonclassical set theories to Crosilla's entry in the
SEP~\cite{crosilla:cst-izf}.

We write~``$R : X \rightrightarrows Y$'' to mean~``$\forall x \in X\_ \exists y
\in Y\_ \langle x,y \rangle \in R$''.

\begin{defn}Let~$X$ and~$R \subseteq X \times X$ be classes. Let~$x_0 \in X$.
\begin{itemize}
\setlength{\itemsep}{0.3em}
\item[$\DC$] \emph{dependent choice} \\ If~$X$ and~$R$ are sets and
if~$R : X \rightrightarrows X$, then there is a function~$f : \NN \to X$ such that~$f(0) =
x_0$ and~$\langle f(k), f(k+1) \rangle \in R$ for all numbers~$k$.
\item[$\RDC$] \emph{relativized dependent choice} \\ If~$R : X
\rightrightarrows X$, then there is a function~$f : \NN \to X$ such that~$f(0)
= x_0$ and~$\langle f(k), f(k+1) \rangle \in R$ for all numbers~$k$.
\item[$\RRS$] \emph{Aczel's relation reflection scheme} \\
If~$R : X \rightrightarrows X$, then there is
a set~$B$ such that~$x_0 \in B \subseteq X$ and~$R : B \rightrightarrows B$.
\item[$\MDC$] \emph{Palmgren's multivalued dependent choice} \\
If~$R : X \rightrightarrows X$, then there is a function~$f : \NN \to P(X)$
(the class of all subsets of~$X$) such that~$x_0 \in f(0)$ and such
that~$\forall x \in f(k)\_ \exists y \in f(k+1)\_ \langle x,y \rangle \in R$
for every number~$k$.
\end{itemize}
\end{defn}

\begin{defn}\label{defn:rrs2}
Let~$X$ and~$R \subseteq X \times X \times X$ be classes. Let~$x_0 \in X$.
\begin{itemize}
\setlength{\itemsep}{0.3em}
\item[$\RRS_2$]
If~$R : X \times X \rightrightarrows X$, then there is a set~$B$ such that~$x_0
\in B \subseteq X$ and~$R : B \times B \rightrightarrows B$.
\item[$\MDC_2$]
If~$R : X \times X \rightrightarrows X$, then there is a function~$f : \NN \to
P(X)$ such that~$x_0 \in f(0)$ and such that~$\forall x \in f(k)\_ \forall x'
\in f(k')\_ \exists y \in f(\max\{k,k'\}+1)\_ \langle x,x',y \rangle \in R$ for
any numbers~$k, k'$.
\end{itemize}
\end{defn}

Aczel's relation reflection scheme~$\RRS$ first surfaced in
the theory of coinductive definitions of classes and enjoys substantial
stability properties, as it passes from the meta theory to XXX[all kinds of]
models. Background on~$\RRS$ can be found in Aczel's original article
introducing it~\cite{aczel:rrs}, and more information on choice axioms in
general is contained in the book draft by Aczel and
Rathjen~\cite[Section~10]{aczel-rathjen:cst}.
$\RRS$ is equivalent, over~$\CZF$ and
a~fortiori over~$\IZF$, to Palmgren's multivalued dependent
choice~\cite{palmgren:mdc}; this observation makes the relationship to
dependent choice more visible.

\begin{rem}Most published renditions of~$\RRS$ and~$\MDC$ do not refer to an initial
element~$x_0 \in X$, but to a set~$A \subseteq X$ and then require instead
of that~$x_0 \in B$, that~$A \subseteq B$. This difference is immaterial, thanks in
one direction to the existence of singleton sets and in the other to strong
collection. The same is true for~$\RRS_2$ and~$\MDC_2$, though the proof is not
as easy.
% XXX give the proof
\end{rem}

% XXX introduce CZF^-

% First prove that in RRS_2^∈, we may suppose that not only a single given
% element x0 is contained in B, but also a further given element x1.
% Do this by applying RRS_2^∈ to X^ := { ∅ } U { {x} | x ∈ X } and
% R^(p,p',q) given by:
% * p = ∅   and p' = ∅    and q = {x0}  or
% * p = ∅   and p' = {x0} and q = {x1}  or  the other way round  or
% * p = {x} and p' = {x'} and q = {y} and R(x,x',y).
%
% Now let R : X × X ⇉ X and a set A ⊆ X be given. We want to verify RRS_2^⊆
% for this data.
%
% Given H ∈ P(X), H' ∈ P(X), consider:
%
%    Let x ∈ H, x' ∈ H'.
%    Then by the strengthened RRS_2^∈, there is a set B ⊆ X
%    such that x, x' ∈ B and R : B × B ⇉ B.
%
% We can use collection to obtain a set J of such B's, and consider U J.
%
% We can then apply RRS_2^∈ to this relation to obtain a set T such that
% A ∈ T ⊆ P(X) and ... Set C := U T. Then A ⊆ C ⊆ X and R : C × C ⇉ C.

Aczel's $\RRS$ should not in itself be regarded as a choice principle; however in
its presence, ordinary~$\DC$ entails~$\RDC$. This result is due to
Aczel~\cite[Theorem~2.4]{aczel:rrs}, who proved the equivalence~$\RDC = \RRS +
\DC$ over~$\CZF^-$, and we give a new proof of this equivalence over the
stronger theory~$\IZF$ in Section~\ref{sect:appl-rdc}.

The axiom scheme~$\RRS_2$ does not appear to have been studied much. Apart from
the PhD thesis by Ziegler~\cite{ziegler:phd}, where it is called the
\emph{strong relation reflection principle}, we have not been able to track
down further mentions of it in the literature; hence it seems prudent to verify
some of its basic properties here.

In the presence of~$\DC$, $\RRS$ is equivalent to~$\RRS_2$:

\begin{prop}\label{prop:rdc-rrs2-dc}
Over~$\CZF^-$, $\RDC$ is equivalent to~$\RRS_2 + \DC$.
\end{prop}

\begin{proof}Trivially,~$\RDC$ entails~$\DC$, and~$\RRS_2 + \DC$
entails~$\RDC$ by Aczel's result since~$\RRS_2$ entails~$\RRS$.

To verify that~$\RDC$ entails~$\RRS_2$, let classes~$X$ and~$R \subseteq X
\times X \times X$ be given, let~$x_0 \in X$ be an element and assume~$R : X
\times X \rightrightarrows X$. Let~$\List(X)$ be the class of finite lists with
entries in~$X$. We declare a class~$\widehat X$ by
\[ \widehat X \defeq \{ \langle i,j,v \rangle \,|\, i,j \in
\NN, v \in \List(X), i,j < \length(v) \} \]
and a relation~$\widehat R \subseteq \widehat X \times \widehat X$ by
defining~$\langle \langle i,j,v \rangle, \langle i',j',v' \rangle \rangle \in
\widehat R$ to be equivalent to
\begin{indentblock}
there exists an element~$y \in X$ such that
\begin{enumerate}
\item $\langle v!i, v!j, y \rangle \in R$ (where~$v!k$ is the element of the
list~$v$ at position~$k$),
\item $v'$ is obtained from~$v$ by adding the single element~$y$ at the end and
\item $\langle i',j' \rangle$ is the next point after~$\langle i,j
\rangle$ in some fixed enumeration of~$\NN^2$ which, for each number~$n$, first visits
all points~$\langle k,l \rangle$ with~$k,l < n$ before it visits any of
the other points.
\end{enumerate}
\end{indentblock}
Then~$\widehat R : \widehat X \rightrightarrows \widehat X$. Applying~$\RDC$
with initial value~$\langle 0,0, [x_0] \rangle \in \widehat X$ yields a
function~$f : \NN \to \widehat X$. Let~$B$ be the set of all
entries of the lists contained in the tuples~$f(k)$. Then~$x_0 \in B
\subseteq X$ and~$R : B \times B \rightrightarrows B$.
\end{proof}

A consequence of Proposition~\ref{prop:rdc-rrs2-dc} is that~$\RRS_2$ holds in
Aczel's type-theoretic ``sets as trees'' model
of~$\CZF$~\cite{aczel:sets-as-trees}, since that model validates~$\RDC$.

\begin{prop}Over~$\CZF^-$, $\RRS_2$ is equivalent to~$\MDC_2$.\end{prop}

\begin{proof}The proof in~\cite{palmgren:mdc} carries over.\end{proof}

\begin{prop}\label{prop:zf-rrs2}
$\ZF$ proves~$\RRS_2$.\end{prop}

\begin{proof}Let~$X$ and~$R \subseteq X \times X$ be classes. Let~$x_0 \in X$
and assume~$R : X \rightrightarrows X$. By the reflection principle, there is a
set~$S \ni x_0$ such that~$R : X \cap S \rightrightarrows X \cap S$. This
concludes the proof as the class~$B \defeq X \cap S$ is a set by separation.
\end{proof}

Fourman and independently Hayashi have shown how to interpret~$\IZF$ in any
Grothendieck topos~\cite{fourman:izf,hayashi:izf}. The following proposition
shows that the axiom scheme~$\RRS_2$ passes from the metatheory to any such
model:

\begin{prop}Over~$\IZF + \RRS_2$, $\RRS_2$ holds in any Grothendieck topos.
\end{prop}

\begin{proof}We employ Streicher's version of the interpretation
of~$\IZF$~\cite{streicher:forcizf}, and follow him also in the notation.

Let~$\CC$ be a Grothendieck site, assumed without loss of generality to possess
a terminal object~$1$ and pullbacks. Let~$V$ be the universe sheaf over~$\CC$. Let
formulas~$\chi$ and~$\varrho$ be given, with parameters from~$V(1)$, defining
classes~$X$ and~$R$ in~$\Sh(\CC)$. Let an element~$x_0 \in V(1)$ be given and assume
\[ 1 \models \speak{$R \subseteq X \times X \times X$} \qquad\text{and}\qquad
  1 \models \speak{$R : X \times X \rightrightarrows X$}, \]
where the corner quotes indicate that translation to formal language is left to
the reader.

For an object~$I \in \CC$, let~$V_I$ be the (external) class of pairs~$(J
\xrightarrow{u} I, x \in V(J))$. Define the (external) classes
\begin{align*}
  X' &\defeq \{ (I,F) \,|\, I \in \CC, F \in P(V_I), \mathrm{fst}[F] \in
  \mathrm{Cov}(I), \forall (J \xrightarrow{u} I, x \in V(J)) \in F\_ J \models x \in X \}
\end{align*}
XXX
\end{proof}


\section{Constructivizing the reflection principle}
\label{sect:constructive-proof}

Our constructive rendition of the reflection principle will require the axiom
scheme~$\RRS_2$ displayed in Definition~\ref{defn:rrs2}. This result is the
best possible, as we verify in Theorem~\ref{thm:refl-entails-rrs2} that
conversely the reflection principle entails~$\RRS_2$.

Even though superficially similar, the following lemma is \emph{not} yet a
constructivization of Lemma~\ref{lemma:zf-smallstep}; these two lemmas differ
in the set from which~$u_1,\ldots,u_n$ are drawn.

\begin{lemma}\label{lemma:izf-microstep}
Let~$\varphi(u_1,\ldots,u_n,x)$ be a formula in the language of set
theory. Then~$\IZF$ proves
\begin{multline*}
  {\qquad}\forall H\_
  \exists H' \supseteq H\_
  \forall u_1,\ldots,u_n \in H\_ \\
  \begin{array}{@{}rcl@{}}
  (\exists x\_ \varphi(u_1,\ldots,u_n,x)) &\Longrightarrow&
  (\exists x \in H'\_ \varphi(u_1,\ldots,u_n,x)) \quad\mathop{\wedge} \\
  (\forall x\_ \varphi(u_1,\ldots,u_n,x)) &\Longleftarrow&
  (\forall x \in H'\_ \varphi(u_1,\ldots,u_n,x)).\end{array}
  {\qquad}
\end{multline*}
Furthermore: (1)~We may suppose that~$H'$ is transitive. (2)~We may suppose
that~$H'$ is closed under subsets. (3)~Given a finite
list~$\varphi_1,\ldots,\varphi_s$ of formulas instead of the single
formula~$\varphi$, we may suppose that~$H'$ has the displayed property for each
of the formulas~$\varphi_i$.
\end{lemma}

\begin{proof}Let~$\Omega \defeq P(\{0\})$ be the set of truth values.
For given elements~$u_1,\ldots,u_n \in H$, we have
\[ \begin{array}{@{}l@{}l@{}}
  \forall a \in \{ a \in \{0\} \,|\, \exists x\_ \varphi(u_1,\ldots,u_n,x) \}\_ &
  \exists x\_ \varphi(u_1,\ldots,u_n,x) \quad\text{and} \\
  \forall p \in \{ p \in \Omega \,|\, \exists x\_ (0 \in p \Leftrightarrow
  \varphi(u_1,\ldots,u_n,x)) \}\_ &
  \exists x\_ (0 \in p \Leftrightarrow \varphi(u_1,\ldots,u_n,x)).
\end{array} \]
Hence, by collection, there are sets~$C$ and~$D$ such that
\[ \begin{array}{@{}rcl@{}}
  (\exists x\_ \varphi(u_1,\ldots,u_n,x)) &\Longrightarrow&
  (\exists x \in C\_ \varphi(u_1,\ldots,u_n,x)) \quad\text{and} \\
  (\forall x\_ \varphi(u_1,\ldots,u_n,x)) &\Longleftarrow&
  (\forall x \in D\_ \varphi(u_1,\ldots,u_n,x)).
\end{array} \]
The union~$C \cup D$ satisfies both of these conditions at once.

Applying collection again, there is a set~$X$ such that for
any~$u_1,\ldots,u_n \in H$ there exists a set~$E \in X$ such that
\[ \begin{array}{@{}rcl@{}}
  (\exists x\_ \varphi(u_1,\ldots,u_n,x)) &\Longrightarrow&
  (\exists x \in E\_ \varphi(u_1,\ldots,u_n,x)) \quad\text{and} \\
  (\forall x\_ \varphi(u_1,\ldots,u_n,x)) &\Longleftarrow&
  (\forall x \in E\_ \varphi(u_1,\ldots,u_n,x)).
\end{array} \]
Hence the set~$H' \defeq H \cup \bigcup X$ has the required property.

To ensure that~$H'$ is transitive and closed under subsets, we pass
first to its transitive closure and then compute the union of all its
finitely-iterated powersets.
% XXX what do we need for this?

In order to accommodate more than a single formula~$\varphi$, we add one summand
in the definition of~$H'$ for each formula~$\varphi_i$.
\end{proof}

The proof of Lemma~\ref{lemma:izf-microstep} makes crucial use of unbounded
separation and the powerset axiom. Hence we do not believe that it can
be improved to work over~$\CZF$. Since we do not have any uniqueness guarantee
on the~``$\exists x$'' quantifiers in the proof, it also does not work
over~$\IZF_\text{Rep}$, the variant of~$\IZF$ with replacement instead of
collection.

\begin{lemma}\label{lemma:izf-smallstep}
Let~$\varphi(u_1,\ldots,u_n,x)$ be a formula in the language of set
theory. Then~$\IZF+\RRS_2$ proves
\begin{multline*}
  {\qquad}\forall M\_
  \exists S \supseteq M\_
  \forall u_1,\ldots,u_n \in S\_ \\
  \begin{array}{@{}rcl@{}}
  (\exists x\_ \varphi(u_1,\ldots,u_n,x)) &\Longrightarrow&
  (\exists x \in S\_ \varphi(u_1,\ldots,u_n,x)) \quad\mathop{\wedge} \\
  (\forall x\_ \varphi(u_1,\ldots,u_n,x)) &\Longleftarrow&
  (\forall x \in S\_ \varphi(u_1,\ldots,u_n,x)).\end{array}
  {\qquad}
\end{multline*}
Furthermore: (1)~We may suppose that~$S$ is transitive. (2)~We may suppose
that~$S$ is closed under subsets. (3)~Given a finite
list~$\varphi_1,\ldots,\varphi_s$ of formulas instead of the single
formula~$\varphi$, we may suppose that~$S$ bounds all the
formulas~$\varphi_i$.
\end{lemma}

\begin{proof}By~$\RRS_2$, there is a set~$B$ such that~$M \in B$ and such that
for any~$H_1, H_2 \in B$, there is a set~$H' \in B$ such that~$H \defeq H_1
\cup H_2$ and~$H'$ are related as in the conclusion of Lemma~\ref{lemma:izf-microstep}.

We set~$S \defeq \bigcup B$. This set has the required property. To verify
this claim, it is useful to observe that given~$u_1,\ldots,u_n \in S$, there is a
common set~$H \in B$ such that~$u_1,\ldots,u_n \in H$.

In order to ensure addenda~(1) and~(2), we apply~$\RRS_2$ in a slightly
different way to guarantee that for any sets~$H_1, H_2 \in B$, there is a
set~$H' \in B$ such that~$H \defeq H_1 \cup H_2$ and~$H'$ are related as in the
conclusion of Lemma~\ref{lemma:izf-microstep} and such that furthermore~$H'$ is
transitive and closed under subsets. Even though it cannot be expected that any
particular set~$H \in B$ will be transitive and closed under subsets, the
union~$S$ will. Addendum~(3) can be ensured because of addendum~(3) of
Lemma~\ref{lemma:izf-microstep}.
\end{proof}

\begin{rem}\label{rem:izf-smallstep-1}
In the special case~$n = 1$, the proof of Lemma~\ref{lemma:izf-smallstep} can
be simplified to only use~$\RRS$ instead of~$\RRS_2$, because in this case it
suffices for the set~$B$ to be such that for any~$H \in B$, there is a set~$H'
\in B$ such that~$H$ and~$H'$ are related as in the conclusion of
Lemma~\ref{lemma:izf-microstep}.
\end{rem}

\begin{thm}\label{thm:izf-bigstep}
Let~$\varphi(x_1,\ldots,x_n)$ be a formula in the language of set
theory. Then~$\IZF+\RRS_2$ proves
\[ \forall M\_
  \exists S \supseteq M\_
  \forall x_1,\ldots,x_n \in S\_
  \varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^S(x_1,\ldots,x_n). \]
Furthermore, the resulting set~$S$ may be supposed to be transitive and to be closed
under subsets; and given not a single formula~$\varphi$ but a finite
list~$\varphi_1,\ldots,\varphi_s$ of formulas, we may suppose that~$S$ reflects
all of them.
\end{thm}

\begin{proof}The proof of Theorem~\ref{thm:zf-bigstep} carries over. The only
difference is that instead of Lemma~\ref{lemma:zf-smallstep},
Lemma~\ref{lemma:izf-smallstep} has to be used, and that the case for the
universal quantifier has to be treated just as the case for the existential
quantifier has to.\end{proof}

\begin{scholium}\label{scholium:izf-bigstep-1}
Let~$\varphi(x_1,\ldots,x_n)$ be a formula in the language of set
theory. Assume that the surrounding scope of
any unbounded quantifier in~$\varphi$ contains at most one free variable.
Then~$\IZF+\RRS$ proves the same conclusion as stated in
Theorem~\ref{thm:izf-bigstep}.
\end{scholium}

\begin{proof}The condition on the number of free variables allows the proof of
Theorem~\ref{thm:izf-bigstep} to be adapted to employ the version of
Lemma~\ref{lemma:izf-smallstep} outlined in Remark~\ref{rem:izf-smallstep-1},
which requires only~$\IZF+\RRS$ instead of~$\IZF+\RRS_2$.
\end{proof}

\begin{thm}\label{thm:refl-entails-rrs2}
Over~$\IZF$, each instance of Aczel's relation reflection scheme~$\RRS_2$ can be
deduced from suitable instances of the assumption that, given a finite list
of formulas, for every set~$M$ there is a set~$S \supseteq M$ reflecting the
given formulas.
\end{thm}

\begin{proof}Let~$X$ and~$R \subseteq X \times X \times X$ be classes. Let~$x_0 \in X$
be an element and suppose~$R : X \times X \rightrightarrows X$.

By assumption, there is a set~$S \ni x_0$ which reflects the three
formulas~``$x \in X$'', ``$\langle x,x',y \rangle \in R$'' and~``$\exists y \in X\_ \langle
x,x',y \rangle \in R$''.

The class~$B \defeq X \cap S$ is a set by separation and contains~$x_0$.
Given~$x,x' \in B$, there is a set~$y$ such that~$y \in X$ and~$\langle x,y,y'
\rangle \in R$. By the reflecting property of~$S$, we can assume that such an
element~$y$ exists in~$S$.

Hence~$R : B \times B \rightrightarrows B$.
\end{proof}


\section{A new proof of~$\RDC = \RRS + \DC$}
\label{sect:appl-rdc}

When he introduced~$\RRS$, Aczel proved that over $\CZF$ without subset
collection, relative dependent choice $\RDC$ is equivalent to the conjunction
of~$\RRS$ and dependent choice~$\DC$~\cite[Theorem~2.4]{aczel:rrs}. Using
reflection, we can provide a new proof of this fact, although over the much
stronger base theory~$\IZF$ instead of~$\CZF^{-}$. The idea is that reflection
allows to reduce~$\RDC$ to~$\DC$.

\begin{prop}Over~$\IZF$, $\RDC$ is equivalent to~$\RRS + \DC$.
\end{prop}

\begin{proof}Trivially,~$\RDC$ implies~$\DC$, and~$\RDC$ implies~$\RRS$ by a
similar, though much simpler, argument as in the proof of
Proposition~\ref{prop:rdc-rrs2-dc}.

Conversely, assume~$\RRS$ and~$\DC$. In order to verify~$\RDC$, let classes~$X$
and~$R \subseteq X \times X$ be given. Let~$x_0 \in X$ and assume~$\forall x
\in X\_ \exists y \in X\_ \langle x,y \rangle \in R$.

We cannot apply Scholium~\ref{scholium:izf-bigstep-1} to the formula~``$\forall
x \in X\_ \exists y \in X\_ \langle x,y \rangle \in R$'' since unbounded
quantifiers implicitly appearing in the formulas~``$x \in X$'' and~``$\langle
x,y \rangle \in R$'' (recalling that~$X$ and~$R$ are classes) may violate the
condition on the number of free variables. However, we can opt to leave these
subformulas to be untranslated when carrying out the~$S$-relativization; with
this understanding, Scholium~\ref{scholium:izf-bigstep-1} can be applied to
yield a set~$S \ni x_0$ such that
\[ \forall x \in S\_ (x \in X \Rightarrow \exists y \in S\_
  (y \in X \wedge \langle x,y \rangle \in R)). \]

Hence~$\forall x \in X \cap S\_ \exists y \in X \cap S\_ \langle x,y \rangle
\in R$. By~$\DC$, there is a choice function~$f : \NN \to X \cap S$ such
that~$f(0) = x_0$ and~$\langle f(k), f(k+1) \rangle \in R$ for all numbers~$k$.
This is a function of the kind required by~$\RDC$.
\end{proof}


\section{An intuitionistic version of Feferman's~$\ZFCS$}
\label{sect:appl-smallness}

\begin{defn}The system $\ES$ is obtained from~$\IZF+\RRS_2$ by
adding a constant symbol~$\SS$ together with axioms
stating that~$\SS$ is transitive, closed under subsets and reflective for all
formulas of the original language.\end{defn}

\begin{prop}The system~$\ES$ is conservative
over~$\IZF+\RRS_2$.\end{prop}

\begin{proof}Because the reflection principle is available in~$\IZF+\RRS_2$,
the same argument as for~$\ZFCS$ applies.\end{proof}

Just as~$\ZFCS$ can serve as a set-theoretic foundation for category theory in
a classical context, we argue that~$\ES$ can serve as such a foundation in an
intuitionistic context (provided, of course, one is willing to
accept~$\RRS_2$).

The system~$\ES$ is also interesting from the point of view of topos theory.
We recall that any topos supports an internal language which can be used to reason about the
objects and morphisms of the topos in a naive element-based language, allowing
us to pretend that the objects are plain sets (or types) and that the morphisms
are plain maps between those sets (\cite[Chapter~6]{borceux:handbook3},
\cite[Section~1.3]{caramello:ttt}, \cite[Chapter~14]{goldblatt:topoi},
\cite[Chapter~VI]{moerdijk-maclane:sheaves-logic}). We refer
to~\cite[Sections~1 and~2]{blechschmidt:phd} for a short introduction and a
review of some of the applications of the internal language.

Given a topos~$\mathcal{E}$ and a formula~$\varphi$ in its internal language,
we write~``$\mathcal{E} \models \varphi$'' to mean that~$\varphi$ holds
in~$\E$. As a special case, truth in the topos~$\Set$, the category of all sets,
coincides with truth in the background theory; symbolically: $\Set \models
\varphi$ iff~$\varphi$.

However, in the context of~($\IZF$ or)~$\ZFC$, it is difficult to make this
claim precise. Because in~$\ZFC$ the category~$\Set$ of all sets can not be
coded as a set,~$\ZFC$ cannot define truth in~$\Set$. We must therefore resort
to a meta theory in order to express this claim, for instance by stating
that primitive recursive arithmetic~$\PRA$ proves that for any
formula~$\varphi$ of~$\ZFC$, $\ZFC$ proves~``$(\Set \models \varphi)
\Leftrightarrow \varphi$'', where~``$\Set \models \varphi$'' is to be unrolled
by~$\PRA$.

An alternative is offered by~$\ZFCI$, $\ZFC$ plus the existence of a
strongly inaccessible cardinal. In this system, there is a Grothendieck
universe~$U$; we can form the category~$\Set_U$ of all sets in~$U$ as an honest
set; define truth in~$\Set_U$; and prove, within the system, that for any
formula~$\varphi$, $(\Set_U \models \varphi) \Leftrightarrow (U \models
\varphi)$. This even holds for formulas of the full infinitary language of
toposes, which allows infinite disjunctions and infinite conjunctions; this
extended language could not be treated by resorting to~$\PRA$ as indicated above.

However, truth in a Grothendieck universe~$U$ need not be related to actual
truth. A solution to this problem is provided by~$\ZFCS$ and by~$\ES$. In these systems, we can
form the topos~$\Set_\SS$ of all sets in~$\SS$, define truth in it, prove for all formulas~$\varphi$
that~$(\Set_\SS \models \varphi) \Leftrightarrow (\SS \models \varphi)$; and
reflection for~$\SS$ ensures that for each (external, standard)
formula~$\varphi$, the system proves~``$(\Set_\SS \models \varphi)
\Leftrightarrow \varphi$''.


\section{Outlook}

We proved that, over~$\IZF$, the reflection principle is equivalent
to~$\RRS_2$. This gives credence to the claim that the reflection principle is
not provable over~$\IZF$ alone. However, the following question remains open:

\begin{question}Does~$\IZF$ prove~$\RRS_2$?\end{question}

If the answer is in the negative, as is most likely, then no conservative
extension could include a constant symbol~$\SS$ such that~$\SS$-relativized
truth is the same as absolute truth.

However, truth in toposes is a more flexible notion than~$S$-relativized
truth for any set~$S$. Hence one might hope that even in this case, the
following question does have a positive answer:

\begin{question}Is there a conservative extension~$\IZF'$ of~$\IZF$, containing
a constant symbol~$\EE$, such that~$\IZF'$ proves that~$\EE$ is an elementary
topos and such that~$\IZF'$ proves~``$(\EE \models \varphi) \Leftrightarrow
\varphi$'' for any formula~$\varphi$?\end{question}

\printbibliography

\end{document}

Cite: https://link.springer.com/chapter/10.1007/BFb0061825

Cite: https://arxiv.org/pdf/1110.2430.pdf (page 10)

https://www.youtube.com/watch?v=lpOiuvzbBtw&list=PL6tK2CutTH9_lN7A0nFul_gEJUDSPJ91i&index=3
Timestamp 29:49
Aczel showed that RRS is stable under passage to sheaves on complete Heyting
algebras.