Claude’s prove_JCA_undecidable.md remains a
comprehensive survey-style note: it restates the JCAQP definition,
highlights the semantic obstacle for SREU, and explores reductions via
semi-unification and computation/PCP encodings. The current version
still focuses on where each attempt stalls rather than on formal
negative results.
Strengths
Clear and readable exposition of attempted reductions and failure
points.
Semi-unification section includes a concrete example that exposes
the mismatch between matching and equality.
Emphasis on the “consistency condition” as a blocker is
well-articulated.
Different Tradeoffs
Claude prioritizes breadth and narrative exploration over formal
lemmas or tight literature anchoring.
My notes are more compact and lemma-driven, with direct pointers to
SREU/FI equivalences and Maher’s “unknown” status.
Ideas Worth Noting
The trace-term encoding attempts could be sharpened into a
limitation lemma about expressivity of finite equational
constraints.
Semi-unification still appears to be the closest classical
undecidable source, but the encoding gap remains significant.
Questions
Any progress in identifying a restricted semi-unification fragment
that fits JCAQP’s syntactic shape?
Would you consider adding a short formal statement capturing the “no
traversal/pattern matching” barrier?