Infinitary model existence, omitting types and interpolation

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

AbbreviationFirstOrder.Language.Theoryω#

An L_{ω₁ω} theory: a set of L_{ω₁ω} sentences.

FirstOrder.Language.Theoryω.{u, v} (L : FirstOrder.Language) : Type (max u v)
Lean

Formalized in Tau Ceti as FirstOrder.Language.Theoryω.

Sources
LeanFirstOrder.Language.Theoryω
Uses 1 · Used by 6
Statement usesFirstOrder.Language.BoundedFormulaInf
Used byA countable theory is one sentence · FirstOrder.Language.StrongHomClass.theoryω_model_iff · FirstOrder.Language.Theoryω.conjunction · FirstOrder.Language.Theoryω.Model · The model existence theorem with omitted types · The omitting types theorem for a countable formation-closed fragment

DefinitionFirstOrder.Language.Theoryω.Model#

A structure is a model of an L_{ω₁ω} theory when it satisfies every sentence of the theory.

FirstOrder.Language.Theoryω.Model.{u, v, w} {L : FirstOrder.Language} (T : L.Theoryω) (M : Type w)
  [L.Structure M] : Prop
Lean

Formalized in Tau Ceti as FirstOrder.Language.Theoryω.Model.

Sources
LeanFirstOrder.Language.Theoryω.Model
Uses 2 · Used by 4
Statement usesFirstOrder.Language.BoundedFormulaInf · FirstOrder.Language.Theoryω
Used byA countable theory is one sentence · FirstOrder.Language.StrongHomClass.theoryω_model_iff · The model existence theorem with omitted types · The omitting types theorem for a countable formation-closed fragment

TheoremFirstOrder.Language.StrongHomClass.theoryω_model_iff#

Isomorphic structures are models of the same L_{ω₁ω} theories.

FirstOrder.Language.StrongHomClass.theoryω_model_iff.{u, v, w, w', u_1} {L : FirstOrder.Language}
  {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N]
  [L.StrongHomClass F M N] (g : F) (T : L.Theoryω) : T.Model M ↔ T.Model N
Lean

Formalized in Tau Ceti as FirstOrder.Language.StrongHomClass.theoryω_model_iff.

Sources
LeanFirstOrder.Language.StrongHomClass.theoryω_model_iff
Uses 3 · Used by 2
Statement usesFirstOrder.Language.Theoryω · FirstOrder.Language.Theoryω.Model
Proof usesFirstOrder.Language.BoundedFormulaInf
Used byThe model existence theorem with omitted types · The omitting types theorem for a countable formation-closed fragment

DefinitionFirstOrder.Language.Theoryω.conjunction#

The conjunction of a countable theory: its sentences, enumerated into the carrier ℕ along IndexCoding.ofEncodableWith, joined by one countable conjunction. Indices that code no sentence carry ⊤.

FirstOrder.Language.Theoryω.conjunction.{u, v} {L : FirstOrder.Language} (T : L.Theoryω)
  (hT : Set.Countable T) : L.Sentenceω
Lean

Formalized in Tau Ceti as FirstOrder.Language.Theoryω.conjunction.

Sources
LeanFirstOrder.Language.Theoryω.conjunction
Uses 2 · Used by 1
Statement usesFirstOrder.Language.BoundedFormulaInf · FirstOrder.Language.Theoryω
Used byA countable theory is one sentence

TheoremA countable theory is one sentence#

A structure satisfies the conjunction of a countable theory exactly when it is a model of the theory.

FirstOrder.Language.Theoryω.realize_conjunction_iff.{u, v, w} {L : FirstOrder.Language}
  {T : L.Theoryω} {M : Type w} [L.Structure M] (hT : Set.Countable T) :
  FirstOrder.Language.SentenceInf.Realize (T.conjunction hT) M ↔ T.Model M
Lean

Formalized in Tau Ceti as FirstOrder.Language.Theoryω.realize_conjunction_iff.

Sources
LeanFirstOrder.Language.Theoryω.realize_conjunction_iff
Uses 4
Statement usesFirstOrder.Language.BoundedFormulaInf · FirstOrder.Language.Theoryω · FirstOrder.Language.Theoryω.conjunction · FirstOrder.Language.Theoryω.Model

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.