Timeline for Proof of global Peano existence theorem in ZF?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 4, 2023 at 9:12 | comment | added | Gro-Tsen | @SamSanders Could you have a look at this other question and give some details there about your “beside the point” comment? | |
| Nov 3, 2023 at 10:53 | comment | added | Mikhail Katz | @Holo, can you elaborate? Do you think the global version of Peano reverses to WKL$_0$? | |
| Nov 3, 2023 at 9:26 | history | edited | Mikhail Katz | CC BY-SA 4.0 |
added 202 characters in body
|
| Nov 2, 2023 at 11:59 | vote | accept | Mikhail Katz | ||
| Oct 5, 2023 at 18:52 | comment | added | Sam Sanders | The following is perhaps a little "beside the point", but since you tagged the question with "reverse math", I will say the following: while an interesting enterprise, the question whether one needs AC for a given theorem is somewhat beside the point from the pov of reverse math: there are basic thms that are equivalent to WKL_0, assuming a little bit of countable choice; these thms are also provable without AC, but a proof without AC needs as much comprehension as Z$_2$ can provide. | |
| Oct 4, 2023 at 22:39 | answer | added | James E Hanson | timeline score: 6 | |
| Oct 4, 2023 at 14:05 | comment | added | Holo | Stephen G. Simpson has shown that over RCA_0, Peano's existence theorem is equivalent to WKL. I would imagine that adding the maximality condition is possible without too much effort | |
| Oct 4, 2023 at 13:06 | comment | added | Mikhail Katz | I should mention that we have a proof of global Peano in SPOT that's currently submitted. | |
| Oct 4, 2023 at 13:06 | comment | added | James E Hanson | Yes it would, but as I indirectly discuss in that answer Peano's theorem (including the maximality condition) should be $\Pi^1_4$. | |
| Oct 4, 2023 at 13:05 | comment | added | Mikhail Katz | @JamesHanson, so if by some weird accident, this method happens not to work for global Peano, that would answer your earlier question about ordinary mathematics? :-) | |
| Oct 4, 2023 at 13:01 | comment | added | James E Hanson | I also asked a question asking for examples of this method not applying to 'ordinary mathematics' and so far no one has supplied an example that isn't closely related to obviously set-theoretic issues. | |
| Oct 4, 2023 at 12:57 | comment | added | James E Hanson | I'd be happy to write it out as an answer, although I don't have time at this moment. I actually wrote up an explanation of almost this specific case in an answer about a month ago. Unfortunately though, a more precise explanation is probably the topic of an expository paper (which I have been contemplating). | |
| Oct 4, 2023 at 12:54 | comment | added | James E Hanson | To be clear, you also want that the resulting solution is maximal in the sense that its interval of definition can't be extended any further, right? | |
| Oct 4, 2023 at 12:52 | comment | added | Mikhail Katz | @JamesHanson, I would much appreciate if you could elaborate. Feel free to post this as an answer. | |
| Oct 4, 2023 at 12:45 | comment | added | James E Hanson | I don't know if it's written out explicitly somewhere, but it should be provable in ZF by a fairly direct absoluteness argument. The vague idea is that you can form a real number $\alpha$ that codes the data associated to the specific IVP. Then in $L[\alpha]$, choice holds and you can solve the IVP there. The solution will then have a unique extension to a differentiable function in $V$ which will still solve the problem. | |
| Oct 4, 2023 at 11:15 | history | asked | Mikhail Katz | CC BY-SA 4.0 |