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 #
T.CompleteType αconsists of complete types over the theory
FirstOrder.Language.Theory.typeOfis the type of a given tuple.
T.realizedTypes M αis the set of types in
T.CompleteType αthat are realized in
M- that is, the type of some tuple in
Main Results #
FirstOrder.Language.Theory.CompleteType.nonempty_iff: The space
T.CompleteType αis nonempty exactly when
FirstOrder.Language.Theory.CompleteType.exists_modelType_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.
T.CompleteType αto sets of formulas
- isMaximal' : FirstOrder.Language.Theory.IsMaximal ↑s
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.
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
v whose type is