Representation of the equality relation between hereditarily finite sets in weak set theories

Question

Consider General Set Theory ($ \mathsf { GST } $) axiomatized by the following.

1. Axiom of Extensionality: The sets $ x $ and $ y $ are the same set if they have the same members: $$ \forall x \forall y \bigl ( \forall z ( z \in x \leftrightarrow z \in y ) \rightarrow x = y \bigr ) \text . $$
2. Axiom of Adjunction: If $ x $ and $ y $ are sets, then there exists a set whose members are just $ y $ and the members of $ x $: $$ \forall x \forall y \exists z \forall w ( w \in z \leftrightarrow w \in x \lor w = y ) $$
3. Axiom Schema of Separation: If $ x $ is a set and $ \phi $ is any property, then there exists a set $ y $ containing just those elements $ z $ in $ x $ which satisfy the property $ \phi $: $$ \forall x \exists y \forall z \bigl ( z \in y \leftrightarrow z \in x \land \phi ( z ) \bigr ) \text . $$

It's rather straightforward to verify that $ \mathsf { GST } $ proves the existence of every hereditarily finite set; i.e. $ \mathsf { GST } \vdash \exists ! x \, \phi ( x ) $ for some formula $ \phi $ defining the intended set. Since the family of hereditarily finite sets gives a model $ \mathfrak M $ of $ \mathsf { GST } $, those are the only sets that provably exist. My question is the validity of the following statement:

If $ \mathsf { GST } \vdash \exists ! x \, \phi ( x ) $, $ \mathsf { GST } \vdash \exists ! x \, \psi ( x ) $ and $ \mathfrak M \models \forall x \forall y \bigl ( \phi ( x ) \land \psi ( y ) \rightarrow x = y \bigr ) $, then $ \mathsf { GST } \vdash \forall x \forall y \bigl ( \phi ( x ) \land \psi ( y ) \rightarrow x = y \bigr ) $.

My motivation is the fact that $ \mathsf { GST } $ is mutually interpretable with $ \mathsf { PA } $. For $ \mathsf { PA } $ (and even much weaker arithmetical theories like Robinson's) we know the following:

1. For every $ n \in \mathbb N $ there is a numeral $ \overline n $ in the language, which is interpreted as $ n $ in the standard model.
2. As $ \mathbb N $ gives a model of $ \mathsf { PA } $, natural numbers are the only objects that $ \mathsf { PA } $ proves to exist.
3. The equality relation between natural numbers is representable in $ \mathsf { PA } $ in the sense that for any $ m , n \in \mathbb N $, $ m = n $ implies $ \mathsf { PA } \vdash \overline m = \overline n $, and $ m \ne n $ impiles $ \mathsf { PA } \vdash \neg \, \overline m = \overline n $.

My question stated above is about representability of equality of hereditarily finite sets in $ \mathsf { GST } $. The similarities explained above make me feel that it must be true.

I understand that $ \mathsf { GST } $ might not be strong enough for proving the desired representability, and one might need to strengthen it (as the family of hereditarily finite sets gives a model for $ \mathsf { ZFC } $ without infinity, we can see that much stronger candidates are available). But since very weak arithmetical theories are enough for proving representability of equality for natural numbers, I suspect that no additional strength would be necessary for set theoris either.

---

P.S. I've only seen the claim that $ \mathsf { GST } $ and $ \mathsf { PA } $ are mutually interpretable in a couple of sources. I don't know of any sources where a proof can be found. I'd really appreciate it if someone could give a reference in the comments section.

Answer 1

This question is based on a misunderstanding of the situation already in $\mathsf{PA}$: equality is representable in $\mathsf{PA}$ only for terms, or at the very least relatively simple formulas. To see this consider, given an arbitrary sentence $\varphi$, the formula (modulo obvious abbreviations) $$\psi(x)\equiv(x=0\wedge\varphi)\vee(x=1\wedge\neg\varphi).$$ Then regardless of what $\varphi$ is we have $\mathsf{PA}\vdash\exists!x\psi(x)$, but if $\varphi$ is independent of $\mathsf{PA}$ then $\mathsf{PA}$ cannot decide whether or not (say) $\forall x(\psi(x)\leftrightarrow x=0)$ holds.

Similarly, only a weak form of "representability of equality" will hold in $\mathsf{GST}$. In fact, your guess must fail for any incomplete theory (with at least "two incompatible element-defining formulas" in the obvious sense).