= Solution
For <quantifier elimination for infinite underlying vector spaces>, we first justify that formulas cannot make finer distinctions than their linear-equation data. In any infinite underlying <vector space>, eliminate an existential variable from a disjunction of <conjunctions> of <linear equations> and inequations. If an equation has a nonzero <scalar multiplication>[coefficient] of that variable, solve for it and substitute. If none does, the inequations forbid only finitely many values, leaving an available value in the infinite domain; the remaining equations concern only the other variables. Terms are <linear combinations>, so induction gives <quantifier elimination> for $T$ and completeness, since closed terms reduce to zero.
For one variable there are two possible <complete types>, zero and nonzero. Both are isolated, and every definable <set> is their <union>. Thus
$$
\boxed{F_1/E_1(T)\cong\mathcal P(\{1,2\}),\qquad |F_1/E_1(T)|=4.}
$$
For <types of pairs of vectors over a finite field>, the <linear relation> kernel $\{(a,b)\in K^2:ax+by=0\}$ determines the <complete type>. If $q=|K|$, the possibilities are one rank-zero pair, $q+1$ rank-one directions, and one rank-two independent type. Concretely these are $(0,0)$; $x\ne0$ with $y=\lambda_a(x)$ for each $a\in K$; $x=0,y\ne0$; and the independent pairs. Their isolating formulas are finite because $K$ is finite. Hence
$$
\boxed{F_2/E_2(T)\cong\mathcal P(\{1,\ldots,q+3\}),\qquad |F_2/E_2(T)|=2^{q+3}.}
$$
Every class is the <union> of a selection of these <atom of a Boolean algebra>[atoms]. <Basis extension> also shows that pairs with the same relation kernel are conjugate by a <linear isomorphism>[linear automorphism] within any infinite-dimensional <first-order model>[model].
Back to article page
