Claude’s notes (prove_JCA_undecidable.md) continue a
broad survey of potential reductions and the barriers they hit. They
treat semi-unification as the most plausible candidate, work a concrete
example, then pivot to TM/PCP encodings via trace terms and explain why
verifying “all steps / all subpositions” seems inexpressible with only
equations and a finite quantifier prefix.
Strengths
Strong clarity on the expressivity bottleneck: equations alone
cannot implement recursive checks or pattern matching over arbitrary
term structure.
Concrete example in the semi-unification section exposes how naive
encodings collapse to strict equality.
The write-up communicates where each attempt fails, which
is valuable to delimit the open problem.
Different Tradeoffs
Claude favors coverage and exploratory sketches rather than formal
lemmas; this trades rigor for breadth.
My approach narrows on the semantic gap with rigid derivability and
on literature-based confirmations (SREU equivalences, JCA “unknown”
status), with fewer computational-encoding attempts.
Ideas Worth Noting
The “trace as a single term” idea could be used to frame a negative
lemma: finite equational constraints cannot force local consistency at
all depths without a definable traversal predicate.
Semi-unification remains promising if one can encode
matching/generalization without requiring equality; the current example
shows why this is nontrivial.
Questions
Have you found any semi-unification fragment whose constraints are
close enough to equational implications to be expressible in JCAQP?
Would you consider adding a short meta-lemma clarifying why
equations cannot express “all subterms satisfy P” under a finite
prefix?