Elimination of quantifiers in the strucure of polynomials and in the structure of exponentials

110 Views Asked by At

I am looking at the elimination of quantifiers.

In my notes there is the following:

$L=\{+, ' , T, 0, 1\}$ ($"="$ is meant to be included in $L$)

First-order Logic: $Q_1 x_1 \dots Q_m x_m \ \ [\phi ]$ where $Q_1, \dots , Q_m$ are the quantifiers ($\exists , \forall$), $\phi$ is a boolean combination of atomic formulae ( $t_1 R t_2$ (where $t_1, t_2$ are terms, $R$ is a predicate), $R(t)$ (where $R$ is a predicate) )

The terms can be built from the elements of the language. Terms are for example: $0$, $x$, $x+y$, $x'$, $(x+y)'+x'+1+1$

A sentence without quantifiers has no variables, for example $1=0$, $1'=0$.

Reduction of sentences to sentences without quantifiers.

Let $\mathcal{A}$ be a structure in that we interpret $L$, for example $\text{Exp}(\mathbb{C})$.

Elimination of quantifiers: For each formula $\psi$ there is a formula $\psi_0$ without quantifiers such that in the strucutre $\mathcal{A}$ the following is a tautology: $$\exists x \ \ \psi (x) \leftrightarrow \psi_0$$ i.e., $$\mathcal{A} \models \exists x \ \ \psi (x) \leftrightarrow \psi_0$$

It suffices to mention only the existential formulas since $$\neg \exists x \ \ \psi (x)\equiv \forall x \ \ \neg \psi (x) \\ \neg \forall x \ \ \psi (x)\equiv \exists x \ \ \neg \psi (x)$$

$$L=\{+, -, ', T, 0, 1\}$$

$$\models \exists x \ \ \left (x=a \land x=b\right ) \leftrightarrow a=b \\ \exists x \ \ \left (x+y=a \land x-y=b\right ) \leftrightarrow 2y=a-b$$

A term $t$ is of the form $$t\equiv t(x)+t_0$$ that means that $t(x)$ is a term that contains $x$, that is constructed by the language $L$, and $t_0$ is constructed by the language $L$ and it doesn't contain $x$.

$$$$


$$$$

Let $T(x)$ be the predicate that $x$ is non-constant.

$$$$

Consider the expression $$\exists x \left (x'+x=1 \land T(x) \right ) \tag 1$$ Since the solution of the differential equation $x'+x=1$ is $x(t)=1-Ce^{-t}$, we can eliminate the quantifier at $(1)$ in the structure $\text{Exp}(\mathbb{C})$, so in this case it is $$\exists x \left (x'+x=1 \land T(x) \right ) \leftrightarrow 0=0$$ but we cannot eliminate the quantifiers in the structure of polynomials, so in this case it is $$\exists x \left (x'+x=1 \land T(x) \right ) \leftrightarrow 1=0$$

Is this correct?

$$$$

Consider the expression $$\exists x \left (x'+x=t \land T(x) \right ) \tag 2$$ Since the solution of the differential equation $x'+x=t$ is $x(t)=Ce^{-t}+t-1$, we cannot eliminate the quantifier at $(2)$ neither in the structure of polynomials nor in the structure $\text{Exp}(\mathbb{C})$. So in both cases it is $$\exists x \left (x'+x=t \land T(x) \right ) \leftrightarrow 1=0$$

Is this correct?

1

There are 1 best solutions below

18
On BEST ANSWER

(1) We can eliminate (alteast) some of the quantifiers in the structure of polynomials as you did (correctly).

(2) Again you eliminated quantifiers correctly (as the sentence is false in both theories).

In both cases you eliminated the quantifiers by replacing the formula by false formula so you are indeed eliminating quantifiers. If the formula in a theory is always false or always true you can eliminate quantifiers from it by the method you used above, just the description of what you did doesn't match what you really did. You are saying that the solution doesn't exist and at the same time you provide one.