Timeline for In choiceless constructivism: If $f'=0$ then is $f$ constant?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 14, 2020 at 2:57 | history | edited | François G. Dorais | CC BY-SA 4.0 |
added warning
|
| Apr 12, 2020 at 20:23 | comment | added | Franka Waaldijk | @AndrejBauer Well you're right. it is not valid in RUSS. Veldman showed that Open Induction implies the fan theorem, but not vice versa, see here. | |
| Apr 12, 2020 at 18:21 | comment | added | Andrej Bauer | @FrankaWaaldijk: is open induction valid in RUSS? | |
| Apr 12, 2020 at 15:42 | comment | added | François G. Dorais | @Andrej Yes, that's the issue from my first comment. | |
| Apr 12, 2020 at 12:34 | comment | added | Franka Waaldijk | Wouldn't any counterexample also be a counterexample to open induction? | |
| Apr 12, 2020 at 10:01 | comment | added | Andrej Bauer | For example, why is $f(1) = \mu(C)$ a computable number? Note that $n \mapsto \sum_{k=0}^n (b_k - a_k)$ is a Specker sequence and hence its limit is only a lower-computable real (but that's not even important as there can be overlap between the intervals). | |
| Apr 12, 2020 at 9:51 | comment | added | Andrej Bauer | Also, how do you compute the value of $f(x)$? I can see that you can compute upper approximations of $f(x)$, but how do you ever get a lower approximation? | |
| Apr 12, 2020 at 9:48 | comment | added | Andrej Bauer | Are you just talking about singular covers here? | |
| Apr 12, 2020 at 7:26 | history | edited | François G. Dorais | CC BY-SA 4.0 |
fixed variable confusion
|
| Apr 12, 2020 at 4:38 | comment | added | François G. Dorais | I think this function $f\colon\mathbb R \to \mathbb R$ might not be well-defined in the effective topos but some variation of this idea might work. | |
| Apr 12, 2020 at 3:54 | history | answered | François G. Dorais | CC BY-SA 4.0 |