From fa17faf510fd082031c8ae095020118d5ed64d7e Mon Sep 17 00:00:00 2001 From: NoneMore Date: Sun, 19 Apr 2026 13:12:57 +0800 Subject: [PATCH] feat(ModelTheory/Definablity): add syntax-to-definability bridge lemmas --- Mathlib/ModelTheory/Definability.lean | 114 ++++++++++++------ .../ModelTheory/ElementarySubstructures.lean | 30 ++--- 2 files changed, 88 insertions(+), 56 deletions(-) diff --git a/Mathlib/ModelTheory/Definability.lean b/Mathlib/ModelTheory/Definability.lean index feeb69a8190509..2452209a76057a 100644 --- a/Mathlib/ModelTheory/Definability.lean +++ b/Mathlib/ModelTheory/Definability.lean @@ -93,35 +93,88 @@ theorem Definable.mono (hAs : A.Definable L s) (hAB : A ⊆ B) : B.Definable L s rw [definable_iff_empty_definable_with_params] at * exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB)) +end Set + +namespace FirstOrder.Language + +open Set + +variable {L : Language.{u, v}} {M : Type w} [L.Structure M] + +variable {A : Set M} {α : Type u₁} + +namespace Formula + +/-- A formula with parameters from `A` defines the set of its realizations. -/ +theorem definable_withConstants (φ : L[[A]].Formula α) : + A.Definable L {v | φ.Realize v} := + ⟨φ, rfl⟩ + +theorem definable (φ : L.Formula α) : + A.Definable L {v | φ.Realize v} := + (empty_definable_iff.mpr ⟨φ, rfl⟩).mono (empty_subset A) + +end Formula + +namespace BoundedFormula + +variable {n : ℕ} + +theorem definable_withConstants (φ : L[[A]].BoundedFormula α n) : + A.Definable L {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)} := by + simpa using φ.toFormula.definable_withConstants + +theorem definable (φ : L.BoundedFormula α n) : + A.Definable L {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)} := by + simpa using φ.toFormula.definable + +theorem definable_boundedSection_withConstants (φ : L[[A]].BoundedFormula Empty n) : + A.Definable L {xs | φ.Realize default xs} := by + convert (φ.toFormula.relabel (Sum.elim Empty.elim id)).definable_withConstants using 1 + ext xs + simp only [Formula.realize_relabel, realize_toFormula] + congr! + +theorem definable_boundedSection (φ : L.BoundedFormula Empty n) : + A.Definable L {xs | φ.Realize default xs} := by + convert (φ.toFormula.relabel (Sum.elim Empty.elim id)).definable + ext xs + simp only [Formula.realize_relabel, realize_toFormula] + congr! + +end BoundedFormula + +end FirstOrder.Language + +namespace Set + +open FirstOrder FirstOrder.Language + +variable {M : Type w} {A : Set M} {L : FirstOrder.Language.{u, v}} [L.Structure M] + +variable {α : Type u₁} {β : Type*} {s : Set (α → M)} + @[simp] theorem definable_empty : A.Definable L (∅ : Set (α → M)) := - ⟨⊥, by - ext - simp⟩ + (⊥ : L[[A]].Formula α).definable_withConstants @[simp] -theorem definable_univ : A.Definable L (univ : Set (α → M)) := - ⟨⊤, by - ext - simp⟩ +theorem definable_univ : A.Definable L (univ : Set (α → M)) := by + simpa using (⊤ : L[[A]].Formula α).definable_withConstants @[simp] theorem Definable.inter {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∩ g) := by rcases hf with ⟨φ, rfl⟩ rcases hg with ⟨θ, rfl⟩ - refine ⟨φ ⊓ θ, ?_⟩ - ext - simp + simpa using (φ ⊓ θ).definable_withConstants @[simp] theorem Definable.union {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∪ g) := by - rcases hf with ⟨φ, hφ⟩ - rcases hg with ⟨θ, hθ⟩ - refine ⟨φ ⊔ θ, ?_⟩ - ext - rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq] + rcases hf with ⟨φ, rfl⟩ + rcases hg with ⟨θ, rfl⟩ + simpa using (φ ⊔ θ).definable_withConstants theorem definable_finset_inf {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) : A.Definable L (s.inf f) := by @@ -161,10 +214,8 @@ theorem definable_iUnion_of_finite {ι : Type*} [Finite ι] {f : ι → Set (α @[simp] theorem Definable.compl {s : Set (α → M)} (hf : A.Definable L s) : A.Definable L sᶜ := by - rcases hf with ⟨φ, hφ⟩ - refine ⟨φ.not, ?_⟩ - ext v - rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not] + rcases hf with ⟨φ, rfl⟩ + simpa using (φ.not).definable_withConstants @[simp] theorem Definable.sdiff {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.Definable L t) : @@ -177,9 +228,7 @@ theorem Definable.sdiff {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.De theorem Definable.preimage_comp (f : α → β) {s : Set (α → M)} (h : A.Definable L s) : A.Definable L ((fun g : β → M => g ∘ f) ⁻¹' s) := by obtain ⟨φ, rfl⟩ := h - refine ⟨φ.relabel f, ?_⟩ - ext - simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel] + simpa using (φ.relabel f).definable_withConstants theorem Definable.image_comp_equiv {s : Set (β → M)} (h : A.Definable L s) (f : α ≃ β) : A.Definable L ((fun g : β → M => g ∘ f) '' s) := by @@ -278,19 +327,15 @@ theorem Definable.image_comp {s : Set (β → M)} (h : A.Definable L s) (f : α lemma Definable.exists_of_finite [Finite β] {S : Set ((α ⊕ β) → M)} (hS : A.Definable L S) : A.Definable L { v : α → M | ∃ u : β → M, Sum.elim v u ∈ S } := by - obtain ⟨φ, hφ⟩ := hS - exists φ.iExs β - ext v - simp [hφ] + obtain ⟨φ, rfl⟩ := hS + simpa using (φ.iExs β).definable_withConstants /-- Finite universal quantifiers preserve definablity. -/ lemma Definable.forall_of_finite [Finite β] {S : Set ((α ⊕ β) → M)} (hS : A.Definable L S) : A.Definable L { v : α → M | ∀ u : β → M, Sum.elim v u ∈ S } := by - obtain ⟨φ, hφ⟩ := hS - exists φ.iAlls β - ext v - simp [hφ] + obtain ⟨φ, rfl⟩ := hS + simpa using (φ.iAlls β).definable_withConstants variable (L A) @@ -478,10 +523,7 @@ theorem definableFun_iff_empty_definableFun_with_params : @[fun_prop] theorem _root_.FirstOrder.Language.Term.definableFun_realize (t : L.Term α) : (∅ : Set M).DefinableFun L (t.realize) := by - rw [empty_definableFun_iff] - refine ⟨(t.relabel some).equal (Term.var none), ?_⟩ - ext v - simp [tupleGraph] + simpa using ((t.relabel some).equal (Term.var none)).definable /-- A function symbol is a definable function. -/ @[fun_prop] @@ -591,9 +633,7 @@ def TermDefinable (f : (α → M) → M) : Prop := theorem TermDefinable.definable_tupleGraph {f : (α → M) → M} (h : A.TermDefinable L f) : A.Definable L f.tupleGraph := by obtain ⟨φ, rfl⟩ := h - use (φ.relabel some).equal (Term.var none) - ext - simp [Function.tupleGraph] + simpa using ((φ.relabel some).equal (Term.var none)).definable_withConstants variable {L} {A B} {f : (α → M) → M} diff --git a/Mathlib/ModelTheory/ElementarySubstructures.lean b/Mathlib/ModelTheory/ElementarySubstructures.lean index 8bd1396a441b9a..7c0b82f6ebe977 100644 --- a/Mathlib/ModelTheory/ElementarySubstructures.lean +++ b/Mathlib/ModelTheory/ElementarySubstructures.lean @@ -159,12 +159,9 @@ theorem closure_eq_self (hA : L.MeetsDefinable A) : closure L A = A := by refine Subset.antisymm ?_ subset_closure rw [coe_closure_eq_range_term_realize] - intro x hx - have : A.Definable₁ L {x} := by - obtain ⟨t, rfl⟩ := hx - use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants - simp [Set.ext_iff] - exact singleton_inter_nonempty.mp <| hA _ (singleton_nonempty x) this + rintro x ⟨t, rfl⟩ + exact singleton_inter_nonempty.mp <| hA _ (singleton_nonempty _) <| + by simpa using ((Term.var 0).equal (t.relabel Sum.inl).varsToConstants).definable_withConstants /-- The closure of a set meeting definable sets is an elementary substructure. -/ theorem isElementary_closure (hA : L.MeetsDefinable A) : @@ -174,20 +171,15 @@ theorem isElementary_closure (hA : L.MeetsDefinable A) : let D : Set M := {y : M | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)} have hD_ne : D.Nonempty := ⟨a,hφ⟩ have hD : A.Definable₁ L D := by - simp only [Definable₁, Definable, Fin.isValue] - refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel - (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0) - (fun j => (L.con ⟨x j, by + apply (φ.definable_boundedSection).preimage_map + simp only [DefinableMap] + refine Fin.lastCases ?_ ?_ + · simp only [Fin.snoc_last]; fun_prop + · intro i; simp only [Fin.snoc_castSucc]; + have : ↑(x i) ∈ A := by nth_rw 1 [← hA.closure_eq_self] - simp only [Subtype.coe_prop] - ⟩).term) i, ?_⟩ - ext v - simp only [Fin.isValue, mem_setOf_eq, Formula.relabel, Formula.Realize, - BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero, - Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D] - rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula] - congr! 1 - ext i; cases i using Fin.lastCases <;> simp + simp + fun_prop (disch := assumption) obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩