FURTHER

To explain why $G_0\to G_1$ is computable, I need to describe the construction. I'll give one version here, which I think makes the point fairly cleanly. If I recall correctly, it's very similar to the original argument given by Higman, Neuman and Neumann, though they do a little better and get an embedding into a two-generator group. I'll stick with three generators for simplicity.

I'll take $G_0$ to be given by a recursive presentation $\langle (a_m\mid m\in\mathbb{N})\mid (r_n\mid n\in\mathbb{N})\rangle$.

First, note that by replacing $G_0$ with $G_0*\langle x\rangle$ and by replacing each $a_m$ by $a_mx^{m+1}$, I may assume that the $a_m$ are all of infinite order and distinct.

Let

$G_{\frac{1}{2}}=G_0*\langle s\rangle$

and consider the subgroups

$H_M=\langle b_m=s^ma_{m-1}s^{-m}\mid m\geq M\rangle$

for $M\geq 1$. An easy argument with normal forms in free products proves:

Lemma: $H_M$ is free on the given generating set.

Therefore, the assignment $b_m\mapsto b_{m+1}$ defines an isomorphism $\phi:H_1\to H_2$. We can therefore define $G_1$ to be the HNN extension

$G_1=G_{\frac{1}{2}}*_\phi$

which has presentation $\langle G_{\frac{1}{2}},t\mid tht^{-1}=\phi(h)~\forall h\in H_1 \rangle$ (relative to $G_{\frac{1}{2}}$). We now appeal to Britton's Lemma to prove that $G_1$ contains a copy of $G_0$.

Britton's Lemma: The natural map $G_{\frac{1}{2}}\to G_{\frac{1}{2}}*_\phi$ is injective.

But $G_1$ is finitely generated; indeed it's generated by $a_0,s,t$.

The map $G_0\to G_1$ is given recursively by the equations

$a_m=s^{-m}b_ms^m$ and $b_m=tb_{m-1}t^{-1}$.

(Of course, $a_0\mapsto a_0$.) In particular, it's certainly computable.

To prove that the word problem is solvable in $G_1$, you need to argue that you can solve the membership problems for $H_0$ and $H_1$ in $G_\frac{1}{2}$.

1

If I've followed this thread correctly, then there is still a question of whether a finitely presented example can be constructed. This follows from standard facts.

Specifically, let $G=G_0$ be the group constructed by Joel or Jason. By the standard Higman--Neumann--Neumann argument, $G_0$ embeds into a finitely generated group $G_1$ because $G_0$ is countable. It's a fact that $G_1$ is recursively presentable if $G_0$ was. By Higman's Embedding Theorem, $G_1$ can be embedded into a finitely presentable group $G_2$ because $G_1$ is recursively presentable.

The embedding of $G_0$ into $G_1$ is computable, and the embedding of $G_1$ into $G_2$ is obviously computable (since both groups are finitely generated).

Finally, one would like all this to be done so that $G_2$ has solvable word problem. That the Higman Embedding can be made to preserve solvability of the word problem follows from a result of Clapham.

(Strictly speaking, one also needs to check that $G_1$ can be taken to have solvable word problem, as I think Clapham starts with a finitely generated group. This must be well known, but Bridson and I wrote out the details in Section 7 of this paper.)