Notes on undecidability of Herbrand JCAQP existence (codex)

Scope and problem statement

• Focus: existence problem for JCAQP over the free term algebra.
• Model: \(\mathcal{M} = \mathcal{T}(\mathcal{F})\) with fixed signature \(\mathcal{F}\). We may choose \(\mathcal{F}\) once for the reduction, but it cannot depend on the input instance.
• Instance: a quantifier prefix \(Q\) and a conjunction of implications \(\bigwedge_i (D_i \Rightarrow C_i)\), where each \(D_i, C_i\) is a conjunction of equations (atoms).
• Question: Does there exist an abduced answer \(\exists \bar\beta: A\) (conjunction of equations) meeting the conditions of Def. 4.1 (relevance/validity/consistency/no-escaping) in \(\mathcal{T}(\mathcal{F})\)?

JCAQP conditions (from thesis Section 4.2)

Let \(Q\) quantify all free variables in the instance. An answer \(\exists\bar\beta: A\) (conjunction of equations) must satisfy:

1. Relevance: \(\mathcal{T}(\mathcal{F}) \models \bigwedge_i (D_i \land A \Rightarrow C_i)\).
2. Validity (prefix): \(\mathcal{T}(\mathcal{F}) \models Q: A[\bar\chi\ \bar\delta := \bar t]\) for some instantiation of parameters.
3. Consistency: for all \(i\), \(\mathcal{T}(\mathcal{F}) \models \exists\,\mathrm{FV}(D_i \land A).\; D_i \land A\).
4. No escaping variables: dependency constraints enforced by \(Q\) (including the strong variant when solved forms are substitutions).

Jointness matters (Maher Example 12)

Maher shows a simple JCA instance whose set of answers cannot be captured by any single

SCA instance (even over Herbrand constraints). This indicates that jointness is a genuine source of complexity and cannot be eliminated by “solve each implication separately and conjoin.”

Complexity note (Maher–Huang)

For SCA over Herbrand constraints, recognizing maximally general or fully maximal answers is co-NP complete, even though checking that a candidate is an answer is easy (linear-time unification). This suggests that even the shape of the answer space is algorithmically hard to control, which partly explains why JCA/JCAQP decision status remains open.

Key semantic constraints in \(\mathcal{T}(\mathcal{F})\)

• Equality is syntactic identity of ground terms.
• A conjunction of equations is satisfiable iff it unifies (i.e., has a substitution that makes all equations syntactically identical).
• The consistency condition is nontrivial: it prevents the common “vacuous implication” trick where \(D_i \land A\) is inconsistent.

Fixed-signature note

• If a reduction source uses arbitrary function symbols, it can usually be encoded over a fixed signature (e.g., constants plus a binary constructor node(tag, args) or pair) by encoding symbols as ground terms (strings over a fixed alphabet). This removes the “growing signature” concern.
• So the fixed signature restriction is not the main obstacle, as long as the target problem admits such encodings.

Reminder: what SREU actually asks for (rigid E-unification)

From standard definitions (e.g., the MSR/Veanes survey), a rigid equation is written E |- s ≈ t with E a finite set of equations. An SREU instance is a finite set { E_i |- s_i ≈ t_i }_i. A substitution θ is a solution if:

1. E_i θ and (s_i ≈ t_i) θ are ground, and
2. E_i θ entails s_i θ ≈ t_i θ in equational logic (i.e., s_i θ and t_i θ are in the congruence closure generated by the ground equations E_i θ).

Thus SREU relies on derivability under axioms (ground equations as rewrite/congruence axioms), not on truth in the free term algebra.

Lemma: entailment by equations in the free term algebra

Let D be a conjunction of equations in the free term algebra. If D is satisfiable and σ is an mgu of D, then for any terms s,t:

• T(F) |= D -> (s ≈ t) iff sσ and tσ are syntactically identical.

So entailment in the free term algebra collapses to unification w.r.t. D; it does not

use D as rewrite axioms in the sense of equational logic with a quotient.

Attempt 1: Reduction from SREU (rigid E-unification)

Attempt 2: Internalize rigid derivability

Idea: add equations to encode a “proof object” witnessing that \(s_i\theta\) rewrites to \(t_i\theta\) using equations in \(E_i\theta\).

Obstacle:

• The constraint language is only equations in the free term algebra. There is no predicate or built-in interpretation of “derives” or “rewrites”.
• Adding symbols like step or proof does not help: in \(\mathcal{T}(\mathcal{F})\), they are uninterpreted constructors, so equations cannot enforce the semantics of rewriting.

Conclusion: encoding derivability requires extending the language/model beyond pure Herbrand equations. That leaves the JCAQP setting.

Attempt 3: Encode computation history as a term

Idea: let the abduced answer \(A\) assert the existence of a term encoding a full computation (e.g., a list of configurations). Use implication constraints to enforce local transitions.

Obstacle:

• With only equations, there is no way to quantify over all adjacent pairs in a list and enforce “valid transition” properties.
• Any finite set of equations can only constrain finitely many positions; it cannot enforce correctness for an unbounded-length witness.

Conclusion: the equational language is too weak to express “every adjacent pair is a valid step” without additional predicates or axioms.

Attempt 4: Reduce from (semi-)unification / higher-order unification

Idea: view abduced \(A\) as an unknown conjunction of equations, i.e., a partial substitution, and encode a known undecidable unification-style problem.

Issues:

• Second-order unification needs function variables. A first-order variable in \(\mathcal{T}(\mathcal{F})\) cannot be “applied” to arguments, and there is no encoding of application semantics in pure equations.
• Semi-unification (if used) requires encoding “instance” constraints; but using only equations and a single global unknown \(A\), this collapses to unification-like constraints, which are decidable in the Herbrand setting.

Conclusion: I do not yet see a faithful encoding of second-order or semi-unification into JCAQP with only equations.

Provisional assessment

• Main obstruction: SREU-style hardness uses rigid derivability under assumptions, but JCAQP uses truth in the fixed free term algebra plus consistency (nonvacuity).
• Any reduction must ensure all premises are satisfiable in \(\mathcal{T}(\mathcal{F})\), ruling out the usual rigid-equality trick.
• The quantifier prefix does give dependency control, but I do not yet see a way to encode an undecidable problem while keeping all premises satisfiable and the constraint language purely equational.

Possible decidability angle (speculative)

If the answer \(A\) fully pins down variables via equations (i.e., encodes a substitution), then each implication \(D_i \land A \Rightarrow C_i\) becomes “ground-truth”:

either \(D_i \land A\) is inconsistent or, when consistent, the fixed substitution makes \(C_i\) syntactically true. This suggests a (very rough) idea that existence of A

could reduce to checking whether there is a substitution compatible with all implications and with the dependency/no-escaping constraints. That looks closer to unification with dependency restrictions than to classic rigid-derivability problems.

However:

• the no-escaping condition prevents \(A\) from freely fixing universal variables;
• the existence of one “global substitution” is far stronger than needed (and may fail even when answers exist);
• the jointness across implications can force \(A\) to be a partial substitution only, which is harder to characterize.

I do not have a precise reduction either way; this is only a possible route if one tries to prove decidability rather than undecidability.

No-escaping as “definable functions” (speculative)

With a prefix like \(\forall x.\exists y\), an equation in \(A\) of the form y = t(x, p̄) makes \(y\) a definable function of \(x\) (with parameters \(p̄\)). This resembles higher-order unification where function variables are restricted to first-order definable functions (a.k.a. context terms / patterns).

If JCAQP effectively only allows such “pattern” dependencies, the problem could be closer to higher-order pattern unification (decidable) rather than full second-order unification (undecidable). This is not a proof, but it suggests that undecidability is not automatic even with quantifier alternation.

Limitation heuristic: finite equations cannot enforce “all positions”

In the free term algebra, a satisfiable conjunction of equations \(E\) induces a single most general unifier \(\sigma\) (up to renaming). Entailment reduces to checking syntactic identity after \(\sigma\). Thus any implication of the form \(E \Rightarrow s \approx t\) can only constrain finitely many positions—those reachable through the finitely many equations in \(E\) and the two terms \(s,t\).

This suggests a meta-lemma: there is no way, using only finitely many equations, to enforce a local “transition” property at every depth of a recursively nested term, because every such enforcement would require a definable traversal/predicate not present in pure equational logic.

This is not formalized, but it explains why the TM/PCP “trace term” idea repeatedly stalls.

Open directions to try next (if time)

1. Look for a known undecidable synthesis problem where premises are always unifiable and the only hardness comes from the existence of a suitable conjunction of equations (i.e., a structured substitution).
2. Explore whether rigid reachability or similar problems can be encoded by introducing a definable derivability relation inside the term algebra (likely requires a richer language than pure equations).
3. Investigate if the no-escaping-variables condition (dependency restriction) can be used to simulate second-order unification more faithfully by treating dependent existential variables as “function variables.”