Non-enumerability of R

0 views
Skip to first unread message

Andrej Bauer

unread,
Jul 12, 2017, 5:05:01 AM7/12/17
to homotopyt...@googlegroups.com
I have been haunted by the question "Is there a surjection from N to
R?" in a constructive setting without choice. Do we know whether the
following is a theorem of Unimath or some version of HoTT:

"There is no surjection from the natural numbers to the real numbers."

Some remarks:

1. Any reasonable definition of real numbers would be acceptable, as
long as you're not cheating with setoids. Also, since this is not set
theory, the powerset of N and 2^N are not "reals".

2. It is interesting to consider different possible definitions of
"surjection", some of which will probably turn out to have an easy
answer.

3. In the presence of countable choice there is no surjection, by the
usual proof. (But we might have to rethink the argument and place
propositional truncations in the correct spots.)

4. It is known that there can be an injection from R into N, in the
presence of depedent choice (in the realizability topos on the
infinite-time Turing machines).

With kind regards,

Andrej

Andrew Swan

unread,
Jul 12, 2017, 5:16:01 PM7/12/17
to Homotopy Type Theory
I don't have an answer, but I've also wondered about this question, so I'll add some more remarks of my own.

1. In the topos of sheaves over the closed unit interval the Dedekind reals are not uncountable (in fact there is a countably enumerable "double negation dense set" in the reals). I think it's reasonable to expect the same thing in Thierry Coquand's cubical stack model and so show the same is consistent with HoTT.

2. I would conjecture that constructing cubical sets internally in the infinite time Turing machine topos gives a model of HoTT with an injection from the reals to the naturals.

3. There is an entirely constructive proof that there is no bijection between the naturals and the reals (for any reasonable definition of real): first if there is an injection then the reals have decidable equality, but then this yields a proof that there is no surjection by a standard diagonal argument.

Best,
Andrew

Andrej Bauer

unread,
Jul 16, 2017, 4:09:28 AM7/16/17
to Homotopy Type Theory
Dear Andrew,

thank you for your remarks.

> 1. In the topos of sheaves over the closed unit interval the Dedekind reals are not uncountable (in fact there is a countably enumerable "double negation dense set" in the reals). I think it's reasonable to expect the same thing in Thierry Coquand's cubical stack model and so show the same is consistent with HoTT.

For the uninitiated, let me just clarify that one such not-not-dense
countable subset is the set P of polynomials with rational
coefficients. One then appeals to density of this set by the
Stone-Weierstraß theorem: for every continuous function on every open
set there is some polynomial in P which intersects its graph, hence R
\ P is empty.

Let us call a set/object/type X *inexhaustible* when for every
sequence a : N → X there is some x in X which is different from all
terms of the sequence. An inexhaustible set clearly is not countable.
What your remark shows is that the reals cannot be shown to be
inexhaustible in intuitionistic logic without choice.


> 2. I would conjecture that constructing cubical sets internally in the infinite time Turing machine topos gives a model of HoTT with an injection from the reals to the naturals.

Yes, but note by your third remarks, that as soon as there is an
injection from reals to natural numbers, there can be no surjection
going the other way. So cubical sets in infinite-time HoTT won't
resolve the question.

> 3. There is an entirely constructive proof that there is no bijection between the naturals and the reals (for any reasonable definition of real): first if there is an injection then the reals have decidable equality, but then this yields a proof that there is no surjection by a standard diagonal argument.

Neat.

With kind regards,

Andrej

Andrej Bauer

unread,
Jul 16, 2017, 4:11:20 AM7/16/17
to Homotopy Type Theory
> One then appeals to density of this set by the Stone-Weierstraß theorem: for every continuous function on every open
> set there is some polynomial in P which intersects its graph, hence R \ P is empty.

In fact, no appeal to Stone-Weierstraß is needed, because that one is
about *uniform* approximation of functions, whereas we only need local
approximation. Yes?

Bas Spitters

unread,
Jul 16, 2017, 2:36:11 PM7/16/17
to Andrej Bauer, Homotopy Type Theory
I once gave a proof (without Stone-Weierstrass) in the appendix of this paper:
http://www.cs.au.dk/~spitters/obs.pdf
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Andrej Bauer

unread,
Jul 17, 2017, 9:52:30 AM7/17/17
to Homotopy Type Theory
> In fact, no appeal to Stone-Weierstraß is needed, because that one is
> about *uniform* approximation of functions, whereas we only need local
> approximation. Yes?

It's still easier than that, isn't it already the case that the
constant functions taking a rational value suffice? On every open
interval every continuous map intersects one of those.

Thomas Streicher

unread,
Jul 18, 2017, 3:54:56 AM7/18/17
to Andrej Bauer, Homotopy Type Theory
At www.mathematik.tu-darmstadt.de/~streicher/rnc.pdf you find a
littele note of mine where I fill in some details in the
Rosolini-Spitters argument that Sh(R) doesn't validate the statement
that for every sequenc a in R^D there is a b in R^D with b # a_n for
all n (# stands for "apart").

But this argument doesn't show that

\neg \exists a : N -> R. \forall b : R. \exists n:N. a_n = b

fails in Sh(R). I don't know any topos where this fails.

Thomas

Nicolai Kraus

unread,
Jul 18, 2017, 10:41:07 AM7/18/17
to Andrej Bauer, homotopyt...@googlegroups.com
Hi Andrej and everyone reading the discussion,

I don't know the answer, but here's a related construction/question. 
Let's say we use "book HoTT" to have a precise definition for "surjective"
and so on, but let's not fix a concrete incarnation of constructive reals R. 
As you said, 2^N is not an accepted definition of the reals (it shouldn't be,
since we would expect that a functions R -> 2 which we can write down is
constant).

Let's write 3 := {0,1,2} and consider the quotient Q := (3^N)/~, where ~ relates
two sequences f,g : N -> 3 if both f and g have a "2" in their image.  (In other
words, we keep 2^N untouched and squash the whole rest into a single
equivalence class; this can directly be expressed as a HIT without any
truncations, by giving a point 'seq(f)' for every sequence f : N -> 3, a point 'other',
and an equality 'seq(f) = other' for every f that contains a 2.)

Question: For which definition of the real numbers R does the projection
3^N ->> 3^N/~ factor through R as in
  (*)  3^N >-> R ->> 3^N/~
        (injection followed by a surjection)?

  (**) Can we show that there is no surjection N -> 3^N/~,
        or what is the status of this?

The point is that most definitions of constructive reals are somewhat involved,
while 3^N/~ seems a bit simpler.  (*) and (**) together imply that there is no
surjection N ->> R.

For example, if R is the Cauchy reals that are defined to be "Cauchy sequences
N -> Q that are quotiented afterwards", then we can construct (*), e.g. by
mapping f to the Cauchy sequence s(f)_n := sum_{i = 0..n} 1/4^i * fi, where the '4'
guarantees that s is injective.  Vice versa, given a Cauchy sequence c, we can
construct a sequence r(c) : N -> 3 as follows.  To find r(c)_{n+1}, we check whether
the limit of c "has a chance" to lie in the interval between
s(c0, c1, ..., cn, 0, 0, 0, ...) and s(c0, c1, ..., cn, 0, 1, 1, 1, ...)
where "having a chance" means that the difference between the interval boundaries
and c_N is small enough (where "N" and "small enough" depend only on n and the
 rate of convergency in the definition of Cauchy reals).  If there "is a chance", we
choose r(c)_{n+1} := 0.
Similarly, we can check whether there "is a chance" that r(c)_{n+1} must be 1.
We can define "there is a chance" such that there cannot be a chance for both 0
and 1.  If there is no chance for either, we just choose r(c)_{n+1} := 2 and thus spoil
the whole sequence (it will necessarily lie in the "other" equivalence class).

The above is very similar to an idea in our partiality paper [1].  For that case,
Gaëtan Gilbert has refined the strategy so that it works with the higher inductive-
inductive reals of the HoTT book.  Does (*) work for the HIIT reals as well?

Best regards,
Nicolai

[1] Altenkirch, Danielsson, K; Partiality, Revisited. https://arxiv.org/abs/1610.09254
[2] Gilbert; Formalising Real Numbers in Homotopy Type Theory.
     https://arxiv.org/abs/1610.05072


--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

Gaetan Gilbert

unread,
Jul 18, 2017, 11:28:39 AM7/18/17
to HomotopyT...@googlegroups.com
I don't see how to do R -> 3^N/~ where R is HIT reals (without choice,
ofc with choice we can just go through quotiented cauchy sequences).

Gaëtan Gilbert
> send an email to HomotopyTypeThe...@googlegroups.com
> <mailto:HomotopyTypeTheory%2Bunsu...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout
> <https://groups.google.com/d/optout>.
>
>
> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com
> <mailto:HomotopyTypeThe...@googlegroups.com>.
Reply all
Reply to author
Forward
0 new messages