What an element can be — the DNA of model theory
A type over a parameter set A in a structure M is a consistent set of formulas with parameters from A. The complete type tp(a/A) of an element a collects every formula φ(x) with parameters from A that M satisfies at a. Types capture everything a structure "knows" about an element, and two elements with the same type are indistinguishable by first-order properties.
The set of all complete n-types of a theory T forms a topological space Sn(T), called the Stone space. This space is compact, Hausdorff, and totally disconnected -- a Stone space in the sense of Stone duality. Its topology is generated by clopen sets of the form [φ] = {p : φ ∈ p}, one for each formula φ.
The Omitting Types Theorem gives a remarkable converse to realization: if T is a countable complete theory and p(x) is a non-isolated type (not determined by a single formula), then T has a countable model that omits p entirely -- no element in that model realizes the type. This is a cornerstone of constructing models with precisely controlled properties.
Choose a structure and select an element to compute its complete type -- the set of all formulas the element satisfies. Elements with identical types are colored alike, revealing the type structure of the model. In dense linear orders, the type of an element is entirely determined by its Dedekind cut.
Dense linear order without endpoints
Select an element:
Elements with the same color share the same type.
Key insight: The complete type of an element captures all first-order information about it. Two elements realize the same type precisely when no formula can distinguish them -- they are "twins" from the perspective of the theory.
The Stone space S1(T) of a theory T organizes all complete 1-types into a compact topological space. Adding a formula φ partitions the space into the clopen sets [φ] and [¬φ]. Click to add formulas and watch the space split into finer regions, each representing a distinct type.
Theory: DLO (dense linear orders without endpoints). Click formulas to partition the Stone space S1(DLO).
S₁(DLO)
Each formula φ splits the space into [φ] and [¬φ]. With n formulas, there are up to 2n regions. The space is compact and totally disconnected.
Key insight: The Stone space is compact and totally disconnected. Every type is an intersection of clopen sets, and the topology encodes which types are "close" to each other -- types that agree on many formulas are topologically near.
Watch a model being built step by step using a Henkin-style construction that deliberately avoids realizing a specified type. At each stage, a witness is chosen to satisfy the next formula while steering clear of the omitted type. The result is a countable model where the forbidden type has no home.
Type to omit: The "right endpoint" type
p(x) = { x > a : for every a in the model } -- the type of an element greater than everything.
Step 1: Start: place an initial element
Witness chosen: 0
Seed element; does not realize the endpoint type since the model is not yet built.
Key insight: A non-isolated type can always be omitted in a countable model. The key is that at each construction step, there is room to choose witnesses that avoid the type -- precisely because no single formula forces the type to be realized.