LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The trivial words of a recursively presented group form a recursively enumerable language

Statement

Let $⟨ X ∣ R ⟩$ be a recursive presentation. Then the language of words on $X ⊔ X^{- 1}$ that represent the identity in the presented group is recursively enumerable.

Facts & Assumptions

Given: A recursive presentation $⟨ X ∣ R ⟩$ and a word $w$ on $X ⊔ X^{- 1}$ .

[L1]

In a presentation $⟨ X ∣ R ⟩$ , a word represents the identity exactly when it lies in the normal closure of $R$ inside the free group on $X$ . (In $⟨ X ∣ R ⟩$ , the words $u$ and $v$ represent the same element if and only if $u^{- 1} v \in ⟨ ⁣ ⟨ R ⟩ ⁣ ⟩$ )

[L2]

The normal closure of $R$ is the set of finite products of conjugates of elements of $R$ and their inverses. (The normal closure of $R$ is the set of finite products of conjugates of elements of $R$ and their inverses)

Proof

technique · direct

1.1

Because the relator language of the recursive presentation is recursively enumerable, there is a procedure that lists all relator words in $R$ and hence also all pairs $(r, ε)$ with $r \in R$ and $ε \in {1, - 1}$ . By dovetailing over lengths, one can therefore enumerate all finite lists of conjugators and signed relators.

givenL2

2.1

First freely reduce the input word $w$ to a reduced word $\overline{w}$ . For each finite list from step 1.1, form the corresponding product of conjugates from [L2] and freely reduce it in the ambient free group. Whenever the result is $\overline{w}$ , accept. If $w$ is trivial in the presented group, then [L1] and [L2] supply a relator expression representing the same free-group element as $w$ , so its free reduction is $\overline{w}$ and the search eventually halts; if $w$ is nontrivial, the search may run forever.

L1L2step 1.1

3.1

Hence the trivial words are exactly the words on which this procedure halts, so they form a recursively enumerable language.

step 2.1algebra∎

Depends on

Used by

Enumerating relator consequences does not decide nontriviality Counterexample
FALSE: recursively enumerable trivial words already give a decision algorithm False statement

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Charles F. Miller III, Decision Problems for Groups - Survey and Reflections (standard reference, not scraped)