>>14132370You're using Kuratowski ordered pairs with von Neumann ordinals. However, Kuratowski's construction is only intended for ordered pairs on set-theoretic elements. However, you're not just asking for a theory of ordered pairs of naturals like (0,1), you also want sets of naturals, like {1,2}. You also want the set theoretic properties of your model to carry over as expected in your theory of sets of naturals, when using von Neumann ordinals.
This is outside of the scope of both the Kuratowski and von Neumann constructions. Even if it weren't, they weren't designed with each other in mind, so you'd probably still have issues. The resulting conflict you see is known, and documented at
>https://en.wikipedia.org/wiki/Ordered_pair#Kuratowski's_definitionInstead, build your own model! Suppose your theory has, in addition to the usual equality relation between pairs of naturals, and the equality between sets of naturals, an additional equality between pairs and sets...that for some reason is always false. But that's fine, because you're autistic and want all these equalities to hold iff it holds set theoretically in the underlying model, okay.
Say, for simplicity, we use Hausdorff's construction, but using "1" and "2" to denote pair indices isn't helpful, since we have naturals in our theory, so let's call the indices "first" and "second". But then what sets are these? For Hausdorff to work, we need to keep them distinct from the naturals.
We can do something like:
first := Ø
second := {Ø}
and then do a von Neumann-like construction for the naturals, but starting at {Ø,{Ø}} instead of Ø. This set would correspond to 2 in the usual construction. We're just shifting it over by two.
This should give you what you want. In this model, your examples should be:
(0,1) := {{0,first},{1,second}} := {{{Ø,{Ø}},Ø},{{Ø,{Ø,{Ø}}},{Ø}}}
{1,2} := {{Ø,{Ø,{Ø}}}, {Ø,{Ø,{Ø,{Ø}}}}}
