# In CZF (w/ Subset Collection removed) the Powerset axiom Implies Subset Collection

The Subset Collection axiom: $$\forall a \forall b \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)))]$$ is often digested by considering the equivalent (in CZF - Subset Collection) axiom of Fullness. Let $$mv(B^A)$$ be the class of all sets $$R \subseteq A \times B$$ satisfying $$\forall a \in A \exists b \in B (\langle a,b \rangle \in R)$$. A set $$C$$ is full in $$mv(B^A)$$ if $$C \subseteq mv(B^A)$$ and $$\forall R \in mv(B^A) \exists S \in C (S \subseteq R).$$ The Fullness axiom states: For all sets $$A$$ and $$B$$ there exists a set $$C$$ such that $$C$$ is full in $$mv(B^A)$$. For completness the Powerset axiom states: $$\forall x \exists y \forall z(z \subseteq x \longleftrightarrow z \in y$$).

Now to show that the Powerset axiom implies Subset Collection (in CZF - Subset Collection) it suffices to show that the Powerset axiom implies Fullness. This proof is claimed to be obvious in many papers. I understand this may be so but I am still having some trouble with it. The difficulty I am having is deciding which set to apply the Powerset axiom to. For $$mv(B^A)$$ is only assumed to be a class (although the Powerset axiom is equivalent to it being a set this result typically comes later so I don't think that is neccesary.) I must admit I am new to proving these meta-set-theoretic results so I am aware the answer is likely right under my nose. I would be delighted for someone to offer some wisdom.

• Maybe it can be done in a different way but using that $mv(B^A)$ is a set immediately gives what you need, does not it? Dec 20, 2021 at 6:16
• I think so. But the proof that Powerset and mv(B^A) is a set are equivalent is not trivial. So for the papers by aczel stating that the proof in question is obvious leads me to believe that isn’t the avenue we should take. Dec 20, 2021 at 6:51
• Well I would say it is a one-liner: $mv(B^A)$ is the inverse image of $A\in\operatorname{pow}(A)$ under the map $\operatorname{pow}(A\times B)\to\operatorname{pow}(A)$ induced by the projection $A\times B\to A$. Dec 20, 2021 at 7:17
• So the powerset axiom combined with restricted separation one concludes $mv(B^A)$ is a set? This seems reasonably straight forward. I just find it strange that here www1.maths.leeds.ac.uk/~rathjen/acend.pdf proposition 2.3 precedes proposition 2.5. Which suggests to me that proposition 2.5 is not required for proposition 2.3. Dec 20, 2021 at 17:45
• In 2.5, deducing $mv(B^A)$ from Powerset is stated to be obvious, the whole proof is for deducing powerset from $mv(B^A)$. In 2.3, deducing Subset Collection from Powerset is stated to be obvious once one has that Subset Collection is equivalent to Fullness. Hence I believe the order in which these statements appear does not matter, since in both cases Powerset $\Rightarrow$ Fullness and even Powerset $\Rightarrow$ $mv(B^A)$ is a set is considered obvious enough so that nothing is said about proofs of these statements in either 2.3 or 2.5 Dec 20, 2021 at 21:33

(2022-04-06 EST: I once changed the terminology "Image" in my answer to "subimage." Thus please remember that "image" in the previous comments must be "subimages.")

A previous answer by aws pointed out how to prove Subset Collection from Powerset:

(…) 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 multi-valued function from $$a$$ to $$b$$. For example, if we had the powerset axiom, we could take $$c$$ to be the powerset of $$b$$.

Let me provide more details on aws's explanation. For sets $$a,b$$ and a multi-valued function $$R:a\rightrightarrows b$$ (which can be a proper class), call a set $$c$$ an subimage of $$R$$ if it satisfies

• For every $$x\in a$$, we can find $$y\in b$$ such that $$(x,y)\in R$$, and
• If $$y\in c$$, then there is $$x\in a$$ such that $$(x,y)\in R$$.

Their formal statements are: if $$R$$ is defined by a formula $$\phi(x,y)$$ then

• $$\forall x\in a\exists y\in c\ \phi(x,y)$$, and
• $$\forall y\in c\exists x\in a\ \phi(x,y)$$.

(If $$R$$ is a set, then $$\phi(x,y)$$ must be $$(x,y)\in R$$.)

You can see that if $$R$$ is functional (that is, if $$R:a\to b$$ is a function) then $$c$$ is exactly the image of $$R$$. Unlike functions, however, a subimage of a multi-valued function is not in general unique:

Example. Let $$a,b=3=\{0,1,2\}$$ and consider $$R=\{(0,0),(0,1),(1,1),(2,2)\}$$. You can see that $$R$$ is a multi-valued function from $$3$$ to $$3$$, but both of $$\{1,2\}$$ and $$\{0,1,2\}$$ are subimages of $$R$$.

As I explained in your previous question, the axiom of subset collection states the following:

For any class family of relations $$R_u\subseteq a\times b$$ parametrized by $$u$$, we can find a set $$c$$ such that if $$R_u\colon a\rightrightarrows b$$, we can find $$d\in c$$ such that $$d$$ is a subimage of $$R_u$$.

You can check that if $$\psi(x,y,u)$$ defines $$R_u$$ in the sense that $$(x,y)\in R_u$$ if and only if $$\psi(x,y,u)$$, then the above statement is just an informal rephrase of Subset Collection.

Then the Subset Collection is an immediate corollary of Powerset: observe that every subimage of $$R_u$$ is a subset of $$b$$, so $$c=\mathcal{P}(b)$$ witnesses Subset Collection.

Added 2022-04-06 EST: I found that the following one would be a simpler but equivalent statement for Subset Collection while pertaining to the notion of subimage:

For any $$a$$ and $$b$$, we can find a set $$c$$ full in subimages of multi-valued functions from $$a$$ to $$b$$, in the sense that if $$r\colon a\rightrightarrows b$$, then we can find a subimage $$d\in c$$ of $$r$$.

For the one direction, Subset Collection applied to $$u$$ implies the above statement. On the other direction, let $$R_u\colon a\rightrightarrows b$$ be a class multi-valued function with a parameter $$u$$. Then $$\mathcal{A}(R_u)\colon a\rightrightarrows a\times b$$. (See below for the definition of $$\mathcal{A}$$.) By Strong Collection, we have $$r$$ such that $$r$$ is a subimage of $$\mathcal{A}(R_u)$$, so $$r\subseteq R_u$$ and $$r\colon a\rightrightarrows b$$ (it follows from the lemma I stated below.)

Now let $$c$$ is full in subimages of multi-valued functions from $$a$$ to $$b$$, and if $$d\in c$$ is a subimage of $$r$$. Then it is straightforward to see that $$d$$ is a subimage of $$R$$.

You may also ask how to connect Fullness and Subset Collection in the way I referred. I found that the following notion is prevalent in proofs about Subset Collection and Fullness:

Definition. Let $$R:a\rightrightarrows b$$ be a multi-valued function. Define $$\mathcal{A}(R):a\rightrightarrows a\times b$$ by $$\mathcal{A}(R)=\{(a,(a,b)) \mid (a,b)\in R\}.$$

Then we can prove the following:

Lemma. Let $$R:a\rightrightarrows b$$ be a multi-valued function, then the following holds:

1. $$\mathcal{A}(R):a\rightrightarrows s \iff R\cap s: a\rightrightarrows b$$, and
2. $$\mathcal{A}(R):a\leftleftarrows s \iff s\subseteq R$$.

(The proof of my lemma is not too hard, but tedious. See my previous blog post or Lemma 2.8 of my preprint.)

We can see that $$R$$ is a subimage of $$\mathcal{A}(R)$$. In fact, $$R$$ is a maximal subimage (or, just the image) of $$\mathcal{A}(R)$$, in the sense that if $$s$$ is a subimage of $$\mathcal{A}(R)$$ then $$s\subseteq R$$. (Observe that $$s$$ is a subimage of $$\mathcal{A}(R)$$ if and only if $$\mathcal{A}(R):a\rightrightarrows s$$ and $$\mathcal{A}(R):a\leftleftarrows s$$ by definition.)

Then we can view the implication of Fullness from Subset Collection in the following way: consider the following (definable) collection of multi-valued functions: $$\mathcal{R} = \{\mathcal{A}(R) \mid R\in\operatorname{mv}(\sideset{^a}{}b)\}.$$

By Subset Collection, there is a collection $$C$$ of subimages of $$\mathcal{R}$$. For each $$r:a\rightrightarrows b$$, let $$s\in C$$ be a subimage of $$\mathcal{A}(r)$$, that is, we have $$\mathcal{A}(r):a\rightrightarrows s$$ and $$\mathcal{A}(r):a\leftleftarrows s$$. By the lemma, we have $$s\subseteq r$$. Hence $$C$$ is a full subset of $$\operatorname{mv}(\sideset{^a}{}b)$$.

• In your example how is $\{0,1\}$ an image when there does not exists a pair for $2$? Dec 22, 2021 at 8:57
• @ToucanIan Wrong example. I am going to replace it with a new one. Dec 22, 2021 at 9:33
• thank you for this detailed answer. This has helped tremendously. Dec 22, 2021 at 17:40
• Can you touch on the relevance/significance of $u$ here? It seems to just be along for the ride. Dec 24, 2021 at 17:29
• @ToucanIan I am not sure this technique is common in $\mathsf{CZF}$, but I am sure that this is not uncommon in the context of classical set theories. Dec 27, 2021 at 8:06