Solution (source code)

= Solution

The <Messuage lemma for groups> is the following effective collapse-versus-embedding statement: from a <finite group presentation> for $K$ and a word $w$, one can algorithmically write a finite presentation $K_w$ such that $w=1$ in $K$ makes $K_w$ trivial, whereas $w\ne1$ makes the specified copy of $K$ embed in $K_w$. It can also be arranged that the image of $w$ normally generates $K_w$. We use this lemma as an assumed construction, as requested; the construction of its presentation does not require deciding which case applies.

Let $P$ be a <finitely presented group> with insoluble <word problem for a group>, whose existence is allowed. Set $K=P*\langle z\rangle$, with $z$ of infinite order. It is finitely presented, and the <normal form theorem for a free product> embeds both $P$ and the infinite cyclic factor. Thus an input word $w$ from $P$ is trivial in $K$ exactly when it is trivial in $P$, while $K$ is certainly infinite.

Apply the <Messuage lemma for groups> to this $K,w$. If $w=1$ in $P$, the constructed group $K_w$ is trivial and hence finite. If $w\ne1$, it contains $K$ and is infinite. Consequently
$$
\boxed{K_w\text{ is infinite}\quad\Longleftrightarrow\quad w\ne1\text{ in }P.}
$$
A hypothetical algorithm deciding infinitude from arbitrary <finite group presentations> would therefore decide every input word in $P$, a contradiction. \b[There is no such algorithm.] The infinite cyclic free factor ensures the reduction does not need an additional assumption about the size of $P$.