$\DeclareMathOperator\Inv{Inv}$Baur-Monk quantifier elimination implies that a sentence in the language of modules is a combination of BG invariant statements.


A BG invariant sentence is a boolean combination of $ \Inv(A,\phi, \psi) \* k$ where $\*$ is one of $=,>,<$ where $\phi$ and $\psi$ are positive primitive formulae.


We define $\Inv(A,\phi, \psi)$ as the cardinality of the quotient group $\phi(A) / \psi(A)$ and $\Inv(A,\phi, \psi) > k$ is equivalent modulo the theory of modules $T$ to the following first-order statement:


\begin{equation\*}
 \forall \overline{v\_1},...,\overline{v\_k} \exists \overline{v} (\phi(\overline{v}) \wedge {\bigwedge\_{i=1}^{k}} \neg \psi (\overline{v}-\overline{v\_i})).
\end{equation\*}


It is then concluded from quantifier elimination that $\Inv(A,\phi, \psi)=\Inv(B,\phi, \psi)$ iff $A 
\equiv B$ (elementarily) where $\phi$ and $\psi$ are positive primitive in *one* free variable.
My question is why it follows that we can restrict to invariants with formulas in one free variable? (Instead of just invariants). I assume that it is because the positive primitive formulas are conjunction closed. Is this correct?



Baur-Monk quantifier elimination (BG-invariants in 1-free variable)
This doesn't follow directly from the statement of QE (and I don't think it has anything to do with the fact that pp formulas are conjunction-closed). To understand it, you really have to look at the proof of QE. For example, see the proof of Theorem 1.1 on p. 155 of Ziegler's paper *[Model Theory of Modules](https://doi.org/10.1016/0168-0072(84)90014-9)*.


The proof of QE works one quantifier at a time. For a fixed module $M$, you show that if $\varphi(x,\overline{y})$ is equivalent (in $M$) to a Boolean combination of pp formulas, then so is $\forall x\, \varphi(x,\overline{y})$. Here $x$ is a single variable. By induction, it follows that every formula is equivalent (in $M$) to a Boolean combination of pp formulas.


But now, examining the proof, you observe that the proof almost works uniformly in $M$: when you show that $\forall x\, \varphi(x,\overline{y})$ is equivalent to the boolean combination of pp formulas $\theta(\overline{y})$, the formula $\theta$ only depends on the values of finitely many $\mathrm{Inv}(M,\psi,\chi)$ where $\psi$ and $\chi$ are pp formulas in the single variable $x$. So if you know all the values of the BG invariants $\mathrm{Inv}(M,\psi,\chi)$ when $\psi$ and $\chi$ are pp formulas in a single variable, then you know which quantifier-free formula every formula is equivalent to. In particular, these values determine whether every sentence is true or false in $M$.


