The Friedman embedding theorem

In this paper, we will present an explicit construction of Harvey Friedman which to every finitely generated group G associates a 2-generator subgroup KG⩽Sym(N) such that G embeds into KG and such that if G≅H, then KG=KH.