Why do definitions need to be ‘proved’ to work

definition

I am reading Elements of set theory by Enderton. I am having a conceptual difficulty with why it seems that certain definitions almost have to be 'proved' to work?

Specifically, I am reading about defining an ordered pair set such that $$\langle x,y \rangle = \langle u,v \rangle$$
are identical objects.

He describes how it is defined as:

$$\langle x,y \rangle = \{\{x\},\{x,y\}\} $$

and also describes various definitions that do not work, such as $$\langle u,v \rangle = \{x,y\}$$

What I don't understand is why either of these are necessary. In his final remark on the section he states 'The preceeding theorem lets us unambiguously define the first coordinate of $\langle x,y \rangle$ to be $x$, and the second coordinate to be $y$'. If this is the ultimate goal, why does it matter that we 'show' the definition works in this way? Why can't we simply say, 'Whenever something of the form $\langle x,y \rangle$ is used, it is an ordered pair and $x$ is the first coordinate and $y$ is the second coordinate.'?

I am only just learning more formal mathematics now, such as the axiomatic approach and so forth, so apologies if I am missing something obvious.

Best Answer

We need to prove that something with the desired properties actually exists. For example, consider the statement:

We write "$\mathfrak{Q}$" to denote the set of all sets not containing themselves.

This "makes sense" linguistically, but hides a crucial assumption: that the set of all sets not containing themselves actually exists. And in fact it does not - this is the conclusion of Russell's paradox.

So we could talk "non-specifically" about some arbitrary ordered pairing notion, but we need to first prove that such a thing exists (and incidentally, even expressing "there is a pairing operation" precisely in the language of set theory is nontrivial, since this pairing operation isn't literally a function - its domain is too large). And the easiest way to show that (in fact, the only way I know) is to build one.


It might be a good idea at this point to consider situations where we want a pairing operator with certain additional properties, where it's not at all clear that such a thing exists. The standard example of such a thing is a flat pairing function.

Related Question