There is a proof of Peano existence theorem in ZF.

Peano existence theorem:

For any open $D \subseteq \mathbb{R}^2$, continuous $f:D \to \mathbb{R}$ and initial condition $\langle t_0,x_0\rangle \in D$, there is an open interval $I \subseteq \mathbb{R}$ with $t_0 \in I$ and a differentiable function $X: I \to \mathbb{R}$ such that $X(t_0)=x_0$ and $X'(t) = f(X(t),t)$ for all $t \in I$, and no strictly larger $I_\ast \supset I$ has such a function extending $f$.

reference: https://mathoverflow.net/a/455875

The proof in the link uses a theorem in mathematical logic called Shoenfield absoluteness to automatically translate ZFC proofs of low quantifier complexity statements about countably coded objects to ZF proofs.

I am not familiar with mathematical logic and advanced set theory, nor do I understand Shoenfield absoluteness. Even if I understand it, I expect the proof generated by automatic translation to be not very human readable.

Is there a proof of this theorem in ZF that can be understood by an undergraduate student who is not a set theory major?


1 Answer 1


Since you are requiring that there is no strictly larger interval on which a solution would be defined, you are talking about the global version of Peano's existence theorem. This was proved in ZF (without choice) without using Shoenfield absoluteness in the following recent publication:

Hrbacek, K.; Katz, M. "Peano and Osgood theorems via effective infinitesimals." Journal of Logic and Analysis 15:6 (2023), 1-19. https://doi.org/10.4115/jla.2023.15.6 https://arxiv.org/abs/2311.01374


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .