Ordinal is Finite iff Natural Number

This article is not under active maintenance. While the contents of this page could be useful, they are currently not being maintained. The correctness, lay-out and usefulness of the article may be compromised, so use whatever you get from here with caution. To discuss this page in more detail, feel free to use the talk page.

Theorem

Let $x$ be an ordinal.

Then $x$ is a finite set if and only if $x$ is an element of the minimally inductive set.

Proof

$x$ is finite if and only if $x \sim \N_n$ for some $n \in \N$, by definition.

But $x$ is an ordinal, and by definition, it is equal to its initial segment.

By definition of the von Neumann construction of natural numbers, it follows that $x \sim n$ for some $n$.

By Finite Ordinal is equal to Natural Number, it follows that $x$ is equal to $n$.

Thus, $x$ is an element of the minimally inductive set.

$\blacksquare$

Sources

• 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 10.30$