# Differential equations and axiom of choice

In the most general context, the Picard-Lindelöf theorem (aka Cauchy-Lipschitz 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?

-
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). –  Ricky Demer Nov 12 '12 at 19:34
The Cauchy-Lipschitz 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_1-x_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