Elementary Set Theory – Why Accept Kuratowski’s Definition of Ordered Pairs?

definitionelementary-set-theory

I've been struggling understanding Kuratowski's definition of ordered pairs.
I understand what it means but I don't see why I should accept it.
I've seen this question and this one, most importantly — through reading the wiki page I've realised one thing.

The only reason $(a,b)=\{\{a\},\{a,b\}\}$ is accepted is because it satisfies

$(a,b)=(c,d) \iff (a=c) \land (b=d)$

Am I not misunderstanding this?
If I can come with my own exotic definition which satisfies the above iff statement, would it be accepted?

Best Answer

We accept this definition because it works, and it works very well.

However do note that almost nobody cares about the actual encoding of ordered pairs, and in most cases set theorists don't really care either. You just want a definition which satisfies the property which you have quoted.

I can't recall any substantial proof in set theory which actually refer to this definition of ordered pairs. Instead we just use the fact that there is some $\varphi(x,y,z)$ which is true if and only if $z$ represents the ordered pair $(x,y)$. Had I chose a different encoding, the proof would stay the same.

So why do we use it? Well, it tells us that set theory is strong enough to support an internal definition of ordered pairs which is another "thumbs up" in its favor as a foundational theory. But also we use it because it was there when we needed such definition, and once you have a working machine you don't really bother replacing the cogs which work perfectly.

Note that on its own, the object of an ordered pair is very uninteresting. So we don't really bother with finding a "better" definition, because nobody really cares about how you encode. We just want to know that it exists within our mathematical universe, and if our mathematical universe is based on set theory (in one way or another) then we want to know that we don't need an extra type in the world in order to have ordered pairs.