The algebraic characterization is the Boone-Higman theorem:
Here need not be finitely generated or finitely presented. We prove the equivalence using the Higman embedding theorem, Britton's lemma and the normal form theorem for a free product. The original characterization is Theorem I of An algebraic characterization of groups with soluble word problem.
First suppose the embeddings exist. Choose a word in representing some fixed , and fixed words in representing the finite generators of . Given a word in those generators, one search enumerates proofs that in the finite group presentation of . A second search enumerates all finite products of conjugates in of , and all proofs that any such product equals . All these searches are effective: a proof of equality is a finite product of conjugates of defining relators, checked in the free group, and dovetailing handles the countably many candidates.
If , simplicity gives , so is such a finite product with conjugators in , which are also elements of . The second search eventually succeeds. If , every such product is trivial, so it cannot equal , but the first search succeeds. Running the two searches in parallel thus decides the word problem for a group in . This is semidecision of nonidentity in simple subgroups; no enumeration of or word algorithm for is required. The choice of the fixed word for is an existence choice of a finite string, not an algorithm for discovering from an arbitrary presentation.
Conversely suppose the word problem for a group in is soluble. We construct a recursive simple envelope by cyclic HNN extensions, keeping all effectiveness requirements explicit. Start with , where has infinite order. Reduced free product words give a word algorithm for and an algorithm testing membership in and recovering its exponent. The original null words of are decidable and therefore enumerable, so has a recursive presentation of a group.
Inductively assume has an effectively enumerable generating set, a recursive presentation, a word algorithm, and an algorithm for membership and exponent in . Form . For each nonidentity word in , introduce distinct stable letters , and introduce another letter , with relations
Let be this multiple HNN extension of . A computable enumeration of all words of , filtered by its word algorithm, indexes the nonidentity used here. Repeated representatives of the same element cause no difficulty: their stable letters are simply distinct.
Every associated subgroup in these relations is infinite cyclic. For , the words and are cyclically reduced free product words with respectively two and four syllables; their nonzero th powers have lengths and . Therefore the reduced syllable length of an input bounds the finitely many possible exponents needed to decide membership in each subgroup and find the exponent. Membership in is immediate, and membership in is inherited from . This proves effective cyclic membership in a free product, including the crucial point that the order of is never needed.
By Britton's lemma, embeds in . To solve its word problem, repeatedly find a pinch in an HNN extension using these membership algorithms, transport the known exponent across its defining isomorphism, and remove two stable letters. With no pinch left, a word retaining stable letters is nontrivial and not in the base; otherwise the base word algorithm applies. The same reduction decides whether an input lies in : if stable letters remain it does not, and if none remain use the base cyclic-membership algorithm. This verifies the inductive effectiveness claims rather than asserting that HNN extensions automatically preserve decidable word problem. Only the finitely many stable letters in the input need inspection.
The union is nontrivial, since retains infinite order under every embedding, and has an effective countable recursive presentation: enumerate each stage's relators and dovetail the enumerations. We now prove simplicity. Let contain , and take a stage with . The commutator belongs to , so its displayed conjugation forces . Conversely, in the quotient by the normal closure of , the relation for forces ; then the relation for forces every nonidentity to be one. Thus the normal closure of contains each . All newly adjoined stable letters belong to a later , so this normal closure is all of . Hence , proving that is a simple group containing .
Finally apply the explicit two-generator HNN embedding from Question 3 to an effective countable list of generators of . Its same free-conjugate-basis argument works for every finite word, and its relations are recursively enumerable, so it embeds in a two-generated recursively presented group . The Higman embedding theorem embeds in a finitely presented group . Composing the inclusions gives , completing the proof of both directions.
A finitely generated group with soluble word problem for a group embeds in a countably generated simple group with a recursive presentation of a group. Start with , retaining decidable membership in . At stage , add a free infinite cyclic generator . For every nonidentity base element , conjugate to and conjugate to ; also conjugate to , using distinct stable letters. All associated subgroups are infinite cyclic, with decidable membership by effective cyclic membership in a free product. Britton's lemma preserves embeddings, decidable word problem and decidable membership in the inherited .
In the union, any nontrivial normal subgroup contains some nonidentity and hence , by the commutator-conjugation relation. The other relations force and then every old into the normal closure of . Every stable letter becomes an old element at a later stage, so the normal closure of is the whole union. The union is nontrivial and simple. Effective word enumeration at each stage makes all relators recursively enumerable. A two-generator HNN embedding followed by the Higman embedding theorem embeds this simple envelope in a finitely presented group.