What an element can be — the DNA of model theory
Everything first-order logic can say about an element is called its type. Compute types, watch them become points of a space, and build a model that leaves one out on purpose.
Choose a structure and click an element to compute its complete type. Elements with the same color share a type; in the dense order, that type is just the element's cut.
Dense linear order without endpoints
Select an element:
Elements with the same color share the same type.
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.
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.
Click formulas to add them and watch the space split into the pieces [φ] and [¬φ]. Each region is a type that the formulas so far can tell apart.
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; combinations that contradict the order on the parameters are empty and not shown. The space is compact and totally disconnected.
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 φ.
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.
Press Next Step to build a countable model one witness at a time. Watch each witness get chosen so that the omitted type, the right endpoint, is never realized.
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.
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.
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.
Spot a mistake or have an idea?