Subset Collection axiom

Question

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?

Answer 1

Subset collection is typically used as a stronger version of exponentiation, rather than a weaker version of power set, so that is why fullness is usually the best way of understanding it.

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.