# Subset Collection axiom

In Constructive Set Theory (CZF) the Power Set axiom is replaced with the Subset Collection axiom which I will state here:

$$\exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \land \forall y \in d \exists x \in a (\psi(x,y,u)))]$$

Typical treatments of CZF (Aczel and Rathjen - CST Book draft) will introduce the notion of fullness to aid in the comprehension of this notably dense axiom. Which is perfectly reasonable. But still I want to get a better feel for what this axiom is saying and what can be done with it in place of the Power Set axiom (for my own research). Is this misguided?

Before discussing about my difficulty in understanding this axiom I will recall the power set axiom.

$$\forall a \exists y \forall x [x \in y \longleftrightarrow x \subseteq a]$$

where $$a \subseteq b$$ is shorthand for $$\forall z(z \in a \to z \in b)$$. This axiom is easy enough to interpret. For any set $$a$$ there exists a set $$y$$ (which we call the powerset of $$a$$) such that for any $$x$$, $$x$$ is in the powerset of $$a$$ if and only if $$x$$ is a subset of $$a$$.

The Subset Collection axiom on the other hand asserts the existence of a set $$c$$ which I assume to be some sort of collection of subsets, before referencing any set for which we wish to take subsets from. Am I thinking about this axiom the wrong way? How would one interpret the variables here?

• One way to put syntactic sugar to Subset Collection is to use the notion of multi-valued function (a relation $R\subseteq A\times B$ for classes $A$ and $B$ is a multi-valued function from $A$ to $B$ means for each $a\in A$ there is (not necessarily unique) $b\in B$ such that $(a,b)\in R$.) I prefer to denote it as $R:A\rightrightarrows B$. Oct 9, 2021 at 3:02
• Then we may state Subset Collection as follows: for a given definable collection of multi-valued functions $\{R_u: a\rightrightarrows b\}$ parametrized by $u\in V$, we can find a set $c$ such that $c$ contains every "image" of $a$ under $R_u$. Honestly, however, neither Subset Collection nor Fullness is handy for me. Oct 9, 2021 at 3:05
• You may convince yourself by examining how to interpret Subset Collection under Aczel's type-theoretic interpretation of $\mathsf{CZF}$ (and, in fact, it is the focal motivation for Constructive ZF.) Oct 9, 2021 at 3:09
• If I understand your question correctly (that is, a way to extract information about $c$ from $a$, $b$, and the multivalued function), the answer would be: extracting information is seemingly unlikely. Oct 9, 2021 at 5:37
• It justifies the existence of function sets, which is usually proven under the axiom of power set. Unfortunately, I do not know any other use of this axiom except for the justification for the existence of Dedekind reals. I believe (and Aczel intended) the type-theoretic interpretation fortifies constructive (and predicative) manner of $\mathsf{CZF}$. Oct 9, 2021 at 7:57

If you want to think of it as a special case of power set, then what it is saying is that given sets $$a$$ and $$b$$ it asserts the existence of a collection of subsets of $$b$$ that contains something like the image of every multivalued function from $$a$$ to $$b$$. For example, if we had the powerset axiom, we could take $$c$$ to be the powerset of $$b$$.
We can see it as a stronger version of exponentiation as follows. Note that it is possible to define the exponentiation axiom as saying that there is a set $$c$$ that contains the image of every function from $$a$$ to $$b$$. It is clear this follows from exponentiation and replacement and for the converse, note that a function from $$a$$ to $$b$$ viewed as a subset of $$a \times b$$, is the image of a function from $$a$$ to $$a \times b$$. However, a priori we cannot quantify over the set of all functions from $$a$$ to $$b$$ (because we don't know it exists yet) so instead we use functional relations, i.e. formulas $$\psi$$ such that $$\forall x \in a\,\exists ! y \in b\,\psi(x, y)$$. For subset collection, we drop the uniqueness requirement and only require $$\forall x \in a\, \exists y \in b\,\psi(x, y)$$, and instead of $$d$$ being the image, we only require that $$d$$ contains at least one witness $$y \in b$$ for each $$x \in a$$.
As Hanul Jeon mentioned, a famous use of subset collection is the construction of the Dedekind reals, since each Dedekind cut $$(L, R)$$ corresponds to a multivalued relation $$R$$ from $$\{(p, q) \in \mathbb{Q} \times \mathbb{Q} \;|\; p < q\}$$ to $$2$$, where $$R((p, q), 0)$$ indicates $$p \in L$$ and $$R((p, q), 1)$$ indicates $$q \in R$$. I think there's another example where it's used in Gambino, Heyting-valued interpretations for Constructive Set Theory, where it's used to show subset collection holds in a Heyting valued model, but if I recall correctly it would still be necessary to assume in the metatheory even if you only want exponentiation in the model. In general it does come up sometimes when you want a collection of sets that each contain enough witnesses to satisfy a certain property, but you have no way to choose a particular witness.