Timeline for In choiceless constructivism: If $f'=0$ then is $f$ constant?
Current License: CC BY-SA 4.0
34 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 12, 2020 at 20:30 | comment | added | Franka Waaldijk | I misjudged Open Induction, since Veldman showed that it implies the Fan Theorem, but not vice versa. The Fan Theorem being (more than) sufficient to prove the constancy principle then leaves Open Induction a quite secondary candidate. | |
| Apr 12, 2020 at 16:35 | comment | added | Emil Jeřábek | I see. Thank you for the explanation. | |
| Apr 12, 2020 at 16:25 | comment | added | Franka Waaldijk | @EmilJeřábek The way of reasoning that I mean here is this: integration over an interval of a uniformly continuous function is an extremely constructive procedure, no choice required. So if for a constructively defined $f$ with continuous derivative and given $x$, we compare $f(x)$ with $f(0)+\int_0^x f'(y)dy$, then both are constructively given real numbers. And it is a priori impossible that we arrive at a difference between these two real numbers, since that would contradict classical mathematics. | |
| Apr 12, 2020 at 16:02 | comment | added | Franka Waaldijk | @EmilJeřábek Sure :-). I just wanted to modify my original answer as little as possible. My original answer was too short, and just indicated the lines along which I was thinking (reconstructing $f$ from $f'$ for any differentiable $f$ with continuous derivative). The OP was correct in stating (in the chat possibly) that my reasoning was circular, since indeed to prove the FToC one would first prove what you demonstrate. However, I often prefer an answer which exhibits a $way$ of constructive reasoning, over one which 'only' gives a (partial) solution. | |
| Apr 12, 2020 at 14:51 | comment | added | Emil Jeřábek | If you assume that $f$ is locally uniformly differentiable with derivative $0$, doesn’t the constancy of $f$ follow trivially from the definition without using any integral identites? Given $x<y$ and $n$, let $K>|x|,|y|$ and $m$ be as in the definition, and fix an integer $d\ge2^m(y-x)$. Then $|f(y)-f(x)|\le\sum_{i<d}|f(x+(i+1)(y-x)/d)-f(x+i(y-x)/d)|\le2^{-n}\sum_{i<d}(y-x)/d=2^{-n}(y-x)$. Since $n$ was arbitrary, $f(x)=f(y)$. | |
| Apr 12, 2020 at 12:13 | comment | added | Franka Waaldijk | @AndrejBauer I'm starting to appreciate your comment about open induction more and more. I think this is perhaps the essence of the OP's question. When compactness really fails, like in RUSS, one still has the Lindelöf property, which 'should' also be sufficient since we do not per se need finite sums for approximation of $f$ through $f'$. But this can only be effective if we know that we will eventually reach $x+y$ from $x$, even if we have to traverse countably many intervals... | |
| Apr 12, 2020 at 11:21 | comment | added | Franka Waaldijk | And in fact, my answer does answer part of your question, since it shows very clearly that the problem can be seen as much in lack of Heine-Borel as in choice. I think that is a worthwhile contribution to reverse constructive mathematics. | |
| Apr 12, 2020 at 11:08 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
minor correction
|
| Apr 12, 2020 at 11:02 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
minor correction
|
| Apr 12, 2020 at 11:01 | comment | added | Franka Waaldijk | Ok I was thinking too much without choice, but there is still a compelling reason in BISH to incorporate 'locally uniformly differentiable''in the definition of 'differentiable'. I have adapted my answer to reflect your comment. | |
| Apr 12, 2020 at 10:58 | comment | added | wlad | Also, your claim that uniform differentiability is needed in BISH is incorrect. In fact, the constancy principle can be proved for pointwise differentiable functions using dependent choice. See: math.fau.edu/richman/docs/ptwise.pdf . In fact, from the perspective of BISH, I don't see the advantage of uniform differentiability over mere pointwise differentiability | |
| Apr 12, 2020 at 10:58 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
lay-out
|
| Apr 12, 2020 at 10:57 | comment | added | wlad | Sadly, this does not answer the question. The question asks specifically about pointwise differentiability, not uniform differentiability | |
| Apr 12, 2020 at 10:53 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
lay-out
|
| Apr 12, 2020 at 9:54 | comment | added | Franka Waaldijk | I will add this suggestion to my answer. | |
| Apr 12, 2020 at 9:54 | comment | added | Franka Waaldijk | @AndrejBauer Yes of course. The OP and I already discussed it briefly over the mail, having the exact same 'solution' in mind, or perhaps 'non-solution' since I have not yet received the OP's reply to my suggestion. | |
| Apr 11, 2020 at 15:28 | comment | added | Andrej Bauer | @FrankaWaaldijk if you think you have a proof please write out the details somewhere, rather than to trickle-truth it in the comments. I would be quite interested to see it. | |
| Apr 10, 2020 at 20:05 | comment | added | wlad | Let us continue this discussion in chat. | |
| Apr 10, 2020 at 20:04 | comment | added | Franka Waaldijk | Well, that is your risk to take... it seems unnecessary and precipitous to me to downvote an answer which you haven't really refuted. I trust you will reconsider. | |
| Apr 10, 2020 at 20:00 | comment | added | wlad | I'm going to downvote your answer. Sorry | |
| Apr 10, 2020 at 19:58 | comment | added | wlad | It may seem obvious to you that the identity can't be violated, but in the absence of a proof we don't know | |
| Apr 10, 2020 at 19:57 | comment | added | Franka Waaldijk | And it is impossible that the above identity should be violated... | |
| Apr 10, 2020 at 19:55 | comment | added | Franka Waaldijk | You have to consider that integration of such polynomial functions is actually computable... | |
| Apr 10, 2020 at 19:54 | comment | added | wlad | You're right about the derivative being uniformly continuous and therefore integrable | |
| Apr 10, 2020 at 19:46 | comment | added | Franka Waaldijk | No I believe it is really weaker. Because one only needs some estimate of the integral value on a certain interval, and one does not need a precise $z$ where a certain function value is assumed. | |
| Apr 10, 2020 at 19:44 | comment | added | wlad | The fragment you're referring to is surely no weaker than the constancy principle, which is the thing we're trying to prove | |
| Apr 10, 2020 at 19:42 | comment | added | Franka Waaldijk | ah yes I figured it out and looked up a proof on wikipedia... I do not think that the proof requires all of the mean value theorem. One only needs a fragment, which is true without choice I think. Also, in this case $f'$ is continuous since it is 0 everywhere... | |
| Apr 10, 2020 at 19:39 | comment | added | wlad | FToC is the Fundamental Theorem of Calculus | |
| Apr 10, 2020 at 19:38 | comment | added | wlad | Also, we have only that $f$ is pointwise differentiable. Its derivative might not even be Riemann integrable | |
| Apr 10, 2020 at 19:37 | comment | added | wlad | You're assuming the FToC which is usually proved using the constancy principle or something stronger | |
| Apr 10, 2020 at 19:36 | comment | added | Franka Waaldijk | ok I was pretty daring about it , please explain why it doesn't work? what is the FToC? | |
| Apr 10, 2020 at 19:36 | comment | added | wlad | You're assuming the FToC, whose proof is via the law of bounded change / mean value theorem | |
| Apr 10, 2020 at 19:35 | comment | added | wlad | That doesn't work | |
| Apr 10, 2020 at 19:31 | history | answered | Franka Waaldijk | CC BY-SA 4.0 |