Timeline for Proof of global Peano existence theorem in ZF?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 3, 2023 at 17:49 | comment | added | James E Hanson | @MikhailKatz At the moment I'm only contemplating writing a paper about these topics, so it won't be done any time soon if I do write one, but thank you for the consideration. | |
| Nov 3, 2023 at 11:14 | comment | added | Mikhail Katz | @JamesHanson, we just posted our text on the arxiv and I updated my question. Let me know if you are planning to publish anything along the line of your answer. Our article is still in galley proofs at JLA and we may be able to include a reference. | |
| Nov 2, 2023 at 11:59 | vote | accept | Mikhail Katz | ||
| Oct 8, 2023 at 15:51 | comment | added | James E Hanson | @MikhailKatz Is the precise version of the theorem you're considering written down somewhere? I'm seeing slightly different versions in places. | |
| Oct 8, 2023 at 15:06 | comment | added | Mikhail Katz | @JamesHanson, there is a related result called Osgood's theorem which is reversed by Simpson to ACA$_0$ but also only locally (rather than on a maximal interval of solution). Osgood theorem asserts the existence of a unique solution greater than all other solutions with the same initial data. Since one is now comparing different solutions, I am not sure this would fit within the $\Pi_4^1$ framework, but maybe it does? | |
| Oct 8, 2023 at 12:28 | comment | added | Mikhail Katz | @Holo, in your opinion would global Peano existence theorem be provable in WKL$_0$ as well? Or rather in a stronger system of second order arithmetic? | |
| Oct 5, 2023 at 13:40 | comment | added | James E Hanson | Officially the quantifiers in $\Pi^1_4$ sentences need to be ranging over real numbers. As Holo is saying, in order to talk about Lebesgue measurability in general you do actually need to quantify over sets of real numbers, not just real numbers. | |
| Oct 5, 2023 at 9:52 | comment | added | Holo | @MikhailKatz everything in Peano's theorem is countably coded, so you don't lose anything when translating it to ZF. Sometimes you do have cases where WKL_0 (or other weak systems) proves statement A but not prove statement B, but ZF- (or other strong system) prove that A is equivalent to B, fortunately it is not the case here, Simpson proved Peano's theorem in it's original form | |
| Oct 5, 2023 at 9:51 | comment | added | Mikhail Katz | @Holo, I am not sure if this answers my question about $\Pi_4^1$. Let's say we are working on the Solovay model of ZF+ADC, where every set is Lebesgue-measurable (so there is no need to code Lebesgue measurable sets). I was wondering why countable additivity of Lebesgue measure is not in $\Pi_4^1$. I don't have much experience working with these classes (I am not a set theorist) and this may be obvious. | |
| Oct 5, 2023 at 9:46 | comment | added | Holo | @MikhailKatz Lebesgue measurable sets are not countably coded | |
| Oct 5, 2023 at 9:41 | comment | added | Mikhail Katz | @Holo, yes, but the reals are represented in weak systems of second-order arithmetic by special coding, especially at low levels such as RCA$_0$ and WKL$_0$. ZFC certainly proves all of those results, but the weak systems sometimes prove results that are not entirely equivalent to their ZF versions. | |
| Oct 5, 2023 at 9:39 | comment | added | Holo | @MikhailKatz by "pure existential statement" James means Peano's existence theorem without the additional "global" condition (that there is a maximal interval). Not sure what you mean by "equivalent to the usual ZF version", ZF proves everything that ${\sf {WKL}}_0$ can prove when talking about sets of naturals (i.e. reals) | |
| Oct 5, 2023 at 8:30 | comment | added | Mikhail Katz | This seems like a bit of a miracle. Can you comment briefly why countable additivity of the Lebesgue measure is not $\Pi_4^1$ ? | |
| Oct 5, 2023 at 8:24 | comment | added | Mikhail Katz | Can you elaborate on what "the pure existential statement" means? My understanding is that due to issues of coding, the WKL$+)$ version of Peano existence is not really equivalent to the usual ZF version. This is of course true of many results, not merely Peano existence theorem. | |
| Oct 4, 2023 at 22:39 | history | answered | James E Hanson | CC BY-SA 4.0 |