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

  • 2
    $\begingroup$ en.wikipedia.org/wiki/… $\endgroup$ – Asaf Karagila Aug 1 '19 at 10:44
  • $\begingroup$ @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]$. $\endgroup$ – Evan Aad Aug 1 '19 at 10:53
  • 3
    $\begingroup$ What if $\varphi(x,y)\equiv y=y$? Or, for immediate Russel-fun, $y\notin y$? $\endgroup$ – Hagen von Eitzen Aug 1 '19 at 11:11
  • 2
    $\begingroup$ 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. $\endgroup$ – 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}$.


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.