User:Dfeuer/Definition:Finite Ordinal
Definition
NOTE: not the definition used in S & F.
A finite ordinal is an ordinal which is strictly well-ordered under the inverse of the epsilon relation.
That is, a finite ordinal is an ordinal which is strictly well-ordered (well-founded and linearly ordered) under the epsilon relation and also under the inverse of the epsilon relation.
Theorem
The successor of a finite ordinal is a finite ordinal.
Proof
Let $n$ be a finite ordinal.
Then $n^+ = n \cup \{n\}$ is an ordinal because the successor of an ordinal is an ordinal.
Let $a$ be a non-empty subset of $n^+$.
If $n \notin a$, then $a \subseteq n$, so $a$ has a greatest element because $n$ is a finite ordinal.
If $n \in a$, then $n$ is the greatest element of $a$.
Theorem
0 is a finite ordinal.
Proof
Vacuous.
Theorem
Element of ordinal is ordinal.
Proof
Let $m \in n$ and let $n$ be an ordinal.
$m$ is strictly well-ordered by the epsilon relation: $n$ is transitive, so $m \subseteq n$. Since $n$ is strictly well-ordered by $\Epsilon$, so is $m$.
$m$ is transitive:
Let $x \in m$ and let $y \in x$.
Since $n$ is an ordinal, $n$ is transitive.
Thus $x \in n$, so $y \in n$.
Since $n$ is strictly well-ordered by $\Epsilon$, $\Epsilon$ is certainly transitive on $n$.
Thus since $y \in x$ and $x \in m$, $y \in m$.
As this holds for all such $x$ and $y$, $m$ is transitive.
Since $n$ is transitive, $m \subseteq n$, so $m$ is strictly well-ordered by $\Epsilon$.
Element of Finite Ordinal is Finite Ordinal
If $m \in n$ and $n$ is a finite ordinal, then $m$ is an ordinal.
Since $n$ is strictly
Intersection of Ordinals is Ordinal
Let $S$ be a non-empty class of ordinals.
Then $T = \bigcap S$ is an ordinal.
Proof
Transitive: the intersection of a non-empty class of transitive sets is transitive.
Strictly well-ordered by $\Epsilon$: The restriction of a strict well-ordering is a strict well-ordering.
Union of Ordinals is Ordinal
Let $S$ be a set of ordinals.
Then $\bigcup S$ is an ordinal.
Proof
$S$ is transitive because any union of transitive sets is transitive.
Let $T$ be a non-empty subset of
FINISH
Trichotomy
Let $x$ and $y$ be ordinals.
Then $x = y$, $x \in y$, or $y \in x$.
Proof
STUB
Predecessor
Each finite ordinal that is not $\varnothing$ has a predecessor.
Proof
Let $n$ be an ordinal which is not $\varnothing$.
Then $n$ is a non-empty subset of $n$, so $n$ has an $\Epsilon$-greatest element $m$.
Then $m$ is an ordinal because an element of an ordinal is an ordinal.
Induction
Suppose that $A$ is a class of finite ordinals, $0 \in A$, and for any finite ordinal $n$, $n \in A \implies n^+ \in A$.
Then $A$ is the class $\omega$ of all finite ordinals.
Proof
Let $P = \omega \setminus A$.
If $A \ne \omega$, then $P$ is not empty.
Thus $P$ has a least element $m$.