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. The theorem is a definability criterion of the Birkhoff kind, and it is exactly that under Jónsson–Tarski duality: modally definable frame classes correspond to varieties of Boolean algebras with operators, and the four closure conditions are the frame-side duals of closure under homomorphic images, subalgebras, products, and the canonical embedding — the reading Goldblatt gave in "Varieties of complex algebras" (1989). The general form of the theorem applies to any class already closed under ultrafilter extensions; the elementary version quoted here is the corollary, and it follows because ue(F) is a bounded morphic image of an ultrapower of F, so an elementary class closed under bounded morphic images is automatically ue-closed. The theorem sits beside van Benthem's characterization, which answers the model-level question — modal logic is the bisimulation-invariant fragment of first-order logic — while Goldblatt–Thomason answers the frame-level one. Analogues have been proved for coalgebras (Kurz and Rosický) and for general frames.

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

Limitations. The elementary hypothesis is a genuine restriction, not a convenience: the class of GL-frames is modally definable and not elementary, so the version stated here says nothing about it, and the general version demands ue-closure, which that class fails. The criterion is not effective — ultrafilter extensions need the ultrafilter lemma, and checking closure under bounded morphic images of an arbitrary class is not a finite test. It is a pure existence result: it asserts that some set Σ of modal formulas defines K without producing one, and gives no bound on Σ, no guarantee that Σ can be taken finite or even recursive, and no information about whether the logic of K is recursively axiomatizable. It also says nothing about completeness: a frame class can be modally definable while the logic determined by it is not the logic of any recursively presented calculus.

© 2026 Lingenic LLC