Is the notion of "expression" formal/rigorous enough? For any set $S$ and field $k$, one can form the vector space over $k$ with basis $S$. As a set, this is the set of all linear combinations ("expressions") of the form $\sum_i\alpha_is_i$ where $\alpha_i\in k$, $s_i\in S$, and all but finitely many $\alpha_i$ are zero. I thought this was a perfectly rigorous definition until I read Example 1.2.4(c) which, in particular, says:

To be completely precise and avoid talking about "expressions", we can define $F(S)$ [the vector space in question] to be the set of all functions $\lambda: S\to k$ such that $s\in S:\lambda(s)\ne 0\}$ is finite.

Why would one want to "rigorize" further the notion of expression and avoid talking about it? Isn't it a perfectly well- and rigorously defined notion already?
 A: For example, if your $S$ consists of the letters $a$, $b$, and $c$, are the strings "$1a$" and "$1a+0b$" and "$0c+1a$" all expressions? If they are all expressions, then are they all elements of your vector space? Are they different elements? If you say they are all elements of your vector space, but are the same element, then how to you get that from any concept of "expression"? They are certainly not the same strings of symbols.
If "$1a+0b$" is not an expression, then which expression is the zero element of your vector space?
How about "$1a+1a$" versus "$2a$"?
How about "$1a+2b$" versus "$2b+1a$"? There is nothing in your informal description that says $S$ comes with a preferred ordering, but expressions are always finite strings of symbols that appear in a particular order.

These problems are not insurmountable showstoppers. It is absolutely possible to give a rigorous definition of "expression", and then define your vector space as the quotient of a set of expressions by all identities that are provable in a certain formal theory -- but doing all that turns out to be more work and in the end less convenient and less rewarding than speaking about functions $S\to k$ with finite support.

A more rewarding thing to do with expressions would be to start by looking at the set of all expressions that can be built with the vector space operations, such as $3\cdot(5\cdot((-b)+7\cdot a+13\cdot(\vec0+c)))$. That is, don't a priori restrict to expressions of a particular form. The quotient out all identities that can be proved from the axioms for $k$-vector spaces (and arithmetic on $k$).
This still gives you a vector space of formal linear combinations of $S$, but this time around the entire construction is openly an example of a general concept of free models for equational theories. This is arguably worthwhile because it shows conceptual parallels to things that might not immediately look similar.
On the other hand, one of the first things one would do with this construction is probably to prove that it is isomorphic to the space of finitely supported functions $S\to k$, and then use the latter for actual computations.
A: $S$ is just a set with no structure, so it is not clear what is meant by multiplying an element of $S$ by a scalar, or adding together two elements of $S$. If $S$ were assumed to be a vector space over a field $F$ this would be no problem. But $S$ is just a set, so we must carefully define what we mean by taking linear combinations of elements of $S$.
For example, suppose that $S$ is, say, the set of all lines in a given plane. Without further explanation, it's not clear what it would mean to take a linear combination of elements of $S$.
