$\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}$?
Best Answer
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}$.