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](https://mathoverflow.net/questions/109566/a-linearly-orderable-monoid-which-does-not-embed-into-a-linearly-orderable-group) and [this question](https://mathoverflow.net/questions/378076/can-every-cancellative-invertible-free-monoid-be-embedded-in-a-group)). 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](https://doi.org/10.2307/2036896)), 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}$?*



Generalized cancelation properties ensuring a monoid embeds into a group
The answer is no. What you call a generalized cancellation rule is called a quasi-identity in universal algebra. Malcev proved in 1939 that there is no finite basis of quasi-identities defining group embeddable monoids or equivalently defining the quasi-variety of monoids generated by groups.


You can find details in Volume 2 of Clifford and Preston's classical text The Algebraic Theory of Semigroups. Malcev gave an infinite basis and Lambek another that has a geometric feel to it based on polyhedra. The precise theorem you want is Theorem 12.30 of Clifford and Preston Volume 2.


