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

## Statement

Suppose $G$ 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, $G$ is a group with solvable word problem.

## 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:

1. Consider a countable list $K_1, K_2, \dots, K_n, \dots$ 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.
2. For each $i$: Construct the list of all homomorphisms from $G$ to $K_i$ (possible by assumption on $G$). For each homomorphism, evaluate the image of the word under the homomorphism as an element of $K_i$. If the image is a non-identity element, then return that the word does not represent the identity element of $G$.

Since $G$ 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 $K_n$, so homomorphisms to $K_n$ 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.