How to formalize $\text{span}(S)=\{c_1v_1+\cdots+c_kv_k\mid v_1,~\cdots,~v_k\in S,~c_1,~\cdots,~c_k\in F\}$ rigorously in first order language? In Linear Algebra, the subspace of a vector space $V$ over a field $F$ spanned by a set $S$ of $V$, is defined to be the set of all linear combinations of $S$.  Symbolically, it may be written as something like $\text{span}(S)=\{c_1v_1+\cdots+c_kv_k\mid  v_1,~\cdots,~v_k\in S,~c_1,~\cdots,~c_k\in F\}$, or $\text{span}(S)=\{c_1v_1+\cdots+c_kv_k\mid\forall i\in\{1,\cdots,k\},~(v_i\in S\wedge c_i\in F)\}$.
It is a satisfactory way to write down the definition for those are just studying linear algebra. However, for someone who has studied rigorous mathematical logic, would definitely argue that this definition is somewhat illed, one reason is that the character of "$k$" here does not explicitly say that itself is mutable; we can pick aribitrary number of vectors in $S$ to generate a linear combination, maybe one, maybe ten. For example, we can choose $v_1,v_2\in S$, then $3v_1+5v_2\in\text{span}(S)$; also, we can choose $w_1,w_2,w_3,w_4,w_5,w_6\in S$, then $3w_1+5w_2+w_3+w_4+2w_5+w_6\in\text{span}(S)$. The predicate which used to generate the set $\text{span}(S)$ by the separtion axiom of $\textsf{ZFC}$, is "$v_1,~\cdots,~v_k\in S,~c_1,~\cdots,~c_k\in F$" or "$\forall i\in\{1,\cdots,k\},~(v_i\in S\wedge c_i\in F)$", they both have a free variable $k$. Also, if we rewrite them as "$\{x\mid \exists k\in\mathbb{N},~v_1,~\cdots,~v_k\in S,~c_1,~\cdots,~c_k\in F,~x=c_1v_1+\cdots c_kv_k\}$". Then is it legal? Can a latter occured variable $v_k$ have a subscript refering to the pre-occuring variable $k$? I never see a well-formed formula in first order language can be built like this way. I think it is illegal and pretty blurred. So, how can we formalize $\text{span}(S)$ in a rigorous first order language? Any suggestions or comments is welcomed.
 A: Like everything else having to do with finiteness, the sentence inquestion isn't written in the first-order language of vector spaces, but instead in the language of set theory: we're not working inside a single vector space, but rather inside a model of (say) ZFC, and in that context we can talk about finiteness, finite linear combinations, etc.
Now, of course, different models of ZFC may have different notions of "finite" (this follows from the Compactness Theorem). So we may have the following situation, very roughly stated (it's a good exercise to figure out a way to describe this precisely): $M$ and $N$ are two models of ZFC where $M$'s version of $\mathbb{N}$ is nonstandard but $N$'s is standard, $V$ is a vector space in both $M$ and $N$, $s$ is a set of vectors in $M$ and $N$, and $v\in V$ such that $M\models v\in \langle s\rangle$ but $N\models v\not\in\langle s\rangle$. 
So notions that make reference to finiteness (among other things) depend on the ambient model of set theory we're living in.

OK, so what does this formula look like? Well, before I say more, the brief summary is:

We're going to find a way to quantify over "finite tuples" (so that we can write "$\exists$ some finite tuple" instead of having a block of quantifiers of variable length, which is of course forbidden) and manage these finite tuples (e.g. talk about the sum of a finite tuple of vectors).

Well, the language of set theory is very . . . parsimonious, so actually writing out explicitly such statements is a serious chore (and this has been used as an argument to develop a different foundation for mathematics than ZFC, one which allows us to express such basic concepts more quickly). But the rough idea is the following. Talking about vector spaces in ZFC is easy if tedious, by using ordered pairs (a vector space is a tuple of sets and functions satisfying some properties). Now we need to talk about finite sequences. Well, ZFC lets us define the things called "finite ordinals." Now, just like nonstandard models of arithmetic will have infinite "natural numbers," these "finite ordinals" might not be actually finite in a given model, but the model will always think that they are. A finite tuple is then a function $f$ with domain a proper initial segment of the set $\omega$ of finite ordinals; and this is perfectly definable in the language of set theory. 
This, in turn, lets us define "finite linear combination." Suppose $U$ is a set of vectors. Then $v\in \langle U\rangle$ iff: 


*

*there are functions $f, g$ with domain the same proper initial segment $I$ of $\omega$ and domain $U$ and $F$ respectively (that is, $f$ is a sequence of vectors in $U$ and $g$ is a sequence of scalars, and they have the same length), and

*there is a function $h$ with domain $I$ and codomain $V$ (the idea is that $h(n)$ will be the $n$th partial sum) such that

*$h(\max(I))=v$, $h(0)=0_V$, and $h(k+1)=h(k)+f(k)*g(k)$ for each $k\in I$.
Barring a stupid indexing mismatch on my part (I'm tired), this gives us the notion of linear combination. Specifically, using this as the definition of span, the theory ZFC will be able to prove all the usual theorems about linear independence etc. But these theorems are not stated in the language of vector spaces - rather, they're stated in the far more powerful language of set theory, and they are proved in the far more powerful theory ZFC rather than the theory of vector spaces over a given field.
