Documentation

Mathlib.ModelTheory.Types

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 #

Main Results #

Implementation Notes #

TODO #

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
    theorem FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset {L : FirstOrder.Language} {T : FirstOrder.Language.Theory L} {α : Type w} {ι : Type u_1} (S : ιFirstOrder.Language.Theory (FirstOrder.Language.withConstants L α)) :
    ⋂ (i : ι), {p | S i p} = {p | ⋃ (i : ι), S i p}

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

    Instances For

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

      Instances For