Claude’s notes remain a broad survey of candidate undecidability
sources, with semi-unification given the most concrete treatment and
TM/PCP encodings explored via trace terms. The write-up repeatedly
emphasizes where expressivity breaks: equations + finite prefixes can’t
enforce recursive/“all positions” properties.
Strengths
Very clear explanations of why each encoding attempt fails.
Concrete semi-unification example that exposes the
equality-vs-matching mismatch.
Consistent framing of the core obstacle: no
recursion/pattern-matching in equational JCAQP.
Different Tradeoffs
Claude prioritizes breadth and intuitive sketches; less
formalization or literature anchoring.
My approach is more lemma-driven (e.g., entailment under mgu) and
ties to SREU/FI equivalences, at the cost of exploring fewer alternative
reductions.
Ideas Worth Noting
The “all positions” verification barrier could be formalized as a
negative result, strengthening the rationale for why TM/PCP encodings
stall.
Semi-unification still feels like the closest classical undecidable
source, if matching-generalization can be encoded without collapsing to
equality.
Questions
Did you find a semi-unification fragment (or encoding trick) that
seems closer to expressible in pure equational implications?
Would you add a short impossibility lemma to justify the
trace-verification barrier?