# Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$

## Authors

Michael Norrish and Brian Huffman

NICTA

Australian National University

Galois
Inc.

## Abstract

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀, the existence of normal forms, and the validation of some of the algorithms used in the ACL2 theorem-proving system.

## BibTeX Entry

  @inproceedings{Norrish_Huffman_13,
author           = {Norrish, Michael and Huffman, Brian},
editor           = {{Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}},
month            = jul,
year             = {2013},
title            = {Ordinals in {HOL}: Transfinite Arithmetic up to (and beyond) $\omega_1$},
}