1
$\begingroup$

Definition. A formula is called simple if it is of the form $$ \exists x(\psi_1\wedge\dots\wedge \psi_n\wedge\neg\chi_1\wedge\dots\wedge\neg\chi_m),$$ where $\psi_1,\dots,\psi_n,\chi_1,\dots,\chi_m$ are atomic formulas.

Definition. Let $L$ be a language, $\Gamma$ a set of $L$-formulas, $M$ and $N$ $L$-structures and $\vec{a}=a_1,\dots,a_n$ and $\vec{b}=b_1,\dots,b_n$ tuples of elements of $M$ and $N$, respectively. Write $\vec{a}\equiv_{\Gamma}\vec{b}$ if for every formula $\phi(x_1,\dots,x_n)$ from $\Gamma$ we have: $$ M\models \phi(\vec{a})\iff N\models \phi(\vec{b}).$$ If $\Gamma$ is the set of quantifier-free $L$-formulas or the set of simple $L$-formulas, then we similarly define $\vec{a}\equiv_{qf}\vec{b}$ and $\vec{a}\equiv_{simple}\vec{b}$.

Lemma. Let $L$ be an arbitrary language. Suppose that an $L$-theory $T$ has the following property: $$ \text{Whenever } M \text{ and } N \text{ are models of } T, \text{ and } \vec{a},\vec{b}\text{ are tuples of elements of } M \text{ and } N, \text{ respectively, then } \vec{a}\equiv_{qf}\vec{b} \text{ implies } \vec{a}\equiv_{simple}\vec{b}.$$ Then $T$ has quantifier elimination.

Prove that the theory of infinite $k$-vector spaces $T_k^{\infty}$ has quantifier elimination.

My attempt:

Let $M,N\models T_k^{\infty}$, $\vec{a}\in M^n$ and $\vec{b}\in N^n$. Suppose $M\models \phi(\vec{a})\iff N\models\phi(\vec{b})$ for all quantifier-free $L_k$-formulas. Consider a simple $L_k$-formula of the form $\exists x\psi(x,\vec{m})$. Then $$M\models \exists \psi(x,\vec{a}) \iff \exists m\in M: M\models \psi(m,\vec{a}) \iff \exists m\in M: N\models \psi(m,\vec{b}),$$ but how can I find an existential witness in $N$?

Thanks.

$\endgroup$
4
  • $\begingroup$ What language are you using to formulate the theory of vector spaces? Are you allowing quantification over elements of the field? Or do you have a function symbol for each element of the field to represent the action of that element on the vector space? $\endgroup$
    – Rob Arthan
    Jun 18 at 14:48
  • $\begingroup$ The language has a constant $0$ and a binary function symbol $+$ to describe the abelian group structure. In addition, for every element $m$ in the field there is a 1-place function symbol $f_m$, describing scalar multiplication. $\endgroup$
    – Zachary
    Jun 18 at 15:06
  • 1
    $\begingroup$ Hint: try to show that $\exists x\psi(x, \vec{m})$ is equivalent to a quantifier-free formula (in any vector space). To do this try to analyse what kind of relation an atomic formula $\chi(x, \vec{m})$ describes between $x$ and $\vec{m}$: what solutions can that relation have? what solutions can its negation have? $\endgroup$
    – Rob Arthan
    Jun 18 at 20:25
  • 1
    $\begingroup$ PS: I should have written "infinite vector space" in my comment. $\endgroup$
    – Rob Arthan
    Jun 19 at 0:10
1
$\begingroup$

As discussed in the comments, the signature for your language $L$ of vector spaces over the field $k$ comprises the signature $(0, +)$ for the abelian group of vectors together with a 1-place function $f_c$ for each $c \in k$ denoting scalar multiplication by $c$. To solve your problem, let's show that any simple formula is equivalent in any infinite $k$-vector space to a quantifier-free formula, allowing you to apply your lemma to conclude that the theory admits quantifier elimination.

The vector space axioms tell us that in any model of the theory of $k$-vector spaces, laws like the following will hold: $$ \begin{align*} f_c(f_d(v)) &= f_{cd}(v) \\ f_c(v + w) &= f_c(v) + f_c(w) \\ f_c(v) + f_d(v) &= f_{c+d}(v) \\ s = t & \Leftrightarrow s - t = 0 \\ f_c(s) = 0 &\Leftrightarrow s = 0 \quad \mbox{provided $c \neq 0$}\\ &\mbox{etc.} \end{align*} $$ Using these laws you can put any atomic predicate into the form: $$ f_{c_1}(y_1) + f_{c_2}(y_2) + \ldots + f_{c_k}(y_k) = 0 $$ where the $c_i$ are all non-zero and you can arrange for $c_1 = 1$ so that the first summand is $f_{1}(y_1) = y_1$. Hence, given a simple formula $$ \Psi \equiv \exists x(\psi_1\wedge\dots\wedge \psi_n\wedge\neg\chi_1\wedge\dots\wedge\neg\chi_m)$$ where the $\psi_i$ and $\chi_j$ are atomic formulas with free variables $x$ and $\vec{m}$, you can assume that each $\psi_i$ and $\chi_j$ has the one of the forms: $$ \begin{align*} & \mbox{(A)} &x + f_{c_1}(m_1) + \ldots + f_{c_k}(m_k) &= 0 \\ \mbox{or}\quad & \mbox{(B)} \quad & f_{c_1}(m_1) + \ldots + f_{c_k}(m_k) &= 0 \end{align*} $$ If any $\psi_i$ or $\chi_j$ has form $\mbox{(B)}$ (so that $x$ does not appear in it), then you can move it outside the existential quantifier, e.g., $$\exists x (f_{c_1}(m_1) + \ldots + f_{c_k}(m_k) = 0 \land \Phi) \Leftrightarrow f_{c_1}(m_1) + \ldots + f_{c_k}(m_k) = 0 \land (\exists x \Phi) $$ and then consider the smaller simple formula $\exists x \Phi$. So we can assume the $\psi_i$ and $\chi_j$ all have form $\mbox{(A)}$. Then, if there are any $\psi_i$, so that $\psi_1$ is present and has form $\mbox{(A)}$, $\psi_1$ is equivalent to $$x = -(f_{c_1}(m_1) + \ldots + f_{c_k}(m_k))$$ which implies that $\Psi$ is equivalent to the quantifier-free formula: $$ (\psi_2\wedge\dots\wedge \psi_n\wedge\neg\chi_1\wedge\dots\wedge\neg\chi_m)[-(f_{c_1}(m_1) + \ldots + f_{c_k}(m_k))/x] $$ If there are no $\psi_i$, $\Psi$ has the form $$ \exists x(\neg\chi_1\wedge\dots\wedge\neg\chi_m)$$ and then $\Psi$ is valid in any infinite $k$-vector space, because given any finite list $\vec{m}$ of vectors we can always find an $x$ that is different from a finite set of vectors of the form $-(f_{c_1}(m_1) + \ldots + f_{c_k}(m_k))$. So in this case $\Psi$ is equivalent to the quantifier-free formula $0 = 0$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.