Alphabeta MathBoone Machine Simulation and Fixed-Presentation Undecidability
About this page
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.
✓ 2 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Combinatorics
Computability Theory
Real Analysis
2 · Logical flowchart
3 · Items
Lemma
Normalized fixed halting machine for boone simulation
Definition
Boone machine semigroup and augmented configurations
Lemma
Boone semigroup histories detect halting
Theorem
Fixed finite semigroup has undecidable terminal equality
Definition
Boone group presentation and special word
Lemma
Boone base groups and associated free bases
Lemma
Boone hnn tower and auxiliary subgroups
Lemma
Boone positive history pushing
Lemma
Boone commutator extracts an auxiliary history
Lemma
Boone reduced auxiliary words have no rule pinches
Lemma
Boone positive history reconstruction
Theorem
Boone special word equivalence
Theorem
Novikov boone undecidability of the word problem
False statement
FALSE: every finitely presented group has solvable word problem
False statement
FALSE: an unsolvable word problem means no individual word can be decided
False statement
FALSE: the Novikov-Boone theorem proves only the uniform problem is unsolvable
Sources
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.420–425, definitions of quadruple/basic move, Exercise 12.11
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.426–427, associated semigroup presentation
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.427–428, Lemmas 12.3–12.4 (corrected augmented invariant)
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.428–430, Theorem 12.5 and Corollary 12.6
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.430–431, sharp notation and Boone presentation
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.438–440, Lemma 12.11 and Corollary 12.12 (corrected free factor)
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.438–440, Lemma 12.11
- Stephen G. Simpson, A Slick Proof, Definition 1, p.1 (independent HNN convention cross-check)
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.432–433, Lemma 12.10 and sufficiency proof
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.440–441, Lemma 12.13
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.442–444, Lemma 12.14 and reduced-length comparison
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, pp.443–447, Lemma 12.15
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, p.431, Lemma 12.7; pp.432–447, both proof directions
- Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, p.431, Theorem 12.8
- Stephen G. Simpson, A Slick Proof, Theorem 8, p.4 (independent fixed-presentation quantifier cross-check)
- Charles F. Miller III, Decision Problems for Groups - Survey and Reflections