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

• FirstOrder.Language.Theory.CompleteType: T.CompleteType α consists of complete types over the theory T with variables α.
• FirstOrder.Language.Theory.typeOf is the type of a given tuple.
• FirstOrder.Language.Theory.realizedTypes: T.realizedTypes M α is the set of types in T.CompleteType α that are realized in M - that is, the type of some tuple in M.

Main Results

• FirstOrder.Language.Theory.CompleteType.nonempty_iff: The space T.CompleteType α is nonempty exactly when T is satisfiable.
• FirstOrder.Language.Theory.CompleteType.exists_modelType_is_realized_in: Every type is realized in some model.

Implementation Notes

• Complete types are implemented as maximal consistent theories in an expanded language. More frequently they are described as maximal consistent sets of formulas, but this is equivalent.

TODO

• Connect T.CompleteType α to sets of formulas L.Formula α.

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

• toTheory : FirstOrder.Language.Theory (FirstOrder.Language.withConstants L α)
• subset' : FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ⊆ ↑s
• isMaximal' : FirstOrder.Language.Theory.IsMaximal ↑s

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.

instance FirstOrder.Language.Theory.CompleteType.Sentence.instSetLike {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} : SetLike (FirstOrder.Language.Theory.CompleteType T α) (FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α))

theorem FirstOrder.Language.Theory.CompleteType.isMaximal {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (p : FirstOrder.Language.Theory.CompleteType T α) : FirstOrder.Language.Theory.IsMaximal ↑p

theorem FirstOrder.Language.Theory.CompleteType.subset {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (p : FirstOrder.Language.Theory.CompleteType T α) : FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ⊆ ↑p

theorem FirstOrder.Language.Theory.CompleteType.mem_or_not_mem {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (p : FirstOrder.Language.Theory.CompleteType T α) (φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)) : φ ∈ p ∨ FirstOrder.Language.Formula.not φ ∈ p

theorem FirstOrder.Language.Theory.CompleteType.mem_of_models {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (p : FirstOrder.Language.Theory.CompleteType T α) {φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)} (h : FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ⊨ᵇ φ) : φ ∈ p

theorem FirstOrder.Language.Theory.CompleteType.not_mem_iff {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (p : FirstOrder.Language.Theory.CompleteType T α) (φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)) : FirstOrder.Language.Formula.not φ ∈ p ↔ ¬φ ∈ p

@[simp]

theorem FirstOrder.Language.Theory.CompleteType.compl_setOf_mem {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)} : {p | φ ∈ p}ᶜ = {p | FirstOrder.Language.Formula.not φ ∈ p}

theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (S : FirstOrder.Language.Theory (FirstOrder.Language.withConstants L α)) : {p | S ⊆ ↑p} = ∅ ↔ ¬FirstOrder.Language.Theory.IsSatisfiable (FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ∪ S)

theorem FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)) : {p | φ ∈ p} = Set.univ ↔ FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} (S : FirstOrder.Language.Theory (FirstOrder.Language.withConstants L α)) : {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)), φ ∈ S → FirstOrder.Language.LHom.onTheory (FirstOrder.Language.lhomWithConstants L α) T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.CompleteType.nonempty_iff {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} : Nonempty (FirstOrder.Language.Theory.CompleteType T α) ↔ FirstOrder.Language.Theory.IsSatisfiable T

instance FirstOrder.Language.Theory.CompleteType.instNonempty {L : FirstOrder.Language} {α : Type w} : Nonempty (FirstOrder.Language.Theory.CompleteType ∅ α)

theorem FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {ι : Type u_1} (S : ι → FirstOrder.Language.Theory (FirstOrder.Language.withConstants L α)) : ⋂ (i : ι), {p | S i ⊆ ↑p} = {p | ⋃ (i : ι), S i ⊆ ↑p}

theorem FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {p : FirstOrder.Language.Theory.CompleteType T α} {t : Finset (FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α))} : List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (Finset.toList t) ∈ p ↔ ↑t ⊆ ↑p

def FirstOrder.Language.Theory.typeOf {L : FirstOrder.Language} (T : FirstOrder.Language.Theory L) {α : Type w} {M : Type w'} [FirstOrder.Language.Structure L M] [Nonempty M] [M ⊨ T] (v : α → M) : FirstOrder.Language.Theory.CompleteType T α

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

@[simp]

theorem FirstOrder.Language.Theory.CompleteType.mem_typeOf {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {M : Type w'} [FirstOrder.Language.Structure L M] [Nonempty M] [M ⊨ T] {v : α → M} {φ : FirstOrder.Language.Sentence (FirstOrder.Language.withConstants L α)} : φ ∈ FirstOrder.Language.Theory.typeOf T v ↔ FirstOrder.Language.Formula.Realize (↑FirstOrder.Language.Formula.equivSentence.symm φ) v

theorem FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {M : Type w'} [FirstOrder.Language.Structure L M] [Nonempty M] [M ⊨ T] {v : α → M} {φ : FirstOrder.Language.Formula L α} : ↑FirstOrder.Language.Formula.equivSentence φ ∈ FirstOrder.Language.Theory.typeOf T v ↔ FirstOrder.Language.Formula.Realize φ v

def FirstOrder.Language.Theory.realizedTypes {L : FirstOrder.Language} (T : FirstOrder.Language.Theory L) (M : Type w') [FirstOrder.Language.Structure L M] [Nonempty M] [M ⊨ T] (α : Type w) : Set (FirstOrder.Language.Theory.CompleteType T α)

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

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