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

Question

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.

Answer 1

(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)$.