### Abstract

We develop a basic theory of ordinals and cardinals in Isabelle/HOL, up to the point where some cardinality facts relevant for the “working mathematician” become available. Unlike in set theory, here we do not have at hand canonical notions of ordinal and cardinal. Therefore, here an ordinal is merely a well-order relation and a cardinal is an ordinal minim w.r.t. order embedding on its field.

### License

BSD License

### History

September 25, 2012
  This entry has been discontinued because it is now part of the Isabelle distribution.

### Topics

- Logic/Set theory

### Session Ordinals_and_Cardinals

- Cardinal_Order_Relation_discontinued

## Cite

×

Ordinals_and_Cardinals-AFP

    @article{Ordinals_and_Cardinals-AFP,
      author  = {Andrei Popescu},
      title   = {Ordinals and Cardinals},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2009},
      note    = {\url{https://isa-afp.org/entries/Ordinals_and_Cardinals.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Sep 9, 2009 : Isabelle2009
- Sep 7, 2009 : Isabelle2009