# Replacing “function” by “binary relation” in ZFC's axiom schema of replacement

$$\text{ZFC}$$'s axiom schema of replacement states, informally, that whenever $$\varphi$$ is a function and $$s$$ is a set, the image $$\varphi[s] = \big\{y :\ \exists x \in s.\ \langle x,y\rangle \in \varphi\big\}$$ is a set. Suppose we don't require $$\varphi$$ to be a function but an arbitrary binary relation. Is the resulting theory still $$\text{ZFC}$$?

More precisely, the axiom schema of replacement is the following collection of sentences in the language of first order logic:

For every

• well-formed formula $$\varphi$$ in the language of first-order predicate logic,
• $$5$$ distinct variables $$s, t, x, y, z$$ of the language of first-order predicate logic such that the free variables of $$\varphi$$ $$\subseteq \{x,y\}$$,

$$\Big(\forall x\exists y\big(\varphi \wedge \forall z(\varphi[z/y] \implies z = y)\big)\Big) \implies \Big(\forall s\exists t\forall y\big(y \in t \iff \exists x(x \in s \wedge \varphi)\big)\Big)\tag{*}$$

Denote by $$\text{ZFC}'$$ the collection of sentences of first order predicate logic that are determined by the axioms and axiom schemas of $$\text{ZFC}$$ without the axiom schema of replacement, and denote by $$R'$$ the collection of sentences of first order predicate logic that result from the modified axiom schema of replacement obtained by omitting the antecedent in $$(*)$$.

Then every theorem of $$\text{ZFC}$$ is a theorem of $$\text{ZFC}' \cup R'$$. Is the converse true? In other words, is every theorem of $$\text{ZFC}' \cup R'$$ a theorem of $$\text{ZFC}$$?

• en.wikipedia.org/wiki/… – Asaf Karagila Aug 1 '19 at 10:44
• @AsafKaragila: Thanks! This is new to me. However, I think the axiom schema of collection described in the Wikipedia article is not quite the axiom schema R' I described in my question, since R' states, informally, that whenever $\varphi$ is a binary relation, the following is a set: $\varphi[s] = \big\{y :\ \exists x \in s.\ \langle x,y\rangle \in \varphi\big\}$, whereas the axiom schema of collection, if I understand correctly, says, informally, that whenever $\varphi$ is a binary relation, there exists a certain subset of $\varphi[s]$, but it needs not be all of $\varphi[s]$. – Evan Aad Aug 1 '19 at 10:53
• What if $\varphi(x,y)\equiv y=y$? Or, for immediate Russel-fun, $y\notin y$? – Hagen von Eitzen Aug 1 '19 at 11:11
• I didn't notice that, and in that case, @Hagen points out the obvious flaw, it is easy to arrange for a relation whose range on any singleton is a proper class. In that case, Collection is exactly why you want to say that there is a "set restriction" kind of, to avoid that situation. – Asaf Karagila Aug 1 '19 at 11:20

It is a simple task to show in $$\mathsf{ZFC'}$$. that $$\tag1\exists s\,\exists x\,x\in s.$$ Let $$\varphi$$ be the well-formed formula $$y\in y.$$ Then $$\forall s\,\exists t\,\forall y\,(y\in t\leftrightarrow\exists x\,(x\in s\land \varphi),$$ specialized to an $$s$$ as in $$(1)$$, gives us $$\exists t\,\forall y\,(y\in t\leftrightarrow \exists x\,(x\in s\land y\notin y).$$ By $$(1)$$, this becomes $$\exists t\,\forall y\,(y\in t\leftrightarrow y\notin y).$$ So for such $$t$$, $$\forall y\,(y\in t\leftrightarrow y\notin y)$$ and specialized to $$t$$, $$t\in t\leftrightarrow t\notin t.$$ I sincerely hope that this is not a theorm of $$\mathsf{ZFC}$$.