A Threshold Theorem for Implication Decidability

The implication problem asks, for a set of constraints Σ and a target constraint/sentence σ, whether Σ |= σ, i.e. whether every structure satisfying Σ also satisfies σ. Implication is undecidable for general embedded dependencies; thus any positive result must identify an exact boundary between (i) expressive regimes that already subsume classical undecidable benchmarks and (ii) weak regimes where no nontrivial universal information is visible from purely existential (witness) assumptions. We study a family of guarded implication problems with existential inputs over a directed-edge schema. The premises are finite sets P of Boolean conjunctive queries (BCQs), i.e. existential conjunctive sentences, over a ternary edge relation Seg(x, y, a) with a distinguished label constant 0. The language is multi-sorted, with a value sort Val whose function symbols (·, −1, 1) satisfy the first-order axioms of abelian groups; models range over all abelian groups interpreting these symbols. The database schema contains binary relations Mul(a, v) and Pot(x, p) intended to be total functional maps (enforced by key EGDs and mild totality TGDs) from labels and vertices to values. The fixed transfer constraint states that along every edge, potentials multiply by the label’s multiplier. The implication queries are universal equalities in the value sort guarded by a CQ-view expressing that a tuple of labels co-occurs within a single witness of a fixed template CQ. An exact three-way boundary is obtained. If the constraint set is allowed to vary with the input and to impose global coupling (e.g. functional and injective constraints on Mul together with totality on active labels), then implication subsumes classical embedded-dependency implication and is undecidable. For the fixed transfer theory Ttr, if co-occurrence guards are replaced by unary label occurrence and consequences are evaluated on the Mul/Occ view, then (assuming satisfiable premises) no universal multiplier equation is forced beyond the identities of abelian groups together with the normalization Mul(0, 1). At the threshold—a fixed transfer constraint set and CQ co-occurrence guards—guarded monomial implication is decidable and admits an exact compilation to integer linear algebra: each template θ yields a computable subgroup Hθ ≤ Zn generated by closed-walk exponent vectors in the template join graph, and (in the satisfiable, non-vacuous case) entailment holds exactly when α − β ∈ Hθ .