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?

2I 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). – user5810 Nov 12 '12 at 19:34

1The 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. – 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 ^ *)$.

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$. – Pietro Majer Jan 23 '13 at 14:35

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

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