Email Gateway (Aug 22 2022 at 20:33): Email Gateway (Aug 22 2022 at 20:33):From: Lawrence Paulson <lp15@cam.ac.uk>
Is anybody aware of a formalisation of an ordinal notation, in particular, Cantor normal form? Preferably in Isabelle, and I’m aware of the following one, in Agda: https://arxiv.org/abs/1904.10759
There, the authors manage to define a type, a relation and a function simultaneously. Impressive!
Larry Paulson
Email Gateway (Aug 22 2022 at 20:33):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hi,
Pierre Casteran worked on this subject in his project of formalization of
the impossibility of proving Goodstein theorem in Peano arithmetic and
related subjects. Here is the reference from his website:
https://www.labri.fr/perso/casteran/CoqArt/le_teaser/teaser.pdf
Kind regards,
José M.
Email Gateway (Aug 22 2022 at 20:34):From: Konrad Slind <konrad.slind@gmail.com>
Matt Kaufmann and I proved epsilon-0 induction in HOL a few years back, as
part of a project to model ACL2 in HOL.
Michael Norrish and Brian Huffmann combined their work in a much more
expansive work.
See
https://link.springer.com/chapter/10.1007/978-3-642-39634-2_12
Email Gateway (Aug 22 2022 at 20:34):From: Mario Carneiro <di.gama@gmail.com>
Ordinal notations for ordinals less than epsilon_0 have been formalized in
lean:
https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/ordinal_notation.lean
Mario
Email Gateway (Aug 22 2022 at 20:34):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Larry,
the hereditarily finite multisets are pretty close to the Cantor normal form for ordinals below epsilon0. See also our (Jasmin Blanchette's, Mathias Fleury's, and mine) FSCD'17 paper
http://people.inf.ethz.ch/trayteld/papers/fscd17-nmult/nmult.pdf
and the corresponding AFP entry
https://www.isa-afp.org/entries/Nested_Multisets_Ordinals.html
We also connect our "hmultiset"s to Brian Huffman's countable ordinals (https://www.isa-afp.org/entries/Ordinal.html), so that one can benefit from both representations.
If you need to go beyond epsilon0, there is of course the ordinals and cardinals library in the Isabelle distribution (HOL-Cardinals). There is a fair bit of ordinal arithmetic but no Cantor normal form.
Cheers,
Dmitriy
Last updated: Apr 23 2024 at 16:19 UTC