Quantifier Elimination: Proving Without Variables

[mathmari]

Hey!

Let $L=\{+, ' , 0, 1, T, C\}$ be the language where $ ' : \frac{d}{dz}$, $T(x) \Leftrightarrow x \notin \mathbb{C}$ (so $x$ is not constant), $C(x) \Leftrightarrow x \in \mathbb{C}$ (so $x$ is constant)

$x, f, g \in \mathbb{C}[z, e^{\lambda z } \mid \lambda \in \mathbb{C}]. $

(In this ring the differential equations have always a solution.)

We have the following formula
$$\exists x \phi (x , \overline{y}) \text{ where } \phi: \displaystyle{\bigwedge_{j=1}^n \phi_j} \text{ with } \phi_j : \left\{\begin{matrix}
Lx=f \\
Lx \neq g
\end{matrix}\right.$$

I want to find an equivalent quantifier-free formula. Some examples are the following:

• $$\begin{pmatrix}
  x'+x=f\\
  x''+x'=g
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  x'+x=f\\
  f'=g
  \end{pmatrix}$$
  
• $$\begin{pmatrix}
  x'+x=f\\
  x''+2x'=g
  \end{pmatrix} \overset{\text{Gauss elimination}}{\underset{\text{Linearity of differentiation}}{\Leftrightarrow}} \begin{pmatrix}
  x'+x=f\\
  f'=g
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  x=f-g+f'\\
  x'=g-f'
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  x=f-g+f'\\
  f-g'+f''=g-f'
  \end{pmatrix}$$
  
• $$\begin{pmatrix}
  x'+x=f\\
  x''+2x' \neq g
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  x'+x=f\\
  x'\neq g-f
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  x'+x=f\\
  x \neq g-2f
  \end{pmatrix} \Leftrightarrow \begin{pmatrix}
  \begin{pmatrix}
  (g-2f)'+(g-2f) \neq f\\
  x'+x=f
  \end{pmatrix}\\
  \begin{pmatrix}
  (g-2f)'+(g-2f)=f\\
  x'+x=f\\
  \text{kern}(x'+x) \neq \{0\}
  \end{pmatrix}
  \end{pmatrix} \overset{\text{In this ring it always stand that kern}(x'+x) = \{0\}}{\Leftrightarrow } \begin{pmatrix}
  (g-2f)'+(g-2f) \neq f\\
  x'+x=f
  \end{pmatrix}$$

To prove that there is a quantifier elimination I thought to do the following:

First by induction on the number of equations $n$ we show that a formula $\phi: \displaystyle{\bigwedge_{j=1}^n L_j x=f_j}$ can be reduced to the formula $Lx=f \land \psi_1$ where $\psi_1$ doesn't contain any $x$.

Then in the same way we show that a formula $\phi: \displaystyle{\bigwedge_{j=1}^n L_j x\neq g_j}$ can be reduced to the formula $Lx\neq g \land \psi_2$ where $\psi_2$ doesn't contain any $x$.

And then $\phi: \displaystyle{\bigwedge_{j=1}^n \phi_j}$ with $\phi_j : \left\{\begin{matrix}
Lx=f \\
Lx \neq g
\end{matrix}\right.$ can be reduced to the formula $L_1 x=f \land L_2 \neq g \land \psi$, where $\psi$ doesn't contain any $x$.

Is my idea correct? (Wondering)

 

[mmwave]

Hello! As a fellow scientist, I can say that your idea seems to be on the right track. However, I would suggest looking into the specific properties of the language $L$ and the equations you are dealing with in order to come up with a more detailed and rigorous proof. Also, it would be helpful to provide some more context and background information for those who may not be familiar with this specific topic. Overall, your approach seems to be a good starting point, but further refinement and clarification may be needed. Good luck with your research!