*To*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Are the countable sets a ccpo*From*: "Lochbihler Andreas" <andreas.lochbihler at inf.ethz.ch>*Date*: Sat, 21 Mar 2015 13:06:57 +0000*Accept-language*: de-DE, de-CH, en-US*In-reply-to*: <20150320152536.GE3321@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*References*: <550C37B4.1030204@inf.ethz.ch> <20150320151538.GD3321@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>, <20150320152536.GE3321@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*Thread-index*: AdBjH5ddRl6nzpvoR92ZMb/Tm76faf//8X4AgAACyQCAAXroHA==*Thread-topic*: [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 :-(. Best, Andreas ________________________________________ Von: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk]" im Auftrag von "Bertram Felgenhauer [bertram.felgenhauer at googlemail.com] Gesendet: Freitag, 20. März 2015 16:25 An: cl-isabelle-users at lists.cam.ac.uk 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. Cheers, Bertram

**References**:**[isabelle] Are the countable sets a ccpo***From:*Andreas Lochbihler

**Re: [isabelle] Are the countable sets a ccpo***From:*Bertram Felgenhauer

**Re: [isabelle] Are the countable sets a ccpo***From:*Bertram Felgenhauer

- Previous by Date: Re: [isabelle] Are the countable sets a ccpo
- Next by Date: Re: [isabelle] Cl-isabelle-users Digest, Vol 117, Issue 32
- Previous by Thread: Re: [isabelle] Are the countable sets a ccpo
- Next by Thread: Re: [isabelle] Are the countable sets a ccpo
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list