Claude compiled a comprehensive notes file in
prove_JCA_undecidable.md, restating the JCAQP definition,
constraints (fixed signature, existence problem), and surveying
candidate undecidable sources (semi-unification, SREU, second-order
unification, PCP). They explored reductions mainly from semi-unification
and from computation/PCP encodings using term-structured traces, then
documented why each path hits expressivity barriers in the pure
equational language over T(F).
Strengths
Clear structure and coverage of multiple candidate source
problems.
Explicit discussion of the “assumption gap” for SREU under
fixed-model semantics.
Concrete worked example for semi-unification, which helps show why a
naive encoding is too strong.
Good articulation of the core obstacle: equational constraints
cannot enforce recursive structure or “for all subpositions”
checks.
Different Tradeoffs
Claude prioritized breadth: surveying multiple undecidable sources
and outlining several partial encodings, trading off depth on any single
reduction.
My approach focused more on formalizing the semantic gap (entailment
in T(F) vs. rigid derivability) and on fixed-signature notes, with less
exploration of PCP/TM encodings.
Ideas Worth Noting
The semi-unification angle might be the most promising among classic
undecidable problems because it is closer to pure unification/matching
than SREU.
The trace-encoding attempt underlines a key constraint: without
pattern matching or recursive predicates, verifying “all steps” seems
infeasible—this could be formalized as a limitation lemma.
Questions
Did you find any specific semi-unification variant (e.g., one-step
semi-unification or a restricted fragment) that seems closer to
expressible in JCAQP?
Would it help to formalize an impossibility result for expressing
“all subterms satisfy property P” using only equations and finite
prefixes, to justify why TM/PCP encodings fail?