# Residually finite and all homomorphisms to any finite group can be listed in finite time implies solvable word problem

## Statement

Suppose is a finitely generated group that is both a residually finite group and a finitely generated group for which all homomorphisms to any finite group can be listed in finite time. Then, is a group with solvable word problem.

## Related facts

### Similar facts

### Applications

- Finitely presented and residually finite implies solvable word problem (obtained by combining with finitely presented implies all homomorphisms to any finite group can be listed in finite time)

## Proof

### Proof outline

Note that in order to solve the word problem, it is sufficient to come up with an algorithm that can, in finite time, show that a given word does *not* represent the identity element if indeed it does not. This is because there already exists an algorithm (for *every* finitely generated group) that can show in finite time that a given word *does* represent the identity element if it does.

The algorithm is as follows:

- Consider a countable list of finite groups such that every finite group is isomorphic to a subgroup of one of these. We could take the list of all finite groups enumerated suitably, but it also suffices to just take the list of all symmetric groups of finite degree. By Cayley's theorem, every finite group is a subgroup of one of these.
- For each : Construct the list of all homomorphisms from to (possible by assumption on ). For each homomorphism, evaluate the image of the word under the homomorphism as an element of . If the image is a non-identity element, then return that the word does
*not*represent the identity element of .

Since is residually finite, it is true that for any non-identity element, there is some finite quotient where its image is a non-identity element. This finite quotient lives inside some , so homomorphisms to will detect that the element is not the identity element. Thus, for any word not representing the identity element, the algorithm terminates in finite time to show that the word does not represent the identity element, as desired.