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.
Solvability of the word problem does not depend on the chosen finite generating set
Statement
Let and be finite presentations of isomorphic groups. Then the word problem is solvable for if and only if it is solvable for .
Facts & Assumptions
Given: Finite presentations and that present isomorphic groups.
Two finite presentations present isomorphic groups if and only if a finite sequence of Tietze transformations and inverses connects them. (Two finite presentations define isomorphic groups if and only if a finite sequence of Tietze transformations and inverses connects them)
In a presentation, equality of represented elements is equivalent to membership of the difference word in the normal closure of the relators. (In , the words and represent the same element if and only if )
Proof
By [L1], it is enough to show that each single Tietze transformation preserves solvability of the word problem.
A relator-addition or relator-deletion Tietze move does not change which words are trivial in the presented group, by the equality criterion [L2]. So the same decision procedure works before and after such a move.
A generator-addition move introduces one new generator together with a defining word . To decide whether a word in the enlarged alphabet is trivial, replace each by and run the original algorithm on the resulting word. The inverse generator-deletion move is the same transport in the opposite direction.
Every finite Tietze chain transports a decision procedure step by step, so solvability for is equivalent to solvability for .
Depends on
- The word problem for a fixed finite presentation
- In $\langle X\mid R\rangle$, the words $u$ and $v$ represent the same element if and only if $u^{-1}v\in\langle\!\langle R\rangle\!\rangle$
- Two finite presentations define isomorphic groups if and only if a finite sequence of Tietze transformations and inverses connects them
Used by
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)