Timeline for Cauchy real numbers with and without modulus
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 4, 2018 at 23:43 | comment | added | Mike Shulman | Also, meaning no disrespect to reverse mathematics, at the moment I'm not interested in eviscerated forms of mathematics where the image of a function might not exist. Can you describe a topos in which this phenomenon happens? | |
| Jan 4, 2018 at 23:40 | comment | added | Mike Shulman | I don't think you need to compute $k$ from $m$ to show that the image of $f$ is decidable. Decidability means $\forall k, (\exists n. f(n)=k) \vee \neg (\exists n. f(n)=k)$, which means that we're simply proving a statement about each $k$. We can therefore use $\exists$-elimination on a no-modulus Cauchy sequence to get an $m$ for that particular $k$, and then check all the $n\le m$ to see whether $f(n)=k$. | |
| Jan 4, 2018 at 22:40 | comment | added | Carl Mummert | Indeed, they comment on p. 193 that $\text{CT}_0$ is equivalent to saying that the function implicitly defined by an arithmetical $(\forall n)(\exists m)$ statement is always computable; finding the modulus of a Specker sequence is just a special case of this. | |
| Jan 4, 2018 at 22:14 | comment | added | Carl Mummert | Looking at Troelstra and van Dalen p. 268, to show that the image of $f$ is computable using their construction requires a modulus. They say "then for any $m$ we can find a $k$ with ..." - but in order to compute the range of $f$ we would need to compute $k$ from $m$, which is to say we need a computable modulus. (They are also working in the context of $\text{CT}_0$ there, but this is primarily to bridge the gap between the constructive meaning of "decidable" and the computable meaning. The range of $f$ does not exist in REC, which does not satisfy $\text{CT}_0$) | |
| Jan 4, 2018 at 21:53 | comment | added | Carl Mummert | @Mike Shulman: it's a bounded increasing sequence of rationals, so classically it is a Cauchy sequence (ignoring the issue of a modulus). Because the sentence expressing that this Specker sequence is (no-modulus) Cauchy is arithmetical, and because the definition of the sequence itself is arithmetical, this means that every $\omega$-model will believe that the sequence is no-modulus Cauchy. | |
| Jan 4, 2018 at 19:53 | comment | added | Mike Shulman | Hmm... I don't know much about recursive models, but I'm looking at the construction of a Specker sequence in Troelstra and van Dalen, and it looks to me as though it proves that if $f:\mathbb{N}\to\mathbb{N}$ is injective and $r_k = \sum_{i=0}^k 2^{-f(i)}$, and if $(r_k)$ is no-modulus Cauchy, then the image of $f$ is decidable -- from which I think one can deduce that $(r_k)$ in fact converges and is with-modulus Cauchy. So I don't understand how a Specker sequence can be no-modulus Cauchy. | |
| Jan 4, 2018 at 17:39 | comment | added | Mike Shulman | Thanks! I find it easier to think about toposes, but presumably there is a realizability topos containing a Specker sequence in which the same argument works. But what I would really understand much better is a topological model. | |
| Jan 4, 2018 at 17:27 | history | answered | Carl Mummert | CC BY-SA 3.0 |