In general, if $\mathcal{A}$ is a variety of algebras and $U : \mathcal{A} \to \mathbf{Sets}$ is the forgetful functor, then we can construct a left adjoint $F : \mathbf{Sets} \to \mathcal{A}$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $\mathcal{A}$. (If you're using ZFC as your foundations, you will likely need a set-theoretic argument to show this can be represented by an actual set rather than a proper class.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $\mathcal{A}$ with formal expressions substituted in, and which also makes all the formal operations be respectful of the equivalence relation. (It is straightforward to show the class of relations on the set of formal expressions from (1) satisfying these requirements is closed under arbitrary intersections; so then, for example, you could construct the desired equivalence relation as the intersection of all such relations.)
Then, in many cases, it's possible to represent each equivalence class by a member of a restricted class of expressions which is easier to work with; and if we're lucky, we might even be able to choose a canonical such expression in each equivalence class.
In the case $\mathcal{A} = \mathbf{Groups}$, for example, it is easy to show that any formal expression from (1), modulo the equivalence relation in (2), is equivalent to a (possibly empty) product of elements $x \in X$ or $y^{-1}$ for $y \in X$ which together form a reduced word. You would prove this by "structural induction" on the general formal expression (or, if you prefer, by strong induction on the "total size" of the general formal expression). The harder part is to show that any two distinct
reduced words end up in different equivalence classes.
To make this process more concrete in the group case, I think it might help to show how this would be encoded in Coq, where for example (1) is very similar to the way you would define an "abstract syntax tree" type in OCaml or Haskell:
(* formal expressions from (1) *)
Inductive free_group (X:Type) : Type :=
| fg_atom (x:X)
| fg_id
| fg_inv (x : free_group X)
| fg_mul (x y : free_group X).
Arguments fg_atom [X] x.
Arguments fg_id [X].
Arguments fg_inv [X] x.
Arguments fg_mul [X] x y.
(* Equivalence relation described in (2) *)
Inductive fg_equiv (X:Type) : free_group X -> free_group X -> Prop :=
| fg_left_id : forall x : free_group X,
fg_equiv X (fg_mul fg_id x) x
| fg_right_id : forall x : free_group X,
fg_equiv X (fg_mul x fg_id) x
| fg_left_inv : forall x : free_group X,
fg_equiv X (fg_mul (fg_inv x) x) fg_id
| fg_right_inv : forall x : free_group X,
fg_equiv X (fg_mul x (fg_inv x)) fg_id
| fg_mul_assoc : forall x y z : free_group X,
fg_equiv X (fg_mul (fg_mul x y) z) (fg_mul x (fg_mul y z))
| fg_equiv_refl : forall x : free_group X,
fg_equiv X x x
| fg_equiv_sym : forall x y : free_group X,
fg_equiv X x y -> fg_equiv X y x
| fg_equiv_trans : forall x y z : free_group X,
fg_equiv X x y -> fg_equiv X y z -> fg_equiv X x z
| fg_equiv_resp_id : fg_equiv X fg_id fg_id
| fg_equiv_resp_inv : forall x x' : free_group X,
fg_equiv X x x' -> fg_equiv X (fg_inv x) (fg_inv x')
| fg_equiv_resp_mul : forall x x' y y' : free_group X,
fg_equiv X x x' -> fg_equiv X y y' ->
fg_equiv X (fg_mul x y) (fg_mul x' y').
(Incidentally, it's also very easy to extend this to describe the group with any given presentation, or in general the object of any variety of algebras with a given presentation: just add the relations from the presentation to the requirements on the equivalence relation in (2).)
Two things before we start:
You are misquoting the definition of free group. What you describe is the "free group on $x_1,\ldots,x_m$", not on "$x_1,\ldots,x_m,x_1^{-1},\ldots,x_m^{-1}$". The symbols $x_1^{-1},\ldots,x_m^{-1}$ are part of the construction, but they are not part of the definition. So here, the set $X$ is going to be $X=\{x_1,\ldots,x_n\}$, and not the set $\{x_1,\ldots,x_m,x_1^{-1},\ldots,x_m^{-1}\}$.
I am going to change your notation, because the use of $F$ is of course natural for "functor", but in this case it conflicts with the usual notation for "free group" and "underlying set." So instead, I am going to take the "data" functor denoted as $\mathsf{U}$, for "underlying set". Your category $\mathcal{C}$ is $\mathsf{Group}$, and $\mathcal{D}$ is $\mathsf{Set}$. So the particular instance of the "free object on $X$" here would be:
A universal morphism from the set $X$ to the "underlying set functor" $\mathsf{U}\colon\mathsf{Group}\to\mathsf{Set}$ (the forgetful functor that sends a group to its undderlying set, and a group morphism to the corresponding function between underlying sets), is a pair $(A,f)$ where $A$ is a group, and $f\colon X\to \mathsf{U}(A)$, the underlying set of $A$. This pair satisfies the universal property; i.e., for every group $B$ and every set map from $X$ to the underlying set of $B$, $g\colon X\to\mathsf{U}(B)$, there exists a unique group homomorphism $h\colon A\to B$ such that $g=\mathsf{U}(h)\circ f$.
You want to understand the "usual" explicit description of "free group on $x_1,\ldots,x_m$" in terms of this definition. (See point 1 above for what the group is free "on").
So, $X$ is going to be the set $x_1,\ldots,x_m$. The group $A$ is going to be the group you describe: the set of "reduced group words" in the alphabet $x_1,\ldots,x_m$; that is, terms of the form
$$w_1^{\epsilon_1}\cdots w_k^{\epsilon_k}$$
where $w_i\in \{x_1,\ldots,x_m\}$, $\epsilon_i\in\{1,-1\}$, $k\geq0$, and where "reduced" means that there is no $i$ such that $w_i=w_{i+1}$ and $\epsilon_i=-\epsilon_{i+1}$. The group operation on $A$ is "concatenate and reduce", which means that you take the words $w_1^{\epsilon_1}\cdots w_k^{\epsilon_k}$ and $v_1^{\delta_1}\cdots v_{\ell}^{\delta_{\ell}}$, and you write the word
$$w_1^{\epsilon_1}\cdots w_k^{\epsilon_k}v_{1}^{\delta_1}\cdots v_{\ell}^{\delta_{\ell}},$$
and then if there are any instances of $x_k$ followed by $x_k^{-1}$, or $x_k^{-1}$ followed by $x_k$, you remove those two letters and you check the result. This is a group, and the easiest way to verify the hard part (associativity) is to use van der Waerden's trick.
So this is the group $A$. The set map $f\colon X\to \mathsf{U}(A)$ is just the inclusion map, since each element of $X$ is itself a reduced word in $A$.
To verify that this is a universal morphism (equivalently, that $(A,f)$ is the free group on $X$) we must show that given any group $B$ and any set map $g\colon X\to B$, there is a unique group morphism $h\colon A\to B$ such that $g=\mathsf{U}(h)\circ f$. This morphism $h$ is defined as follows: given a reduced group word $w_1^{\epsilon_1}\cdots w_k^{\epsilon_k}\in A$, with $w_i\in \{x_1,\ldots,x_m\}$, $\epsilon_i\in\{1,-1\}$, we define
$$h(w_1^{\epsilon_1}\cdots w_k^{\epsilon_k}) = g(w_1)^{\epsilon_1}\cdots g(w_k)^{\epsilon_k}.$$
It is then a bit of work, but not too hard, to verify that this is indeed a group homomorphism and that it satisfies $g=\mathsf{U}(h)\circ f$. Moreover, it is the unique map that will do this, because $A$ is generated by $f(X)$, and the values of any morphism $\mathfrak{h}\colon A\to B$ is completely determined by its value on the generating set $f(X)$; so if $\mathfrak{h}$ satisfies that $\mathfrak{h}(x_i) = g(x_i)$, then $\mathfrak{h}=h$.
The more common way to think about the free group on $X$ within category theory is in terms of adjoint functors. Specifically, we have the concretizing functor $\mathsf{U}\colon\mathsf{Group}\to\mathsf{Set}$, the underlying set functor, which is faithful. We define a functor $\mathsf{F}\colon \mathsf{Set}\to\mathsf{Group}$ with the following property: given a set $X$ and a group $G$, there is a natural bijection
$$\mathsf{Set}(X,\mathsf{U}(G)) \cong \mathsf{Group}(\mathsf{F}(X),G).$$
The functor $\mathsf{F}$ is called the left adjoint of $\mathsf{U}$, and $\mathsf{U}$ is the right adjoint of $\mathsf{F}$; $\mathsf{F}$ is the "free group functor", that associates to each set $X$ the free group on $X$. The standard way to express the universal property is the following, which elides the functor $\mathsf{U}$:
The free group on $X$, $(\mathsf{F}(X),\iota)$, is a group $F(X)$ and a set function $\iota\colon X\to \mathsf{F}(X)$ such that for every group $G$ and every set function $g\colon X\to G$, there exists a unique group homomorphism $h\colon F(X)\to G$ such that $g=h\circ\iota$.
Throughout we are abusing notation by considering a function between groups to be the same as the corresponding function between underlying sets.
So we usually think of "free object on $X$" as the image of $X$ under a functor that is the left adjoint of a concretizing functor, rather than as an object whose image is a universal arrow in the category $\mathsf{Set}$. This gives the "free commutative ring with unity on $X$" (the polynomial ring $\mathbb{Z}[X]$); the "free vector space over $F$ on $X$" (the vector space $F^{(X)}$), the "free topological space on $X$" (the set $X$ together with the discrete topology on $X$), etc.
Another way to think about the free group on $X$, entirely within the confines of group theory (without reference to functors), is to think of "the free group on $X$" as "the most general group that contains $X$ among its elements". In that sense, the set of reduced group words can be thought of as "all group elements we could construct starting from the elements of $X$, subject only to the rules that are inherent in any group: associativity, existence of inverses, and that inverses cancel each other out." You can think of it as taking products of elements, but "leaving everything that is not obvious indicated". We know that $x$ and $x^{-1}$ multiply to the identity, but in general we do not know what $x_1$ and $x_2$ will yield when multiplied... so we just "leave it indicated" by writing $x_1x_2$. When we identify the elements of $X$ with specific elements of a group $G$ via the map $f\colon X\to G$, we can now "evaluate" these products, because now we know which elements of the known group $G$ they are, and the morphism $h$ is just the "go ahead and evaluate all the expressions left indicated" morphism.
Note that like any universal object, there is in general no such thing as "the" free group on $X$. Rather, the free group on $X$ is only determined up to (unique) isomorphism, and there are many constructions that may reify it. "The set of reduced group words on $X$" is one such construction. If you want to see two other constructions, I recommend George Bergman's An Invitation to General Algebra and Universal Constructions, which is published by Springer. There is an older version available as a PDF from his website. In particular, take a look at the extensive discussion of three ways to construct "the free group" in Chapter 3.
Best Answer
For your first question: the proof of theorem $2.2.7$ explicitly explains what $\hat{s}$ is: it's an additional disjoint copy of $S$ whose elements play the roles of inverses. In fact, it's the very first paragraph of the proof.
For your second question: since $s\in S$ and $\hat s \in S$ are different (and belong to different, disjoint copies of $S$) we need to define how they both operate on the group element $x$, which is why both points $1$ and $2$ are given. You can indeed go from $I(abc)$ to $\hat{c}\hat b\hat a$ and this is also the expected right-inverse of the word $abc$ in a group.
And for your last question the answer is again that this explicitly connects the nominal inverse $\hat s$ with the inverse of the homomorphism $\varphi$ so both need to be defined.