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
