Type Spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 #

first_order.language.Theory.complete_type: T.complete_type α consists of complete types over the theory T with variables α.
first_order.language.Theory.type_of is the type of a given tuple.
first_order.language.Theory.realized_types: T.realized_types M α is the set of types in T.complete_type α that are realized in M - that is, the type of some tuple in M.

Main Results #

first_order.language.Theory.complete_type.nonempty_iff: The space T.complete_type α is nonempty exactly when T is satisfiable.
first_order.language.Theory.complete_type.exists_Model_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.complete_type α to sets of formulas L.formula α.

source

structure first_order.language.Theory.complete_type {L : first_order.language} (T : L.Theory) (α : Type w) :

Type (max u v w)

to_Theory : (L.with_constants α).Theory
subset' : (L.Lhom_with_constants α).on_Theory T ⊆ self.to_Theory
is_maximal' : self.to_Theory.is_maximal

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.

Instances for first_order.language.Theory.complete_type

first_order.language.Theory.complete_type.has_sizeof_inst
first_order.language.Theory.complete_type.sentence.set_like
first_order.language.Theory.complete_type.nonempty

source

@[protected, instance]

def first_order.language.Theory.complete_type.sentence.set_like {L : first_order.language} {T : L.Theory} {α : Type w} :

set_like (T.complete_type α) (L.with_constants α).sentence

Equations

first_order.language.Theory.complete_type.sentence.set_like = {coe := λ (p : T.complete_type α), p.to_Theory, coe_injective' := _}

source

theorem first_order.language.Theory.complete_type.is_maximal {L : first_order.language} {T : L.Theory} {α : Type w} (p : T.complete_type α) :

↑p.is_maximal

source

theorem first_order.language.Theory.complete_type.subset {L : first_order.language} {T : L.Theory} {α : Type w} (p : T.complete_type α) :

(L.Lhom_with_constants α).on_Theory T ⊆ ↑p

source

theorem first_order.language.Theory.complete_type.mem_or_not_mem {L : first_order.language} {T : L.Theory} {α : Type w} (p : T.complete_type α) (φ : (L.with_constants α).sentence) :

φ ∈ p ∨ first_order.language.formula.not φ ∈ p

source

theorem first_order.language.Theory.complete_type.mem_of_models {L : first_order.language} {T : L.Theory} {α : Type w} (p : T.complete_type α) {φ : (L.with_constants α).sentence} (h : (L.Lhom_with_constants α).on_Theory T ⊨ φ) :

φ ∈ p

source

theorem first_order.language.Theory.complete_type.not_mem_iff {L : first_order.language} {T : L.Theory} {α : Type w} (p : T.complete_type α) (φ : (L.with_constants α).sentence) :

first_order.language.formula.not φ ∈ p ↔ φ ∉ p

source

@[simp]

theorem first_order.language.Theory.complete_type.compl_set_of_mem {L : first_order.language} {T : L.Theory} {α : Type w} {φ : (L.with_constants α).sentence} :

{p : T.complete_type α | φ ∈ p}ᶜ = {p : T.complete_type α | first_order.language.formula.not φ ∈ p}

source

theorem first_order.language.Theory.complete_type.set_of_subset_eq_empty_iff {L : first_order.language} {T : L.Theory} {α : Type w} (S : (L.with_constants α).Theory) :

{p : T.complete_type α | S ⊆ ↑p} = ∅ ↔ ¬((L.Lhom_with_constants α).on_Theory T ∪ S).is_satisfiable

source

theorem first_order.language.Theory.complete_type.set_of_mem_eq_univ_iff {L : first_order.language} {T : L.Theory} {α : Type w} (φ : (L.with_constants α).sentence) :

{p : T.complete_type α | φ ∈ p} = set.univ ↔ (L.Lhom_with_constants α).on_Theory T ⊨ φ

source

theorem first_order.language.Theory.complete_type.set_of_subset_eq_univ_iff {L : first_order.language} {T : L.Theory} {α : Type w} (S : (L.with_constants α).Theory) :

{p : T.complete_type α | S ⊆ ↑p} = set.univ ↔ ∀ (φ : (L.with_constants α).bounded_formula empty 0), φ ∈ S → (L.Lhom_with_constants α).on_Theory T ⊨ φ

source

theorem first_order.language.Theory.complete_type.nonempty_iff {L : first_order.language} {T : L.Theory} {α : Type w} :

nonempty (T.complete_type α) ↔ T.is_satisfiable

source

@[protected, instance]

def first_order.language.Theory.complete_type.nonempty {L : first_order.language} {α : Type w} :

nonempty (∅.complete_type α)

source

theorem first_order.language.Theory.complete_type.Inter_set_of_subset {L : first_order.language} {T : L.Theory} {α : Type w} {ι : Type u_1} (S : ι → (L.with_constants α).Theory) :

(⋂ (i : ι), {p : T.complete_type α | S i ⊆ ↑p}) = {p : T.complete_type α | (⋃ (i : ι), S i) ⊆ ↑p}

source

theorem first_order.language.Theory.complete_type.to_list_foldr_inf_mem {L : first_order.language} {T : L.Theory} {α : Type w} {p : T.complete_type α} {t : finset (L.with_constants α).sentence} :

list.foldr has_inf.inf ⊤ t.to_list ∈ p ↔ ↑t ⊆ ↑p

source

def first_order.language.Theory.type_of {L : first_order.language} (T : L.Theory) {α : Type w} {M : Type w'} [L.Structure M] [nonempty M] [M ⊨ T] (v : α → M) :

T.complete_type α

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

Equations

T.type_of v = {to_Theory := (L.with_constants α).complete_theory M (L.with_constants_Structure α), subset' := _, is_maximal' := _}

source

@[simp]

theorem first_order.language.Theory.complete_type.mem_type_of {L : first_order.language} {T : L.Theory} {α : Type w} {M : Type w'} [L.Structure M] [nonempty M] [M ⊨ T] {v : α → M} {φ : (L.with_constants α).sentence} :

φ ∈ T.type_of v ↔ (⇑(first_order.language.formula.equiv_sentence.symm) φ).realize v

source

theorem first_order.language.Theory.complete_type.formula_mem_type_of {L : first_order.language} {T : L.Theory} {α : Type w} {M : Type w'} [L.Structure M] [nonempty M] [M ⊨ T] {v : α → M} {φ : L.formula α} :

⇑first_order.language.formula.equiv_sentence φ ∈ T.type_of v ↔ φ.realize v

source

@[simp]

def first_order.language.Theory.realized_types {L : first_order.language} (T : L.Theory) (M : Type w') [L.Structure M] [nonempty M] [M ⊨ T] (α : Type w) :

set (T.complete_type α)

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

Equations

T.realized_types M α = set.range T.type_of

source

theorem first_order.language.Theory.exists_Model_is_realized_in {L : first_order.language} (T : L.Theory) {α : Type w} (p : T.complete_type α) :

∃ (M : T.Model), p ∈ T.realized_types ↥M α