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?

3more comments