Cardinals in Isabelle/HOL

Conference paper

Blanchette, J., Popescu, A. and Taytel, D. 2014. Cardinals in Isabelle/HOL. 5th International Conference on Interactive Theorem Proving. Vienna, Austria 14 - 17 Jul 2014 Springer. pp. 111-127
TypeConference paper
TitleCardinals in Isabelle/HOL
AuthorsBlanchette, J., Popescu, A. and Taytel, D.

We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced was the inability of higher-order logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation identifying ordinals with well-orders, with all concepts and results proved to be invariant under order isomorphism. We also discuss several applications of this general theory in formal developments.

Research GroupFoundations of Computing group
Conference5th International Conference on Interactive Theorem Proving
Page range111-127
Publication dates
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via

Additional information

Published paper appears in: Interactive Theorem Proving, Volume 8558 of the series Lecture Notes in Computer Science pp 111-127, 2014

Web address (URL)
Book titleInteractive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Permalink -

Download files

Accepted author manuscript
  • 15
    total views
  • 5
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as