feat(ModelTheory): add characterizations of complete theories (leanprover-community#32146)

Add `isComplete_eq_complete_theory` and `isComplete_iff_models_elementarily_equivalent` to connect syntactic completeness with semantic properties.

Author: foderm

Mathlib/ModelTheory/Satisfiability.lean

@@ -412,6 +412,47 @@ theorem realize_sentence_iff (h : T.IsComplete) (φ : L.Sentence) (M : Type*) [L
       iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M))
         ((h.models_not_iff φ).1 hφn)
 
+/-- A complete theory is the `completeTheory` Th(M) of one of its models. -/
+theorem eq_complete_theory (h : T.IsComplete) (M : Type*) [L.Structure M] [M ⊨ T] [Nonempty M] :
+    {φ | T ⊨ᵇ φ} = L.completeTheory M := by
+  ext φ
+  simp only [Set.mem_setOf_eq, L.mem_completeTheory]
+  refine ⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩
+  cases h.2 φ with
+  | inl hT => exact hT
+  | inr hT =>
+      have : M ⊨ φ.not := hT.realize_sentence M
+      rw [Sentence.realize_not] at this
+      contradiction
+
+/-- A theory is complete iff it is satisfiable and all its models are elementarily equivalent. -/
+theorem isComplete_iff_models_elementarily_equivalent :
+    T.IsComplete ↔
+    T.IsSatisfiable ∧ ∀ (M N : ModelType.{u, v, max u v} T), ElementarilyEquivalent L M N := by
+  constructor
+  · intro hcomp
+    refine ⟨hcomp.1, ?_⟩
+    intro M N
+    rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
+  · rintro ⟨hsat, h⟩
+    refine ⟨hsat, ?_⟩
+    intro φ
+    obtain ⟨M⟩ := hsat
+    by_cases hφ : M ⊨ φ
+    · left
+      exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ
+    · right
+      exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
+        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)
+
+/-- If a theory is complete all its models are elementarily equivalent. -/
+theorem models_elementarily_equivalent
+    (h : T.IsComplete)
+    (M N : Type*) [L.Structure M] [L.Structure N]
+    [M ⊨ T] [N ⊨ T] [Nonempty M] [Nonempty N] :
+    ElementarilyEquivalent L M N := by
+  rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]
+
 end IsComplete
 
 /-- A theory is maximal when it is satisfiable and contains each sentence or its negation.