Context: an obvious necessary condition for a monoid to embed into a group (as submonoid) is to satisfy the left and right cancelation rules: $$xy=xz \quad\Longrightarrow y=z;$$ $$yx=zx \quad\Longrightarrow y=z.$$ It's sufficient for commutative monoids, by an easy standard construction. However, in general it's known not to be sufficient, as already mentioned at MO (see this question and this question). The first such construction is due to Malcev. Malcev's proof (1936), as described in this 1969 paper by R. Johnson (Proc AMS, link with unrestricted access), consists in checking that a in a group, we have the (straightforward) "generalized cancelation" rule:
$$ea=db,eb=fa,ec=fb \quad \Longrightarrow \quad eb=dc$$
Malcev's result consists then in constructing a cancelative monoid in which this rule fails (which is the less trivial part, and is not my point here).
Motivated by the above, we can define a generalized cancelation rule as a rule of the form $$w_1=w'_1,\dots,w'_n=w'_n \quad \Longrightarrow \quad w_0=w'_0$$ where $w_i,w'_i$ are non-negative words in some countable alphabet. A monoid is said to satisfy this generalized cancelation rule if it satisfies the above implication for each replacement of the letters by monoid elements.
Let $\mathcal{G}$ be the set of generalized cancelation rules that are satisfied by all groups.
Clearly a monoid that embeds into a group, satisfies all rules in $\mathcal{G}$. One can first ask about the converse: if a monoid satisfies all rules in $\mathcal{G}$, does it embed into a group?
The answer is actually a trivial yes! Indeed, starting from such a monoid $M$, define the enveloping group $i:M\to G_M$ in the obvious way (presentations: generators = $M$, relators = monoid law). Then $i$ is injective: indeed every relation of the form $i(m)=i(m')$ can be interpreted as some generalized cancelation rule, and eventually implies $m=m'$.
At a formal level this hence provides a characterization of monoids embedding into groups. But it's hopelessly non-practical. My question is then:
Is there a finite set $\mathcal{F}\subset\mathcal{G}$ of generalized cancelation rules such that a monoid embeds into a group iff it satisfies all the rules in $\mathcal{F}$?
