I am interested in developing a formal proof that free groups exist, i.e. for any set $S$ there is a group $G\supseteq S$ such that for any group $H$ and any function $f:S\to H$ there is a homomorphism $\sigma\supseteq f$ from $G$ to $H$. (I don't think it is necessary for $\sigma$ to be unique for the existence proof.) Is there any way to prove this other than the explicit construction: (I hope I can give you a flavor of why this would be really annoying to do formally.)
- Let $\Sigma=2\times S=\{\langle 0,x\rangle, \langle 1,x\rangle:x\in S\}$.
- Let $X=\bigcup_{n\in\omega}\Sigma^n$.
- Define the concatenation operation $\sqcup:X\times X\to X$ by $$\def\dom{\operatorname{dom}} x\sqcup y=x\cup\{\langle n+\dom x+1,z\rangle:\langle n,z\rangle\in y\}.$$
- Define ${}^{-1}:\Sigma\to\Sigma$ such that $\langle 0,x\rangle^{-1}=\langle 1,x\rangle$ and $\langle 1,x\rangle^{-1}=\langle 0,x\rangle$.
- Define the equivalence $\sim$ as the reflexive/symmetric/transitive closure of $$\{\langle x,y\rangle:\exists n\in \Sigma, \exists z,w\in X\,(x=z\sqcup w\land y=z\sqcup\{\langle 0,n\rangle, \langle 1,n^{-1}\rangle\}\sqcup w) \}.$$
- Define $G=(X,\sqcup)/\sim$. Then $G$ is a group, where $S$ is embedded as $x\mapsto[\{\langle 0,\langle 0,x\rangle\rangle\}]_\sim$.
What I am looking for are "slick" proofs that avoid all the dirty details here to show that there exists a group satisfying the categorical property of a free group without this concatenation/reduction stuff.
Although I can do some category theory, I'm not a big fan of it since it seems to bury any concept in several layers of definition for little gain. Thus I'm going to restate Martin Brandenburg's answer to a variation on this question in "elementary" terms, following the suggestions of Jakob Werner and Derek Holt on this page.
Let $\Sigma=2\times S$, $X=\bigcup_{n\in\omega}\Sigma^n$. Now this looks similar to the setup in the OP, but we aren't going to use it to define any algebra of words; this is purely needed for its cardinality. If $G$ is a group and $S$ generates $G$, then the function $\sigma:X\to G$ defined by $\sigma(x)=\tau(x_1)\tau(x_2)\dots\tau(x_n)$ where $\tau:\Sigma\to G$ sets $\tau(0,x)=x,\tau(1,x)=x^{-1}$ must be a surjection onto $G$. Thus $|G|\le|X|$ (looks like some AC snuck in, any suggestions for how to eliminate this?).
Now let $\cal G$ be the set of all pairs $(G,\phi_G)$ such that $G$ is a group whose base set is a subset of $X$, and $\phi_G$ is an injection from $S$ to $G$ that generates $G$ (here is where we use boundedness of $X$ to show that $\cal G$ is a set), and define $P=\prod_{(G,\phi_G)\in\cal G}G$ as a group with the operation of pointwise group operation. $S$ is embedded into $P$ as $x\in S\mapsto((G,\phi_G)\in{\cal G}\mapsto\phi_G(x))$, and let $F$ be the subgroup of $P$ generated by $S$ under this map.
The claim is that $F$ is freely generated by $S$. Given a group $H$ and a function $f:S\to H$, let $T$ be the subgroup of $H$ generated by $f(S)$. Then $|T|\le|X|$, so let $i$ be an injection from $T$ to $X$. We have $i(T)\subseteq X$, and with the group operation inherited from $H$, $i(T)$ is a group, so $(i(T),i\circ f)\in\cal G$, and we can define $\sigma:P\to H$ as $\sigma(x)=i^{-1}(x(i(T),i\circ f))$; this is a homomorphism, and its restriction to $F$ is unique.
Believe it or not this kind of argumentation is much easier to formalize and does not require too much details about groups (since it's ultimately a category theory proof), although one needs to know that the "generation" operation does not make a set too much bigger, hence the "ugly stuff" in the second paragraph.