Recursive presentation of a group

A recursive presentation has an effectively enumerable alphabet of generators and a recursively enumerable set of relators. Usually the alphabet is finite; when it is countably infinite this is specified explicitly. Enumerating finite products of conjugates of relators and their inverses enumerates all null words. Conversely the enumerable null words can themselves serve as the relators. Recursive presentability does not imply a soluble word problem for a group.

A finitely generated group embeds in a finitely presented group if and only if it has a recursive presentation of a group. The necessity follows by enumerating proofs that substituted generator words are trivial in the larger finite group presentation. The sufficiency is the embedding theorem; it also applies to effectively countably generated recursive presentations after an effective two-generator embedding. This is the theorem of Subgroups of finitely presented groups.