Classical model theory proves its most powerful results using compactness: if every finite subset of a set of sentences has a model, then the entire set has a model. This is the engine behind the Łoś-Tarski theorem (every sentence preserved under substructures is equivalent to a universal sentence), the Lyndon preservation theorem (every sentence preserved under surjective homomorphisms is equivalent to a positive sentence), and a family of related results that convert semantic properties into syntactic guarantees. The proofs are existential — they establish that a sentence with the right form exists, but they don't build it.
Finite model theory has no compactness. Over finite structures, the existential route is closed. The Łoś-Tarski theorem fails finitely. The Lyndon theorem fails finitely. Result after result from the classical setting collapses when the structures cannot be infinite.
Van Benthem, ten Cate, and Yang (arXiv:2603.12171) ask what survives. Their answer: the bisimulation safety theorem transfers to finite structures. A modal formula is safe for bisimulation — invariant under this structural equivalence — if and only if it is equivalent to a basic modal formula. This holds over all structures, and it holds over finite structures.
The difference is in the proof. The bisimulation safety theorem's proof is constructive. Given a formula that is invariant under bisimulation, the proof builds the equivalent modal formula directly, translating the semantic property into syntax step by step. There is no appeal to compactness. There is no existential claim that the equivalent formula exists somewhere in the logical universe. The proof produces it.
This is the structural point: what survives the transition from infinite to finite is what was constructed rather than inferred. The existential proofs — the ones that say “a sentence with property P exists” via a compactness argument that might construct an infinite chain of approximations — break because their intermediate objects might not fit inside a finite structure. The constructive proof — the one that says “here is the sentence, and here is why it works” — breaks nothing, because every step of the construction is finite.
The analogy is engineering rather than mathematics: a bolt that was machined to specification works in any setting where the specification applies. A bolt that was proved to exist via a nonconstructive existence argument provides no bolt.
The paper also examines finite-domain analogues of the Goldblatt-Thomason theorem and modal correspondence theory. The pattern repeats: where proofs are constructive, results transfer; where proofs rely on infinite combinatorial arguments, they fail. Finiteness does not degrade theorems uniformly. It selects against a proof method — the nonconstructive existence proof — and preserves everything that was built from the ground up.