Defining ordered pairs using only first-order logic

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$$?

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.)

$$p= \langle x, y \rangle \iff \forall z (z \in p \iff \exists w_1 \exists w_2 ((z=w_1 \lor z=w_2) \land ((\forall t_1(t_1 \in w_1 \iff t_1=x)) \land \forall t_2(t_2 \in w_2 \iff (t_2 = x \lor t_2 = y)))).$$

Translating this to English, $$w_1$$ and $$w_2$$ are the two elements of the set comprising our ordered pair, with $$t_1$$ as the element of $$w_1$$ (which we're forcing to be $$x$$) and $$t_2$$ as the elements of $$w_2$$ (which we're forcing to be $$x$$ or $$y$$).

• The phrase “[with] $t_2$ as the elements of $w_2$...” might be unclear, so a possibly easier translation to English: $p = \langle x,y\rangle$ if and only if there exist sets $w_1,w_2$ for which a) $p=\{w_1,w_2\}$, b) $w_1$ is the singleton set $\{x\}$ and c) $w_2$ is the set $\{x,y\}$. Note that $x$ and $y$ need not be distinct, in which case a)-c) are uniquely satisfied by $w_1=w_2=\{x\}$, and $p=\{\{x\}\}$. Dec 26, 2020 at 2:25
• I think this definition is not unique, also accepting both $\{\{x\}\}$ and $\{\{x,y\}\}$ as representing that ordered pair, as they satisfy the conditions that the sets $w_1=\{x\}$ and $w_2=\{x,y\}$ exist and every set $z$ in them satisfies $(z=w_1 \lor z=w_2)$ Dec 27, 2020 at 4:20
• The biconditional in $t_2 \in w_2 \iff (t_2=x \lor t_2=y)$ forces $w_2$ to allow both $x$ and $y$ as members. Dec 27, 2020 at 5:43
• @RobertShore Indeed there's a flaw in my argument. I've tried to come up counter-example after not being able to prove the property of uniqueness for $p$, assuming extentionality. Do you think extentionality is sufficient to prove its uniqueness? Dec 27, 2020 at 12:38
• @RobertShore Indeed, and I believe that your answer is correct. However, I'm still struggling to find a proof of uniqueness for $p$. I've posted a related question to address this. Once I'm able to prove the uniqueness property, I'll be back to accept your answer. Dec 28, 2020 at 19:52


$$\ordp{a}{b} = p \iff \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]]$$

In this definition, $$p$$ is our ordered pair, and every set $$Z$$ in $$p$$ has to be either $$\mset{a}$$ or $$\mset{a,b}$$. This is more explicit with the equivalent set of definitions:

$$\mset{a} = p \iff \forall x[x \in p \liff x = a] \\ \mset{a,b} = p \iff \forall x[x \in p \liff x = a \lor x = b] \\ \ordp{a}{b} = p \iff \forall Z [Z \in p \liff Z=\mset{a} \lor Z=\mset{a,b}] \\$$

The former is more in line with the question, since it is a single definition and uses only primitive symbols. However, I found the latter nicer to work with, as it makes proofs a lot less verbose. In any case, they are equivalent, so a proof that is valid for one is valid for the other.

We may prove that set-theory guarantees their unique existence. The first definition will be used in this example.

The following statements trivially follow from Paring, Specification and Extensionality: $$\begin{array}{l} \text{[1]}:\forall a \exists A \forall x[x \in A \liff x = a] \\ \text{[2]}:\forall a \forall b \exists A \forall x[x \in A \liff x = a \lor x = b] \\ \text{[3]}:\forall p \forall q \forall a[\forall x[x \in p \liff x = a] \land \forall x[x \in q \liff x = a] \lif p = q] \\ \text{[4]}:\forall p \forall q \forall a \forall b[\forall x[x \in p \liff x = a \lor x = b] \land \forall x[x \in q \liff x = a \lor x = b] \lif p = q] \\ \end{array}$$

We may use the first two to introduce the sets $$A_{\alpha a}$$ and $$A_{\beta ab}$$, which represent $$\mset{a}$$ and $$\mset{a,b}$$, and then introduce $$p_{\alpha ab}$$, which represents our ordered pair:

$$\small \fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl \vdots\fendl } & \scol { \exists A \forall x[x \in A \liff x = a] \\ \exists A \forall x[x \in A \liff x = a \lor x = b] \\ \forall x[x \in A_{\alpha a} \liff x = a] \\ \forall x[x \in A_{\beta ab} \liff x = a \lor x = b] \\ \exists A \forall x[x \in A \liff x = A_{\alpha a} \lor x = A_{\beta ab}] \\ \forall x[x \in p_{\alpha ab} \liff x = A_{\alpha a} \lor x = A_{\beta ab}] \\ Z \in p_{\alpha ab} \liff Z = A_{\alpha a} \lor Z = A_{\beta ab} \\ \rlap{\vdots} \hphantom{\subcol{\subcol{\forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab}}}} \\ } & \tcol{ [1]\ \forall\text{E} \fendl [2]\ \forall\text{E} \fendl 1\ \exists\text{E} \fendl 2\ \exists\text{E} \fendl [2]\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}] \fendl 5\ \exists\text{E}[A/p_{\alpha ab}] \fendl 6\ \forall\text{E}[x/Z] \fendl \rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl } }$$

Then, we prove that $$p_{\alpha ab}$$ follows the defined properties, which means that a being with these properties exists (line $$36$$):

$$\small \fitch{ \fcol{\vdots\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22:\fendl 23:\fendl 24:\fendl 25:\fendl 26:\fendl 27:\fendl 28:\fendl 29:\fendl 30:\fendl 31:\fendl 32:\fendl 33:\fendl 34:\fendl 35:\fendl 36:\fendl \vdots\fendl } & \scol { \rlap{\vdots} \startsub\subcol{ Z \in p_{\alpha ab} \\ \hline Z = A_{\alpha a} \lor Z = A_{\beta ab} \startsub\subcol{ Z = A_{\alpha a} \\ \hline \forall x[x \in Z \liff x = a] \\ \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ }\endsub Z = A_{\alpha a} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \startsub\subcol{ Z = A_{\beta ab} \\ \hline \forall x[x \in Z \liff x = a \lor x = b] \\ \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ }\endsub Z = A_{\beta ab} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ }\endsub Z \in p_{\alpha ab} \lif \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \startsub\subcol{ \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \startsub\hline\subcol{ \forall x[x \in Z \liff x = a] \\ \hline \forall x[x \in Z \liff x=a] \land \forall x[x \in A_{\alpha a} \liff x=a] \lif Z = A_{\alpha a} \\ Z = A_{\alpha a} \\ Z = A_{\alpha a} \lor Z = A_{\beta ab} \\ }\endsub \forall x[x \in Z \liff x = a] \lif Z = A_{\alpha a} \lor Z = A_{\beta ab} \startsub\subcol{ \forall x[x \in Z \liff x = a \lor x = b] \\ \hline \forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab} \\ Z = A_{\beta ab} \\ Z = A_{\alpha a} \lor Z = A_{\beta ab} \\ }\endsub \forall x[x \in Z \liff x = a \lor x = b] \lif Z = A_{\alpha a} \lor Z = A_{\beta ab} \\ Z = A_{\alpha a} \lor Z = A_{\beta ab} \\ Z \in p_{\alpha ab} }\endsub \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \lif Z \in p_{\alpha ab} \\ Z \in p_{\alpha ab} \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ \forall Z[Z \in p_{\alpha ab} \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\ \exists p \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\ \rlap{\vdots} \\ } & \tcol{ \rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl \text{P}[Z] \fendl 7,8\ {\liff}\text{E} \fendl \text{P}[Z] \fendl 3,10\ {=}\text{S}[A_{\alpha a}/Z] \fendl 11\ {\lor}\text{I} \fendl 10,12\ {\lif}\text{I}\ \fendl \text{P}[Z] \fendl 4,14\ {=}\text{S}[A_{\beta ab}/Z] \fendl 15\ {\lor}\text{I} \fendl 14,16\ {\lif}\text{I} \fendl 9,13,17\ {\lor}\text{E} \fendl 8,18\ {\lif}\text{I} \fendl \text{P}[Z,a,b] \fendl \text{P}[Z,a,b] \fendl [3]\ \forall\text{E}[p/Z,q/A_{\alpha a}] \fendl 3,21,22\ {\lif}\text{E} \fendl 22\ {\lor}\text{I} \fendl 20,23\ {\lif}\text{I} \fendl \text{P}[Z,a,b] \fendl [4]\ \forall\text{E}[p/Z,q/A_{\beta ab}] \fendl 4,26,27\ {\lif}\text{E} \fendl 27\ {\lor}\text{I} \fendl 25,28\ {\lif}\text{I} \fendl 20,25,30\ {\lor}\text{E} \fendl 7,31\ {\liff}\text{E} \fendl 20,32\ {\lif}\text{I} \fendl 19,33\ {\liff}\text{I} \fendl 34\ \forall\text{I}\ \fendl 35\ \exists\text{I}\ \fendl \rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \fendl } }$$

Then we prove that this being is unique, by showing that if any two sets $$p$$ and $$q$$ follow these properties, they are one and the same (line $$45$$):

$$\small \fitch{ \fcol{\vdots\fendl 37:\fendl 38:\fendl 39:\fendl 40:\fendl 41:\fendl 42:\fendl 43:\fendl 44:\fendl\fendl\fendl 45:\fendl\fendl\fendl 46:\fendl } & \scol { \rlap{\vdots} \hphantom{\subcol{\subcol{\forall x[x \in Z \liff x=a \lor x=b] \land \forall x[x \in A_{\beta ab} \liff x=a \lor x=b] \lif Z = A_{\beta ab}}}} \startsub\subcol{ \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\ \forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\ \hline Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b] \\ Z \in p \liff Z \in q \\ \forall Z[Z \in p \liff Z \in q] \\ p = q \\ } \endsub \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad\ \land \forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad \lif p = q \\ \forall p \forall q[\forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad\ \land \forall Z[Z \in q \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\\quad \lif p = q] \\ \exists p! \forall Z[Z \in p \liff \forall x[x \in Z \liff x = a] \lor \forall x[x \in Z \liff x = a \lor x = b]] \\ } & \tcol{ \rlap{\vdots} \hphantom{aaa\ \forall\text{E}[a/A_{\alpha a},b/A_{\beta ab}]} \\ \text{P}[p,a,b] \fendl \text{P}[q,p,a,b] \fendl 37\ \forall\text{E} \fendl 38\ \forall\text{E} \fendl 39,40\ {\liff}\text{Tr} \fendl 41\ \forall\text{I} \fendl 42,\text{Ext.}\ \forall\text{I} \fendl 37,38,43\ {\lif}\text{I} \fendl\fendl\fendl 45\ \forall\text{I} \fendl\fendl\fendl 36,45\ \exists!\text{I} \fendl } }$$

As such, there exists a unique $$p$$ with these properties (line $$46$$).

We may also prove that they obey the characteristeric property for ordered pairs, namely: $$\forall x \forall y \forall a \forall b[\ordp{x}{y} = \ordp{a}{b} \liff x = a \land y = b]$$. The second definition will be used in this example.

The following statements trivially follow from the definitions of $$\mset{a}$$ and $$\mset{a,b}$$, and Extentionality: $$\begin{array}{l} \text{[1]}:\forall a \forall b [\mset{a} = \mset{b} \liff a=b] \\ \text{[2]}:\forall a [\mset{a,a} = \mset{a}] \\ \text{[3]}:\forall a \forall b [\mset{a,b} = \mset{a} \liff a=b] \\ \text{[4]}:\forall a \forall b \forall c [a \neq b \lif \mset{c} \neq \mset{a,b}] \\ \text{[5]}:\forall a \forall b \forall c [\mset{a,b} = \mset{a,c} \liff b = c] \\ \end{array}$$

We start by proving the trivial implication from RHS to LHS:

$$\small \fitch{ \fcol{ 1:\fendl 2:\fendl 3:\fendl 4:\fendl \vdots\fendl } & \scol { \subcol{ x=a \land y=b \\ \hline \ordp{x}{y} = \ordp{x}{y} \\ \ordp{x}{y} = \ordp{a}{b} \\ } \endsub x=a \land y=b \lif \ordp{x}{y} = \ordp{a}{b} \\ \rlap{\vdots} \hphantom{\subcol{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}}} \\ } & \tcol{ \text{P}[x,y,a,b] \fendl \text{T} \fendl 1,2\ {=}\text{S} \fendl 1,3\ {\lif}\text{I} \fendl \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl } }$$

For the trickier LHS to RHS, we start by assuming that $$\ordp{x}{y} = \ordp{a}{b}$$ and using the definition to establish a relationship between the sets (line $$14$$). From that relationship, we extract some useful statements about them (lines $$19$$ to $$22$$):

$$\small \fitch{ \fcol{ \vdots\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl 12:\fendl 13:\fendl 14:\fendl 15:\fendl 16:\fendl 17:\fendl 18:\fendl 19:\fendl 20:\fendl 21:\fendl 22:\fendl \vdots\fendl } & \scol { \subcol{ \rlap{\vdots} \\ \ordp{x}{y} = \ordp{a}{b} \\ \hline \ordp{a}{b} = \ordp{x}{y} \liff \forall Z [Z \in \ordp{x}{y} \liff Z=\mset{a} \lor Z=\mset{a,b}] \\ \ordp{x}{y} = \ordp{a}{b} \liff \forall Z [Z \in \ordp{a}{b} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\ \forall Z [Z \in \ordp{x}{y} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\ \forall Z [Z \in \ordp{a}{b} \liff Z=\mset{a} \lor Z=\mset{a,b}] \\ Z \in \ordp{x}{y} \liff Z=\mset{a} \lor Z=\mset{a,b} \\ Z \in \ordp{a}{b} \liff Z=\mset{x} \lor Z=\mset{x,y} \\ Z \in \ordp{a}{b} \liff Z=\mset{a} \lor Z=\mset{a,b} \\ Z=\mset{a} \lor Z=\mset{a,b} \liff Z=\mset{x} \lor Z=\mset{x,y} \\ \forall Z [Z=\mset{a} \lor Z=\mset{a,b} \liff Z=\mset{x} \lor Z=\mset{x,y}] \\ \mset{a}=\mset{a} \lor \mset{a}=\mset{a,b} \liff \mset{a}=\mset{x} \lor \mset{a}=\mset{x,y} \\ \mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \liff \mset{x}=\mset{x} \lor \mset{x}=\mset{x,y} \\ \mset{a,b}=\mset{a} \lor \mset{a,b}=\mset{a,b} \liff \mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\ \mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y} \\ \mset{a}=\mset{x} \lor \mset{a}=\mset{x,y} \\ \mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\ \mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\ \mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \\ \rlap{\vdots} } } & \tcol{ \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl \text{P}[x,y,a,b] \fendl \text{Def.}\ \forall\text{E}[p/\ordp{x}{y}] \fendl \text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}] \fendl 5,6\ {\liff}\text{E} \fendl 5,7\ {\liff}\text{E} \fendl 8\ \forall\text{E} \fendl 9\ \forall\text{E} \fendl 5,10\ {=}\text{S} \fendl 11,12\ {\liff}\text{Tr} \fendl 13\ \forall\text{I} \fendl 14\ \forall\text{E}[Z/\mset{a}] \fendl 14\ \forall\text{E}[Z/\mset{x}] \fendl 14\ \forall\text{E}[Z/\mset{a,b}] \fendl 14\ \forall\text{E}[Z/\mset{x,y}] \fendl 15\ {\liff}\text{E} \fendl 16\ {\liff}\text{E} \fendl 17\ {\liff}\text{E} \fendl 18\ {\liff}\text{E} \fendl \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl } }$$

Now, either $$a = b$$ or $$a \neq b$$. So we may prove that in both cases it follows that $$a=x$$ and $$b=y$$. In the case that $$a = b$$:

$$\small \fitch{ \fcol{ \vdots\fendl 23:\fendl 24:\fendl 25:\fendl 26:\fendl 27:\fendl 28:\fendl 29:\fendl 30:\fendl 31:\fendl 32:\fendl 33:\fendl 34:\fendl 35:\fendl 36:\fendl 37:\fendl 38:\fendl 39:\fendl 40:\fendl 41:\fendl \vdots\fendl } & \scol { \subcol{ \rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}} \\ a=b \lor a \neq b \startsub\subcol{ a = b \\ \hline \mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\ \mset{x}=\mset{a} \lor \mset{x}=\mset{a,a} \\ \mset{a,a} = \mset{a} \\ \mset{x}=\mset{a} \lor \mset{x}=\mset{a} \\ \mset{x}=\mset{a} \\ \mset{x}=\mset{a} \liff x=a \\ x=a \\ \mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \\ x=b \\ \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,x} \\ \mset{x,x}=\mset{x} \\ \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x} \\ \mset{x,y}=\mset{x} \\ \mset{x,y}=\mset{x} \liff x=y \\ x=y \\ y=b \\ } \endsub a=b \lif (x=a \land y=b) \\ \rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}} \\ } } & \tcol{ \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl \text{T} \fendl \text{P}[x,y,a,b] \fendl 20\ \text{C} \fendl 24,25\ {=}\text{S}[b/a] \fendl [2]\ \forall\text{E} \fendl 27,26\ {=}\text{S}[\mset{a,a}/\mset{a}] \fendl 28\ {\lor}\text{E} \fendl [1]\ \forall\text{E}[a/x,b/a] \fendl 29,30\ {\liff}\text{E} \fendl 22\ \text{C}\ \fendl 24,31\ {=}\text{Tr} \fendl 32,33\ {=}\text{S}[b/x] \fendl [2]\ \forall\text{E}[a/x] \fendl 34,35\ {=}\text{S}[\mset{x,x}/\mset{x}] \fendl 36\ {\lor}\text{E} \fendl [3]\ \forall\text{E}[a/x,b/y] \fendl 37,38\ {\liff}\text{E} \fendl 33,39\ {=}\text{Tr} \fendl 24,31,40\ {\lif}\text{I} \fendl \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl } }$$

In the case that $$a \neq b$$:

$$\small \fitch{ \fcol{\vdots\fendl 42:\fendl 43:\fendl 44:\fendl 45:\fendl 46:\fendl 47:\fendl 48:\fendl 49:\fendl 50:\fendl 51:\fendl 52:\fendl 53:\fendl 54:\fendl 55:\fendl 56:\fendl 57:\fendl 58:\fendl } & \scol { \subcol{ \rlap{\vdots} \hphantom{\mset{x,y}=\mset{a} \lor \mset{x,y}=\mset{a,b} \liff \mset{x,y}=\mset{x} \lor \mset{x,y}=\mset{x,y}} \startsub\subcol{ a \neq b \\ \hline \mset{x}=\mset{a} \lor \mset{x}=\mset{a,b} \\ a \neq b \lif \mset{x} \neq \mset{a,b}\\ \mset{x} \neq \mset{a,b} \\ \mset{x}=\mset{a} \\ \mset{x}=\mset{a} \liff x=a \\ x = a \\ \mset{a,b}=\mset{x} \lor \mset{a,b}=\mset{x,y} \\ \mset{a,b}=\mset{x,y} \\ \mset{a,b}=\mset{a,y} \\ \mset{a,b}=\mset{a,y} \liff b=y\\ b = y } \endsub a \neq b \lif (x=a \land y=b) \\ x=a \land y=b } \endsub \ordp{x}{y} = \ordp{a}{b} \lif x=a \land y=b \\ \ordp{x}{y} = \ordp{a}{b} \liff x=a \land y=b \\ \forall x \forall y \forall a \forall b[\ordp{x}{y} = \ordp{a}{b} \liff x=a \land y=b] \\ } & \tcol{ \rlap{\vdots}\hphantom{\text{Def.}\ \forall\text{E}[a/x,b/y,p/\ordp{a}{b}]} \fendl \text{P}[x,y,a,b] \fendl 20\ \text{C} \fendl [4]\ \forall\text{E}[c/x] \fendl 42,44\ {\lif}\text{E} \fendl 43,45\ {\lor}\text{E} \fendl [1]\ \forall\text{E}[a/x,b/a] \fendl 46,47\ {\liff}\text{E} \fendl 21\ \text{C} \fendl 45,49\ {\lor}\text{E} \fendl 48,50\ {=}\text{S}[x/a] \fendl [5]\ \forall\text{E}[c/y] \fendl 51,52\ {\liff}\text{E} \fendl 42,53\ {\lif}\text{I} \fendl 23,41,54\ \text{TI} \fendl 5,55\ {\lif}\text{I} \fendl 4,56\ {\liff}\text{I}\ \fendl 57\ \forall\text{I}\ \fendl } }$$

As such, the definitions obey the characteristic property for ordered pairs.