Expansion system

An expansion system is an ordinal notation system defined in a special way. It is defined through expansion, with standard form constructed from a specified set called the base of the standard form (usually with order type \( \omega \)).

More precisely, the definition involves only a set \( S \) of well-formed terms, a function \( []: S\times\mathbb{N}\to S \) (where [](x,n) is written as x[n]), and a set \( X_0 \). Then with \( X \) being the closure of \( X_0 \) under \( x\mapsto x[n] \) for every \( n\in\mathbb{N} \), and with \( x<y \) equivalent to the existence of \( m,n_0,n_1,...,n_m\in\mathbb{N} \) such that \( x=y[n_0][n_1]...[n_m] \), the expansion system is the set \( X \) ordered by \( < \). Such an ordered set still needs to be well-ordered in order to be an ordinal notation system, and the definition simply having this form is not enough to imply well-orderedness.

Expansion systems may also be called "dom-type systems" or similarly, in reference to the fact that some of them have a function \( dom \) assigning a "domain" to each element \( x\in S \), so that \( x[\alpha] \) is defined precisely for \( y\in dom(x) \). However, restricting the domain of an element is often not necessary, especially when the domain can only be \( \varnothing, \{0\} \) or \( \mathbb{N} \). Many expansion systems are also sequence systems, although there can be exceptions.