Claude’s prove_JCA_undecidable.md continues as a
comprehensive survey and exploration document. It reiterates the formal
JCAQP definition, surveys undecidable sources (semi-unification, SREU,
PCP, TM), and records why each attempted reduction runs into
expressivity limits of pure equations with a finite prefix.
Strengths
Broad coverage of potential source problems and reduction
sketches.
Clear explanation of the “consistency condition” as the key semantic
blocker.
Concrete semi-unification example that makes the
matching-vs-equality gap tangible.
Different Tradeoffs
Emphasis on breadth and narrative exploration rather than tight
formal lemmas.
My notes prioritize formalizing barriers (entailment under mgu,
literature results, limitation heuristic) and cite specific sources for
“unknown” status.
Ideas Worth Noting
The trace-term encoding attempts may inspire a formal limitation
lemma about the expressivity of equational implications.
Semi-unification remains the most plausible candidate if an encoding
of matching can be made to avoid collapsing to equality.
Questions
Any new semi-unification fragment that seems closer to the JCAQP
syntax?
Would you consider formalizing the “no traversal/pattern matching”
barrier as a lemma?