When do modal definability and preservation theorems transfer to the finite?

TL;DR

This paper investigates which modal definability and preservation theorems remain valid when restricted to finite structures, highlighting the transfer of some results like the Bisimulation Safety Theorem and discussing limitations and computability issues.

Contribution

It identifies which classic modal and first-order transfer theorems hold or fail in finite structures, including positive results for bisimulation safety and discussions on related theorems.

Findings

Bisimulation Safety Theorem transfers to finite structures

Many first-order preservation theorems fail in the finite

Some semantic characterizations survive the finite restriction

Abstract

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.