Precisely describing the set of "the subgroup generated by S" In group theory, one equivalent way to define the subgroup generated by the set $S$ is the following:
$$\big \langle S \big \rangle = \{s_{1}^{e_1}...s_n^{e_n}\mid n=1,2,...,; i=1,2,...,n; e_i=\pm1, s_i \in S \}$$
Obviously, this form of describing the set is rather imprecise. So, this is my attempt at writing it in a more "precise" fashion (I'll assume we know what a finite product of the elements of a group is):
$$ \big \langle S \big \rangle = \{x \mid (\exists n \in \mathbb{N})(\forall 1 \leq i \leq n)(\exists e_i \in \{1,-1\})(\exists s_i \in S)(x = {\displaystyle \prod_{j=1}^{n} s_{j}^{e_j}})\}$$
Is this version correct? I'm not sure if we are allowed to use subscripts as a bound variable within quantifiers, without defining exactly what a subscript is. If that is the case, I'd be thankful if you could recommend a precise definition for subscripts (and superscripts).
 A: I would say that the original formula is (modulo one small issue mentioned below) precise. You seem to be conflating two different issues.
Being precise has to do with vagueness and the possibility of misinterpretation. I do not see any way how your definition can be misinterpreted.
Being formal has to do with whether your definition conforms to the precise specification of some formal language or another. Your definition, of course, does not, but so what?
Unless your intended audience is an automatic proof assistant which requires that its input be given in some formal language, this is not a problem. Assuming that the intended context is in a text made for human consumption, the second definition is not in any way an improvement on the first. In fact, it is worse than the first definition because it is more difficult to read. If you want to write mathematics well, focus on how easy it is for humans to understand your text, not on whether your text conforms to the definition of a formula of ZFC (or some other theory) given in a logic course.
The only point of actual imprecision in your definition is that if $S$ is empty, your definition outputs the empty set, but it should in fact output the trivial subgroup. The easiest way to fix this is not to mess with the formula itself, but to change the context slightly. You could say something like: the subgroup generated by a non-empty set $S$ is
$\langle S \rangle = \{ s_{1}^{e_{1}} \cdots s_{n}^{e_{n}} \mid s_{i} \in S \text{ and } e_{i} \in \{ +1, -1 \} \text{ for } 1 \leq i \leq n \text{ with } n \in \omega \}$.
Notice in particular that you are allowed to use normal English words inside set builder notation.
