the solution of ode can be encoded as first order logic

122 Views Asked by At

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.

1

There are 1 best solutions below

1
On

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.