Centralizing HNN extension detects subgroup membership (source code)

= Centralizing HNN extension detects subgroup membership
{title2=$t^{-1}ptp^{-1}=1\ \Longleftrightarrow\ p\in L$}

In the <HNN extension> $\langle P,t\mid t^{-1}\ell t=\ell\ (\ell\in L)\rangle$, the displayed equivalence follows from <Britton's lemma>. If $p\in L$, the word collapses by the defining isomorphism; otherwise it has stable letters and no pinch, so it is nonidentity. When $P$ is finitely presented and $L$ is finitely generated, imposing commutation with the finitely many subgroup generators gives a finite presentation. An undecidable membership problem for $L$ then becomes an undecidable <word problem for a group> in the extension.