Logic of proofs involving variables and “for all” statements It is taught that in order to prove "for all" statements such as
$$P(G): \mathrm{For \ all \ groups} \ G \ \mathrm{it \ holds \ that} \ \{(g,g+g) \in G \times G \ | \ g \in G\} \ \mathrm{is \ a \ set}$$ one assumes that $G$ is a group and then proves the statement $P(G)$. I wonder about the logic behind this and "what is logically allowed", which is never explained in introductory courses.
Q$1$: What does "Let $G$ be a group" even mean? A$1$: As far as I can tell, it means that one assumes that all properties of the object of interest, in this case a group, are true and one calls the object of interest $G$. Explicitly this would mean that it is true that $G$ is a set equipped with an addition/multiplication (whatever definition you are using) satisfying the group laws.
Note that as far as I can tell one does not know which elements are contained in $G$, only that $G$ is a set satisfying some extra properties.
Q$2$: Why is the above a set? Since I use the naive set definition, meaning that any unordered collection of objects are sets, it is true that the collection of all $(g,g+g)$ is a set, which is exactly $\{(g,2g) \in G \times G \ | \ g \in G\}$.
Q$3$: Why does this prove the statement? Or more generally, why does this method suffice to prove a for all statement in general? I think there would be two ways to view this: $(1)$ One proved the statement is correct using nothing but the properties of a group which any group obviously satisfies. Thus the proof is "a path" one could follow for any explicit group to show that the statement is indeed true. $(2)$ Assume there exists a group which does not satisfy a statement proven this way. Then one could go through the process of the proof with this object and comes to a contradiction.
 A: The ways of of concluding that are allowed in proofs ultimately boil down to the so-called rules of inference. Your desired example is of the form
$$ \forall G\colon \text{isGroup}(G)\to \text{isSet}(\{\,(g,g+g)\mid g\in G\,\})$$
so one would try to prove
$$\text{isGroup}(G)\to \text{isSet}(\{\,(g,g+g)\mid g\in G\,\})$$
and for this try to deduce the right from the left, i.e.,
$$\text{isGroup}(G)\vdash \text{isSet}(\{\,(g,g+g)\mid g\in G\,\})$$
and then do this in terms of the "actual" proof.
The nitty-gritty details hide in the notation. The predicate "isGroup" can be written in terms of "isSet" and the group axioms. But what should "isSet" even mean? When working in set theory, typically "everything" is a set and such a predicate makes no sense. In that case, one rather has to justify what the notation $\{\,(g,g+g)\mid g\in G\,\}$ even means. (Or one also works with classes, in which case "isSet" is formalized in some way and one may have a general interpretation of the notation  $\{\,(g,g+g)\mid g\in G\,\}$ at least as a class). The justification (at least in $\mathsf{ZFC}$) is of course the

Axiom Schema of Replacement:  If $A$ is a set and $F$ a functional predicate, then there exists a set $B$ such that $y\in B\iff \exists x\in A\colon x=F(a)$.


Notation: We denote this (unique per Axiom of Extension) set as $F[A]$ or $\{\,F(x)\mid x\in A\,\}$

A: When we begin a proof of

$$\mathrm{For \ all \ groups} \ G, \ \ \{(g,g+g) \in G {\times} G \ | \ g \in G\} \ \mathrm{is \ a \ set}$$

by writing $$\text{Let $G$ be a group}$$ we are declaring the placeholder $G$ as a representative member of the set of objects that conform to the definition of a group and have its attendant properties, which we then employ to attain the required result $$\{(g,g+g) \in G \times G \ | \ g \in G\} \ \mathrm{is \ a \ set}.$$
As $G$ can be any group, we have actually been reasoning sufficiently generally, so the result applies to every group. As such, we have proved that $$\mathrm{For \ each \ group} \ G, \ \ \{(g,g+g) \in G {\times} G \ | \ g \in G\} \ \mathrm{is \ a \ set}.$$
In the statement $$\text{Let $G$ be a group}$$ $G$ is being assigned a definition rather than being instantiated with a specific value, and the adjective ‘arbitrary’ has been left tacit rather than made explicit.
Also: ‘Any’ versus ‘arbitrary’ and How to interpret “let... suppose” in mathematics?
A: Two elements of explanation : conditional proof and universal generalization.


*

*The statement you want to prove is of the form :

$\forall x$ IF $G(x) \rightarrow P(x)$.

*

*In ordre to prove a conditional statement, you assume the antecedent is true, and you try to derive the consequent . By the conditional proof rule, this amounts to showing that  the antecedent implies the consequent.

For example suppose I want to prove : $A\rightarrow (B\rightarrow A)$.
First I assume $A$ is true, that is, I put myself in the situation  where the antecedent is true ( since a conditional says nothing more that " in case ... is true , then ... is also true").
Then, under this hypothesis, I make the assumption that $B$ is true. Under this second assumption I derive $A$ ( since $A$ is still true in the hypothetical situation I am in).
I can therefore conclude, still under my original assumption that $ B$ implies $A$. And since I have derived this while supposing that $A$ is true, it means that the hypothesis that $A$ is true implies the conditional $A \rightarrow B$. I have then proved, not hypothetically, but categorically, that $ A \rightarrow (A \rightarrow B)$.

*

*Now, the conditional statement you want to prove is quantified universally.
In order to reach a universal statement, you will have to work first with an arbitrary object, and the hypothesis under which you will work will refer to this arbitrary object. Call this object $g$ ( or whatever letter) and make the following hypothesis : $G(g)$ ,  $g$ is a group ( which amounst to saying that $g$ is a set with such and such properties ...). Under this hypothesis , derive the sentence $P(g)$ , and then use conditional proof to assert categorically :

IF  $G(g)$ THEN $P(g)$.

*

*At this point your conclusion only holds for object $g$. But since $g$ is arbitrary and since you did not use any particular property of $g$ except that $g$ is a group, your derivations works for any $g$ whatever ( even a $g$ that is not a group, for that would make the antecedent false, and therefore the whole conditional true*).


*As a consequence, you are allowed to generalize ( using universal generalization) and to say : for all $x$ , if $x$ is a group , then ....
(*) Note . this is due to the truth table of the " if ... then" operator
