3
$\begingroup$

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?

$\endgroup$
8
  • 1
    $\begingroup$ 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$. $\endgroup$
    – Hanul Jeon
    Oct 9, 2021 at 3:02
  • 1
    $\begingroup$ 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. $\endgroup$
    – Hanul Jeon
    Oct 9, 2021 at 3:05
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Hanul Jeon
    Oct 9, 2021 at 3:09
  • 1
    $\begingroup$ 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. $\endgroup$
    – Hanul Jeon
    Oct 9, 2021 at 5:37
  • 1
    $\begingroup$ 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}$. $\endgroup$
    – Hanul Jeon
    Oct 9, 2021 at 7:57

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for the reply. I am specifically interested in the completion of a lattice in a constructive set theory. To preform the completeness one must take certain subsets of the lattice (complete ideals) and show that they form a complete lattice. In IZF (Intuitionistic Set Theory) the power set axiom allows for us to consider these subsets but I'm unsure if this is possible CZF (Constructive Set Theory) which instead uses Subset Collection. $\endgroup$
    – ToucanIan
    Oct 10, 2021 at 22:24
  • 1
    $\begingroup$ Do you mean Dedekind-McNeille completion? That would not provably be a set in CZF. The most common approach I've seen is to allow lattices to be proper classes to include this case, but then require the lattice to have a set of generators, or some variation of this so you still have some control over it. As it happens, this is mentioned in the paper by Gambino I linked to (section 2). $\endgroup$
    – aws
    Oct 10, 2021 at 22:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.