Linear independence without choice

The notions of linear and metric independence are investigated in relation to the property: if U is a set of n+1 independent vectors, and X is a set o f n independent vectors, then adjoining some vector in U to X results in a set of n+1 independent vectors. It is shown that this properly holds in any normed linear space. A related property - that finite-dimensional subspace s are proximinal - is established for strictly convex normed spaces over th e real or complex numbers. It follows that metric independence and linear i ndependence are equivalent in such spaces. Proofs are carried out in the co ntext of intuitionistic logic without the axiom of countable choice. (C) 20 00 Elsevier Science B.V. All rights reserved. MSC. 03F65; 15A03.