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

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.

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).
• Thanks for pointing out my misunderstanding. So the "real" analogous phenomenon would be for theories like $\mathsf { GST }$ in a language extended with a constant symbol for the empty set and a function symbol for adjunction, and representability of equality for the closed terms in that theory. That way there will be a closed term for any hereditarily finite set, and the representability of equality for them will hold. Am I right? Commented Oct 18, 2021 at 19:34