KRF.kb_logic_impl

/-
Proposition (prop:kb_logic_impl; full appendix proof): every KB is logically
implementable — for the CWA-set σ there is a set Σ of FO-sentences whose
UNA-circumscriptive minimal models of D ∪ Σ answer exactly K. Along with the
supporting apparatus of the appendix: UNA-structures, the ⊆_σ order and the
minimal-model class Mod^u_m.
-/
import Definitions.Def_KRF_Machinery

noncomputable section

open KRFCore
open KRFCore.FStruct

namespace KRF

variable {σD σQ σ : Sig}

/-- UNA-structure: distinct constants are interpreted distinctly. -/
def UNAStruct (A : FStruct σ) : Prop := Function.Injective A.ctm

/-- The paper's order A ⊆_{υ_c} B: same domain, CWA-predicates shrink, all
other (OWA-)predicates are unchanged, constants agree. -/
def StructLeq (eD : SigEmb σD σ) (A B : FStruct σ) : Prop :=
  ∃ hD : A.Dom = B.Dom,
    (∀ p, σD.cwa p → (σ.arity p).isSome →
      ∀ xs : Fin ((σ.arity p).getD 0) → A.Dom,
        A.rel p xs →
          let ys : Fin ((σ.arity p).getD 0) → B.Dom := fun i => hD ▸ xs i
          B.rel p ys) ∧
    (∀ p, ¬ σD.cwa p → (σ.arity p).isSome →
      ∀ xs : Fin ((σ.arity p).getD 0) → A.Dom,
        A.rel p xs ↔
          let ys : Fin ((σ.arity p).getD 0) → B.Dom := fun i => hD ▸ xs i
          B.rel p ys)

/-- Mod^u_m(D,Σ,σ_c): UNA-structures that are ⊆_σ-minimal models of D and Σ
(with σ_c = the CWA-predicates of σ_D, matching the paper's definition). -/
def MinModels (eD : SigEmb σD σ) (Sigma : Set (Fm σ)) (D : PreDatabase σD) : Set (FStruct σ) :=
  { A | UNAStruct A ∧ SatDB eD A D ∧ (∀ ψ, ψ ∈ Sigma → A.Satisfies ψ) ∧
        ∀ B, UNAStruct B → SatDB eD B D → (∀ ψ, ψ ∈ Sigma → B.Satisfies ψ) →
          StructLeq eD B A → StructLeq eD A B }

theorem kb_logic_impl {Q : QueryLanguage σQ} (K : KB (𝒟 := DBAll σD) Q) (eD : SigEmb σD σ) (eQ : SigEmb σQ σ) :
    ∃ Sigma : Set (Fm σ), ∀ (D : Database σD) (φ : Fm σQ),
      (∀ A, A ∈ MinModels eD Sigma (D : PreDatabase σD) → A.Satisfies (eQ.embFm φ)) ↔ K.mem D φ := by
  sorry

end KRF