# the solution of ode can be encoded as first order logic

Consider the following sytem of ODEs

$\dot{x}= Ax$, and given $x(0)$,

where $A$ is a $n\times n$ matrix with rational entries.

Can I encode the solution, say $x(t)$ for a given $t$, as a first order logic formula over $(R, +, \cdot, e^x, 0, 1)$?

Here, let us assume that $x(t)$ has real entries.

The difficulty I can see is that some eigenvalue of A is an algebraic number, so the solution invloes some sin and cosin. I do not know how to overcome this.

Thanks.

-
Here(en.wikipedia.org/wiki/Differential_algebra) but nothing elsea is a link to the Wikipedia page for differential algebra. I recalled the existence but nothing else of this field. Perhaps it will help. – Jay Jul 8 '12 at 23:44

Partial answer. This seems to be equivalent to asking whether you chosen language can express the notion "$n$ is an integer".
First, if you can express solutions to linear ODEs, then an "integer" is a number $t$ such that $\sin(\pi t)=0$, and $(\sin,\cos)$ are solutions to a well-known ODE system of the kind you're considering.
On the other hand, if we can express integerness and also have $\cdot$ and $+$, then every computable function can be expressed (using Gödel's $\beta$ function to encode primitive recursion and building up from there). And then we can just program a numerical simulation of the ODE and write down a first-order-formula for "the limit of the output of the simulation as the step size tends to 0".
So can integers be recognized by $(\mathbb R, {+}, {\cdot}, \exp, 0, 1)$? Beats me. It's not obviously possible, but on the other hand the real exponential function is closely enough related to the complex one that I won't rule it out either.
As an example of something that almost but not quite works: $a\in\mathbb R$ is a nonnegative integer iff every higher derivative of $x\mapsto e^{a\cdot \log x}$ is bounded on $(0,1)$. Unfortunately, "every higher derivative" is hard to express without already having integers in the first place. – Henning Makholm Jul 9 '12 at 0:46