= Set of well-order codes
{title2=$\mathrm{WF}$}
The <set of well-order codes> $\mathrm{WF}\subseteq\omega^\omega$ consists of codes for strict <well-orders> $(D,R)$ on subsets $D\subseteq\omega$. The norm $\lVert x\rVert$ is their <order type>. Every <countable ordinal>, including finite ordinals and zero, has such a code.
For a coding convenient for games, ignore $x(0)$ as a tag. At coordinate $x(n+1)$ record the domain bit for $n$ and the finitely many relation bits $R(i,j)$ with $\max(i,j)=n$, in a fixed order. Read these bits from the binary expansion, ignoring unused higher bits. The code belongs to $\mathrm{WF}$ exactly when the decoded relation is a strict <well-order> of its decoded domain. This convention makes local recoding operations explicit and allows an arbitrary domain subset, rather than incorrectly requiring every well-order to have domain all of $\omega$.
Back to article page
