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 #

first_order.language.Theory.complete_type: T.complete_type α consists of complete types over the theory T with variables α.

Main Results #

first_order.language.Theory.complete_type.nonempty_iff: The space T.complete_type α is nonempty exactly when T is satisfiable.

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