Can Quantifiers Be Eliminated in These Differential Equations?

[mathmari]

Hey!

I am looking at the elimination of quantifiers.

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)$ when we are looking at the exponentials, but not when we are looking at the polynomials.

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 at the case of polynomials nor at the case of exponentials.

Is this correct?

 

[Evgeny.Makarov]

Could you explain what you mean by "eliminating the quantifier" and "looking at the exponentials"?

 

[mathmari]

Could you explain what you mean by "eliminating the quantifier" and "looking at the exponentials"?

Let $\mathcal{A}$ be a structure, 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$$ For example, when we have the formula $$\exists x \left (x'+x=0 \land T(x)\right )$$ since the solution is $x(t)=Ce^{-t}$, in the structure $\text{Exp}(\mathbb{C})$, i.e., at the exponentials, we can eliminate the quantifier (the existential symbol $\exists$) since $$\exists x \left (x'+x=0 \land T(x)\right ) \leftrightarrow Ce^{-t}$$
But in the structure of polynomials we cannot eliminate the quantifier, since the solution is not a polynomial.

 

[Evgeny.Makarov]

I'll say up front that I am not very knowledgeable at quantifier elimination, so I can provide only "common sense" discussion. It's OK if this is not sufficient for you.

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

What is $\text{Exp}(\mathbb{C})$ and what is the polynomial structure you are talking about?

For example, when we have the formula $$\exists x \left (x'+x=0 \land T(x)\right )$$ since the solution is $x(t)=Ce^{-t}$, in the structure $\text{Exp}(\mathbb{C})$, i.e., at the exponentials, we can eliminate the quantifier (the existential symbol $\exists$) since $$\exists x \left (x'+x=0 \land T(x)\right ) \leftrightarrow Ce^{-t}$$

What is $T(x)$? You can't say $\dots\leftrightarrow Ce^{-t}$ because the right-hand side is not a formula. Also, why not say $\exists x \left (x'+x=0 \land T(x)\right ) \leftrightarrow\top$ where $\top$ is some tautology?

Are you working with first-order logic? If yes, then how do you quantify over the function $x$?

 

[mathmari]

What is $\text{Exp}(\mathbb{C})$ and what is the polynomial structure you are talking about?

We define $\text{Exp}(\mathbb{C})$ to be the set of expressions $$a=a_0+a_1 e^{\mu_1 z}+ \dots +a_Ne^{\mu_N z}$$ (beyond the "zero function", $0$, which we will consider to be also an element of $\text{Exp}(\mathbb{C})$)
where $a_0, a_1, \dots , a_N \in \mathbb{C} \setminus \{0\}$ and $\mu_i \in \mathbb{C} \setminus \{0\}$; in writing such an expression we will always assume that the $\mu_i$ are pairwise distinct.

The polynomials structure is the set of expressions $$p=p_0+p_1 z+ \dots +p_N z^N$$

What is $T(x)$?

$T$ is a one-place predicate, meaning: $$T(x) \Leftrightarrow x \notin \mathbb{C}$$ i.e. $T(x)$ means that the function $x$ is not a constant function.

You can't say $\dots\leftrightarrow Ce^{-t}$ because the right-hand side is not a formula.

So the right-hand side should be an expression containing $"="$ ?

Also, why not say $\exists x \left (x'+x=0 \land T(x)\right ) \leftrightarrow\top$ where $\top$ is some tautology?

Do you mean that it should be of the form $\exists x \left (x'+x=0 \land T(x)\right ) \leftrightarrow 0=0$ ?

Are you working with first-order logic?

Yes.

If yes, then how do you quantify over the function $x$?

What do you mean?

 

[Evgeny.Makarov]

First of all, elimination of quantifiers for closed formulas is trivial. If you have a closed formula $A$ (i.e., $A$ has no free variables) and a stricture $\mathcal{S}$, then either $\mathcal{S}\models A$ or $\mathcal{S}\not\models A$. In the first case, you can take some tautology $\top$ (yes, for example, $0=0$); then $\mathcal{S}\models A\leftrightarrow\top$. In the second case take a contradictory formula $\bot$ (e.g., $\bot=\neg\top$); then $\mathcal{S}\models A\leftrightarrow\bot$.

The whole point of quantifier elimination lies in formulas with free variables. For example, if $A(x,\vec{y})$ has free variables $x$ and $\vec{y}$, then one has to find a quantifier-free formula $B(\vec{y})$ such that $\mathcal{S}\models \forall\vec{y}\;\big((\exists x\,A(x,\vec{y}))\leftrightarrow B(\vec{y})\big)$.

We define $\text{Exp}(\mathbb{C})$ to be the set of expressions $$a=a_0+a_1 e^{\mu_1 z}+ \dots +a_Ne^{\mu_N z}$$ (beyond the "zero function", $0$, which we will consider to be also an element of $\text{Exp}(\mathbb{C})$)
where $a_0, a_1, \dots , a_N \in \mathbb{C} \setminus \{0\}$ and $\mu_i \in \mathbb{C} \setminus \{0\}$; in writing such an expression we will always assume that the $\mu_i$ are pairwise distinct.

The polynomials structure is the set of expressions $$p=p_0+p_1 z+ \dots +p_N z^N$$

And the operations in these structures are addition and multiplication by numbers?

$T$ is a one-place predicate, meaning: $$T(x) \Leftrightarrow x \notin \mathbb{C}$$ i.e. $T(x)$ means that the function $x$ is not a constant function.

Yes, sorry I did not see this in post #1. But wait, if $x \notin \mathbb{C}$ means that $x$ is not a constant function, then $\Bbb C$ is not the set of complex numbers?

So the right-hand side should be an expression containing $"="$ ?

Yes.

What do you mean?

What exactly is the signature (i.e., constants as well as functional and predicate symbols) of your logic? In first-order logic variables can quantify over elements of the domain (or universe), but not over functions over the domain. If the structure is natural numbers, then variables range over numbers, not numerical functions. So in first-order logic one cannot write a predicate $T(x)$ saying $\exists t_1,t_2\;x(t_1)\ne x(t_2)$ because here $x$ acts as a functional symbols and is supposed to be interpreted as a function.

But I assume you are viewing elements of the domain as formal expressions and not as functions. I.e., the polynomial $p_0+p_1 z+ \dots +p_N z^N$ is viewed simply as the sequence $(p_0,\dots,p_n)$, and being non-constant means that the length of the sequence is greater than 1. Is this so?

In any case, quantifier elimination for closed formulas is trivial.

 

[mathmari]

And the operations in these structures are addition and multiplication by numbers?

We looking at the language $L=\{+, ' , T, 0, 1\}$ and the operations are on these structures. ( $'$ is the symbol of differentiation.)

Yes, sorry I did not see this in post #1. But wait, if $x \notin \mathbb{C}$ means that $x$ is not a constant function, then $\Bbb C$ is not the set of complex numbers?

I found this definition here:

View attachment 4820
View attachment 4821

What exactly is the signature (i.e., constants as well as functional and predicate symbols) of your logic? In first-order logic variables can quantify over elements of the domain (or universe), but not over functions over the domain. If the structure is natural numbers, then variables range over numbers, not numerical functions. So in first-order logic one cannot write a predicate $T(x)$ saying $\exists t_1,t_2\;x(t_1)\ne x(t_2)$ because here $x$ acts as a functional symbols and is supposed to be interpreted as a function.

But I assume you are viewing elements of the domain as formal expressions and not as functions. I.e., the polynomial $p_0+p_1 z+ \dots +p_N z^N$ is viewed simply as the sequence $(p_0,\dots,p_n)$, and being non-constant means that the length of the sequence is greater than 1. Is this so?

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$.

 

[mathmari]

how do you quantify over the function $x$?

We interpret the structure in the language $L=\{+, ' , T, 0, 1\}$. $x$ is a term of the language and $x'$ is definable.
So $x$ is not a function. That's why we can quantify over $x$.
Is this correct?