Hi, In Michael Norrish and Brian Huffman's paper [1] about HOL’s ordinals, it’s said, “the distinct types ``:unit ordinal``, ``:bool ordinal``, and ``:num ordinal`` will all be isomorphic (they will all be copies of the countable ordinals).” “On the other hand, the type “:(num -> bool) ordinal” is large enough to include the first uncountable ordinal, w1.”
I have a strange question here: what about “:string ordinal”? Is it large enough to include the first uncountable ordinal? (or generally speaking, how can I know if an ordinal type based on an infinite type is large enough to be uncountable?) Regards, Chun Tian [1] Norrish, M., Huffman, B.: Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) w1. (2013).
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
