# What would be the effect of replacing Separation by Injective Replacement?

Let "Injective Replacement" be the following schema:

If $\phi(x,y)$ is a formula in which only x,y occur free, and only free, then:

$\small \forall A \ [\forall x \in A \exists y (\phi(x,y)) \wedge \forall x,y,z,u (\phi(x,y) \wedge \phi(z,u) \rightarrow (x=z \leftrightarrow y=u)) \rightarrow \exists B \ \forall y \ (y \in B \leftrightarrow \exists x \in A (\phi(x,y))]$

In English, we require that the replacement function be an injection.

Now if we replace the Separation scheme in Zermelo's set theory, $Z$, by the above axiom schema, call the resulting theory "Injective Zermelo", $Z^{inj}$, then:

1. Would $Z^{inj} + GCH$ interpret $ZF$ ?

2. Can $Z^{inj} \pm C$ prove Cantor's theorem for an arbitrary power set?

3. What is the exact consistency strength of $Z^{inj} \pm C$?

Note: the rest of axioms of $Z^{inj}$ are:

Extensionality: $\small \forall A,B \ (\forall z (z \in A \leftrightarrow z \in B) \rightarrow A=B)$

Pairing: $\small \forall A,B \ \exists x \ \forall y \ (y \in x \leftrightarrow \ y=A \lor y=B)$

Union: $\small \forall A \ \exists x \ \forall y \ (y \in x \leftrightarrow \ \exists z \in A (y \in z))$

Power:$\small \forall A \exists x \ \forall y \ (y \in x \leftrightarrow \ \exists \forall z \in y (z \in A))$

Regularity: $\small \exists x \in A \rightarrow \exists x \in A \ \forall y \in A (y \not \in x)$

Choice: $\small \forall x \ \exists y \ (Ord(y) \wedge x \ is \ equinumerous \ to \ y)$

where "equinumerous to" stands for existence an injection in either direction between x and y.

"ord" stands for Von Neumann ordinal defined as a transitive set of transitive sets.

Note: the original question was asked with the formula in injective replacement being:

$\small [\forall x,y,z,u (\phi(x,y) \wedge \phi(z,u) \rightarrow (x=z \leftrightarrow y=u)) ] \rightarrow \forall A \exists B \ \forall y \ (y \in B \leftrightarrow \exists x \in A (\phi(x,y))$

However, I've corrected it to the one above, since that was my original primary intention.

Replacing separation with injective replacement is equivalent to adding the usual replacement axiom, and so your theory $Z^{inj}$ is the same as ZF. From this, you can easily answer all your questions.

The first thing is to note [thanks to Emil in the comments below] is that because you have stated your injective replacement axiom to concern only partial functions, you can deduce the usual separation axiom. If $A$ is any set and you want to show $\{a\in A\mid \psi(a)\}$ exists, then let $\phi(x,y)$ be the assertion $x=y\wedge\psi(x)$. That is, we map $x$ to itself, if $\psi(x)$ holds, and otherwise do nothing. This is injective, and the replacement of $A$ under this function is the desired subset.

Next, suppose that you have an instance of ordinary replacement, so every set $x$ has a unique $y$ with $\phi(x,y)$. Consider a new instance of injective replacement: define that $\psi(x,y')$ holds, if $y'=\langle x,y\rangle$, where $\phi(x,y)$ holds. That is, we replace the witness $y$ with the pair $\langle x,y\rangle$, which makes it injective. Applying your injective replacement axiom, for any set $A$ we get the set of pairs $\langle x,y\rangle$ with $\phi(x,y)$ for $x\in A$ exists. Now, by the usual Zermelo axioms, we can project onto the second coordinate (this does not need replacement), and get the desired instance of replacement.

Update. Your revised question, where you state injective replacement only for total functions, is much more difficult. Of course, my argument above still shows that all one needs is sufficient separation to project to the second coordinates of a set of ordered pairs. This doesn't use replacement at all, and indeed even very weak set theories such as KP, with only $\Delta_0$-separation, can prove this.

But if you insist on throwing out separation completely, then your theory seems to be too weak to do much with at all. I don't see even how to prove even that $A\cap B$ exists. Indeed, how can one prove even that one can remove a point from a set, that is, that $A\setminus\{a\}$ exists? One might argue that without any separation axiom at all, one might not really have a set theory.

If we add a certain version of the axiom of choice, however, then we can make progress. Consider the axiom: for any function $f$ mapping elements $a\in A$ to disjoint nonempty sets, there is a selector set, a set containing exactly one element from each $f(a)$. If we have this, then consider a modified version of the argument above, where we form the set of pairs $\langle x,\{y\}\rangle$ where $x\in A$ and $\phi(x,y)$. The set of these pairs is a function $f$, and so by choice there is a selector set $Y$, which has exactly one element from each $f(x)$, which is to say that $Y$ is precisely the set of $y$ for which $\phi(x,y)$ for $x\in A$. So we have verified the replacement axiom.

I don't see at the moment how to make the argument work with the other more usual forms of the axiom of choice.

• Separation for $\psi(x)$ follows from injective replacement with $\phi(x,y)$ being $x=y\land \psi(x)$, doesn't it? – Emil Jeřábek Feb 7 '18 at 11:23
• @EmilJeřábek Oh, I see, he is using partial functions, so you are right. Sometimes one states the replacement axiom as the assertion: if everybody in $A$ has a unique witness, then you can replace them with those witnesses. But the way he states it, it could be that some people in $A$ have no witnesses. – Joel David Hamkins Feb 7 '18 at 11:30
• I see, I need to correct the question then. Since I meant $A$ to be the domain of $\phi$. – Zuhair Al-Johar Feb 7 '18 at 12:07
• To my way of thinking, it is not necessarily sensible to speak of $\beth_i$ or GCH or even of the ordinals in a theory in which one cannot necessarily prove basic set-theoretic properties like low-complexity instances of separation. The problem is that basic facts about these quantities may simply not hold in the weak theory, and the usually equivalent formulations of those properties may no longer be equivalent. – Joel David Hamkins Feb 7 '18 at 19:05
• If you have injective replacement (for total functions), and if any two sets have an intersection, then you have full separation: in order to construct $\{x\in A:\phi(x)\}$, use two instances of i.r. to get $B=\{0\}\times A$ and $C=\{\langle0,x\rangle:x\in A\land\phi(x)\}\cup\{\langle1,x\rangle:x\in A\land\neg\phi(x)\}$, take $B\cap C=\{\langle0,x\rangle:x\in A\land\phi(x)\}$, and then $\{x\in A:\phi(x)\}$ follows by yet another instance of i.r. – Emil Jeřábek Feb 7 '18 at 22:57