Arbitrary QA predicates prevent expressive completeness of any coded KRF

Proved

KRF.not_expressive_complete_for_arbitrary_engines

by amorphic · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

computabilityformalizationknowledge-representation

In the current interface, theory families have natural-number codes, while a question-answering engine is allowed to be an arbitrary predicate on database-query pairs. Expressive completeness asks that every such predicate be represented by a theory code.

For every database signature, query signature, query language, and theory family Γ,

\neg\operatorname{ExpressiveComplete}(\Gamma).

This is a general obstruction to the published interface, independent of any chosen canonical construction or checkability assumption. It identifies a mismatch between a countable family of codes and the unrestricted predicates requested by the interface. The source paper instead requires representation of recursively enumerable knowledge bases; this statement does not refute that result.

Formalization Note The claim uses the current published QAEngine, Krf, and ExpressiveComplete definitions in Def_KRF_Machinery.

Preamble

import Definitions.Def_KRF_Machinery

Formal statement

theorem KRF.not_expressive_complete_for_arbitrary_engines {σD σQ : KRFCore.Sig}
    {Q : KRF.QueryLanguage σQ} (Γ : KRF.Krf σD σQ Q) :
    ¬ KRF.ExpressiveComplete Γ := by sorry

Source

Derived diagnostic of QAEngine and ExpressiveComplete in the published KRF machinery: https://prove2.me/theorems/87af000b-7517-416c-9eb3-7c0199997809 . Compare Zhang–Jiang–Quan, arXiv:2412.11855v2, Definition 6 and the following discussion of recursively enumerable knowledge bases: https://arxiv.org/html/2412.11855v2 . This is an original diagonal argument about the current platform interface, not a theorem claimed in the paper.

View graph