MHB Can Quantifiers Be Eliminated in These Differential Equations?

  • Thread starter Thread starter mathmari
  • Start date Start date
  • Tags Tags
    Elimination
mathmari
Gold Member
MHB
Messages
4,984
Reaction score
7
Hey! :o

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?
 
Physics news on Phys.org
Could you explain what you mean by "eliminating the quantifier" and "looking at the exponentials"?
 
Evgeny.Makarov said:
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.
 
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.

mathmari said:
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?

mathmari said:
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$?
 
Evgeny.Makarov said:
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$$
Evgeny.Makarov said:
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.

Evgeny.Makarov said:
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 $"="$ ?
Evgeny.Makarov said:
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$ ?

Evgeny.Makarov said:
Are you working with first-order logic?

Yes.
Evgeny.Makarov said:
If yes, then how do you quantify over the function $x$?

What do you mean?
 
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)$.

mathmari said:
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?

mathmari said:
$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?

mathmari said:
So the right-hand side should be an expression containing $"="$ ?
Yes.

mathmari said:
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.
 
Evgeny.Makarov said:
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.)
Evgeny.Makarov said:
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
Evgeny.Makarov said:
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$.
 

Attachments

  • def1.PNG
    def1.PNG
    39.4 KB · Views: 90
  • def2.PNG
    def2.PNG
    26.9 KB · Views: 92
Evgeny.Makarov said:
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?
 
Back
Top