Is ZFGC, minimally modified to allow two Quine atoms instead of the empty set, synonymous\bi-interpretable with ZFGC?

Question

Working in $\sf ZFGC$, remove Foundation, stipulate the existence of exactly two Quine atoms. Restrict Separation to fulfillable formulas, i.e. $\{x \in A \mid \phi \}$ exists as long as $\phi$ holds of at least one $x \in A$. And make a similar adjustment on Replacement, so $\{f(x) \mid x \in A \}$ exists as long as $f(x)$ exists for at least one $x \in A$. We replace the axiom of Foundation by an axiom asserting the non-existence of descending membership sets all elements of which are not Quine atoms. Formall, this is: $$ \neg \exists h: \forall x \in h \, (\exists y \in h \ (y \in x) \land x \neq \{x\})$$. The theory ought to prove that every set is an element of some $ V_\alpha$ where $V_0 = \{x \mid x=\{x\}\}$, the rest of stages $V_\alpha$ are constructed through iterative powering over $V_0$ in the usual manner.

Is this theory bi-interpretable with $\sf ZFGC$?

Is this theory synonymous with $\sf ZFGC$?

Note: $\sf GC$ is the axiom of Global Choice, formally stated by adding a new primitive total unary function $C$ to the signature of $\sf ZF$, then axiomatizing:

$\forall x : (\exists y: y \in x) \to C(x) \in x \\\forall x: (\forall y: y \not \in x)\to C(x)=x$

Of course, in the theory defined above $\sf GC$ simply turns to $\forall x: C(x) \in x$.

Answer 1

$\sf ZFGC$ is synonymous with the theory you defined, with an additional statement $\varphi$.

Define $x \in' y \Leftrightarrow x \in y$, except if $y$ is $\varnothing$, $\{\varnothing\}$, $\{\{\varnothing\}\}$, or a natural number; make $\varnothing$ and $\{\varnothing\}$ Quine atoms (so $\varnothing \in' \varnothing$ and $\{\varnothing\} \in' \{\varnothing\}$), $\{\{\varnothing\}\}$ into $0$ (so $x \in' \{\{\varnothing\}\} \Leftrightarrow x \in 0$), and $n$ into $n+1$ ($x \in' n \Leftrightarrow x \in n+1$). Define $C'(x) = C(x)$, except if $x$ is $\{\varnothing,\{\varnothing\}\}$, $\{\{\varnothing\}\}$ or a natural number; $C'(\{\varnothing,\{\varnothing\}\}) = \varnothing$, $C'(\{\{\varnothing\}\}) = C(0)$ and $C'(n) = C(n+1)$ (because the $\in'$ elements of $n$ are the $\in$ elements of $n+1$). Define $\varphi$ as $C(\{\varnothing,\{\varnothing\}\}) = \varnothing$.

In the other direction, define $a_1$ as $C'(\{x | x \in' x\})$, and $a_2$ as the Quine atom that is not $a_1$. Define $x \in y \Leftrightarrow x \in' y$, except if $y \in' y$ or $y$ is a natural number; if $y$ is a Quine atom, $x \in y$ iff $x = a_1$ and $y = a_2$, $x \in 0$ iff $x = a_2$, $x \in n+1$ iff $x \in' n$. Define $C(x) = C'(x)$, except if $x$ is $\{a_1,a_2\}$ or a natural number; $C(\{a_1,a_2\})$ is $a_1$ if $\varphi$ is true and $a_2$ otherwise, $C(0) = a_2$, $C(n+1) = C'(n)$.

These definitions are inverses of each other, and the axioms are all equivalent, if we're careful about the construction of $\mathbb{N}$. Define $0$ as $\{\varnothing,\{\varnothing\}\}$ (from $\in$) or $\{a_1,a_2\}$ (from $\in'$), and $S(n) = n \cup \{n\}$. None of these transitively contain $\{\{\varnothing\}\}$. We can't quite use these, because they can contain each other, but if we actually use the singletons of these numbers ($\{0\}$, $\{1\}$, $\{2\}$) as the natural numbers, it works. These numbers don't contain $\{\{\varnothing\}\}$ or each other, and also aren't $\varnothing$, $\{\varnothing\}$, $\{\{\varnothing\}\}$, or Quine atoms, so all of the elements of natural numbers are completely unchanged (except the Quine atoms). This implies that Foundation is still true, and also that which natural number a set is (or whether it is a natural number at all) will not be "unexpectedly" changed.

The theory you defined is synonymous with itself with an additional statement $\varphi$. Define $C''(x) = C'(x)$, except $C''(\{0,1\})$ is $0$ if $\varphi$ is true and $1$ otherwise, and $C''(\{n+1,n+2\}) = C'(\{n,n+1\}) + 1$. In the other direction, define $C'(x) = C''(x)$, except $C'(\{n,n+1\}) = C''(\{n+1,n+2\}) - 1$, and define $\varphi \Leftrightarrow C'(\{0,1\}) = 0$. These definitions are inverses of each other. (This paragraph could be "merged" into the previous ones, to avoid having to define a third global choice function $C''$, but I think it's probably easier this way...?)

So your theory is synonymous with $\sf ZFGC$.