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.
Decision Problems for Finitely Presented Groups - Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Construction of the Natural Numbers
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Decision Problems for Finitely Presented Groups
- Finite Counting, Factorials and Binomial Coefficients
- Free Groups and Presentations
- Group Homomorphisms and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Relations, Functions, and Quotients
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
These examples keep the abstract decision-problem language concrete: free reduction in a free group, coordinate reduction in a cyclic presentation, one free-group conjugacy calculation, one partial coset-enumeration warning, and a small relator-area computation. The counterexample isolates the gap between enumerating positive instances and deciding all instances.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Free reduction decides a word in a free group
Example
In the free group on generators , the word
is nontrivial because its free reduction is .
Facts & Assumptions
Given: The free-group word-problem criterion.
A word in a finitely generated free group is trivial exactly when its free reduction is empty. (The word problem for a finitely generated free group is solvable by free reduction)
Verification
Cancel the adjacent pair in , then cancel the adjacent pair . The resulting reduced word is .
The reduced word is not empty, so [L1] implies that the original word is nontrivial.
The word problem in a finite cyclic presentation
Example
In the cyclic presentation , the word is equal to and therefore is not trivial.
Facts & Assumptions
Given: The word problem is solvable in finitely generated abelian groups.
Every finitely generated abelian group has solvable word problem. (The word problem for finitely generated abelian groups is solvable)
Verification
In the cyclic group of order , exponents are taken modulo , so .
Because , the element is not the identity. This is the abelian coordinate check promised by [L1].
Conjugacy in a free group by cyclic reduction
Example
In the free group on , the cyclically reduced words and are conjugate.
Facts & Assumptions
Given: The conjugacy problem asks whether two words represent conjugate elements.
In a free group, two cyclically reduced words are conjugate if and only if one is a cyclic permutation of the other. (Two cyclically reduced words in a free group are conjugate if and only if one is a cyclic permutation of the other)
Verification
The word is obtained from by moving the initial letter to the end. So it is a cyclic permutation of the first word.
Both words are cyclically reduced, and [L1] therefore makes them conjugate in the free group.
Todd-Coxeter as a partial coset-enumeration procedure
Example
Coset enumeration can certify some negative word-problem instances without thereby giving a uniform solution.
Facts & Assumptions
Given: A fixed finite presentation.
The word problem for a fixed finite presentation asks whether an input word is trivial in the presented group. (The word problem for a fixed finite presentation)
Verification
In a finite quotient obtained from a partial Todd-Coxeter table, if the input word acts nontrivially on some enumerated coset, then the word is certainly nontrivial in the presented group, because every quotient homomorphism preserves equality with the identity.
This shows how a partial enumeration can settle some instances by exhibiting a separating finite quotient. It does not claim that every enumeration terminates or every instance is decided.
Computing an algebraic relator area
Example
In the presentation , the null word has algebraic relator area .
Facts & Assumptions
Given: The relator-area definition for a finite presentation.
The algebraic relator area of a null word is the least number of conjugates of defining relators and their inverses whose product equals that word. (Algebraic relator area and the Dehn function of a finite presentation)
Every null word has a minimal algebraic relator area. (Every null word has a minimal algebraic relator area)
Verification
The word is the product , so [L1] gives .
It is not , because a single conjugate of the only relator or its inverse is just or in this cyclic presentation. Thus [L2] forces the minimum to be exactly .
Enumerating relator consequences does not decide nontriviality
Statement refuted
Enumerating all relator consequences of a recursive presentation decides nontriviality of words in that presentation.
Facts & Assumptions
Given: The recursive presentation and the word .
The trivial words of a recursively presented group form a recursively enumerable language. (The trivial words of a recursively presented group form a recursively enumerable language)
A reduced nonempty word in a free group is nonidentity. (The word problem for a finitely generated free group is solvable by free reduction)
Counterexample
The presentation presents the free group on . The word is reduced and nonempty, so [L2] says that it is nontrivial.
By [L1], enumerating relator consequences lists precisely the trivial words. Since is nontrivial by step 1.1, it never appears, and waiting for it gives no halting certificate of nontriviality.
Hence the asserted decision procedure is false, and the claimed principle is refuted.