When do modal definability and preservation theorems transfer to the finite?
This addresses foundational issues in modal logic for finite structures, which is relevant for computer science applications, but the results are largely incremental as they extend known theorems to a restricted setting.
The paper investigates which classic modal definability and preservation theorems remain valid when restricted to finite structures, finding that some semantic characterizations survive while many first-order preservation theorems fail, with the main positive result being that the Bisimulation Safety Theorem transfers to the finite.
We study which classic modal definability and preservation results survive when attention is restricted to finite structures, where many first-order transfer theorems are known to break down. Several semantic characterizations for modal formula classes survive the passage to the finite, while a number of first-order preservation theorems for basic frame operations fail. Our main positive result is that the Bisimulation Safety Theorem does transfer to finite structures. We also discuss computability aspects, and analogues in the finite for the Goldblatt-Thomason theorem and for modal correspondence theory.