# Is the following injectivity schema provable in ZF-foundation?

Is the injectivity scheme present in the below axiomatic exposition of a first-order set theory provable in $\text{ZF}$?

Extensionality: $\forall A,B \ [\forall x \ (x \in A \leftrightarrow x \in B) \to A=B]$

Empty: $\exists O \ \forall x \ (x \not \in O)$

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

Intersection: $\forall A \ \exists I \ \forall x (x \in I \leftrightarrow \exists y \in A (x \in y) \ \wedge \forall y \in A (x \in y))$

Injectivity: If $\phi(x,A)$ is a formula in which the symbols $x", A"$ occur free and only free and in which the symbol $B"$ doesn't occur, and $\phi(x,B)$ is the formula obtained from $\phi(x,A)$ by merely replacing all occurrences of the symbol $A"$ by the symbol $B"$, then all closures of:

$\forall wf(A) \ [\forall x \ (\phi(x,A) \to wf(x))] \wedge \\ \forall A,B \ \big{(} \forall x (\phi(x,A) \leftrightarrow \phi(x,B) ) \to A=B\big{)} \\ \to \forall A \ \exists B \ \forall x \ \big{(}x \in B \leftrightarrow \phi(x,A) \big{)}$

are axioms.

where $wf$ stands for the predicate "is well founded", defined as:

$$wf(x) \iff \not \exists c \ ( x \in c \wedge \forall m \in c \ (\exists n (n \in m \wedge n \in c)))$$

Infinity: $\exists N \ [\emptyset \in N \wedge \ \forall x \in N (x \cup \{x\} \in N)]$

The point of this question is that the above theory (if consistent) then it proves all axioms of $\text{ZF-Foundation}$, and so it interprets the whole of $\text{ZFC}$, Injectivity would prove injective replacement of elements of well-founded sets by well-founded sets, Pairing trivially follow, and Separation follows from having intersection with injective replacement, of course Power trivially follows from Injectivity. However, I couldn't manage to prove the injectivity schema in $\text{ZF-Foundation}$. Which raises suspicion about its consistency with the other axioms.

There is another related aside question, should this prove to be consistent relative to $\text{ZF}$, what should we regard the non-well founded objects that must exist in this theory? Are they sets? if they are not sets? then why did they play a rule in the construction of well-founded set? In a more general sense: If it proves very useful to have non-well founded objects to construct well-founded sets, then how are we to consider those non-well founded objects, would they be considered as "sets"? or still as another kind of objects?

Afternote: The Injectivity axiom schema is inconsistent. Andreas Blass has shown that we can have a set of all ordinals $\geq 2$ and singletons of elements a set $A$, for any arbitrary set $A$, now take $A=\emptyset$, and we get the set of all ordinals $\geq 2$, take its union and then we can get the set of all ordinals, which is inconsistent. I don't think this can be easily fixed.

• Can you elaborate on your after note? I'm not sure that I get what it's saying. Mar 5, 2018 at 17:07

No, some instances of the injectivity scheme are refutable in ZF. For example, let $\phi(x,A)$ say "either $x$ is an ordinal $\geq2$ or $x=\{y\}$ for some $y\in A$. (To verify the second hypothesis of injectivity for this $\phi$, use that an ordinal $\geq2$ is never a singleton.)
• Perhaps more simply, we could take $\phi(x, A)$ to be $x \not \in A$. Then the Injectivity axiom gives us complements. Taking the complement of the Empty set gives us a universal set, and having Separation available as well gives us the paradoxical Russell set. Mar 5, 2018 at 19:01
• @SridharRamesh all $\{y\}$ for each $y \in A$ would be well founded as long as $A$ is well founded, so take $\phi(x,A)$ to be the formula $(x \text{ is an ordinal } \geq 2 \lor \exists y \in A (x=\{y\}))$ then both hypothesis in the antecedent of injectivity would be satisfied for that formula. There is no need for foundation to prove that (I suppose). Mar 6, 2018 at 13:17