Non-enumerability of R

Non-enumerability of R

[Andrej Bauer]

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

Non-enumerability of R

[Andrew Swan]

[-- Attachment #1: Type: text/plain, Size: 926 bytes --]

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

Re: [HoTT] Non-enumerability of R

[Andrej Bauer]

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

Re: [HoTT] Non-enumerability of R

[Andrej Bauer]

> 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?

Re: [HoTT] Non-enumerability of R

[Bas Spitters]

I once gave a proof (without Stone-Weierstrass) in the appendix of this paper:
http://www.cs.au.dk/~spitters/obs.pdf

On Sun, Jul 16, 2017 at 10:11 AM, Andrej Bauer <andrej...@andrej.com> wrote:
>> 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?
>
> --
> 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.

Re: [HoTT] Non-enumerability of R

[Andrej Bauer]

> 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.

Re: [HoTT] Non-enumerability of R

[Thomas Streicher]

On Mon, Jul 17, 2017 at 03:52:28PM +0200, Andrej Bauer wrote:
> > 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.

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

Re: [HoTT] Non-enumerability of R

[Nicolai Kraus]

[-- Attachment #1: Type: text/plain, Size: 4485 bytes --]

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


On Wed, Jul 12, 2017 at 10:04 AM, Andrej Bauer <andrej...@andrej.com>
wrote:

> 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
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 5600 bytes --]

Re: [HoTT] Non-enumerability of R

[Gaetan Gilbert]

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

On 18/07/2017 16:41, Nicolai Kraus wrote:
> 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
>
>
> On Wed, Jul 12, 2017 at 10:04 AM, Andrej Bauer 
> <andrej...@andrej.com <mailto:andrej...@andrej.com>> wrote:
>
>     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
>
>     --
>     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:HomotopyTypeTheo...@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>.
> For more options, visit https://groups.google.com/d/optout.