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 #
- 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.
T.complete_type α to sets of formulas
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.