Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cl-isabelle-users Digest, Vol 117, Issue 32


view this post on Zulip Email Gateway (Aug 19 2022 at 17:28):

From: "W. Douglas Maurer" <maurer@gwu.edu>
I think that Joachim is right. My doctorate is in mathematics, and we
got a very thorough lecture on countability (it might have been from
Leon Henkin). If by a chain you mean a sequence, so a countable set
of countable sets, then yes, that is countable. For example, the set
of all ordered pairs of natural numbers, (x, y), is the (countable)
union of the sets of all such ordered pairs for fixed x and arbitrary
y, each one of which is countable. But you can set up an enumeration
(0, 0), (1, 0), (0, 1), (2, 0), (1, 1), (0, 2), (3, 0), (2, 1), (1,
2), (0, 3), etc.
I'm not sure that there actually is a least uncountable ordinal
number. In fact, when I was at that lecture, it wasn't known, at that
time, whether there were any ordinals between aleph-0 and aleph-1.
Since then I believe that that question has been shown to be
unprovable, one way or the other.
Part of the confusion here, I think is that, on the one hand, every
set can be well-ordered, but, on the other hand
(http://en.wikipedia.org/wiki/Well-order), "it is possible to show
that the ZFC+GCH axioms alone are not sufficient to prove the
existence of a definable (by a formula) well-order of the reals (S.
Feferman: "Some Applications of the Notions of Forcing and Generic
Sets", Fundamenta Mathematicae, 56 (1964) 325-345)".


Last updated: Apr 26 2024 at 01:06 UTC