Timeline for What happens when we print the digits of a real number?
Current License: CC BY-SA 2.5
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 30, 2010 at 8:36 | vote | accept | Neel Krishnaswami | ||
| Jul 29, 2010 at 17:04 | comment | added | Andrej Bauer | @Neel: essentially, no, because the TTE people don't care about the fact that they are working inside a model of intuitionistic logic. What they call a realizer for a multivalued map is in fact a realizer for a $\forall \exists$ statement claiming that the map always gives at least one result. There is nothing mysterious going on. Whenever you have $\forall x \exists y . R(x,y)$ you can define a multivalued map $f(x) = \lbrace y \mid R(x,y) \rbrace$ and be sure that $f(x)$ is inhabited. And this is equivalent to working with total relations via isomorphism $P(Y)^X \cong \Omega^{X \times Y}$. | |
| Jul 29, 2010 at 12:46 | comment | added | Neel Krishnaswami | @Andrej: Also, I find the idea that multivalued functions have an autonomous status intuitionistically very intriguing. Is there a good reference to its use in type two effectivity? | |
| Jul 29, 2010 at 11:11 | comment | added | Andrej Bauer |
Let me be a bit more specific: pure Martin-Löf type theory is not a good foundation of mathematics, provided we interpret mathematical spaces as members of the universe Set. To get real mathematics going, we need to pass to the more complicated setoids (sets equipped with a notion of equality), as was already mentioned by Peter in another answer. But why make our lives so complicated? It is then easier and conceptually cleaner to just axiomatize setoids in terms of (another level) type theory with primitive logical connectives that are not identified with type constructors.
|
|
| Jul 29, 2010 at 11:07 | comment | added | Andrej Bauer | @Neel: it cannot be so viewed. But type theory with proof relevance everywhere in sight isn't a reasonable foundatation for mathematics, if you ask me. Existential quantifiers are not proof relevant and so they should not be interpreted by $\Sigma$'s. I rather like the idea of having a type theory with logic on top, a la Peter Aczel and Nicola Gambino, or a la Giovanni Sambin and Milly Maietti. | |
| Jul 29, 2010 at 8:15 | comment | added | Neel Krishnaswami | @Andrej: the existential in your option 1 cannot be viewed as a $\Sigma$-type in type theory (with an equality type and fst/snd-style elims for sigma), right? Two representations of the same real can yield different digit expansions, and so I guess we can't view the statement as a function? | |
| Jul 29, 2010 at 7:35 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
incorporated comments
|
| Jul 29, 2010 at 7:24 | comment | added | Andrej Bauer | @Carl: If I am not mistaken, assuming convergence of a Specker sequence of the usual kind, namely $a_n = \sum_{j < n} 3^{-e(j)}$ where $e$ enumerates the Halting set without repetitions, we can solve the Halting problem. So a convergent Specker sequence entails some amount of omniscience. It is interesting to think what happens in topological models. Any particular Specker sequence is convergent there (because modulus of convergence need not be computable in order to exist), but I am not sure that the space of Specker sequences (what would that be?) is contained in $\mathbb{R}$. | |
| Jul 29, 2010 at 7:21 | comment | added | Andrej Bauer | @Carl: That's an interesting observation. So assuming countable choice we have: for every Cauchy sequence there exists one with a fixed modulus of convergence (but there is no conversion function), and there is a map which goes from fixed-modulus Cauchy sequences to fixed-modulus monotone Cauchy-sequences. Nevertheless, we cannot show that every fixed-modulus monotone Cauchy sequence has a decimal digit expansion. I will edit my answer. | |
| Jul 29, 2010 at 0:02 | comment | added | Carl Mummert | The answer to my last question is easier than I thought. If there was a continuous map like that, there would be an initial segment of (2, 3, 3, all 3's ... ) which was enough to guarantee that the limit of the corresponding increasing sequence was larger than 2, so the map would give a bad result for any sequence that starts out like that one and then goes back to 2 after that initial segment. But if we fix a modulus of convergence, there is a continuous map that works for all sequences with that modulus of convergence, e.g. $F((a_i),n)=\max \{ a_i−2^{−i} :i \leq n \}$. | |
| Jul 28, 2010 at 22:49 | comment | added | Carl Mummert | I deleted a comment about the continuity argument, which should have been before the previous comment. I don't completely understand your continuity argument, but we agree on the conclusion in any case. Is there some easy way to see (with no proof theory) that, classically, "we cannot continuously deform a Cauchy sequence into an increasing Cauchy sequence converging to the same limit"? That, really, is what I was thinking about. | |
| Jul 28, 2010 at 22:40 | comment | added | Carl Mummert | As for the constructive side: of course you know more about these things than I do. But regarding Specker sequences: we don't need to prove Specker sequences are Cauchy sequences, we only need a model in which they are (without decimal expansions). If the informal system you are thinking of has enough choice (which is constructively unproblematic anyway, in the context of arithmetic), then it proves every Cauchy sequence has a modulus of convergence. If it has sufficiently limited choice then REC should be a model of your system, which contains a Specker sequence without a decimal expansion. | |
| Jul 28, 2010 at 21:39 | comment | added | Andrej Bauer | And another thing: Specker sequences cannot be shown to be Cauchy sequences, unless you're assuming something non-constructive, so that's not a counter-example in this context. As I said, I was doing informal constructive mathematics and I meant that seriously. | |
| Jul 28, 2010 at 21:36 | comment | added | Andrej Bauer | @Carl: Where did I say that a decimal expansion can be computed from an increasing Cauchy sequence? Unless I am blind, I didn't, so I don't know how to answer your comment. | |
| Jul 28, 2010 at 19:36 | comment | added | Carl Mummert | I don't see how having increasing Cauchy sequences would help with computing the decimal expansion. The fundamental example of a computable Cauchy sequence without a computable decimal expansion is a Specker sequence, which is already increasing. | |
| Jul 28, 2010 at 19:34 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
added 163 characters in body
|
| Jul 28, 2010 at 19:28 | history | answered | Andrej Bauer | CC BY-SA 2.5 |