Centralizing HNN extension detects subgroup membership ($t^{-1}pt{p}^{-1}=1⟺p\in L$)

In the HNN extension $⟨P,t\mid t^{-1}\ell t=\ell (\ell \in L)⟩$, 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.

For a finitely presented base group $G$ and subgroup $H$, the extension $⟨G,t\mid [t,h]=1(h\in H)⟩$ is finitely presented exactly when $H$ is finitely generated. Sufficiency follows by imposing commutation with finitely many subgroup generators. For necessity, any finite set normally generating the defining kernel uses only finitely many centralizing relators. If their subgroup $H_0$ is proper in $H$, Britton's lemma makes $t^{-1}ht{h}^{-1}$ nonidentity in the partial extension for $h\in H\setminus H_0$, contradicting the claimed kernel equality.

// Target: algebra.bigb