Independence of a pair is not definable over an infinite field
ID: independence-of-a-pair-is-not-definable-over-an-infinite-field
In the one-sorted vector-space language naming each scalar multiplication, a first-order formula reduces by quantifier elimination to finitely many linear equations. An independent pair satisfies only the identically zero equations among them. A dependent pair with nonzero satisfies the same listed equations if the scalar avoids their finitely many forbidden ratios, which is possible over an infinite field. Thus no formula defines pair independence. The complete independent-pair type is still consistent in an infinite-dimensional model; it is nonisolated.
New to topics? Read the docs here!