Editing Word problem for groups (section)

===Proof that there is no universal solvable word problem group===
Suppose <math>G</math> were a universal solvable word problem group. Given a finite presentation <math>P = \langle X \, | \, R \rangle</math> of a group <math>H</math>, one can recursively enumerate all homomorphisms <math>h : H \to G</math> by first enumerating all mappings <math>h^\dagger : X \to G</math>. Not all of these mappings extend to homomorphisms, but, since <math>h^\dagger(R)</math> is finite, it is possible to distinguish between homomorphisms and non-homomorphisms, by using the solution to the word problem in <math>G</math>. "Weeding out" non-homomorphisms gives the required recursive enumeration: <math>h_1, h_2, \ldots, h_n, \ldots</math>.

If <math>H</math> has solvable word problem, then at least one of these homomorphisms must be an embedding. So given a word <math>w</math> in the generators of <math>H</math>:

::<math>\text{If}\ w\ne 1\ \text{in}\ H,\ h_n(w)\ne 1\ \text{in}\ G\ \text{for some}\ h_n </math>
::<math>\text{If}\ w= 1\ \text{in}\ H,\ h_n(w)= 1\ \text{in}\ G\ \text{for all}\ h_n </math>

Consider the algorithm described by the pseudocode:

 '''Let''' ''n'' = 0
 '''Let''' ''repeatable'' = TRUE
 '''while''' (''repeatable'')
     increase ''n'' by 1
     '''if''' (solution to word problem in ''G'' reveals ''h<sub>n</sub>''(''w'') ≠ 1 in ''G'')
         '''Let''' ''repeatable'' = FALSE
 output 0.

This describes a recursive function:

::<math>f(w) = 
\begin{cases} 
0 &\text{if}\ w\neq1\ \text{in}\ H \\
\text{undefined/does not halt}\ &\text{if}\ w=1\ \text{in}\ H.
\end{cases}</math>

The function <math>f</math> clearly depends on the presentation <math>P</math>. Considering it to be a function of the two variables, a recursive function {{tmath|f(P,w)}} has been constructed that takes a finite presentation <math>P</math> for a group <math>H</math> and a word <math>w</math> in the generators of a group <math>G</math>, such that whenever <math>G</math> has soluble word problem:

::<math>f(P,w) = 
\begin{cases} 
0 &\text{if}\ w\neq1\ \text{in}\ H \\
\text{undefined/does not halt}\ &\text{if}\ w=1\ \text{in}\ H.
\end{cases}</math>

But this uniformly solves the word problem for the class of all finitely presented groups with solvable word problem, contradicting Boone-Rogers. This contradiction proves <math>G</math> cannot exist.