Word problem for groups

DefinitionSolvable word problem#✓fully proved

Let \(G\) be a group, \(n\) a natural number and \(\varphi\) a homomorphism from the free group on \(n\) generators to \(G\). The word problem is solvable for \(\varphi\) when the predicate on words \(w\) (finite lists of letters, each a generator together with a sign) given by \(\varphi(w) = 1\) in \(G\) is computable: some algorithm decides, given a word \(w\), whether \(\varphi(w) = 1\).

When \(\varphi\) is surjective, for instance the quotient map of a presentation of \(G\) on \(n\) generators, this is the classical word problem for \(G\) with respect to these generators.

def WordProblemSolvable {G : Type*} [Group G] {n : ℕ}
    (φ : FreeGroup (Fin n) →* G) : Prop :=
  ComputablePred (fun w : List (Fin n × Bool) => φ (FreeGroup.mk w) = 1)

Used by 5

Used byKourovka Problem 17.29 (V. V. Bludov, A. M. W. Glass) · The Bludov–Glass question (Kourovka 17.28) · Boone–Higman theorem (easy direction) · Kuznetsov's theorem on finitely presented simple groups · Novikov–Boone theorem (unsolvability of the word problem)

TheoremNovikov–Boone theorem (unsolvability of the word problem)#●ready to prove

There exist a natural number \(n\) and a finite set \(R\) of elements of the free group \(F_n\) on generators \(g_1, \dots, g_n\) such that the word problem of the canonical surjection from \(F_n\) onto the presented group \(\langle g_1, \dots, g_n \mid R \rangle\) is not solvable: no algorithm decides, for a word \(w\) in the \(g_i\) and their inverses, whether \(w\) represents the identity of \(\langle g_1, \dots, g_n \mid R \rangle\).

public theorem_wanted novikov_unsolvable :
    ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
      rels.Finite ∧ ¬ WordProblemSolvable (PresentedGroup.mk rels)

def WordProblemSolvable {G : Type*} [Group G] {n : ℕ}
    (φ : FreeGroup (Fin n) →* G) : Prop :=
  ComputablePred (fun w : List (Fin n × Bool) => φ (FreeGroup.mk w) = 1)

WantedExt/GroupTheory/WordProblemSolvableShared.lean:48

Sources

P.S. Novikov, 'On the algorithmic unsolvability of the word problem in group theory', Trudy Mat. Inst. Steklov. 44 (1955) 1–143 (Russian); W.W. Boone, 'The word problem', Ann. of Math. (2) 70 (1959) 207–265 (announced 1958). §122 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem novikov_unsolvable of the lean-eval benchmark.

Uses 1

Statement usesSolvable word problem

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.