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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
