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 : 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

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.isMaximal {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) : FirstOrder.Language.Theory.IsMaximal ↑p

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) : φ ∈ p ∨ FirstOrder.Language.Formula.not φ ∈ p

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) : FirstOrder.Language.Formula.not φ ∈ p ↔ φ ∉ p

@[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

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

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' := ⋯ }

@[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

• T.realizedTypes M α = Set.range T.typeOf

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) α