Pointwise checkability prevents universal KRFs under computable reductions
ProvedKRF.not_universal_of_pointwise_checkabilityIn the current KRF interface, a theory family has a decidable domain of natural-number codes, and each theory separately admits a partial recursive question-answering procedure. The interface does not require one procedure that accepts the theory code as part of its input. A reduction between families must be a single computable map on theory codes.
For arbitrary database and query signatures, every such family Γ fails to be universal:
Equivalently, for every candidate family there exists another family satisfying the same interface that has no computable reduction into it. This identifies an obstruction in the formal interface and supplies a reusable diagnostic for the canonical-family targets. It makes no claim against the source paper, whose Definition 5 requires joint effective checkability in the theory code, database, and query.
Formalization Note The statement refers to the current published Krf, Checkable, Reduction, and Universal definitions in Def_KRF_Machinery.
import Definitions.Def_KRF_Machinery
theorem KRF.not_universal_of_pointwise_checkability {σD σQ : KRFCore.Sig}
{Q : KRF.QueryLanguage σQ} (Γ : KRF.Krf σD σQ Q) :
¬ KRF.Universal Γ := by sorry