Free abelian group generated by a set Let $S$ be a set. Then one can construct the free abelian group with basis $S$ as the set of all functions from $S \to \mathbb{Z}$ with finite support: $$\mathbb{Z}^{(S)}:=\{f:S \to \mathbb{Z} \ | \ \mathrm{supp}(f) \ \text{has finite cardinality}\}.$$ One can define an addition on $\mathbb{Z}^{(S)}$ the usual way $$+:\mathbb{Z}^{(S)} \times \mathbb{Z}^{(S)} \to \mathbb{Z}^{(S)}, \ (f,g) \mapsto f+g$$ with $(f+g)(s):=f(s)+g(s)$ for all $s \in S$. This gives $\mathbb{Z}^{(S)}$ the structure of an abelian group. Now, every $f \in \mathbb{Z}^{(S)}$ can be written uniquely as $$f=\sum_{\{x \in S \ | \ f(x) \neq 0 \}} f(x) 1_x.$$ However, this does technically not have $S$ as a basis, but rather the functions $1_x$ for all $x \in S$. Surely, those are in $1:1$ correspondence with the elements of $S$, but does that allow for writing $\sum_{\{x \in S \ | \ f(x) \neq 0\}} f(x)x$, or is that incorrect? I have often seen this formal sum definition, which is why I suspect that it is correct, but I am unsure. I don't know what the existence of a set of formal sums would be, if there is any.
An alternative notation is to write $f$ as $$f=\sum_{x \in S} f(x)1_x$$ and mention that this sum is indeed finite. However, isn't this rather also a bit inaccurate?
As a somewhat related question: I wanted to remind myself why one can write $f=\sum f(x)1_x$ despite not "knowing" the $f(x)$. This was because one knows those exist and satisfy the condition that for all $s \in S$ $f(s)=(\sum f(x)1_x)(s)$. "Not knowing the elements" was a silly sidethought I had, I just wanted to make sure if my explanation here is correct, since this is kind of related.
 A: If by "correct" or "incorrect" you mean "this exact formula is true in set theory", then yes, the formula
$$f=\sum_{\{x \in S \ | \ f(x) \neq 0 \}} f(x) x$$
is, strictly talking, "wrong", since the elements $x\in S$ are not elements of $\mathbb Z^{(S)}$. Now, if the set $S$ does not have an operation already, then people usually say something along the lines of "I will use the notation $x$ for $1_x$ whenever it is added to something or multiplied by a scalar".
That is because in this context, for any integer $n\in\mathbb Z$ the notation $nx$ could not possibly be confused with anything other than $n1_x$, and similarly the notation $3x+2y$ could not mean anything other than $3\cdot 1_x + 2\cdot 1_y$ (actually I think this last one is more confusing by the jusxtaposition of $3$ and $2$ with $1$).
A: Starting wit a set $S$ we can go for finding an abelian group that is free over $S$.
This boils down to finding an abelian group $F(S)$ together with a function $\eta:S\to F(S)$ such that for every function $g:S\to A$ where $A$ denotes an abelian group there is a unique group homomorphism $\gamma:F(S)\to A$ with $g=\gamma\circ\eta$.
With $F(S):=\mathbb Z^{(S)}$ and $s\mapsto1_s$ as prescription for $\eta$ this is neatly accomplished, so an abelian group free over $S$ has been constructed.
You however want to see $S$ as basis of $F(S)$ or equivalently you want $\eta$ to be an inclusion so that $S\subseteq F(S)$.
Well, you could go for defining $F(S)$ as collection of finite sums of form:$$n_1s_1+\cdots+n_ks_k$$
where $n_i\in\Bbb Z$ and distinct $s_i\in S$ and $1s:=s$.
This $F(S)$ must then be equipped with an addition. Are things better now? Not really I would say. If e.g. we try to find a suitable way to define this addition then it is quite likely that $\mathbb Z^{(S)}$ pops up in our mind.
IMV it is better if you exchange the concept "$S$ basis of $F(S)$" for the more general "$F(S)$ free over $S$". I only see advantages.

Edit:
Let me add that in the situation described above the image of $S$ under $\eta$ is actually a basis of $F(S)$.
