Cardinals in Isabelle/HOL
Authors: Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
Paper Information
| Title: | Cardinals in Isabelle/HOL |
| Authors: | Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel |
| Proceedings: | ITP 2014 LNCS Proceedings |
| Editors: | Gerwin Klein and Ruben Gamboa |
| Keywords: | ordinal number, wellorder, cardinal number, higher-order logic, Isabelle/HOL |
| Abstract: | ABSTRACT. 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 wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss several applications of this general theory in formal developments. |
| Pages: | 16 |
| Talk: | Jul 15 12:15 |
| Paper: |  |