The word problem for finite groups The word problem for finite groups is decidable. Is it obvious that this is true? 
In particular, I'm not entirely sure about what it means for the problem to be decidable (in this case---I think I understand what decidable means in general). I assume it means that we are given a fixed group G (do we have to assume this), but is the generating set (the letters) also fixed? 
To decide the word problem for the group of symmetries of a square, with reflection $r$ and transposition $t$ as the generators, I would first find a canonical form for the group elements $1,r,r^2,r^3,t,tr,tr^2,tr^3$, and then note that using the relations $r^4=1$ and $rt=tr^3$ to show that any word can be reduced to something on my list. However, this seems like a lot of work, and it's not obvious to me what should be done in the case of an arbitrary finite group. 
 A: The sense in which I think this statement is usually meant is that you are given the entire multiplication table of the group.  Then it's obvious that the word problem is decidable.  You seem to be thinking about a different question: maybe you are given generators and relations and you are told that they define a finite group, then asked to solve the word problem.  This question, to me, is not obvious.
A: One can prove quite simply a much more general result due to McKinsey, viz.


A: The easiest way to see that a finite group has solvable word problem is to notice that the solution is not required to be uniform over all finite groups. Given a finite group (presentation) there is an algorithm that takes that group (presentation) as input but ignores it. The algorithm then uses the group table, which is hard-coded into the algorithm, to reduce the word. The algorithm reduces the word by always replacing the product of the first two elements with a single element until there's just one element remaining.
A: 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.
