Hi Michael,
Thanks very much, it helps a lot. I took me some time to digest all the
words, that's why I reply late.
Regards,
Chun
On 10 October 2017 at 00:26, <michael.norr...@data61.csiro.au> wrote:
> Strings have the same cardinality as numbers (there is a bijection between
> them established in string_numTheory), so string ordinal will be the same
> type (up to isomorphism) as num ordinal. There’s no general way to know
> what the cardinality of a type is unless you have theorems to hand that
> make it clear.
>
>
> In other words, the collection of countable ordinals is an uncountable
> set, so every ordinal type will have uncountably many elements. The first
> uncountable ordinal is that which has uncountably many predecessors, and
> will only be present if the type parameter has cardinality greater than
> aleph-0.
>
> To be pedantic about your last question: in the HOL formalisation all
> ordinal types are uncountable; not all ordinal types contain ω₁. In other
> words, the collection of countable ordinals is an uncountable set, so every
> ordinal type will have uncountably many elements. The first uncountable
> ordinal is that which has uncountably many predecessors, and will only be
> present if the type parameter has cardinality greater than aleph-0.
>
> Hope this helps,
> Michael
>
> On 10/10/17, 08:40, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> 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).
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
