\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{subset collection}

\hypertarget{subset_collection}{}\section*{{Subset collection}}\label{subset_collection}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{statements}{Statements}\dotfill \pageref*{statements} \linebreak
\noindent\hyperlink{relation_to_other_axioms}{Relation to other axioms}\dotfill \pageref*{relation_to_other_axioms} \linebreak
\noindent\hyperlink{relation_to_type_theory}{Relation to type theory}\dotfill \pageref*{relation_to_type_theory} \linebreak
\noindent\hyperlink{definition_of_}{Definition of $\mathbf{R}$}\dotfill \pageref*{definition_of_} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In [[set theory]] and the [[foundations]] of mathematics, the axiom of \textbf{fullness} is an axiom intermediate in strength between the existence of [[power sets]] and [[function sets]]. Of course, these can only be distinguished in [[constructive mathematics]], since classically power sets and function sets are equivalent (at least if you have the set $\mathbf{2} = \{\top, \bot\}$).

The axiom of \textbf{subset collection} combines fullness with the [[axiom of collection]] to apply in the situations where fullness is used. In the presence (I think) of either collection or [[full separation]], subset collection is equivalent to fullness.

\hypertarget{statements}{}\subsection*{{Statements}}\label{statements}

In its guise as \emph{fullness}, the axiom states that, given any [[sets]] $X$ and $Y$, there is a set $F_{X,Y}$ of \emph{enough [[entire relations]]} from $X$ to $Y$ in this sense:

\begin{itemize}%
\item Every element of $F_{X,Y}$ is an entire relation from $X$ to $Y$;
\item If $R$ is an entire relation from $X$ to $Y$, then for some $S \in F_{X,Y}$, $S \subseteq R$.

\end{itemize}
We have written this in a [[material set theory|material]] fashion; [[structural set theory|structurally]], the axiom says that $F_{X,Y}$ \emph{parametrises} enough entire relations in this sense:

\begin{itemize}%
\item There is a [[subset]] $E_{X,Y}$ of $F_{X,Y} \times X \times Y$ such that:

\begin{itemize}%
\item for every element $r$ of $F_{X,Y}$ and every element $a$ of $X$, there is an element $b$ of $Y$ such that $(r,a,b) \in E_{X,Y}$;

\end{itemize}
(we think of $E_{X,Y}$ as giving the evaluation, as a [[truth value]], of $r$, as an entire relation, on the elements $a$ and $b$).


\item If $R$ is an entire relation from $X$ to $Y$, then for some $s$ in $F_{X,Y}$:

\begin{itemize}%
\item for every element $a$ of $X$ and $b$ of $Y$, if $(s,a,b) \in E_{X,Y}$, then $a$ is $R$-related to $b$;

\end{itemize}
(we think of $s$ as an entire relation via $E_{X,Y}$ and say that it is contained in $R$).



\end{itemize}
In the context of material set theory, the structural axiom is weaker than the material axiom, but they become equivalent in the presence of [[axiom of replacement|restricted replacement]], which is quite weak.

You can also write down an [[internalization|internal]] version of fullness by adding arbitrary additional parameters to the structural version above (analogously to the generalisation from [[power set]] to [[power object]], although more complicated since $F_{X,Y}$ is not given by a [[universal property]]).

In its guise as \emph{subset collection}, the axiom states \ldots{}

I need to look this up again, including the conditions for its equivalence with fullness. In the meantime, see \href{http://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html}{the Stanford Encyclopedia's list of axioms}.

\hypertarget{relation_to_other_axioms}{}\subsection*{{Relation to other axioms}}\label{relation_to_other_axioms}

In the presence of the usual basic axioms of set theory (in particular, the axioms of [[bounded separation]] and [[axiom of pairing|pairing]] in a material set theory and the existence of [[equalisers]] and [[products]] in a structural set theory), we have:

\begin{quote}%
power sets $\rightarrow$ fullness $\rightarrow$ function sets


\end{quote}
On the one hand, $F_{X,Y}$ can be constructed as the [[subset]] of the [[power set]] $\mathcal{P}(X \times Y)$ consisting of \emph{all} entire relations from $X$ to $Y$. On the other hand, the [[function set]] $Y^X$ may be constructed as a subset of $F_{X,Y}$ consisting of those elements $S$ such that $S \subseteq R$ for $R$ (the graph of) some function from $X$ to $Y$; (the key here is that $S = R$ must follow when $S$ is entire and $R$ is a function). Conversely, if we have function sets, then the [[axiom of choice]] states precisely that the function set $Y^X$ always qualifies as $F_{X,Y}$ (although function sets and [[excluded middle]] are already sufficient for power sets and thus fullness).

Fullness also follows from function sets in the presence of [[COSHEP]], a fairly strong but constructive (in that it implies no general [[principle of omniscience]]) form of the [[axiom of choice]]. If $P$ is a [[projective set]] with a [[surjection]] $p\colon P \to X$ (which this axiom asserts must exist), then we may take $Y^P$ as $F_{X,Y}$, with $(r,a,b) \in E_{X,Y}$ iff, for some $c$ in $P$, $p(c) = a$ and $r(c) = b$.

Note that $F_{X,Y}$ is not categorical (in the logicians' sense); that is, there may be many sets $F, F', \ldots$ that all satisfy the axiom without being (in an appropriate sense) equal. This is the downside to adopting the fullness axiom, compared to power sets or function sets; this is also why the internal version is complicated.

As fullness is weaker than power sets in a constructive framework, we may consider it [[predicative mathematics|predicative]] in the sense of the constructive school; this is one reason for adopting it while rejecting power sets. One reason for adopting it instead of (only) function sets is this: it is strong enough to construct the set $\mathbf{R}$ of (located Dedekind) [[real numbers]] from the set $\mathbf{N}$ of [[natural numbers]] \emph{without} assuming [[excluded middle]] or [[countable choice]]; see below.

\hypertarget{relation_to_type_theory}{}\subsection*{{Relation to type theory}}\label{relation_to_type_theory}

Subset collection is justified by predicative versions of constructive [[type theory]] in the sense of Martin--L\"o{}f or Thierry Coquand. To see this, note that these theories justify [[COSHEP]]; their types define (not sets in general but) \emph{[[presets]]} (following Bishop) or \emph{[[completely presented sets]]}, which (as sets) are projective. Analogously, an element of $F_{X,Y}$ may be considered an \emph{operation} or \emph{prefunction} (following `preset') from $X$ to $Y$.

But note that the type of prefunctions from $X$ to $Y$, like the preset underlying $X$, is a categorical (unique) construction in type theory, while $F_{X,Y}$, like COSHEP, is not. Thus type theory (or rather preset theory) gives us constructions that are not available in set theory (even with fullness or even COSHEP), such as the predicate that states whether two functions have equal underlying prefunctions.

\hypertarget{definition_of_}{}\subsection*{{Definition of $\mathbf{R}$}}\label{definition_of_}

We consider this application in some detail; see also [[real number object]].

Using [[function sets]], one can easily construct the set $\mathbf{R}_C$ of [[Cauchy reals]] as a [[subquotient]] of the function set $\mathbf{N}^{\mathbf{N}}$. Both classical and constructive mathematicians usually adopt axioms in which one can prove that $\mathbf{R} = \mathbf{R}_C$; this is equivalent to a [[weak countable choice]] principle (identified by [[Fred Richman]] et al) that follows from either [[excluded middle]] (classically accepted) or [[countable choice]] (usually constructively accepted). But there are (for example) some [[Grothendieck toposes]] in which $\mathbf{R} = \mathbf{R}_C$ (as a statement in the [[Mitchell–Bénabou language]]) fails, so any sort of constructive mathematics that wants to apply to such toposes cannot rely on this method to define the [[real numbers object]] $\mathbf{R}$.

Of course, in a topos, there are other ways to define $\mathbf{R}$, but what if you want your theory to \emph{also} be predicative? If you adopt the fullness axiom, then you can modify the definition of $\mathbf{R}_C$ to produce a definition of $\mathbf{R}$ \emph{without} assuming any choice principle. Instead of using $\mathbf{N}^{\mathbf{N}}$, you use $F_{\mathbf{N},\mathbf{N}}$ instead; $\mathbf{R}$ can be constructed as a subquotient of that set.

Let an element of $F_{\mathbf{N},\mathbf{N}}$ be a \emph{pre[[sequence]]} of natural numbers, and fix a [[bijection]] $\phi\colon \mathbf{N} \to \mathbf{Q}$ between $\mathbf{N}$ and the set $\mathbf{Q}$ of [[rational numbers]]. We call such a presequence $r$ \emph{regular} if, whenever $i,j,x,y$ are natural numbers such that $r(i,x)$ and $r(j,y)$, we have

\begin{displaymath}
{|\phi(x) - \phi(y)|} \leq 1/i + 1/j .
\end{displaymath}
(It is common, but not really necessary in the presence of function sets, to use regular sequences instead of the more general Cauchy sequences when defining $\mathbf{R}_C$ in constructive mathematics, and we follow that here.) We call two regular presequences $r,s$ \emph{equivalent} if, whenever $i,j,x,y$ are natural numbers such that $r(i,x)$ and $s(j,y)$, we have

\begin{displaymath}
{|\phi(x) - \phi(y)|} \leq 1/i + 1/j .
\end{displaymath}
Then this defines an [[equivalence relation]] on the set of regular presequences, and the [[quotient set]] is $\mathbf{R}$. (That is, it may be given, in the usual way, the structure of a [[linear order|linearly ordered]] [[Heyting field]] which is [[Dedekind-complete]] relative to located pairs of upper and lower sets.)

category: foundational axiom

[[!redirects axiom of fullness]] [[!redirects fullness axiom]] [[!redirects axiom of subset collection]] [[!redirects subset collection]]



\end{document}