---
tag: P7TZ694FCM
kind: statement
role: theorem
name: Higman embedding theorem
msc: ["20F10", "20F05", "03D40"]
uses: [082DWWXMRJ, TJKANTKASZ, 0JGEQXQ4AC, 0X1JXT47GA]
about: [TJKANTKASZ, 082DWWXMRJ]
sources:
  - url: https://en.wikipedia.org/wiki/Higman%27s_embedding_theorem
same_as:
  wikidata: Q17029787
  wikipedia: Higman's embedding theorem
---

## Statement

Let $G$ be a [[finitely generated group|082DWWXMRJ]].
Call $G$ *recursively presented* if it has a [[presentation|0JGEQXQ4AC]] $\langle S \mid R \rangle$ with $S$ finite and $R$ [[computably enumerable|TN9G24VABN]].
Here $R$ is a set of words in the elements of $S$ and their inverses.
Then $G$ is isomorphic to a [[subgroup|0X1JXT47GA]] of a [[finitely presented group|TJKANTKASZ]] if and only if $G$ is recursively presented.

## Remarks

One direction is easy.
Let $G$ be generated by finitely many elements of a finitely presented group $P$.
A program can list all consequences of the finitely many relators of $P$.
So it can list all words in the generators of $G$ that equal $1$ in $P$.
The other direction is the hard part of Higman's 1961 proof.
It builds the finitely presented group by a long chain of [[HNN extensions|YEYERRY37K]] and amalgamated free products that encode the enumeration of $R$.

Example: the wreath product $\Z \wr \Z$ has the presentation $\langle a, t \mid [a, t^n a t^{-n}] = 1 \text{ for } n \ge 1 \rangle$.
The set of relators is computably enumerable, so $\Z \wr \Z$ embeds in a finitely presented group, although it is not finitely presented itself.

There are uncountably many $2$-generated groups up to isomorphism, but only countably many finitely presented groups, each with countably many finitely generated subgroups.
So the hypothesis cannot be dropped: some finitely generated groups do not embed in any finitely presented group.

## Explanations

### L1 human

A finitely presented group is described by finitely many generators and finitely many rules.
The theorem says exactly which finitely generated groups live inside such groups.
They are the groups whose rules can be listed one by one by a computer program, even if the list never ends.
It is a bridge between group theory and the theory of computation.

### L2 human

The theorem shows that there is a finitely presented group that contains every finitely presented group as a subgroup.
It also gives another route to finitely presented groups with unsolvable [[word problem|PBGTTAVMMT]].
Take a computably enumerable set of integers that is not computable.
Encode it into the relators of a recursively presented group with unsolvable word problem, and embed this group in a finitely presented group.
The word problem of the big group cannot be solvable, since it would solve the word problem of the subgroup.