Apologies for duplicated paragraphs below…
Michael
On 10/10/17, 09:27, "michael.norr...@data61.csiro.au"
<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
------------------------------------------------------------------------------
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
