Re: [isabelle] Are the countable sets a ccpo

Dear Bertram,

Thanks a lot for the counterexample. Of course, I was thinking of uncountable chains, which are used in the definition of the ccpo class in Complete_Partial_Order. Otherwise the question is trivial. So, there is no ccpo instance for cset :-(.

Von: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at]" im Auftrag von "Bertram Felgenhauer [bertram.felgenhauer at]
Gesendet: Freitag, 20. März 2015 16:25
An: cl-isabelle-users at
Betreff: Re: [isabelle] Are the countable sets a ccpo

Bertram Felgenhauer wrote:
> Andreas Lochbihler wrote:
> > Dear all,
> >
> > I am wondering whether the countable sets ordered by inclusion forms a
> > chain-complete partial order. In other words: If C is a chain of countable
> > sets, is the union of all the sets in C countable again?
> The answer is no. For example, let C be the least uncountable ordinal
> number; then all its elements are countable, but their union is C
> itself, because C is a limit ordinal.

NB. I'm here using the set-theoretic definition of ordinal numbers,
where each ordinal number is the set of its predecessors. In the
context of Isabelle/HOL, I would start with an uncountable type,
use the well-ordering principle on that, and then consider the
smallest element l that has an uncountable number of predecessors.
Then C = {{ x | x < l'} | l' < l} is a chain of countable sets
whose union is {x | x < l}, hence uncountable.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.