Well, after reading a paper [1] on Isabelle’s cardinals, I started to think: maybe what’s “missing" in HOL4 is a theory of “Cardinal Arithmetic” - the current cardinalTheory can only express the relative cardinality between two sets (cardleq). Michael’s work [2] was mainly on ordinals and ordinal arithmetic, he didn’t say if we can use some of those ordinals as cardinals (if it’s possible).
But maybe I don’t need this at all. I see many essential ordinals in HOL4’s
ordinalTheory was defined by the “oleast” operator. Maybe I just need to
express “the least ordinal which satisfies a proposal P” and without knowing
what exactly it is I can just use it in the rest of the proof. And the only
difficulty will be carefully choosing P such that it’s not universally false.
I don’t know, but this will be my next move.
—Chun
[1] Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle/HOL. In:
Interactive Theorem Proving. pp. 111–127. Springer, Cham, Cham (2014).
[2] Norrish, M., Huffman, B.: Ordinals in HOL: Transfinite Arithmetic up to
(and Beyond) w_1. 1–14 (2013).
> Il giorno 12 ott 2017, alle ore 18:47, Mario Castelán Castro
> <marioxcc...@yandex.com> ha scritto:
>
> Hello.
>
> Note: I know nothing about process algebra. I had to perform a web
> search to know what the term means.
>
> Do you really need to consider set of arbitrary cardinalities? Aren't
> your structures always below some cardinality? Would it suffice for your
> formalization to speak of _representations_ of ordinals below, say, ε0?
> Those can be represented as finite formulas in ordinal arithmetic, so
> the set of all such representations can fit within a single monomorphic
> HOL4 type.
>
>> If I've learnt correctly, in standard set theory, all cardinals are
>> ordinals, but the reverse is not true, because not every ordinals “has the
>> same number (as itself) of smaller ordinals”.
>
> As far as I know, that “all cardinals are ordinals” is just an effect of
> the “standard” definition of ordinal numbers and cardinal numbers in ZFC
> (card A is the least ordinal X such that X === A [End, p. 197]) but it
> is not a property intrinsic to the informal concept of cardinal numbers.
> I think of this as a technical definition analogous to the Kuratowski
> definition of ordered pairs. One can also define card A as the _class_
> “{X | X === A}” in a theory that admits classes (like von
> Neumann-Gödel-Bernays, and HOL4's “pred_set”), then this property no
> longer holds (w.r.t. the standard way of defining ordinals, which is
> also due to von Neumann).
>
>> “Let c be the smallest infinite cardinal, such that NODES(p) and NODES(q)
>> has less than c nodes.
>
> If NODES(p) and NODES(q) are of type “bool -> 'a” (or you have one
> equinumerous term with such a type), then you can define the cardinality
> of p and q as “{X | ∃f. BIJ f (NODES p) X}” but I do not know how this
> applies to your case.
>
> [End] Herbert B. Enderton “Elements of set theory” (1977).
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
> ------------------------------------------------------------------------------
> 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
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
