Classical model theory for the NE-free fragment of QBSML

[AvO23] Proposition 4.1 composed with the standard translation (Logic/Modal/FirstOrder/Correspondence.lean): NE-free QBSML support at a singleton state is mathlib Formula.Realize over the correspondence structure (support_singleton_iff_st), support forces the closed translation as a sentence and conversely (models_toSentence_of_support, exists_support_of_models_toSentence), and mathlib's first-order compactness transfers to finite team satisfiability (support_compactness).

Proposition 4.1, composed: QBSML support is first-order realization

theorem QBSML.support_singleton_iff_st {W : Type u_1} {Var : Type u_2} {Const : Type u_3} {Pred : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] [Inhabited Domain] (M : Model W Domain Const Pred) {φ : Formula Var Const Pred} {τ : (FirstOrder.Language.monadicWithConstants Const Pred).ModalFormula Var} {k : ℕ} (hτ : φ.toModal? = some τ) {i : Index W Var Domain} {v : Var → Domain} (u : ℕ → W) (hv : ∀ (y : Var), i.assign y = some (v y)) (hu : u k = i.world) : support M φ {i} ↔ (FirstOrder.Language.ModalFormula.st k τ).Realize (FirstOrder.Language.stVal v u)

NE-free QBSML support is single-structure first-order satisfaction: [AvO23] Proposition 4.1 composed with the standard translation. Support at a singleton state is mathlib Formula.Realize of the standard translation over M.correspondence — the link along which classical model theory (compactness, Löwenheim–Skolem) transfers to the NE-free fragment.

theorem QBSML.models_toSentence_of_support {W : Type u_1} {Var : Type u_2} {Const : Type u_3} {Pred : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] [Inhabited Domain] (M : Model W Domain Const Pred) {φ : Formula Var Const Pred} {τ : (FirstOrder.Language.monadicWithConstants Const Pred).ModalFormula Var} (hτ : φ.toModal? = some τ) (hcl : FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 τ)) = ∅) {i : Index W Var Domain} {v : Var → Domain} (hv : ∀ (y : Var), i.assign y = some (v y)) (hsupp : support M φ {i}) : (W ⊕ Domain) ⊨ (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 τ)).toSentence hcl

Support at a singleton state forces the closed standard translation, as a sentence of M.correspondence.

theorem QBSML.exists_support_of_models_toSentence {W : Type u_1} {Var : Type u_2} {Const : Type u_3} {Pred : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] [Inhabited Domain] (M : Model W Domain Const Pred) {φ : Formula Var Const Pred} {τ : (FirstOrder.Language.monadicWithConstants Const Pred).ModalFormula Var} (hτ : φ.toModal? = some τ) (hcl : FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 τ)) = ∅) (h : (W ⊕ Domain) ⊨ (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 τ)).toSentence hcl) : ∃ (i : Index W Var Domain) (v : Var → Domain), (∀ (y : Var), i.assign y = some (v y)) ∧ support M φ {i}

Conversely, the closed standard translation as a sentence of M.correspondence yields support at some singleton state.

Compactness for the NE-free fragment

theorem QBSML.support_compactness {Var : Type u_6} [DecidableEq Var] [Fintype Var] {Const : Type u} {Pred : Type v} {ι : Type u_7} {φs : ι → Formula Var Const Pred} {τs : ι → (FirstOrder.Language.monadicWithConstants Const Pred).ModalFormula Var} (hτ : ∀ (i : ι), (φs i).toModal? = some (τs i)) (hcl : ∀ (i : ι), FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 (τs i))) = ∅) (hfin : ∀ (s : Finset ι), ∃ (W : Type (max u v)) (Domain : Type (max u v)) (x : DecidableEq W) (x_1 : DecidableEq Domain) (x_2 : Fintype Domain) (x_3 : Inhabited Domain) (M : Model W Domain Const Pred) (i : Index W Var Domain) (v : Var → Domain), (∀ (y : Var), i.assign y = some (v y)) ∧ ∀ j ∈ s, support M (φs j) {i}) : FirstOrder.Language.Theory.IsSatisfiable (Set.range fun (i : ι) => (FirstOrder.Language.stClose 0 (FirstOrder.Language.ModalFormula.st 0 (τs i))).toSentence ⋯)

Compactness transfer for NE-free QBSML ([AvO23] Proposition 4.1, the standard translation, and mathlib's Theory.isSatisfiable_iff_isFinitelySatisfiable): if every finite subfamily of a family of NE-free formulas is supported at a singleton state of some model, the family's closed standard translations are jointly satisfiable in a single first-order structure.

The converse recovery of a team model from that structure would need Finset-branching accessibility and a Fintype domain, which an arbitrary first-order structure does not supply, so the transfer is stated one-way. Compactness for team-semantic consequence is proved directly (ultraproducts and saturation, without translation) by [PQ24], who also separate satisfiability- from entailment-compactness in team logics.