= Bounded successor characterization of finite ordinals
{title2=$x\in\omega\iff\operatorname{Ord}(x)\land\operatorname{Succ}_0(x)\land\forall y\in x\ \operatorname{Succ}_0(y)$}
A <Von Neumann ordinal> $x$ is finite exactly when $x$ and every member of $x$ are either zero or <successor ordinals>. Every <finite ordinal> has that property. Conversely, an infinite <ordinal> is either $\omega$, which is a nonzero limit, or is greater than $\omega$ and contains that nonzero <limit ordinal>. The test can be expressed by a bounded <first-order formula>: ordinality uses transitivity and membership comparability, and a nonempty <ordinal> is a successor exactly when it has a greatest member. This defines the class of <natural numbers> without quantifying over arbitrary infinite <inductive sets>.
Back to article page
