Documentation

Mathlib.ModelTheory.Types

Type Spaces #

This file defines the space of complete types over a first-order theory. (Note that types in model theory are different from types in type theory.)

Main Definitions #

Main Results #

Implementation Notes #

TODO #

structure FirstOrder.Language.Theory.CompleteType {L : FirstOrder.Language} (T : L.Theory) (α : Type w) :
Type (max (max u v) w)

A complete type over a given theory in a certain type of variables is a maximally consistent (with the theory) set of formulas in that type.

  • toTheory : (L.withConstants α).Theory
  • subset' : (L.lhomWithConstants α).onTheory T self
  • isMaximal' : (↑self).IsMaximal
Instances For
    theorem FirstOrder.Language.Theory.CompleteType.subset' {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (self : T.CompleteType α) :
    (L.lhomWithConstants α).onTheory T self
    theorem FirstOrder.Language.Theory.CompleteType.isMaximal' {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (self : T.CompleteType α) :
    (↑self).IsMaximal
    instance FirstOrder.Language.Theory.CompleteType.Sentence.instSetLike {L : FirstOrder.Language} {T : L.Theory} {α : Type w} :
    SetLike (T.CompleteType α) (L.withConstants α).Sentence
    Equations
    • FirstOrder.Language.Theory.CompleteType.Sentence.instSetLike = { coe := fun (p : T.CompleteType α) => p, coe_injective' := }
    theorem FirstOrder.Language.Theory.CompleteType.subset {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) :
    (L.lhomWithConstants α).onTheory T p
    theorem FirstOrder.Language.Theory.CompleteType.mem_or_not_mem {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) (φ : (L.withConstants α).Sentence) :
    theorem FirstOrder.Language.Theory.CompleteType.mem_of_models {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) {φ : (L.withConstants α).Sentence} (h : (L.lhomWithConstants α).onTheory T ⊨ᵇ φ) :
    φ p
    theorem FirstOrder.Language.Theory.CompleteType.not_mem_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) (φ : (L.withConstants α).Sentence) :
    @[simp]
    theorem FirstOrder.Language.Theory.CompleteType.compl_setOf_mem {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : (L.withConstants α).Sentence} :
    {p : T.CompleteType α | φ p} = {p : T.CompleteType α | FirstOrder.Language.Formula.not φ p}
    theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory) :
    {p : T.CompleteType α | S p} = ¬((L.lhomWithConstants α).onTheory T S).IsSatisfiable
    theorem FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : (L.withConstants α).Sentence) :
    {p : T.CompleteType α | φ p} = Set.univ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
    theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory) :
    {p : T.CompleteType α | S p} = Set.univ φS, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
    theorem FirstOrder.Language.Theory.CompleteType.nonempty_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} :
    Nonempty (T.CompleteType α) T.IsSatisfiable
    Equations
    • =
    theorem FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {ι : Type u_1} (S : ι(L.withConstants α).Theory) :
    ⋂ (i : ι), {p : T.CompleteType α | S i p} = {p : T.CompleteType α | ⋃ (i : ι), S i p}
    theorem FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {p : T.CompleteType α} {t : Finset (L.withConstants α).Sentence} :
    List.foldr (fun (x1 x2 : (L.withConstants α).Sentence) => x1 x2) t.toList p t p
    def FirstOrder.Language.Theory.typeOf {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {M : Type w'} [L.Structure M] [Nonempty M] [M T] (v : αM) :
    T.CompleteType α

    The set of all formulas true at a tuple in a structure forms a complete type.

    Equations
    • T.typeOf v = { toTheory := (L.withConstants α).completeTheory M, subset' := , isMaximal' := }
    Instances For
      @[simp]
      theorem FirstOrder.Language.Theory.CompleteType.mem_typeOf {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {M : Type w'} [L.Structure M] [Nonempty M] [M T] {v : αM} {φ : (L.withConstants α).Sentence} :
      φ T.typeOf v (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v
      theorem FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {M : Type w'} [L.Structure M] [Nonempty M] [M T] {v : αM} {φ : L.Formula α} :
      FirstOrder.Language.Formula.equivSentence φ T.typeOf v φ.Realize v
      def FirstOrder.Language.Theory.realizedTypes {L : FirstOrder.Language} (T : L.Theory) (M : Type w') [L.Structure M] [Nonempty M] [M T] (α : Type w) :
      Set (T.CompleteType α)

      A complete type p is realized in a particular structure when there is some tuple v whose type is p.

      Equations
      Instances For
        theorem FirstOrder.Language.Theory.exists_modelType_is_realized_in {L : FirstOrder.Language} (T : L.Theory) {α : Type w} (p : T.CompleteType α) :
        ∃ (M : T.ModelType), p T.realizedTypes (↑M) α