* Non-enumerability of R @ 2017-07-12 9:04 Andrej Bauer 2017-07-12 21:16 ` Andrew Swan 2017-07-18 14:41 ` Nicolai Kraus 0 siblings, 2 replies; 9+ messages in thread From: Andrej Bauer @ 2017-07-12 9:04 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Non-enumerability of R 2017-07-12 9:04 Non-enumerability of R Andrej Bauer @ 2017-07-12 21:16 ` Andrew Swan 2017-07-16 8:09 ` [HoTT] " Andrej Bauer 2017-07-18 14:41 ` Nicolai Kraus 1 sibling, 1 reply; 9+ messages in thread From: Andrew Swan @ 2017-07-12 21:16 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-12 21:16 ` Andrew Swan @ 2017-07-16 8:09 ` Andrej Bauer 2017-07-16 8:11 ` Andrej Bauer 0 siblings, 1 reply; 9+ messages in thread From: Andrej Bauer @ 2017-07-16 8:09 UTC (permalink / raw) Cc: 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-16 8:09 ` [HoTT] " Andrej Bauer @ 2017-07-16 8:11 ` Andrej Bauer 2017-07-16 18:35 ` Bas Spitters 2017-07-17 13:52 ` Andrej Bauer 0 siblings, 2 replies; 9+ messages in thread From: Andrej Bauer @ 2017-07-16 8:11 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-16 8:11 ` Andrej Bauer @ 2017-07-16 18:35 ` Bas Spitters 2017-07-17 13:52 ` Andrej Bauer 1 sibling, 0 replies; 9+ messages in thread From: Bas Spitters @ 2017-07-16 18:35 UTC (permalink / raw) To: Andrej Bauer; +Cc: 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 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. ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-16 8:11 ` Andrej Bauer 2017-07-16 18:35 ` Bas Spitters @ 2017-07-17 13:52 ` Andrej Bauer 2017-07-18 7:54 ` Thomas Streicher 1 sibling, 1 reply; 9+ messages in thread From: Andrej Bauer @ 2017-07-17 13:52 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-17 13:52 ` Andrej Bauer @ 2017-07-18 7:54 ` Thomas Streicher 0 siblings, 0 replies; 9+ messages in thread From: Thomas Streicher @ 2017-07-18 7:54 UTC (permalink / raw) To: Andrej Bauer; +Cc: Homotopy Type Theory 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-12 9:04 Non-enumerability of R Andrej Bauer 2017-07-12 21:16 ` Andrew Swan @ 2017-07-18 14:41 ` Nicolai Kraus 2017-07-18 15:28 ` Gaetan Gilbert 1 sibling, 1 reply; 9+ messages in thread From: Nicolai Kraus @ 2017-07-18 14:41 UTC (permalink / raw) To: Andrej Bauer; +Cc: HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Non-enumerability of R 2017-07-18 14:41 ` Nicolai Kraus @ 2017-07-18 15:28 ` Gaetan Gilbert 0 siblings, 0 replies; 9+ messages in thread From: Gaetan Gilbert @ 2017-07-18 15:28 UTC (permalink / raw) To: HomotopyTypeTheory 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. ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2017-07-18 15:28 UTC | newest] Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-07-12 9:04 Non-enumerability of R Andrej Bauer 2017-07-12 21:16 ` Andrew Swan 2017-07-16 8:09 ` [HoTT] " Andrej Bauer 2017-07-16 8:11 ` Andrej Bauer 2017-07-16 18:35 ` Bas Spitters 2017-07-17 13:52 ` Andrej Bauer 2017-07-18 7:54 ` Thomas Streicher 2017-07-18 14:41 ` Nicolai Kraus 2017-07-18 15:28 ` Gaetan Gilbert
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).