Email Gateway (Aug 19 2022 at 17:27): Email Gateway (Aug 19 2022 at 17:27):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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? I have been thinking about this for quite a while, but I could
not come up with a stringent argument nor a counterexample. Does anybody know the answer?
In case of yes, we could make the type cset an instance of the class ccpo.
Best,
Andreas
Email Gateway (Aug 19 2022 at 17:27):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Andreas Lochbihler wrote:
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.
HTH,
Bertram
Email Gateway (Aug 19 2022 at 17:27):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Bertram Felgenhauer wrote:
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
Email Gateway (Aug 19 2022 at 17:27):From: Joachim Breitner <breitner@kit.edu>
Hi,
but is C a chain, e.g. totally ordered?
I would say the answer is yes:
A countable set over 'a can be represented as "nat => 'a", a chain of
those would be "nat => nat => 'a". So using any bijection
"nat => (nat × nat)", we can show that there are countable many 'a’s in
there.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 17:27):From: Joachim Breitner <breitner@kit.edu>
Hi,
... yes, because you are talking about ordinals.
So I guess the question is what definition of chain Andreas needs. I was
thinking of HOLCF’s countable chains, but now that I think about it that
can’t be the one he is looking at, as I’m sure that he knows that the
countable union of countable sets is countable. Hence I conclude he is
thinking in the same terms as Bertram, so I retract my answer and go to
bed.
Good night!
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 17:27):From: Lawrence Paulson <lp15@cam.ac.uk>
If a chain is necessarily indexed by the natural numbers, then your problem is trivial. Without that restriction, the set of countable ordinals is a counterexample to your proposition. This set is totally ordered, and uncountable.
--lcp
Email Gateway (Aug 19 2022 at 17:28):From: Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de>
Of course, the union of a countable chain of countable sets is countable
again.
However, the union of an uncountable chain of countable sets generally
is not, nor can such a chain be represented as object of type "nat =>
nat => 'a".
Best, Till
Email Gateway (Aug 19 2022 at 17:28):From: Christian Sternagel <c.sternagel@gmail.com>
On Mar 20, 2015 22:42, "Joachim Breitner" <breitner@kit.edu> wrote:
Hi,
Am Freitag, den 20.03.2015, 16:15 +0100 schrieb Bertram Felgenhauer:
Andreas Lochbihler wrote:
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.but is C a chain, e.g. totally ordered?
I would say the answer is yes:
A countable set over 'a can be represented as "nat => 'a", a chain of
those would be "nat => nat => 'a".
Maybe it should be clarified whether we are talking about countable chains
here, or arbitrary totally ordered sets of sets?
So using any bijection
"nat => (nat × nat)", we can show that there are countable many 'a’s in
there.Greetings,
Joachim--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
Email Gateway (Aug 19 2022 at 17:28):From: Christian Sternagel <c.sternagel@gmail.com>
Sorry for my previous odd interjection into this thread. Somehow my
mobile device managed to just show me Joachim's original mail but not
all the replies that were sent in the meantime.
chris
Email Gateway (Aug 19 2022 at 17:28):From: Lochbihler Andreas <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Nov 21 2024 at 12:39 UTC