mathlib3 documentation


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 #

Main Results #

Implementation Notes #


structure first_order.language.Theory.complete_type {L : first_order.language} (T : L.Theory) (α : Type w) :
Type (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.

Instances for first_order.language.Theory.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) :
( (i : ι), {p : T.complete_type α | S i p}) = {p : T.complete_type α | ( (i : ι), S i) p}
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) :

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


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