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 theoryT
with variablesα
.
Main Results #
first_order.language.Theory.complete_type.nonempty_iff
: The spaceT.complete_type α
is nonempty exactly whenT
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 formulasL.formula α
.
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
@[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' := _}
theorem
first_order.language.Theory.complete_type.is_maximal
{L : first_order.language}
{T : L.Theory}
{α : Type w}
(p : T.complete_type α) :
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
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
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
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
@[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}
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
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 ⊨ φ
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 ⊨ φ
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
@[protected, instance]
def
first_order.language.Theory.complete_type.nonempty
{L : first_order.language}
{α : Type w} :
nonempty (∅.complete_type α)
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) :
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