I'm working on a construction of the free group, and as the proof is taking me further afield than I'd expected I'd like some verification that I'm going the right direction and there is not some easier approach to what I am doing. Note that I am writing a formal proof, so extra emphasis on the rigor (I already know the "big picture" handwavy proof).
Let $S$ be the given set of generators, and let $W=\Sigma^*$, $\Sigma= S\times\{0,1\}$ be the set of all strings of the elements $\langle s,0\rangle$, representing the generator $s\in S$, and $\langle s,1\rangle$, for the inverse of $s$. Define the function ${}^{-1}:\Sigma\to\Sigma$ by $\langle s,i\rangle^{-1}=\langle s,1-i\rangle$, and define $T:W\to{\cal P}(W)$ by demanding that $v\in T(w)$ iff for some $x,y\in W$ and $\sigma\in\Sigma$, $w=xy$ and $v=x\sigma\sigma^{-1}y$. Thus $T$ is the set of all "direct extensions" of $w$ by one cancelling pair $\sigma\sigma^{-1}$.
Define $\sim$ to be the smallest equivalence relation such that $w\sim v$ for all $w\in W,v\in T(w)$, and let $G=W/\sim$, where $\langle W,+\rangle$ here is given the free monoid structure of concatenation. Claim I want to prove that $G$ is free on $S$, with generating set $\{[\langle s,0\rangle],s\in S\}$.
This differs slightly from other treatments, which prefer to use reduced words only. Define $D=W\setminus\bigcup_{w\in W}T(w)$; these are sets which are not the direct extension of any word, and thus are reduced as much as possible. Can we show that every equivalence class $[w]$ contains a unique $d\in D$?
To this end, consider the notion of "extension sequence". We define $\langle w_0,\dots,w_k\rangle$ to be an extension sequence if $w_0\in D$ and for each $i$, $w_{i+1}\in T(w_i)$.
Theorem Every $w\in W$ is the end of some extension sequence. Proof by complete induction on $|w|$. If $w\in D$ then $\langle w\rangle$ is an extension sequence; otherwise $w\in T(v)$ for some $v$, so $|w|=|x\sigma\sigma^{-1}y|=|xy|+2=|v|+2>|v|$, and so by the induction hypothesis there is some extension sequence $\langle v_0,\dots,v_{k-1},v\rangle$, and so $\langle v_0,\dots,v_{k-1},v,w\rangle$ is an extension sequence.
It follows from this that every equivalence class contains a reduced word, because for any extension sequence ending at $w$ we have $D\ni w_0\sim w_1\sim\dots\sim w_k=w$.
To show uniqueness, I am trying to leverage extension sequences again: Claim If $\langle a_k\rangle_k,\langle b_k\rangle_k$ are extension sequences both ending in $w$, then $a_0=b_0$.
Skipping this for the moment, we can address the free group theorem itself: Let $H$ be a group and $A:S\to H$ a function, and define $F:\Sigma\to H$ by $F(s,0)=A(s),F(s,1)=A(s)^{-1}$. Then define $\phi(w_0\dots w_n)=F(w_0)\dots F(w_n)$. Then $\phi$ is a monoid homomorphism, and $\phi(x\sigma\sigma^{-1}y)=\phi(x)F(\sigma)F(\sigma^{-1})\phi(y)=\phi(x)F(\sigma)F(\sigma)^{-1}\phi(y)=\phi(xy)$, so the relation $v\approx w\iff \phi(v)=\phi(w)$ is an equivalence relation which also satisfies $v\in T(w)\to v\approx w$, so by definition of $\sim$, $v\sim w\to\phi(v)=\phi(w)$, and $\phi$ lifts to a monoid homomorphism $\phi':G\to H$ (which is a group homomorphism because $G$ is a group).
Something bothers me about the above argument: Without the reduced word argument, I don't even know how to prove that $s\mapsto[\langle s,0\rangle]$ is injective, but here I already have shown the existence of a homomorphism with the expected properties (which of course separates any $s,t\in S$ with $A(s)\ne A(t)$), seemingly "for free" (although it requires a suitably chosen large group $H$ to establish injectivity directly from this).
Continuing work on the reduced word problem:
Proof If $k=0$ then $w_k=w_0\in D$, and conversely if $k>0$ then $w_k\in T(w_{k-1})$ so $w_k\notin D$.
Proof by complete induction on $|w|$ (so suppose we have already proven the claim for $|w'|<|w|$). If $w\in D$, then by Lemma 1 $m=n=0$, so $a_0=a_m=b_n=b_0$. Otherwise, $m,n\ge1$ so we have $w=a_m\in T(a_{m-1}),w=b_n\in T(b_{n-1})$. Find $r,s,t,u,\sigma,\tau$ such that $a_{m-1}=rs$, $b_{n-1}=tu$, and $w=r\sigma\sigma^{-1}s=t\tau\tau^{-1}u$, and WLOG assume $|r|\ge|t|$.
Case 1: $|r|=|t|$. In this case, since $r$ and $t$ are equal-length substrings of $w$, $r=t$, and similarly $|s|=|u|$ implies $s=u$, so $a_{m-1}=b_{n-1}$, and applying the induction hypothesis to the extension sequences $\langle a_0,\dots,a_{m-1}\rangle,\langle b_0,\dots,b_{n-1}\rangle$ we find $a_0=b_0$.
Case 2: $|r|=|t|+1$. In this case, matching substrings we have $r=t\tau$, $\sigma=\tau^{-1}$, and $\sigma^{-1}s=\tau s=u$ so $a_{m-1}=t\tau s=b_{n-1}$ and we can conclude as in Case 1.
Case 3: $|r|\ge|t|+2$. In this case we have $r=t\tau\tau^{-1}x$ and $u=x\sigma\sigma^{-1}s$ for some word $x$, so that $w=t\tau\tau^{-1}x\sigma\sigma^{-1}s$, and $a_{m-1}=t\tau\tau^{-1}xs$, $b_{n-1}=tx\sigma\sigma^{-1}s$. In this case we will generally have $a_{m-1}\ne b_{n-1}$. Let $c=txs$ and find an extension sequence $\langle c_0,\dots,c_k\rangle$ with $c_k=c$. Note that $a_{m-1}$ and $b_{n-1}$ are both direct extensions of $c$. By the induction hypothesis applied to $\langle c_0,\dots,c_k,a_{m-1}\rangle,\langle a_0,\dots,a_{m-1}\rangle$, we have $a_0=c_0$, and applied to $\langle c_0,\dots,c_k,b_{n-1}\rangle,\langle b_0,\dots,b_{n-1}\rangle$, we have $b_0=c_0$. Thus $a_0=b_0$ as desired. $\tag*{$\Box$}$
The OP already shows existence, by taking any extension sequence and relating the elements of the sequence. For uniqueness, define the equivalence relation $v\approx w$ iff there are extension sequences $\langle d,\dots,v\rangle$, $\langle d,\dots,w\rangle$ for some $d$. This is reflexive by existence of extension sequences, and trivially symmetric; for transitivity, if we have $\langle d,\dots,w_1\rangle$, $\langle d,\dots,w_2\rangle$, $\langle d',\dots,w_2\rangle$, $\langle d',\dots,w_3\rangle$, then by the above Theorem $d=d'$, so $w_1\approx w_3$. Finally, if $v\in T(w)$ then $\langle d,\dots,w\rangle$, $\langle d,\dots,w,v\rangle$ demonstrate $v\approx w$. Thus $v\sim w\to v\approx w$ by minimality of $\sim$, so if $d_1\sim w\sim d_2$ for $d_1,d_2\in D$ we have $\langle d,\dots,d_1\rangle$, $\langle d,\dots,d_2\rangle$, and by lemma 1, $d_1=d=d_2$. $\tag*{$\Box$}$