# Countable Ordinals

 Title: Countable Ordinals Author: Brian Huffman Submission date: 2005-11-11 Abstract: This development defines a well-ordered type of countable ordinals. It includes notions of continuous and normal functions, recursively defined functions over ordinals, least fixed-points, and derivatives. Much of ordinal arithmetic is formalized, including exponentials and logarithms. The development concludes with formalizations of Cantor Normal Form and Veblen hierarchies over normal functions. BibTeX: @article{Ordinal-AFP, author = {Brian Huffman}, title = {Countable Ordinals}, journal = {Archive of Formal Proofs}, month = nov, year = 2005, note = {\url{https://isa-afp.org/entries/Ordinal.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Nested_Multisets_Ordinals