Goldblatt-Thomason Theorem

Origin. Goldblatt and Thomason (1974). Characterizes modally definable frame classes. Frame conditions expressible by modal formulas. Closure conditions: bounded morphisms, generated subframes, disjoint unions, ultrafilter extensions.

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: ue(F): ultrafilter extension of F. If F ∈ K, then ue(F) ∈ K.

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

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

Reflects ue: If ue(F) ∈ K, then F ∈ K.

Applications: Reflexivity, transitivity: modally definable. Irreflexivity: not modally definable. Antisymmetry: not modally definable.

Symbols.

Symbol	Unicode	Name	Meaning
K	—	Class	Frame class
⊎	U+228E	Disjoint union	Frame combination
ue	—	Ultrafilter ext	Extension
⊨	U+22A8	Validity	Frame satisfies

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.