Theory of infinite vector spaces admits quantifier elimination

Question

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.

Answer 1

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