Quantifier Elimination: Proving Without Variables

  • MHB
  • Thread starter mathmari
  • Start date
  • Tags
    Elimination
In summary, the conversation discusses the language $L$ and its properties, as well as the search for an equivalent quantifier-free formula in this language. The idea presented is to use induction to reduce a formula with multiple equations to a simpler form without any $x$ variables. It is suggested to consider the specific properties of $L$ and the equations in order to come up with a more thorough proof. More context and background information is also recommended for those unfamiliar with the topic.
  • #1
mathmari
Gold Member
MHB
5,049
7
Hey! :eek:

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)
 
Physics news on Phys.org
  • #2


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!
 

FAQ: Quantifier Elimination: Proving Without Variables

What is quantifier elimination?

Quantifier elimination is a method used in mathematical logic and computer science to prove the existence of a solution to a logical formula without explicitly using variables. It simplifies the formula by eliminating the quantifiers, such as "for all" and "there exists", and replacing them with equivalent statements.

How does quantifier elimination work?

Quantifier elimination works by transforming a logical formula into an equivalent formula without any quantifiers. This is achieved by using techniques such as substitution, rewriting, and simplification. The resulting formula is often easier to work with and can be used to prove the existence of a solution without the need for variables.

What types of problems can be solved using quantifier elimination?

Quantifier elimination can be used to solve a wide range of problems in mathematics and computer science, including polynomial equations, linear inequalities, and boolean satisfiability problems. It is particularly useful in automated theorem proving and model checking, where it can significantly reduce the complexity of the problem.

What are the benefits of using quantifier elimination?

The main benefit of using quantifier elimination is that it simplifies the problem by eliminating the need for variables, making it easier to prove the existence of a solution. It also helps to reduce the complexity of the problem, making it more tractable for automated reasoning tools. Additionally, quantifier elimination can provide insights into the structure of the problem, leading to new discoveries and proofs.

Are there any limitations to quantifier elimination?

While quantifier elimination can be a powerful tool, it does have some limitations. It is only applicable to certain types of logical formulas, and the resulting formula may still be complex and difficult to work with. Additionally, the process of quantifier elimination can be computationally intensive, making it impractical for certain types of problems.

Similar threads

Replies
4
Views
1K
Replies
9
Views
1K
Replies
5
Views
1K
Replies
10
Views
1K
Replies
6
Views
1K
Replies
3
Views
1K
Replies
16
Views
2K
Back
Top