Why do definitions need to be 'proved' to work?

Question

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.

Answer 1

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.

Answer 2

Definitions do not need proof. Constructions do, if they are to satisfy a requirement.

Definition: An ordered pair is an object $P(x,y)$ such that $P(x_1,y_1)=P(x_2,y_2)$ iff $x_1=x_2$ and $y_1=y_2$.

In principle, ordered pairs need not exist. But they do:

Theorem: $P(x,y)=\{\{x\},\{x,y\}\}$ is an ordered pair.

On the other hand, not all constructions work:

Theorem: $P(x,y)=\{x,y\}$ is not an ordered pair.