Word problem for orderable groups

DefinitionBi-invariant linear orders on a group#✓fully proved

For a group \(G\), the bi-invariant orders of \(G\) are the linear orders \(\le\) on \(G\) (reflexive, antisymmetric, transitive and total relations) that are invariant under left and right multiplication: for all \(a, b, c \in G\), \(a \le b\) implies \(ca \le cb\) and \(ac \le bc\).

def biOrders (G : Type*) [Group G] : Set (G → G → Prop) :=
  {r | IsLinearOrder G r ∧ ∀ a b c : G, r a b → r (c * a) (c * b) ∧ r (a * c) (b * c)}

Used by 1

Used byKourovka Problem 17.29 (V. V. Bludov, A. M. W. Glass)

DefinitionKourovka Problem 17.29 (V. V. Bludov, A. M. W. Glass)#✓fully proved

The statement that there is a finitely presented group \(G\) that admits a bi-invariant linear order and has a finite generating family \(g_1, \dots, g_k\) for which the word problem is insoluble: no algorithm decides, given a word in the \(g_i\) and their inverses, whether it equals \(1\) in \(G\).

def finitelyPresentedOrderableInsolubleWordProblem : Prop :=
  ∃ (G : Type) (_ : Group G), Group.IsFinitelyPresented G ∧ (biOrders G).Nonempty ∧
    ∃ (k : ℕ) (gens : Fin k → G), Subgroup.closure (Set.range gens) = ⊤ ∧
      ¬ WordProblemSolvable (FreeGroup.lift gens)

Uses 2 · Used by 1

Statement usesBi-invariant linear orders on a group · Solvable word problem

Used byBludov–Glass: a finitely presented orderable group with insoluble word problem

TheoremBludov–Glass: a finitely presented orderable group with insoluble word problem#●ready to prove

There is a finitely presented group \(G\) that admits a bi-invariant linear order and has a finite generating family \(g_1, \dots, g_k\) for which the word problem is insoluble: no algorithm decides, given a word in the \(g_i\) and their inverses, whether it equals \(1\) in \(G\).

public theorem_wanted finitelyPresentedOrderableInsolubleWordProblem_holds :
    finitelyPresentedOrderableInsolubleWordProblem

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 17.29 (V. V. Bludov, A. M. W. Glass); resolution: V. V. Bludov and A. M. W. Glass, Bull. London Math. Soc. 44 (2012), 85-98, Kourovka Archive, Problem 17.29 (Such a group is constructed).

Uses 1

Statement usesKourovka Problem 17.29 (V. V. Bludov, A. M. W. Glass)

DefinitionRecursively presented group#✓fully proved

Let \(G\) be a group, \(k\) a natural number and \(\varphi\) a homomorphism from the free group on \(k\) generators to \(G\). The group \(G\) is recursively presented with respect to \(\varphi\) when the set of words \(w\) (finite lists of letters \((i, \varepsilon)\) with \(i < k\) and \(\varepsilon\) true or false, the letter \((i, \mathrm{false})\) standing for the inverse of the \(i\)-th generator) with \(\varphi(w) = 1\) in \(G\) is recursively enumerable.

When \(\varphi\) is surjective, this is the same as a presentation of \(G\) on the images of the generators with a recursively enumerable set of relators; it is the enumerable counterpart of a solvable word problem.

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

Used by 1

Used byThe Bludov–Glass question (Kourovka 17.28)

DefinitionRight orders of a group#✓fully proved

The right orders of G: linear orders (as relations) invariant under right multiplication.

def rightOrders (G : Type*) [Group G] : Set (G → G → Prop) :=
  {r | IsLinearOrder G r ∧ ∀ a b c : G, r a b → r (a * c) (b * c)}

Used by 1

Used byThe Bludov–Glass question (Kourovka 17.28)

DefinitionThe Bludov–Glass question (Kourovka 17.28)#✓fully proved

The statement that there exist a soluble group \(G\) that admits a right order, a natural number \(k\) and elements \(g_0, \dots, g_{k-1}\) generating \(G\) such that, for the homomorphism \(\varphi\) from the free group on \(k\) generators to \(G\) sending the \(i\)-th generator to \(g_i\), the group \(G\) is recursively presented with respect to \(\varphi\) and the word problem for \(\varphi\) is not solvable. In words: there is a finitely generated, recursively presented, soluble right-orderable group with insoluble word problem.

def solubleRightOrderableInsolubleWordProblem : Prop :=
  ∃ (G : Type) (_ : Group G), Group.IsSolvable G ∧ (rightOrders G).Nonempty ∧
    ∃ (k : ℕ) (gens : Fin k → G), Subgroup.closure (Set.range gens) = ⊤ ∧
      IsRecursivelyPresented (FreeGroup.lift gens) ∧ ¬ WordProblemSolvable (FreeGroup.lift gens)

Uses 3 · Used by 1

Statement usesRecursively presented group · Right orders of a group · Solvable word problem

Used byA soluble right-orderable group with insoluble word problem (Kourovka 17.28)

TheoremA soluble right-orderable group with insoluble word problem (Kourovka 17.28)#●ready to prove

There exist a soluble group \(G\) that admits a right order, a natural number \(k\) and elements \(g_0, \dots, g_{k-1}\) generating \(G\) such that, for the homomorphism \(\varphi\) from the free group on \(k\) generators to \(G\) sending the \(i\)-th generator to \(g_i\), the group \(G\) is recursively presented with respect to \(\varphi\) and the word problem for \(\varphi\) is not solvable.

Resolved true: Darbinyan constructs a two-generated, recursively presented, bi-orderable (hence right-orderable) soluble group of derived length 3 with undecidable word problem; the Kourovka Archive answers 17.28 "Yes, there is".

public theorem_wanted solubleRightOrderableInsolubleWordProblem_holds :
    solubleRightOrderableInsolubleWordProblem

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 17.28 (V. V. Bludov, A. M. W. Glass); resolution: A. Darbinyan, Computability, orders, and solvable groups, J. Symbolic Logic 85 (2020), 1588-1598 (arXiv:1909.05720), abstract, result (2) (a bi-orderable, two-generated, recursively presented solvable group of derived length 3 with undecidable word problem, answering the question of Bludov and Glass); Kourovka Archive, Problem 17.28 (Yes, there is), https://arxiv.org/abs/1909.05720.

Uses 1

Statement usesThe Bludov–Glass question (Kourovka 17.28)

5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.