Is adding abstractions (in the below mentioned manner) over $ZFC$ inconsistent? if not then does it result in increment of consistency strength?
The idea is to add a new primitive binary relation "is abstracted from", denoted as: $``\curvearrowleft"$, to the language of set theory (first order logic with equality and membership) and we add the following extensionality and comprehension axioms for abstractions.
- Extensional abstractions: $\forall \zeta \eta \ [\forall x (\zeta \curvearrowleft x \leftrightarrow \eta \curvearrowleft x) \to \zeta=\eta]$
In English: Abstractions abstracted from the same objects are identical.
- Abstracting scheme: If $R$ is a binary relation symbol defined after a formula in the language of set theory that doesn't use the symbol $``\zeta"$, then:
$ R \text{ is equivalence relation } \to \forall x \ \exists \zeta \ \forall y (\zeta \curvearrowleft y \leftrightarrow y \ R \ x)$
is an axiom.
So to re-iterate my questions:
Is the above addition on top of $ZFC$ consistent?
If Yes, would it increase the consistency strenght or not?
if we unleash the abstracting schema for abstractions to come from any equivalence relation, i.e. just remove the restriction to language of set theory; would that result in an inconsistent theory?