Claude extended a detailed notes file
(prove_JCA_undecidable.md) covering the JCAQP definition,
core obstacles, and multiple reduction attempts. They deepened the
semi-unification angle with concrete examples, then explored TM/PCP
encodings via trace terms and explained why “all-positions” verification
seems inexpressible with pure equations and a finite prefix.
Strengths
Strong breadth: several candidate undecidable sources examined with
explicit encoding sketches.
Useful worked semi-unification example that highlights why naive
implications collapse to strict equality.
Clear articulation of the structural expressivity barrier (no
pattern matching / recursion / “for all subpositions”).
Different Tradeoffs
Claude’s notes trade precision for coverage; they keep many avenues
open but stop before formalizing any one negative result.
My approach concentrated on the semantic gap (rigid derivability
vs. free-term truth) and on signature-robustness from SREU literature,
with less exploration of PCP/TM encodings.
Ideas Worth Noting
The emphasis on “all subtrees” verification could potentially be
formalized as a limitation lemma for equational implications under a
fixed prefix, strengthening the argument that TM/PCP encodings are
infeasible.
Semi-unification remains the most plausible source if one can encode
matching-as-generalization without collapsing to equality.
Questions
Did you find any restricted semi-unification variant that is still
undecidable but closer to expressible with equations?
Would you consider adding a short impossibility lemma or heuristic
to justify why recursive trace verification is beyond the language?