# Am I allowed to realize one object twice within one set-theory?

Say I consider a set theory with the Axioms of Extensionality and the Axiom of Pairing.

As I understand it, stating the axiom allows me to make a definition like

$$(a,b):=\{\{a\},\{a,b\}\}$$

and work with that $(a,b)$ in the context of my theory. Pairing says "it exists" (I can write it down with my language) and Extensionality says the abstract idea of it is unique as a set.

Is that way of thinking correct? Is that the purpose?

Because (if I know $a$ and $b$ exists and since I know what set brackets are) in a way I feel the set $\{\{a\},\{a,b\}\}$ existed already before the existence of a pair was guaranteed by the axiom - the possibility of nesting of sets as for the definition seems to be apriori to me, I asked a related question here.

Secondly, since there are more set-constructions of the ordered pair, like say

$$(a,b)':=\{b,\{a,b\}\}$$

as an alternative, I wonder:

Am I allowed to realize the ordered pair twice in one theory?

Then I could for example put ordered pairs as elements of ordered pairs of the second type and so on.

Is there really only one realization of the ordered pair in say ZFC or are there in fact all thinkable versions in the theory and we just choose one if we prove stuff about the abstract thing (which implies that the statements are true for all models)?

Or another idea: Should I view the whole thing in a way that I only define the thing using a concrete relization so that I can prove stuff about the "actual" abstract object, which is really only implicitly postulated to exist in the axiom. If that point of view ist true then I don't really see what the real difference of two realizations can be.

-
You can have many different definitions that achieve the same end, namely, an "object" that distinguishes between the "first component" and the "second component". You should not use the same notation to denote two different constructions, and most of the time you don't care what the construction actually is: you want to use its "universal property" rather than its actual construction in the proofs. Then, it doesn't matter if you and I are using the exact same definition of the object, we just care that we are using the universal property of the object. –  Arturo Magidin Jul 7 '12 at 22:39
J.H. Conway complained at the end of On Numbers and Games that mathematicians were too concerned with the specific implementation of objects such as ordered pairs. I wrote some slightly more detailed comments about this, which are too long to reproduce here. –  MJD Jul 8 '12 at 0:39

I think I wrote this as an answer to one of your previous questions and then I deleted it (I think Henning wrote another answer incorporating the point I was making).

We hardly make actual use of the properties of an ordered pair beyond the fact that it is actually a collection of two elements which may not be distinct and the order does matter.

Much like the proofs in real analysis do not depend on how you interpret the real numbers within a model of ZFC, but rather on the properties of the structure, a similar thing can be said here.

What we write when we write a proof is more of a schema for a proof. We consider abstract (non-pure set) objects and we say "plug the definition here, and insert the definition there". Ordered pairs make an excellent example as they appear almost everywhere. However there are only a few places where you actually care for the contents of the interpretation of the ordered pair.

Most of the time you care about the fact that an ordered pair allows you to distinguish between the two elements, even if they are the same (e.g. $\langle a,a\rangle$). As long as you have a way of telling which is the left coordinate and which is the right there is no real danger in replacing the definition.

However you should remember, again, that every time you are using an instance of the replacement axiom schema in contexts of ordered pairs then the axiom you are using may be different; but the logic behind the proof remains the same.

-
I refer to this question in my first sentence. 10k users can also read my deleted answer and the comments ensued. –  Asaf Karagila Jul 7 '12 at 22:36
Okay, so if I read this correctly, you imply that one could in principle also just not make a definition like $(a,b):=\{\{a\},\{a,b\}\}$ but work everything out purely in terms of chains of already given logic language symbols. And then the axioms are only the additional inference rules I need to get from $A$ to $B$ in that derivation. –  NikolajK Jul 7 '12 at 22:39
@Nick: Consider the proof with a variable, $\varphi(a,b,x)$ which says that $x$ is an ordered pair $\langle a,b\rangle$. We almost always use the properties of the ordered pair, not its realization, so we can simply write formulae that when given $\langle a,b\rangle$ return $a$ or $b$ as objects (e.g. $\varphi(u,v)$ says that $u$ is an ordered pair and $v$ is the element in the left coordinate), then the actual interpretation doesn't matter, what matters is that we have a formula defining the "model of an ordered pair" up to isomorphism. –  Asaf Karagila Jul 7 '12 at 22:44
I guess that means yes? –  NikolajK Jul 7 '12 at 22:56
@Nick: In a way, yes. I just wanted to make my point perhaps clearer, but I can get unclear when writing relatively long answers. –  Asaf Karagila Jul 7 '12 at 22:58

You can realize ordered pair as many ways as you want, but what's the point? What matters is not how you implement the ordered pair but the fundamental property that an ordered pair ought to satisfy, namely that $(a, b) = (a', b')$ if and only if $a = a'$ and $b = b'$.

-
If you want to prove the claim $1\in\langle 0,1\rangle$ then you do care about the interpretation. –  Asaf Karagila Jul 7 '12 at 22:31
Okay, but why would you ever want to do that? –  Qiaochu Yuan Jul 7 '12 at 22:31
I am really bored, or I want to post on MathOverflow that ZFC is bad because it proves that $1\in\langle 0,1\rangle$ and get a lot of upvotes... :-) –  Asaf Karagila Jul 7 '12 at 22:32
@Nick: The standard interpretation (or if you wish to think about von Neumann ordinals) has $1=\{\varnothing\}$ and the Kuratowski definition of $\langle 0,1\rangle$ is $\{\{0\},\{1\}\}=\{\{\varnothing\},\{\{\varnothing\}\}\}$. Note that this implies that $1=\{0\}$ and therefore $1\in\langle 0,x\rangle$ for all $x$. In fact $\{1\}=\langle 0,0\rangle$! –  Asaf Karagila Jul 7 '12 at 22:48
@AsafKaragila: That's really awesome! (Doesn't the Kuratowski definition contain a set with two elements, i.e. is there a $0$ missing next to the $1$ in the $\{\{0\},\{1\}\}$-expression?) –  NikolajK Jul 7 '12 at 22:54