feat(model_theory/types): Realized types (#17848)

awainverse · awainverse · commit 98bd247d933f · 2023-04-25T12:54:02.000Z
Defines `first_order.language.Theory.type_of`, the type of a given tuple.
Defines what it means for a type to be realized.



Co-authored-by: Aaron Anderson &lt;65780815+awainverse@users.noreply.github.com&gt;
diff --git a/src/model_theory/types.lean b/src/model_theory/types.lean
@@ -13,10 +13,15 @@ This file defines the space of complete types over a first-order theory.
 ## Main Definitions
 * `first_order.language.Theory.complete_type`:
   `T.complete_type α` consists of complete types over the theory `T` with variables `α`.
+* `first_order.language.Theory.type_of` is the type of a given tuple.
+* `first_order.language.Theory.realized_types`: `T.realized_types M α` is the set of
+  types in `T.complete_type α` that are realized in `M` - that is, the type of some tuple in `M`.
 
 ## Main Results
 * `first_order.language.Theory.complete_type.nonempty_iff`:
   The space `T.complete_type α` is nonempty exactly when `T` is satisfiable.
+* `first_order.language.Theory.complete_type.exists_Model_is_realized_in`: Every type is realized in
+some model.
 
 ## Implementation Notes
 * Complete types are implemented as maximal consistent theories in an expanded language.
@@ -151,6 +156,54 @@ end
 
 end complete_type
 
+variables {M : Type w'} [L.Structure M] [nonempty M] [M ⊨ T] (T)
+
+/-- The set of all formulas true at a tuple in a structure forms a complete type. -/
+def type_of (v : α → M) : T.complete_type α :=
+begin
+  haveI : (constants_on α).Structure M := constants_on.Structure v,
+  exact { to_Theory := L[[α]].complete_theory M,
+    subset' := model_iff_subset_complete_theory.1 ((Lhom.on_Theory_model _ T).2 infer_instance),
+    is_maximal' := complete_theory.is_maximal _ _ },
+end
+
+namespace complete_type
+
+variables {T} {v : α → M}
+
+@[simp] lemma mem_type_of {φ : L[[α]].sentence} :
+  φ ∈ T.type_of v ↔ (formula.equiv_sentence.symm φ).realize v :=
+begin
+  letI : (constants_on α).Structure M := constants_on.Structure v,
+  exact mem_complete_theory.trans (formula.realize_equiv_sentence_symm _ _ _).symm,
+end
+
+lemma formula_mem_type_of {φ : L.formula α} :
+  formula.equiv_sentence φ ∈ T.type_of v ↔ φ.realize v :=
+by simp
+
+end complete_type
+
+variable (M)
+
+/-- A complete type `p` is realized in a particular structure when there is some
+  tuple `v` whose type is `p`. -/
+@[simp] def realized_types (α : Type w) : set (T.complete_type α) :=
+set.range (T.type_of : (α → M) → T.complete_type α)
+
+theorem exists_Model_is_realized_in (p : T.complete_type α) :
+  ∃ (M : Theory.Model.{u v (max u v w)} T),
+    p ∈ T.realized_types M α :=
+begin
+  obtain ⟨M⟩ := p.is_maximal.1,
+  refine ⟨(M.subtheory_Model p.subset).reduct (L.Lhom_with_constants α), (λ a, (L.con a : M)), _⟩,
+  refine set_like.ext (λ φ, _),
+  simp only [complete_type.mem_type_of],
+  refine (formula.realize_equiv_sentence_symm_con _ _).trans (trans (trans _
+    (p.is_maximal.is_complete.realize_sentence_iff φ M)) (p.is_maximal.mem_iff_models φ).symm),
+  refl,
+end
+
 end Theory
 end language
 end first_order
