General algebraic systems Terms, identities and equational logic Problem

Word problem for free algebras of a variety

Builds on Free algebra in a variety Variety of algebras Equational basis Equational theory Identity Computable function

Problem

Let $\mathcal{V}$ be a variety of finite signature with a finite equational basis $\Sigma$ . Let $X$ be a countably infinite set of variables, and let $F_{\mathcal{V}}(X)$ be the free algebra of $\mathcal{V}$ on $X$ . The problem asks for an algorithm, that is, a computable function, with the following task. For any two terms $s$ and $t$ over $X$ , it decides whether $s$ and $t$ denote the same element of $F_{\mathcal{V}}(X)$ . Equivalently, it asks whether the equational theory of $\mathcal{V}$ is decidable. That is, can one decide whether the identity $s \approx t$ holds in every algebra of $\mathcal{V}$ ?

Remarks

Since $\Sigma$ is finite, the identities of $\mathcal{V}$ are computably enumerable by listing all derivations in equational logic; the difficulty is to certify that an identity fails. The problem is solvable for many classical varieties. In groups, every element of a free group has a unique reduced word. In semigroups and monoids, the free algebras are the algebras of words, so equality is literal equality of words. In Boolean algebras, an identity holds exactly when it holds in the two-element Boolean algebra, which can be checked by truth tables. It is unsolvable in general: Tarski showed that the equational theory of relation algebras, which form a finitely based variety, is undecidable.

Reading path

To understand this page from the ground up, read these 7 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Computable function concept
Equational basis concept
Equational theory concept
Free algebra in a variety concept
Identity concept
Variety of algebras concept
Word problem for free algebras of a variety problem

Tag	`AR14VMVHNG`
URI	`m2://AR14VMVHNG`
Kind	problem
Writing	W0 stub
MSC	08A50, 08B20, 03B25
Status	This copy of the site has no build data. Run `m2 status AR14VMVHNG`.
About	Free algebra in a variety, Equational theory
Uses	Free algebra in a variety, Variety of algebras, Equational basis, Equational theory, Identity, Computable function
Changed	2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.