= Solution
<Hartogs theorem> says that for every set $A$ there is a least <ordinal> $h(A)$ that does not inject into $A$. This theorem requires no <axiom of choice>.
To prove it, collect all <well-orderings> of subsets of $A$. They are set-sized data, coded by pairs from $\mathcal P(A)$ and $\mathcal P(A\times A)$. Each has a unique <ordinal> order type, so replacement gives a set $H$ of their order types. If $\eta\in H$ and $\xi<\eta$, restricting the corresponding <well-order> to an initial segment shows $\xi\in H$. Hence $H$ is an <ordinal>. If this <ordinal> itself injected into $A$, its transported <well-order> would put $H$ among its own elements, impossible for an <ordinal>. Every smaller <ordinal> does inject by definition. Thus $h(A)=H$ has the asserted property.
\b[The recursion printed in the source needs two boundary restrictions.] Its new-row successor clause allows $\beta=\alpha$, which would assign a value at $(\alpha,\alpha+1)$ outside the declared domain. Also, at $\alpha=0$, its row-start clause gives $g_1(0,0)=0$ while its column-start clause gives $g_1(0,0)=g_1(0,0)+1$. Taken literally, these clauses do not define a function.
The intended extension fills the new row first and the remaining new column second. Restrict the row successor clause to $\beta<\alpha$, and apply the column-start clause only when $\alpha>0$. With these two restrictions the domains are disjoint:
$$
\alpha\times\alpha,\qquad\{(\alpha,\beta):\beta\leq\alpha\},\qquad
\{(\beta,\alpha):\beta<\alpha\}.
$$
All successors here are <ordinal> successors. Simultaneous <transfinite induction> proves a stronger result: $g_\alpha$ is a <bijection> of $\alpha\times\alpha$ onto an <ordinal> $\gamma_\alpha$, and the functions extend one another.
At zero this is the <empty function>. Assuming it at $\alpha$, the least missing <ordinal> is $\gamma_\alpha$. Recursion down the new row gives values $\gamma_\alpha+\beta$ for $\beta\leq\alpha$; recursion down the remaining column gives $\gamma_\alpha+(\alpha+1)+\beta$ for $\beta<\alpha$. These enumerate two disjoint consecutive <ordinal> intervals above the old range, so the extension is well defined and bijective, with
$$
\boxed{\gamma_{\alpha+1}=\gamma_\alpha+(\alpha+1)+\alpha.}
$$
At a limit $\lambda$, take the union of the earlier functions. Compatibility makes it a function, and every pair of coordinates below $\lambda$ is already present at some earlier stage. Its range is the <ordinal> $\bigcup_{\alpha<\lambda}\gamma_\alpha$, and injectivity is preserved by the compatible union. This completes the construction of the <row-and-column enumeration of an ordinal square>.
For finite stages $\gamma_n=n^2$. For example the table of $g_3$, with the first coordinate indexing rows, is
$$
\begin{pmatrix}0&3&7\\1&2&8\\4&5&6\end{pmatrix}.
$$
The remaining parts refer to this domain-consistent construction. The source's literal boundary claims are preserved in the archive, rather than silently asserted as valid.
Back to article page
