In the most general context, the PicardLindelöf theorem (aka CauchyLipschitz in French) asserts the existence of a maximal solution for $\dot{x}(t) = f(t,x(t))$, i.e. of a solution $x(t)$ defined on a interval $I$ such that there exist no other solution whose restriction to $I$ coincide with $x$. The usual proofs of this (when $f$ is such that there is no local unicity) use Zorn's lemma, or some other weaker form of choice. But is this result actually not provable in ZF?

2$\begingroup$ I though the ODE theorem for when $f$ is such that there is no local unicity, was the $\hspace{.5 in}$ en.wikipedia.org/wiki/Peano_existence_theorem (in English). $\endgroup$ – user5810 Nov 12 '12 at 19:34

1$\begingroup$ The CauchyLipschitz theorem in french or in any other language is dealing with the case where $f$ is locally Lipschitz continuous with respect to $x$, i.e. satisfies an estimate of type $$ \vert f(t,x_1)f(t,x_2)\vert\le \alpha(t) \vert x_1x_2\vert, $$ with $\alpha \in L^1_{loc}$. In that case, local uniqueness occurs for the ODE. $\endgroup$ – Bazin Nov 12 '12 at 21:20
At least for scalar equations $\dot x(t)=f(t,x(t))$, that is with a nonlinearity $f\in C^0(\Omega,\mathbb{R})$, defined on an open set $\Omega\subset \mathbb{R}^2$, the Zorn's lemma is not necessary: the order structure of $\mathbb{R}$ allows to select a preferred solution (actually, two)
Any IVP admits an upper and a lower solution, whose domains are maximal intervals. For $(t_0,x_0)\in\Omega$, define, for $t\in\mathbb{R}$ $$x ^ * (t):=\sup\big\{x(t)\, : x\in C^1(\mathrm{co}(t_0,t),\, \mathbb{R}),\, \mathrm{graph}(x)\subset\Omega, x(t_0)=x_0, \dot x(s)=f(s,x(s)) \big\}\, ,$$ (where of course $\sup\emptyset=\infty$). Define $\mathrm{dom}(x ^ *)$ to be the connected component of $t_0$ in the set $\{ t: x ^ *(t) \in\mathbb{R} \}$. Then, $x ^ *$ is a solution of the ODE with IVC $x(t_0)=x_0$, maximally defined on the interval $\mathrm{dom}(x ^ *)$.

$\begingroup$ As to the case of systems, that is $\Omega\subset\mathbb{R}\times\mathbb{R}^n$ and $f\in C^0(\Omega,\mathbb{R}^n)$, it seems to me that the same construction can be used, using the lexicographic order on $\mathbb{R}^n$. $\endgroup$ – Pietro Majer Jan 23 '13 at 14:35

$\begingroup$ A similar proof can be found in the paper of Wolfgang Walter American Math Monthly vol 78 1971 pages 170173 . $\endgroup$ – Mohan Ramachandran Jan 23 '13 at 19:19

1$\begingroup$ Actually, one should go and see the original proof of the theorem, by Giuseppe Peano. No surprise if we found it's the best proof. $\endgroup$ – Pietro Majer Jan 23 '13 at 19:33