The usual definition of an ordered pair $\langle x,y \rangle$ is $\{\{x\},\{x,y\}\}$, but how may one define that using purely first-order logic contructs (variables, logical operations, quantifiers) and the $\in$ relation?
After reading the wiki, which defines the properties:
- $x$ is the first coordinate of $p$: $\forall A[A \in p \rightarrow x \in A]$
- $x$ is the second coordinate of $p$: $\exists A[A \in p \land x \in A] \land \forall A \forall B[A \in p \land B \in p \rightarrow (A \neq B \rightarrow x \notin A \lor x \notin B)]$
I arrived at the following definition:
$$
\langle x,y \rangle = p \leftrightarrow \forall A[A \in p \rightarrow x \in A] \land \exists A[A \in p \land y \in A] \land \forall A \forall B[A \in p \land B \in p \rightarrow (A \neq B \rightarrow y \notin A \lor y \notin B)]
$$
However, this definition would also consider $\{\{x\},\{x,y\},\{x,z\}\}$ or $\{\{x\},\{x,y,z\}\}$ as representing that ordered pair, and as such, it is not unique.
So, how may one define ordered pairs using only first-order logic such that only the set $\{\{x\},\{x,y\}\}$ represents the ordered pair $\langle x,y \rangle$?
Best Answer
Here is a more or less mechanical way to do the expansion. First, $p = \langle x, y \rangle = \{ \{ x \}, \{ x, y \} \}$ is equivalent to: $$\forall a, a \in p \leftrightarrow (a = \{ x \} \vee a = \{ x, y \}).$$ Now, we can (by manual recursion) replace $a = \{ x \}$ with: $$\forall b, b \in a \leftrightarrow b = x.$$ Similarly, replace $a = \{ x, y \}$ with: $$\forall b, b \in a \leftrightarrow (b = x \vee b = y).$$ Therefore, substituting in, we get that $p = \langle x, y \rangle$ is equivalent to: $$\forall a, a \in p \leftrightarrow [(\forall b, b \in a \leftrightarrow b = x) \vee (\forall b, b \in a \leftrightarrow (b = x \vee b = y))].$$
Note that a generalization of this procedure (formalized) comes up in model theory, under the name of "conversative extension by definition". (However, in general, in expanding a formula not of the form variable = definition, we might need to introduce some more variables. For example, if you wanted to expand $\langle x, y \rangle \in z$ instead, then you would first need to expand this to $\exists p, p = \langle x, y \rangle \wedge p \in z$, and then proceed to expand $p = \langle x, y \rangle$ as above.)