7
$\begingroup$

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

$\endgroup$

3 Answers 3

2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

$\endgroup$
10
  • $\begingroup$ 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\}\}$. $\endgroup$
    – Steve Kass
    Dec 26, 2020 at 2:25
  • $\begingroup$ 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)$ $\endgroup$ Dec 27, 2020 at 4:20
  • $\begingroup$ 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. $\endgroup$ Dec 27, 2020 at 5:43
  • $\begingroup$ @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? $\endgroup$ Dec 27, 2020 at 12:38
  • 1
    $\begingroup$ @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. $\endgroup$ Dec 28, 2020 at 19:52
0
$\begingroup$

$$ \newcommand\liff{\leftrightarrow} \newcommand\lif{\rightarrow} \newcommand\lfi{\leftarrow} \newcommand\ordp[2]{\langle #1,#2 \rangle} \newcommand\mset[1]{\{ #1 \}} \newcommand\isRel[1]{#1 \text{ is a relation}} \newcommand\isFunc[1]{#1 \text{ is a function}} \newcommand\isOneOne[1]{#1 \text{ is one-one}} \newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}} \newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn \newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn \newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn \newcommand{\startsub}{\\[-0.29em]} %adjusts line spacing slightly \newcommand{\endsub}{\startsub} %adjusts line spacing slightly \newcommand{\fendl}{\\[0.044em]} %adjusts line spacing slightly $$

$$\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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.