# Theory of infinite vector spaces admits quantifier elimination

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.

• 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? Jun 18, 2021 at 14:48
• 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. Jun 18, 2021 at 15:06
• 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? Jun 18, 2021 at 20:25
• PS: I should have written "infinite vector space" in my comment. Jun 19, 2021 at 0:10
• @MUbicuas: for finite $k$, you dont have q.e. for the theory of finite spaces, e.g., consider a sentence asserting that the dimension is 1. If $k$ is infinite, then finite spaces are trivial, so you have q.e. for trivial reasons, as all equations are true. Feb 9, 2022 at 18:18

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