# mathlib3documentation

model_theory.types

# 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 α.
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
@[simp]
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 : | S i p}) = {p : | ( (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.

Equations
@[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
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 α} :
@[simp]

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

Equations
• α =