Goldblatt-Thomason Theorem

Origin. Goldblatt and Thomason (1974). Characterizes modally definable frame classes. Frame conditions expressible by modal formulas. Closure under bounded morphic images, generated subframes and disjoint unions — plus reflection of ultrafilter extensions, which runs in the opposite direction from the other three.

Models. Which classes of frames are definable by a set of modal formulas? Answer: exactly those closed under specific operations. Connects modal expressiveness to frame structure.

Formalism.

Modal definability: Class K of frames is modally definable if ∃Σ. K = {F | F ⊨ φ for all φ ∈ Σ}

Closure conditions:

Bounded morphic images: f: F → G surjective, ∀ preserving, ◇ reflecting. If F ∈ K and G is bounded morphic image, G ∈ K.

Generated subframes: H ⊆ F generated if closed under R. If F ∈ K and H generated subframe, H ∈ K.

Disjoint unions: ⊎ᵢFᵢ: disjoint union of frames. If all Fᵢ ∈ K, then ⊎Fᵢ ∈ K.

Ultrafilter extensions — reflected, not preserved: ue(F): ultrafilter extension of F. If ue(F) ∈ K, then F ∈ K. This is the one condition that runs the other way, and the direction is not a stylistic choice. Modally definable classes need not be closed under ue: (ℕ, <) is transitive and conversely well-founded, so it validates Löb's axiom, but ue(ℕ, <) contains non-principal ultrafilters and is not conversely well-founded, so it does not. The class of GL-frames is therefore modally definable and not ue-closed. What always holds is the reflecting direction — validity transfers from ue(F) down to F, because F embeds in ue(F) by principal ultrafilters.

Theorem: Elementary class K is modally definable iff K is closed under:

• Bounded morphic images
• Generated subframes
• Disjoint unions and reflects ultrafilter extensions.

Applications: Reflexivity, transitivity: modally definable. Irreflexivity: not modally definable. The one-point reflexive frame is a bounded morphic image of the irreflexive (ℤ, successor) — map everything to the single point — so the class of irreflexive frames is not closed under bounded morphic images, and the first condition already fails. Antisymmetry: not modally definable.

Symbols.

Metatheory. Characterization theorem. First-order expressible + closure = modal definable. van Benthem characterization for formulas. Sahlqvist correspondence.

Applies to. Modal logic design. Frame correspondence theory. Expressiveness analysis. Transfer results.

Limitations. Elementary class assumption. Ultrafilter extension abstract. Doesn't give axiomatization. Meta-level result.

© 2026 Lingenic LLC