Timeline for In choiceless constructivism: If $f'=0$ then is $f$ constant?
Current License: CC BY-SA 4.0
32 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 1, 2022 at 23:38 | history | edited | verret | CC BY-SA 4.0 |
edited title
|
| Dec 1, 2022 at 0:31 | answer | added | saolof | timeline score: 0 | |
| Nov 29, 2022 at 17:44 | history | edited | wlad | CC BY-SA 4.0 |
edited title
|
| Nov 29, 2022 at 17:20 | history | edited | wlad | CC BY-SA 4.0 |
Easier to understand than "constancy"
|
| Apr 12, 2020 at 19:05 | answer | added | Andrej Bauer | timeline score: 3 | |
| Apr 12, 2020 at 7:17 | comment | added | François G. Dorais | @AndrejBauer I added an answer (indeed based on a singular cover). I think it might be broken but perhaps there is a way to fix it... | |
| Apr 12, 2020 at 3:54 | answer | added | François G. Dorais | timeline score: 0 | |
| Apr 11, 2020 at 18:10 | comment | added | Andrej Bauer | @FrançoisG.Dorais: I don't have a proof, and in fact now I am worried that some trickery is possible with singular covers. | |
| Apr 11, 2020 at 15:29 | comment | added | Andrej Bauer | @FrançoisG.Dorais I would be interested in a reference showing the existence of such a function, too, especially since I think I can prove that it does not exist. | |
| Apr 11, 2020 at 15:25 | comment | added | Andrej Bauer | The approximate IVT requires no choice. | |
| Apr 11, 2020 at 9:39 | comment | added | François G. Dorais | I should be asleep by now, but unless I am mistaken you can get such a function from the "usual" proof that [0,1] is not compact in Eff. If that's not the case, I'll look back at this later this week. | |
| Apr 11, 2020 at 9:10 | comment | added | wlad | @FrançoisG.Dorais Is there a reference for the existence of such functions in the Effective Topos? | |
| Apr 11, 2020 at 9:00 | comment | added | François G. Dorais | So what goes wrong with a non-constant yet locally constant function for the definition of pointwize derivative? | |
| Apr 11, 2020 at 8:58 | comment | added | wlad | @FrançoisG.Dorais Locally constant but non-constant functions could be useful, but not in the Effective Topos. The constancy principle can be proved from Dependent Choice, which is available in the Effective Topos | |
| Apr 11, 2020 at 8:57 | comment | added | François G. Dorais | Non-constant locally constant functions don't exist because $\mathbb R$ is connected, but they do exist in the effective topos, for example, if I remember correctly. | |
| Apr 11, 2020 at 8:55 | comment | added | wlad | @FrançoisG.Dorais Classically, if a function has derivative $0$ everywhere then it is constant. Any such counterexample would also be a classical counterexample. So I think you're mistaken | |
| Apr 11, 2020 at 8:53 | comment | added | François G. Dorais | The question? Or am I mistaken? (I'm not entirely sure about the definition of derivatives.) | |
| Apr 11, 2020 at 8:52 | comment | added | wlad | @FrançoisG.Dorais To? | |
| Apr 11, 2020 at 8:52 | comment | added | François G. Dorais | Wouldn't a non-constant yet locally constant function be a counterexample? | |
| Apr 11, 2020 at 8:26 | comment | added | wlad | @EmilJeřábek I believe it is constructive, but the proof uses dependent choice | |
| Apr 11, 2020 at 8:23 | comment | added | Emil Jeřábek | Is an approximate mean value theorem also nonconstructive? | |
| Apr 10, 2020 at 19:43 | comment | added | Noah Schweber | Note for readers more familiar with classical model theory, "open induction" in Andrej Bauer's comment does not mean what it means in the context of weak theories of arithmetic in classical logic (namely, $IOpen$). | |
| Apr 10, 2020 at 19:31 | answer | added | Franka Waaldijk | timeline score: 3 | |
| Apr 10, 2020 at 18:07 | history | edited | wlad | CC BY-SA 4.0 |
added 26 characters in body
|
| Apr 10, 2020 at 15:46 | history | edited | wlad | CC BY-SA 4.0 |
edited title
|
| Apr 10, 2020 at 15:44 | comment | added | wlad | I see. Thanks hal.inria.fr/hal-01376054/document | |
| Apr 10, 2020 at 15:32 | comment | added | wlad | @AndrejBauer looking up "open induction" | |
| Apr 10, 2020 at 15:28 | comment | added | Andrej Bauer | Interesting. I think I can prove it using open induction, but not without anything. | |
| Apr 10, 2020 at 14:45 | comment | added | Andrej Bauer | I think a better title would be "The constancy principle in choiceless constructive foundations". | |
| Apr 10, 2020 at 12:17 | history | edited | wlad |
edited tags
|
|
| Apr 10, 2020 at 11:15 | history | edited | wlad | CC BY-SA 4.0 |
added 105 characters in body
|
| Apr 10, 2020 at 10:56 | history | asked | wlad | CC BY-SA 4.0 |