Countable Ordinals

Brian Huffman 🌐

November 11, 2005

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Ordinal