Logic of defining a function on an abstract set Obviously in practice it is common to define functions given a set $S$, however I have never thought about the concept behind this and why "I am allowed to do that". Please keep in mind that I have never read any logic lecture notes or visited any lecture on those topics, besides the standard material. If one is in the setting of an algebraic structure, e.g. a group $G$, and one wants to prove a statement, e.g. $$\varphi:G \to G, \ g \mapsto 2g$$ is a function, what is the logic behind this being true for an arbitrary group? It is standard to prove this by assuming a group $G$ is given and then showing the statement.
Q$1$: Is this to be interpreted to be given an explicit but arbitrary/unknown group? What I mean by that is that this is to be interpreted as $G$ being any explicit group, such as a set consisting of a multiplication map satisfying the usual properties of the definition?
In this setting one does not know what set one is working with, however one would know that an "explicit" set $G$ is underlying, which means that it is known which elements belong to $G$ and which do not. Therefore it is possible to speak of "$g \in G$", is this correct? As far as I can tell, this is necessary in order to do this. This allows to even make sense of a statement for all $g \in G : P(g)$. Since one knows which elements belong to $G$ and which do not, one can then define an assignment for those elemnts, an example given above.
One could sum up that I am confused whether it needs justification to talk about "for all elements of the set the property $P$ holds" without knowing the set and why one is able to do so. Since defining a function is sort of a statement of that kind, I found this to be fitting. This is then solved since one knows that $G$ is some explicit but unknown/arbitrary set. If anything of what I said is wrong I would appreciate corrections, since those are only my thoughts. Thank you in advance for any comments!
 A: If you have a completely abstract set $X$ (i.e., a set whose elements you know nothing about and which is is not equipped with any other structure), then (in ordinary mathematical practice, outside formal set theory) there are very few functions you can define on it: essentially just the identity function on $X$ and the constant function $x \mapsto y$ for any fixed member $y$ of some set $Y$.
When working with algebraic structures like groups, we often forget in our notation that a group comprises a set $G$ and some additional information: e.g., the identity element $e$ and the multiplication operation $(\cdot)$. Strictly speaking, as you have observed in your question, we should think of the group as a triple $\mathbf{G} = (G, e, \cdot)$ (or maybe $(G, 0, +)$ if $\mathbf{G}$ is abelian). (Here, I am using a common convention of univeral algebra to use bold for the triple $\mathbf{G}$ giving the algebraic structure and and ordinary font for the set $G$ of elements of that structure.) So now, if you know $\mathbf{G}$ (rather than just $G$) you can meaningfully use notations like $x \mapsto x^2$ (if you write the group operation as $(\cdot)$) or $x \mapsto 2x$ (if you write the group operation as $(+)$) to define operations that work in any group. If you work through the text of your question you should able to see where you need $\mathbf{G}$ instead of just $G$ to make the notation make sense.
A: I think you are confusing yourself by worrying about what you know or what has been defined explicitly rather than simply worrying about what is true.  You say that in order to prove that $\varphi$ is a function, you start by "assuming a group $G$ is given."  Perhaps the word "given" is confusing you, so let's leave it out. To prove that $\varphi$ is a function, you start by assuming that $G$ is a group and then prove that there is a unique function fitting the description of $\varphi$.  Whether or not $G$ has been given has nothing to do with whether or not $\varphi$ is a function.
Of course, in a context in which you are discussing a group $G$ that has not been explicitly specified, you may not know what the elements of $G$ are, and you may not know how to compute $\varphi(g)$ for any $g \in G$.  But what you know, or what you are able to compute, is not the issue.  The issue is whether or not the definition of $\varphi$ defines a unique function, and it does, whether anyone knows how to compute its values or not.
A: Not sure if I've identified exactly what OP is confused about, but I'll give it a shot.
The first proof we will do is the following:

Suppose $(G, +)$ is a group. Then there is a unique function $f : G \to G$ such that $f(x) = x + x$ for all $x \in G$.

Hopefully, it's easy to see that this is true. The exact proof depends on what foundation of mathematics you're using. In set theory, we would typically define $f = \{(x, y) \in G^2 | y = x + x\}$ and prove that this is the only function $f : G \to G$ such that $f(x) = x + x$ for all $x \in G$. In a foundation based on type theory and/or the lambda calculus, we would simply define $f(x) = x + x$ and then show that this specifies $f$ uniquely using function extensionality.
The second proof is the following:

For all groups $(G, +)$, there is a unique function $f : G \to G$ such that $f(x) = x + x$ for all $x \in G$.

This follows immediately from the rules of logic and the first proof.
A: 
If one is in the setting of an algebraic structure, e.g. a group $G$,
and one wants to prove a statement, e.g.  $\varphi:G \to G,  g \mapsto 2g$ is a function, what is the logic behind this being true for an
arbitrary group?

In your example, I assume we have the group $(G,*)$, and$ ~2\in G$. And that you want to prove there exists a function $\varphi:G \to G$ such that $\forall g\in G: \varphi(g)=2*g$.
Proof: Simply construct the set of ordered pairs $\varphi = \{ (a,b)\in G\times G ~\land ~|~ b=2*a\}$. Then it is trivial to prove that $\varphi$ is the required function and we can write, using the prefix notation, that $\forall g\in G: \varphi(g)=2*g$  as required.
