Evans's theorem on word problems

Remarks

From 1 to 2: take the presentation whose generators are the elements of $P$ and whose relations are the entries of the partial operation tables. Then $P$ embeds in $\mathcal{V}$ exactly when distinct elements of $P$ stay distinct in the presented algebra. From 2 to 1: given relations $R$ and terms $s, t$, let $S$ be the finite set of subterms of $s$, $t$ and the terms in $R$. Then $s \ne t$ in $\langle X \mid R \rangle_{\mathcal{V}}$ exactly when some quotient of $S$, as a partial algebra, satisfies $R$, separates $s$ and $t$, and embeds in $\mathcal{V}$. There are finitely many quotients to test. A useful sufficient condition: if $\mathcal{V}$ is finitely based and every finite partial algebra that embeds in $\mathcal{V}$ embeds in a finite algebra of $\mathcal{V}$, then condition 2 holds. Indeed, one can search at the same time for two things. One is a finite algebra of $\mathcal{V}$ in which $P$ embeds. The other is an equational derivation that identifies two distinct elements of $P$ in the presented algebra. Example: Boolean algebras are finitely based. A finite partial Boolean algebra that embeds in some Boolean algebra embeds in the finite subalgebra it generates. So finitely presented Boolean algebras have solvable word problem.

Going deeper

For a student

The theorem, due to Trevor Evans, connects the word problem with embeddings of partial algebras. Combined with the finite embeddability property, it explains why finitely based varieties such as Boolean algebras have solvable word problems. It also explains why unsolvability results for semigroups and groups are hard: one must build finite partial algebras whose embeddability encodes a halting problem.