= Quantifier elimination for infinite underlying vector spaces
In the language naming addition, zero and every <scalar multiplication> over a fixed <field>, the <first-order theory>[theory] of infinite underlying <vector spaces> eliminates <quantifiers>. In a <conjunction> of <linear equations> and inequations, an equation with a nonzero <scalar multiplication>[coefficient] solves for the quantified variable. Otherwise the variable is excluded from only finitely many values, so infinitude supplies a witness. Disjunction and induction finish elimination. This works over <finite fields> with infinite <dimension of a vector space>[dimension] and over infinite <fields> with every nonzero <dimension of a vector space>[dimension].
Back to article page
