KRF.ksigma_isKB

Proved

KRF.ksigma_isKB

by jario · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Example 2 of arXiv 2412.11855: logic-induced pair classes are knowledge bases (with the Sigma renaming-closure side condition from the faithfulness audit).

Preamble

import Definitions.Def_KRF_Data
import Definitions.Def_KRF_Machinery
import Definitions.Def_KRF_RenamingProps
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ σ : Sig}

Formal statement

theorem KRF.ksigma_isKB {σD σQ σ : Sig} {Q : QueryLanguage σQ}
    (eD : SigEmb σD σ) (eQ : SigEmb σQ σ) (Sigma : Set (Fm σ)) (𝒟 : Set (Database σD))
    (hren : ∀ (τ : Nat → Nat), Function.Injective τ → ∀ ψ, ψ ∈ Sigma → (ψ.rename τ) ∈ Sigma) :
    ∃ K : KB 𝒟 Q, K.mem = KSigma eD eQ Sigma Q :=
  sorry

Source

arXiv 2412.11855v2

View graph