3
$\begingroup$

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

$\endgroup$
4
  • 2
    $\begingroup$ en.wikipedia.org/wiki/… $\endgroup$
    – Asaf Karagila
    Commented Aug 1, 2019 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
    Commented Aug 1, 2019 at 10:53
  • 3
    $\begingroup$ What if $\varphi(x,y)\equiv y=y$? Or, for immediate Russel-fun, $y\notin y$? $\endgroup$ Commented Aug 1, 2019 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
    Commented Aug 1, 2019 at 11:20

1 Answer 1

7
$\begingroup$

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}$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .