feat(ModelThoery): add exClosure definition for first-order formulas

Author: NoneMore

Mathlib/ModelTheory/Semantics.lean

@@ -902,6 +902,47 @@ theorem realize_iExsUnique [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α →
 
 end BoundedFormula
 
+namespace Formula
+
+@[simp]
+theorem realize_exClosure [DecidableEq α] (φ : L.Formula α) :
+    φ.exClosure.Realize M ↔
+      ∃ v : φ.freeVarFinset → M, Formula.Realize (φ.restrictFreeVar id) v := by
+  simp [Sentence.Realize, Formula.exClosure, Formula.realize_iExs]
+
+theorem realize_exClosure_of_realize_equivSentence [DecidableEq α] [L[[α]].Structure M]
+    [(L.lhomWithConstants α).IsExpansionOn M] {φ : L.Formula α}
+    (h : (Formula.equivSentence φ).Realize M) : φ.exClosure.Realize M := by
+  rw [Formula.realize_exClosure]
+  exists fun a => (L.con (a : α) : M)
+  apply (BoundedFormula.realize_restrictFreeVar'
+    (s := (φ.freeVarFinset : Set α)) Set.Subset.rfl
+    (v := fun a => (L.con a : M))).2
+  exact (φ.realize_equivSentence M).1 h
+
+theorem exists_realize_equivSentence_of_realize_exClosure [DecidableEq α] [Nonempty M]
+    {φ : L.Formula α} (h : φ.exClosure.Realize (M := M)) :
+    ∃ v : α → M,
+      @Sentence.Realize _ M (@Language.withConstantsStructure L M _ α (constantsOn.structure v))
+        (Formula.equivSentence φ) := by
+  classical
+  obtain ⟨v, hv⟩ := (φ.realize_exClosure (M := M)).1 h
+  let v' : α → M := fun a =>
+    if hmem : a ∈ φ.freeVarFinset then v ⟨a, hmem⟩ else Classical.choice inferInstance
+  exists v'
+  have hvEq : v' ∘ (↑) = v := by aesop
+  have hv' : Formula.Realize (φ.restrictFreeVar id) (v' ∘ (↑)) := by
+    simp_all only [realize_exClosure]
+  have hφ : φ.Realize v' := by
+    apply
+      (BoundedFormula.realize_restrictFreeVar' (s := (φ.freeVarFinset : Set α))
+        Set.Subset.rfl).1
+    simpa [Set.inclusion_eq_id] using hv'
+  exact
+    (Formula.realize_equivSentence_symm M (Formula.equivSentence φ) v').1 (by simpa)
+
+end Formula
+
 namespace StrongHomClass
 
 variable {F : Type*} [EquivLike F M N] [StrongHomClass L F M N] (g : F)

Mathlib/ModelTheory/Syntax.lean

@@ -784,6 +784,12 @@ noncomputable def iExsUnique [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formul
     ((φ.relabel (fun a => Sum.elim (.inl ∘ .inl) .inr a)).imp <|
       .iInf fun g => Term.equal (var (.inr g)) (var (.inl (.inr g))))
 
+variable [DecidableEq α] in
+/-- `exClosure φ` is the sentence asserting that there exist values for all free variables of `φ`
+such that `φ` holds. -/
+noncomputable def exClosure (φ : L.Formula α) : L.Sentence :=
+  iExs φ.freeVarFinset (Formula.relabel Sum.inr (φ.restrictFreeVar id))
+
 /-- The biimplication between formulas, as a formula. -/
 protected nonrec abbrev iff (φ ψ : L.Formula α) : L.Formula α :=
   φ.iff ψ