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

Question

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.

Answer 1

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.