2
$\begingroup$

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.

$\endgroup$
0

1 Answer 1

4
$\begingroup$

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).

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Commented Oct 18, 2021 at 19:34
  • $\begingroup$ @MohsenShahriari Yes, that looks right to me. $\endgroup$ Commented Oct 18, 2021 at 19:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.