I think there is still an issue because your existing CCS term may use all of
the available ordinals for that type. Then you can never find a least one in
that type that is bigger than them all (because there are none left).
It seems to me that you have two options. You either prove a result along the
lines of
!ct0 : ‘a CCS. ?ct: (‘a -> bool) CCS. …
which admits that you have to change your underlying type when you assert the
existence of the result.
Or, alternatively, you constrain the cardinality of the graph/sum, so that the
result looks like
!ct0: ‘a CCS. Ordinals_of ct0 =~ univ(:num) ==> ?ct: ‘a CCS. …
If there are only countably many ordinals in your graph (or if the size of the
sum is only countably big), then there will always be a bigger ordinal (take
the sup + 1), and you can stay within the same type.
Michael
- -
On 13/10/17, 06:28, "Chun Tian" <binghe.l...@gmail.com> wrote:
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
------------------------------------------------------------------------------
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
