A famous result by G. Higman in group theory says that a finitely generated group can be embedded in a finitely presented group precisely if it has a presentation whose defining relations are a recursively enumerable set of words. It has been conjectured by the group theorist W. Boone that the same result holds more generally for every single-sorted algebraic theory.

Statement

…

Lawvere on the Boone conjecture

There is an issue involving recursivity that categorists should settle: How general is Higman’s theorem? In group theory the word problem (whether a given finitely generated group is recursively related) is equivalent to the purely algebraic one of whether the given group can be embedded as a subgroup of a finitely presentable one. For which other algebraic categories is the same statement true? or is it possibly true for the category of single-sorted algebraic theories? The latter problem was posed by Bill Boone, but as far as I know, is not yet resolved.

For the category of first-ordertheories, a theorem analogous to Higman’s was proved by Craig and Vaught; for that case, they gave a kind of intuitive argument: using a few additional predicates one can express enough of number theory to encode a fragmentary satisfaction relation and any given recursive set of axioms, so that one can then add the one additional axiom that says “all those axioms are true”. Of course, it is non-trivial that this argument actually works. (Lawvere 2002)