My structure can contain (‘a ordinals) as part of it, and I have a function, given any ordinal N, for all n < N, f(n) is a different value of my structure (which contains ordinal too). Its cardinality must be very huge, and that’s the only thing I know.
—Chun
> 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
