On the uncountability of the set of reals
Ingo Blechschmidt
you might know that for several of the various possibilites of making
this statement precise, it's an open problem whether there is an
intuitionistic proof that the set of reals is uncountable. (I first
learned of this somewhat embarassing situation by Andrej Bauer.)
I'm toying with collecting what we know about this problem in a central
place so that anybody who wants to study it doesn't have to spend their
time rederiving known results.
One could of course argue that one should never consider the raw set of
reals (but rather study point-free versions of them) and that the
problem is therefore of no particular interest. But still it seems that
it would be good to have definitive closure on this manner, either by
producing an intuitionistic proof of uncountability or by producing a
model in which the reals are uncountable.
Here is what I know:
* The following assumptions each individually suffice to exclude a
surjection from the naturals to any kind of reals which are
Cauchy-complete: law of excluded middle, dependent choice, countable
choice, the reals are discrete, Heine--Borel for countable covers.
* There is an intuitionistic proof that the MacNeille reals are
uncountable in the strong sense that for all maps N -> R, there is a
number which is not in the image. (Has this been known before? I
stumbled on this in joint work with Matthias Hutzler, adapting a proof
by Eliahu Levy.)
* There are intuitionistic proofs of the following statements:
- For all maps N -> 2^N, there is an element of the codomain which is
not in the image.
- For all maps N -> Omega^N, there is an element of the codomain which is
not in the image.
- There is no injective map Omega^N -> N.
(However, these facts doesn't seem to be particularly relevant, as the
reals might not be isomorphic to 2^N or Omega^N.)
* In the effective topos, there is a surjection from a subset of the
naturals to the reals. (This property isn't specific to the reals at all.)
* In the realizability topos built using infinite-time Turing machines,
there is an injection from the reals to the naturals. This is due to
Andrej Bauer, whose proof that there is an injection from 2^N to N
carries over mutatis mutandis. If the absence of the law of excluded
middle was available, we could apply Cantor–Schröder–Bernstein to
deduce that there is a bijection between the naturals and the reals,
yielding a contradiction.
* There is no intuitionistic proof of the statement "for all maps N -> R,
there is a real number which is not in the image" and of the weaker
statement "for all maps N -> R, there is not not a real number which
is not in the image", if we mean by "R" the Dedekind numbers. There
are sheaf models where these statements fail. I believe this is due to
Bas Spitters, please correct me if I'm wrong.
* Assuming that there is no surjection from N to the Cauchy reals in the
metatheory, no Grothendieck topos which admits a point contains a
surjection from N to the Cauchy reals, to the Dedekind reals or to the
Dedekind reals. Therefore no nontrivial Grothendieck topos with enough
points contains such a surjection. In particular, no nontrivial topos
of sheaves over a topological space contains such a surjection.
* The topos of surjections from N to R, constructed as a suitable
classifying locale, doesn't have any points (assuming that there is no
surjection from N to R in the metatheory) but is still nontrivial.
It trivially contains a surjection from the constant sheaf N to the
constant sheaf R. However, assuming dependent choice in the
metatheory, it verifies dependent choice, being zero-dimensional in
the appropriate sense. Therefore it can't contain a surjection from N
to the (Cauchy or Dedekind) reals.
* Given a surjection from N to R (Cauchy, Dedekind, MacNeille) and a
real number x, we can explicitly write down a monotonically increasing
sequence of real numbers with the following property: It's not not the
case that the sequence is eventually constant with the minimal
preimage of x under the surjection as eventual value. (If we could
remove the "not not" here, we could show that the reals are discrete.)
We can also explicitly write down a sequence of real numbers with the
following property: All of its values are strictly greater than x,
and it's not not the case that it stabilizes with eventual value
being the first number in the given enumeration of the reals which is
strictly greater than x. (If we could upgrade this property, we could
mimic Cantor's original proof of the uncountability of the reals.)
I'm grateful for any pointers and comments.
Cheers,
Ingo
Andrew Swan
- It is provably false that there is both an injection from the reals to the naturals and a surjection from the naturals to the reals (and in particular no bijection). The reason is that the existence of the injection implies that the reals are discrete.
- A weak version of the axiom of countable choice is good enough. We only need that every multivalued relation from N to 2 has a choice function. It's maybe an interesting question to ask what is the weakest form of choice which is known to imply the reals are uncountable.
- The real numbers are uncountable in the Lifschitz realizability topos.
frank waaldijk
Andrej Bauer
the present discussion is hapenning within a context in which
countable choice is not allowed and "reals" means either Dedekind
reals (an intuitionistic version of Dedekind cuts construction) or
Cauchy reals (a quotient of the set of Cauchy sequences). Should there
be any doubts about the exact foundation, let me suggest that we
should take the internal language of a topos (higher-order
intuitionistic logic with a natural number).
For instance, Bishop's idea of reals as a set of Cauchy sequences with
an equivalence relation is outside of the context, as that is *not* a
quotient as is normally understood. In fact, the entire BISH setup is
suspect, even if we drop countable choice, because of its treatment of
quotients as not quite quotients. (And I am not doing philsophy here,
just mathematics.)
AC_11 is not relevant because it implies AC_00, which immediately
implies that the reals are not countable. I think this was summarized
by Ingo in his first message.
With kind regards,
Andrej
Andrej Bauer
> theories (the other one is RUSS), it would seem to me a good idea for anyone
> working in or around constructive mathematics to
models of them, namely realizability toposes over Kleene's second and
first algebras (or some variants of those). In this sense INT is
studied quite comprehensively, at least from the point of view of
computable analysis, as it is the setting in which Type Two
Effectivity takes places, except that the community that carries out
the research prefers to not use this fact. In any case, function
realizability (which is the best approximation of what Brouwer might
have meant) is studied in quite some detail and many people are aware
of its virtues.
> b) use the word `intuitionistic' to indicate INT, so as not to add
> unnecessarily to the general-math community's mistaken impression that INT
> is vague and hard to understand.
do we call the thing that is usually called "intuitionistic logic"
(namely first-order or higher-order logic without excluded middle)? I
would suggest a nomenclature that mentions Brouwer. What is wrong with
the more specific "Brouwer's intuitionism"?
With kind regards,
Andrej
Bas Spitters
Kleene-Vesley realizability model and the Kreisel-Troelstra
elimination translation, which can be captured by sheaf models.
https://ncatlab.org/nlab/show/continuous+truth
There's a nice paper by Awodey and Bauer that compares the two approaches:
https://www.andrew.cmu.edu/user/awodey/preprints/stfr.pdf
> You received this message because you are subscribed to the Google Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
frank waaldijk
Douglas Bridges
Re real numbers: most of you on this thread probably don't know that in our 2006 book on constructive analysis, Luminita Vita and I used an interval-arithmetic-style construction of the reals. (Actually, I suspect that most readers, being logicians, either are unaware that our book exists or, if they are so aware, have never looked at it).
Douglas
Sent: Monday, 11 June 2018 15:26
To: frank waaldijk
Cc: constructivenews
Subject: Re: On the uncountability of the set of reals
frank waaldijk
These two are stable because there are identifiable mathematical
models of them, namely realizability toposes over Kleene's second and
first algebras (or some variants of those). In this sense INT is
studied quite comprehensively, at least from the point of view of
computable analysis, as it is the setting in which Type Two
Effectivity takes places, except that the community that carries out
the research prefers to not use this fact. In any case, function
realizability (which is the best approximation of what Brouwer might
have meant) is studied in quite some detail and many people are aware
of its virtues.
If we use "intuitionistic" for Brouwer's version of mathematics, what
do we call the thing that is usually called "intuitionistic logic"
(namely first-order or higher-order logic without excluded middle)? I
would suggest a nomenclature that mentions Brouwer. What is wrong with
the more specific "Brouwer's intuitionism"?
Erik Palmgren
It is known that Bishop's set-up can be consistently (and naturally!) interpreted in Martin-L"of type theory understanding Bishop's notion of set as setoid (type with an equivalence relation). See e.g.
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/palmgren.pdf
Also it has quotients (but one may have take to heed of which universe of types they are quotients wrt).
I don't see what could be suspect about his approach. In fact it seems that Bishop experimented with theories with higher types (based on G"odel's T) as foundations. The general Sigma- and Pi-types from M-L type theory seems to be the missing pieces.
Skickat: den 11 juni 2018 16:24
Till: Andrej Bauer; frank waaldijk
Kopia: constructivenews
Ämne: Re: On the uncountability of the set of reals
Bhupinder Singh Anand
Dear Frank and Ingo,
Curiously, you might be faced by an intuitionistically undecidable proposition in this case! Here’s why:
1. In a paper that appeared in the December 2016 issue of `Cognitive Systems Research’ (link below), I informally introduced the concept of `evidence-based reasoning’ (say ER):
Paper: ‘The Truth Assignments That Differentiate Human Reasoning From Mechanistic Reasoning: The Evidence-Based Argument for Lucas' Goedelian Thesis’
Author’s update: https://www.dropbox.com/s/8nql7dd4ci1rgfc/28_Human_Reasoning_v_Mechanistic_Reasoning_Update.pdf?dl=0
2. I formally define ER in my thesis (under finalisation), where I argue that ER is constructively more stringent than intuitionistic reasoning, say IR (see Chapter 3).
Thesis: ‘Three Dogmas of First-Order Logic and some Evidence-based Consequences for Constructive Mathematics of differentiating between Hilbertian Theism, Brouwerian Atheism and Finitary Agnosticism’
Author’s update: https://www.dropbox.com/s/czbc08yc58gzqbt/39_Anand_Dogmas_Reference_Universe.pdf?dl=0
3. In ER there is a proof that the first-order Peano Arithmetic PA is finitarily consistent; ergo so is the first-order logic FOL, in which LEM is a theorem (see Chapter 9 of my thesis).
4. Since LEM does not entail Hilbert’s non-constructive definitions of quantification in terms of his epsilon choice function, IR rejects LEM by choice, not by constructive necessity.
5. In ER, a real is an algorithmically verifiable Cauchy sequence, but not necessarily an algorithmically computable (i.e., realizable) Cauchy sequence; ergo not every well-defined real can be treated as the completable infinity of some Cauchy sequence. In other words the so-called `Cauchy limit’ of some Cauchy sequences under any well-defined evidence-based interpretation is a mathematical fiction that, sometimes, has no geometric interpretation (see Fig.2 on p.209 in Chapter 24, Section 24.7 of my thesis).
6. In ER, a real number is well-defined if, and only if, it is definable in the first-order Peano arithmetic PA; ergo:
· a real number does not really exist in any well-defined interpretation of a mathematical proof until sufficient digits in its decimal representation are actually defined by some first-order formula so as to differentiate the number from any previously defined real number;
· the Cauchy sequences of reals which are algorithmically verifiable, but not algorithmically computable, are essentially incompletable infinities that belong only to the language of geometry (set theory---which is the language of what we can unambiguously conceive), whereas the algorithmically computable reals belong to the language of arithmetic (PA---which is the language of what we can unambiguously communicate);
· the set theory ZF and PA may be treated formally as mathematically complementary languages (as is done in ACA_0), even though they are functionally incompatible under interpretation (see Chapters 20 and 24 of my thesis).
7. Since a first-order language has only denumerable formulas that are available to define a real, the reals are not `uncountable’ in ER (see Chapter 19).
8. Not being constrained by LEM, there would be assertions, such as in 7 above, which would not be decidable in IR.
Kind regards,
Bhup
======================
From: construc...@googlegroups.com
[mailto:construc...@googlegroups.com] On Behalf Of frank waaldijk
Sent: Monday, June 11, 2018 12:32 PM
To: constructivenews
Subject: Re: On the uncountability of the set of reals
-----
Theorem (INT)
Let a_0, a_1,... be a sequence of reals, then there is a real number x such that x # a_n for all n in N.
Proof: elementary application of successive trisection of the unit interval
-----
In 1990 I started doing research in constructive mathematics (my master's thesis describes how to construct the algebraic-and-metric completion of any discrete field with valuation). Ever since I have been amazed by the lack of basic knowledge of INT, especially in the constructive-math community. Now if INT were difficult, compared to other theories, it would explain the general disinterest. But the contrary is true.
Since INT is one of the only two long-term stable constructive mathematical theories (the other one is RUSS), it would seem to me a good idea for anyone working in or around constructive mathematics to
a) study at least the basics of intuitionistic mathematics, in order to get a picture of its precision, simplicity and elegance.
b) use the word `intuitionistic' to indicate INT, so as not to add unnecessarily to the general-math community's mistaken impression that INT is vague and hard to understand.
best wishes,
Frank
======================
On Sunday, June 10, 2018 at 1:45:50 PM UTC+2, Ingo Blechschmidt wrote:
Dear friends of the reals,
you might know that for several of the various possibilites of making this
statement precise, it's an open problem whether there is an intuitionistic
proof that the set of reals is uncountable. (I first learned of this somewhat
embarassing situation by Andrej Bauer.)
I'm toying with collecting what we know about this problem in a central place
so that anybody who wants to study it doesn't have to spend their time re deriving
known results.
One could of course argue that one should never consider the raw set of reals
(but rather study point-free versions of them) and that the problem is
therefore of no particular interest. But still it seems that it would be good
to have definitive closure on this manner, either by producing an intuitionistic
proof of uncountability or by producing a model in which the reals are
uncountable.
Here is what I know:
* The following assumptions each individually suffice to exclude a surjection
from the naturals to any kind of reals which are Cauchy-complete: law of
excluded middle, dependent choice, countable choice, the reals are discrete,
Heine--Borel for countable covers.
* There is an intuitionistic proof that the MacNeille reals are uncountable in
the strong sense that for all maps N -> R, there is a number which is not
in the image. (Has this been known before? I stumbled on this in joint work
with Matthias Hutzler, adapting a proof by Eliahu Levy.)
* There are intuitionistic proofs of the following statements:
Andrej Bauer
I have always felt uneasy about not knowing the precise formal setup
that corresponds to Bishop's mathematics. Suggestions were given, but
to my mind they are not satisfactory. Bishop's mathematics is
agnostic, even universal, and should be applicable in many situations.
In your book with Fred Richman on varities of constructivism this was
made quite clear. Those ideas deserve an expansion and a comprehensive
treatment: a semantics with a great wealth of models, rather than just
a handful, an wide applicability in many situations. The best way I
know of achieving such a goal is realizability theory, which captures
many ideas of Bishop nicely (for instance the difference between an
operation and a function). However, realizability is not quite the
same as Bishop's setup, especially in its treatment of quotients.
Therein lies the origin of my suspicion: the best formal fit is not a
perfect fit. Are there theorems in Foundations of Constructive
Mathematics that cannot be translated to realizability? Which ones? Is
there an alternative setup which is an even better fit than
realizability (that's hard to imagine)?
One may be proud of lack of formalism, or even refuse formalism on
philosophical grounds, but at the end of the day formal logic is the
final arbitrer. Without sufficiently precise foundation we run the
risk of confusion or blindness. A prime example is Martin Escardó's
result which shows that Brouwerian continuity principles are
inconsistent under some entirely reasonably looking formalizations of
the BHK interpretation. His analysis would not have been possible with
a very careful formal study of the various notions of constructive
existence. Could Bishop's constructivism suffer from a similar defect?
With kind regards,
Andrej
P.S. I have the Bridgest & Vita book on my shelf. I wish I could get
my hands on Varities of constructivism as well.
Martin Escardo
Regarding this, in particular:
On 11/06/18 23:15, Bhupinder Singh Anand wrote:
> 7. Since a first-order language has only denumerable formulas that
are available to define a real, the reals are not `uncountable’ in ER
(see Chapter 19).
which people, in particular Brouwer (maybe first) and (then) Hilbert,
were aware of at the beginning of the 20th century.
In ZFC, you can define only countably many reals: this is a
meta-linguistic statement - the meta-level set of ZFC-definable real
numbers is countable. Still, the object-level ZFC-set of real numbers is
(provably!) uncountable. (This assumes a non-constructive meta-language,
to be able to conclude that any subset of a countable sets is countable,
including the subset of ZFC-sentences that define real numbers.)
This is of course similar to Skolem's so-called paradox. There are
models of ZFC in which all sets are countable, and yet ZFC can prove
that there are uncountable sets. There is no contradiction or paradox.
It just happens that we have built a model of ZFC-sets using meta-level
sets that are meta-level countable, but not ZFC-countable.
This may seem philosophically mysterious, but is bread-and-butter in
computer programming. For example, a programming language called system
T cannot count the functions N->N, but anybody can easily write down a
program (in a more powerful programming language, such as Haskell or
OCaml or Agda or Java) that counts the system-T-definable functions N->N.
-- .. -- .. --
(2) To anybody still listening:
I think Andrej's question (are the reals uncountable?) and Ingo's
original thoughts in this thread are very interesting.
Suppose you take the most neutral approach to mathematics, compatible
with both classical mathematics, and as many possible existing or
to-be-found varieties of constructive mathematics. Can you prove that
the reals are uncountable?
Andrej called this "agnostic mathematics". But "agnostic" indicates lack
of (dis-)belief. I think that "neutral" (more) or "absolute" (less) are
better terminologies, because this is not about belief, but about what
we can prove that all mathematicians of any variety, constructive or
not, will accept and understand. Perhaps "universal mathematics"
describes the intended effect better.
See "absolute geometry", also called "neutral geometry".
https://en.wikipedia.org/wiki/Absolute_geometry
The above is vague. A precise, and sufficiently "universal" set-up for
mathematics, admitting both classical mathematics, and many varieties of
constructive mathematics (and probably varieties of mathematics going
much beyond classical or constructive) is topos theory (models) and
higher-order logic (syntax). We can try to approach the question there
first, which is, as I understand, what Ingo was doing.
Martin
Steve Vickers
This is just to set on record that in geometric reasoning elementary topos theory and higher-order logic are much further from immediate acceptance, so non-neutral. It's a nontrivial task to make the translation, as you can for example by comparing my geometric "Cosheaves and connectedness in formal topology" with the impredicative proofs in the Bunge-Funk book "Singular covers of toposes" from which I took much of my inspiration.
The "formal topology" label tends to favour predicativity, indicating a dissatisfaction with the powerobjects and subobject classifiers of elementary toposes. Geometricity goes further: its benefits depend also on not using exponentials as a general logical principle (of course, they are useful when they exist), so higher order logic too becomes a non-neutral feature.
All the best,
Steve.
> On 14 Jun 2018, at 21:29, construc...@googlegroups.com wrote:
>
> (2) To anybody still listening:
>