Skip to main content
2 of 2
correct url
aws
  • 4.4k
  • 19
  • 18

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.

aws
  • 4.4k
  • 19
  • 18