#paper # Abstract This technical report documents the work done leading up to a paper on a theory of ordinal submitted to the Tableaux 2017 conference. # Summary ## Syntactics The paper gives a formal review of the theory of ordinals in first order logic. It starts with the language $\{<,S,0,\omega,\sup\}$ where lt;$ is a binary relation, $S$ a unary function for successor, $\sup$ a binary function, $0,\omega$ constants, which gives the *Core Theory* $Th^{0}_{Ord}$ (pg. 4). It then defines the usual notions such as a limit ordinal, ordinal arithmetic (addition, multiplication and exponentiation), and states (mostly without proof) various basic lemmas. The core theory plus the definition of the auxiliary notions constitute $Th_{Ord}$ (pg. 5,8). It then defines the syntactic notion of a *normal form* - a notion similar to [[Cantor normal form]], where the requirement is that also the exponents are presented in normal form. The definition is by recursion. Several facts regarding normal forms are proved, including uniqueness, how to add and multiply them, etc. Every term can be proved to be equivalent to a normal form. ## Semantics **Def. 9** The *$\epsilon$-Standard Model* is the model whose universe is the ordinal $\epsilon_{0}$ with the usual interpretations of the symbols. Lemma 9 ensures that $\epsilon_{0}$ is closed under the operations $+,*,exp,\sup$, and hence (Thm.2) it is a model of $Th_{Ord}$. ## Applications Termination of programs. Goodstein sequences.