Free groups are torsion-free

First work in the reduced-word model and let $w$ be a nonidentity element. Then $w$ is itself a nonempty reduced word, and [L1] gives a literal reduced factorisation $w=tct^{-1}$ with $c$ nonempty and cyclically reduced.

For every $n\geq1$, the literal concatenation $c^n$ is reduced and nonempty: each copy is reduced, and the seam between consecutive copies does not cancel because the last letter of $c$ is not the inverse of its first.

In the product $w^n$, the adjacent factors $t^{-1}t$ cancel between copies, leaving $tc^nt^{-1}$; its two outer seams are the same seams as in the reduced word $tct^{-1}$, so it is reduced and nonempty by step 2.1, and [L2] therefore shows that $w^n$ is not the identity.

The reduced-word model is a free group on $X$ by [L2], so [L3] gives a generator-compatible isomorphism from an arbitrary free group on $X$ onto it; transporting $g$ along that isomorphism, which preserves the identity and natural powers, step 3.1 gives $g^n\neq e$.

Thus no nonidentity element has a positive power equal to the identity, so by [F2] every nonidentity element has infinite order and every free group, including the trivial free group on the empty set, is torsion-free.