KRF.compactness_UNA

/-
Theorem (thm:compactness_una; appendix): compactness for UA-entailment — if
Σ entails φ over all UNA-structures then some finite Σ₀ ⊆ Σ already does.
Stub (ultraproduct infrastructure out of scope for this stage).
-/
import Definitions.Def_KRF_Machinery

noncomputable section

open KRFCore
open KRFCore.FStruct

namespace KRF

variable {σ : Sig}

def EntailsUNA (Sigma : Set (Fm σ)) (φ : Fm σ) : Prop :=
  ∀ A : FStruct σ, Function.Injective A.ctm →
    (∀ ψ, ψ ∈ Sigma → A.Satisfies ψ) → A.Satisfies φ

theorem compactness_UNA (Sigma : Set (Fm σ)) (φ : Fm σ) :
    EntailsUNA Sigma φ → ∃ S0 : Set (Fm σ), S0 ⊆ Sigma ∧ Set.Finite S0 ∧ EntailsUNA S0 φ := by
  sorry

end KRF