The word problem for finite groups

Solution 1:

One can prove quite simply a much more general result due to McKinsey, viz.

Solution 2:

I would recommend Rotman's book "An Introduction to the Theory of Groups" for basic material on word problems of groups, and for a reasonably accessible proof of the Novikov-Boone theorem which asserts the existence of finitely presented groups with unsolvable word problem.

The notion of the word problem of a group is generally applied to groups defined by a specific finite presentation, but it is not hard to prove that, for a group $G$, the solvability of the word problem of $G$ is independent of the given presentation of $G$, so it is customary simply to say that the word problem of $G$ is or is not solvable.

Lots of familiar classes of groups are known to have solvable word problem, including finite groups, finitely presented residually finite groups (proof given above by Bill Dubuque), automatic groups, finitely generated nilpotent groups. But, by a recent result of Olga Kharlampovich, there exist finitely presented solvable groups of derived length $3$ with unsolvable word problem.

Note that the word problem is semi-decidable for all groups given by a recursively enumerable presentation, in the sense that if you are given a word in the generators that does represent the identity element of the group, then it is possible to prove that it does. You can do that naively by systematically trying all possibilities for expressing the word as a product of conjugates of defining relators, but there are more efficient and practical methods of attempting this by using rewriting systems or coset enumeration.