Equivalence of Definitions of Ordinal

From ProofWiki
Jump to navigation Jump to search


The following definitions of the concept of Ordinal are equivalent:

Definition 1

Let $S$ be a set.

Let $\Epsilon \! \restriction_S$ be the restriction of the epsilon relation on $S$.

Then $S$ is an ordinal if and only if:

$S$ is a transitive set
$\Epsilon \! \restriction_S$ strictly well-orders $S$.

Definition 2

Let $A$ be a set.

Then $A$ is an ordinal if and only if $A$ is:

epsilon-connected, that is:
$\forall x, y \in A: x \ne y \implies x \in y \lor y \in x$

Definition 3

An ordinal is a strictly well-ordered set $\struct {S, \prec}$ such that:

$\forall a \in S: S_a = a$

where $S_a$ is the initial segment of $S$ determined by $a$.

From the definition of an initial segment, and Ordering on Ordinal is Subset Relation, we have that:

$S_a = \set {x \in S: x \subsetneqq a}$

From Initial Segment of Ordinal is Ordinal we have that $S_a$ is itself an ordinal.


Definition 1 is equivalent to Definition 2

This follows immediately from the definition of a strict well-ordering.


Definition 1 implies Definition 3

Let $S$ be an ordinal according to Definition 1.

Let $a \in S$.


\(\ds S_a\) \(=\) \(\ds \set {x \in S: x \in_S a}\) Definition of Initial Segment
\(\ds \) \(=\) \(\ds \set {x: x \in S \land x \in a}\)
\(\ds \) \(=\) \(\ds S \cap a\) Definition of Set Intersection
\(\ds \) \(=\) \(\ds a\) as $a \subseteq S$ by transitivity


Definition 3 implies Definition 1

Let $\struct {S, \prec}$ be an ordinal according to Definition 3.

Let $a \in S$.

Then $a = S_a \subseteq S$ and so $S$ is transitive.

Also, by the definition of set equality:

\(\ds \forall x: \, \) \(\ds x \in a\) \(\iff\) \(\ds x \in S_a\)
\(\ds \leadstoandfrom \ \ \) \(\ds \forall x: \, \) \(\ds x \in a\) \(\iff\) \(\ds \paren {x \in S \land x \prec a}\)

It has been shown that if $x, a \in S$ then:

$x \in a \iff x \prec a$

Therefore, $\operatorname \prec = \struct {S, S, R}$ where:

\(\ds R\) \(=\) \(\ds \set {\tuple {x, a} \in S \times S: x \prec a}\)
\(\ds \) \(=\) \(\ds \set {\tuple {x, a} \in S \times S: x \in a}\)
\(\ds \) \(=\) \(\ds \in_S\) Definition of Epsilon Restriction

Hence $\operatorname \prec = \Epsilon {\restriction_S}$.