Model Existence

Results named in Tau Ceti's TauCeti.ModelTheory.ModelExistence modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe fragment Tarski–Vaught criterion #

If, for every universal member ∀ x, φ of A and every tuple a from N, whenever φ has a counterexample at f ∘ a in M it has one in the image of f, then f is A-elementary.

FirstOrder.Language.aElementary_of_tarskiVaught.{u, v, w, w'} {L : FirstOrder.Language} {M : Type w}
  {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} (f : L.Embedding N M)
  (htv :
    ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty (n + 1)),
      ⟨n, FirstOrder.Language.BoundedFormulaInf.all φ⟩ ∈ A →
        ∀ (a : Fin n → N),
          (∃ m, ¬FirstOrder.Language.BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc (⇑f ∘ a) m)) →
            ∃ b,
              ¬FirstOrder.Language.BoundedFormulaInf.Realize φ Empty.elim
                  (Fin.snoc (⇑f ∘ a) (f b))) :
  FirstOrder.Language.AElementary A f

Lean

Formalized in Tau Ceti as FirstOrder.Language.aElementary_of_tarskiVaught.

Sources

LeanFirstOrder.Language.aElementary_of_tarskiVaught

Uses 1

Statement usesFirstOrder.Language.BoundedFormulaInf

TheoremThe model existence theorem with omitted types #

Over a language with countably many function and relation symbols, let p i be countably many countable partial types such that every member t of the consistency property C and every tuple c of Henkin constants admit some ψ ∈ p i for which t together with the refutation ¬ψ[c] is again a member. Then every countable member s of C has a countable nonempty model, in any universe w, in which every element is the interpretation of a Henkin constant and which omits every p i.

FirstOrder.Language.ConsistencyProperty.model_existence_omitting.{u, v, w, u_1}
  {L : FirstOrder.Language} [Countable ((n : ℕ) × L.Functions n)]
  [Countable ((n : ℕ) × L.Relations n)] (C : L.ConsistencyProperty) {ι : Type u_1} [Countable ι]
  {n : ι → ℕ} (p : (i : ι) → Set ((L.withConstants ℕ).BoundedFormulaω Empty (n i)))
  (hp : ∀ (i : ι), (p i).Countable)
  (hC :
    ∀ (i : ι),
      ∀ t ∈ C.sets,
        ∀ (c : Fin (n i) → ℕ),
          ∃ ψ ∈ p i,
            insert
                (FirstOrder.Language.BoundedFormulaInf.substBounds (fun j => (L.con (c j)).term)
                    ψ).not
                t ∈
              C.sets)
  {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ C.sets) (hsc : Set.Countable s) :
  ∃ M x,
    Countable M ∧
      Nonempty M ∧
        s.Model M ∧
          (Function.Surjective fun c => ↑(L.con c)) ∧
            ∀ (i : ι), FirstOrder.Language.OmitsType M (p i)

Lean

Formalized in Tau Ceti as FirstOrder.Language.ConsistencyProperty.model_existence_omitting.

Sources

LeanFirstOrder.Language.ConsistencyProperty.model_existence_omitting

Uses 4 · Used by 1

Statement usesFirstOrder.Language.BoundedFormulaInf · FirstOrder.Language.Theoryω · FirstOrder.Language.Theoryω.Model

Proof usesFirstOrder.Language.StrongHomClass.theoryω_model_iff

Used byThe omitting types theorem for a countable formation-closed fragment

TheoremThe omitting types theorem for a countable formation-closed fragment #

A satisfiable theory of sentences of the fragment has a countable nonempty model, in any universe, omitting any countable family of partial types in the fragment, none isolated over the theory in the fragment. Countability of the language follows from countability and formation closure of the fragment.

FirstOrder.Language.Theoryω.exists_countable_model_omitting.{u, v, w, u_1} {L : FirstOrder.Language}
  {A : L.Fragment} {T : L.Theoryω} (hAc : (↑A).Countable) (hA : A.FormationClosed)
  (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) (hTs : T.IsSatisfiable) {ι : Type u_1} [Countable ι] {n : ι → ℕ}
  (p : (i : ι) → Set (L.BoundedFormulaω Empty (n i))) (hp : ∀ (i : ι), ∀ ψ ∈ p i, ⟨n i, ψ⟩ ∈ A)
  (hnp : ∀ (i : ι), ¬FirstOrder.Language.Theoryω.IsolatesIn A T (p i)) :
  ∃ M x, Countable M ∧ Nonempty M ∧ T.Model M ∧ ∀ (i : ι), FirstOrder.Language.OmitsType M (p i)