# Decidability of differential equations

Is there anything well-known about the algorithmic decidability of the satisfiability of an ODE $\dot{x}=f(x)$, $x: [0,1]\to R^n$ with an initial condition $x(0)=x_0$, given that $f(x)$ belongs to some specified class of functions -- for example, component-wise polynomial?

• Please define "satisfiabiity". – Alexandre Eremenko Jan 13 '14 at 2:01
• Existence of a $C^1$ solution. – Peter Franek Jan 13 '14 at 2:21
• I think the standard Picard existance theorem would answer the question as posed, and it only requires that $f(x)$ be Lipschitz. But then it's not clear to me what the "decidability" and "differential-algebra" tags have to do with the question. – Igor Khavkine Jan 13 '14 at 3:33
• The Theorem you mention only gives local solution (on some neighborhood). My question is about the existence of a global solution, on [0,1] (or, (0, infty)..) – Peter Franek Jan 13 '14 at 3:34

If $f$ is a polynomial, then $C^1$ solution is the same as analytic solution. For analytic solutions, very similar questions are considered in the paper

MR1011182
Denef, J., Lipshitz, L. Decision problems for differential equations. J. Symbolic Logic 54 (1989), no. 3, 941–950,

which also contains a survey of earlier results.

I suppose that one can conclude from this paper, and the results cited in it, that the question is undecidable. They also mention some cases when it is decidable.

• Do you maybe know where I can find the paper you are referring at? Do you maybe have a link? Or can you send it to me? – Mary Star Aug 28 '15 at 0:58
• If you are in a US university, and your library does not have it, use ILL service (interlibrary loan). If you are in other country, ask your librarian. – Alexandre Eremenko Aug 28 '15 at 1:08
• If none of the above helps, write to the authors, and request a copy. – Alexandre Eremenko Aug 28 '15 at 1:09

In the the paper Boundedness of the Domain of Definition is Undecidable for Polynomial ODEs by Daniel S. Graça et al. (preprint version) they prove the undecidability of deciding the boundedness of the maximal domain of solution of a polynomial ODE.