Timeline for Does the Brouwer fixed point theorem admit a constructive proof?
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 14, 2015 at 15:12 | comment | added | Asaf Karagila♦ | @Emil: It wasn't a constructive comment. :-) | |
| Apr 13, 2015 at 21:33 | comment | added | Emil Jeřábek | @AsafKaragila: I was just joking or not Can you prove this constructively? | |
| Apr 13, 2015 at 18:29 | history | edited | François G. Dorais | CC BY-SA 3.0 |
added 2 characters in body
|
| Apr 13, 2015 at 18:21 | comment | added | François G. Dorais | @AsafKaragila: I knew you were kidding, but it's still an interesting factoid about the argument. | |
| Apr 13, 2015 at 18:20 | history | edited | François G. Dorais | CC BY-SA 3.0 |
A more convincing view of the Bouwerian counterexample
|
| Apr 13, 2015 at 18:09 | comment | added | Asaf Karagila♦ | Now I'm not sure if you got that I was just joking or not. :| | |
| Apr 13, 2015 at 17:56 | comment | added | François G. Dorais | @coudy: We do have an algorithm to compute the $f$ I give and you can get a counterexample to BFPT using the usual trick that a fixed point of $f(x) + x$ is a root of $f(x)$. So it's easy to rescale and translate $f$ to show that BFPT is not constructive for the unit interval. | |
| Apr 13, 2015 at 17:50 | comment | added | François G. Dorais | @AsafKaragila: No, the argument is constructive: its a proof of a negation, not a proof by contradiction! I show that it is impossible to have a constructive proof of IVT, which is the constructive way of proving a negative statement. | |
| Apr 13, 2015 at 17:26 | comment | added | coudy | This is an interesting answer. My question is in the spirit of Guntram comment though. Assume we have an algorithm to compute the values of f, can we find an arbitrary approximation to a fixed point. IVT and dichotomy look constructive to me from that viewpoint. What about BFPT? | |
| Apr 13, 2015 at 16:54 | comment | added | Asaf Karagila♦ | This is not a constructive proof, since it relies on the law of excluded middle, that either LLPO is constructive or it is not. What happens if this information cannot be computed? :-) | |
| Apr 13, 2015 at 16:31 | comment | added | François G. Dorais | @Guntram: That's right: what I show is that IVT is actually equivalent to LLPO (assuming you believe LLPO can be repeated indefinitely in order to carry out the usual bisection argument). So if you believe LLPO is constructive or you have other ways to get around this issue, then everything is fine! | |
| Apr 13, 2015 at 16:22 | comment | added | Guntram | This is not a constructive answer. Obviously what is meant by "constructive proof" is that when everything in sight is computable and decidable, then the proof allows to extract an algorithm which yields an approximation scheme. | |
| Apr 13, 2015 at 16:04 | history | answered | François G. Dorais | CC BY-SA 3.0 |