Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Johan van Benthem, Balder ten Cate, Xi Yang

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.

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

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.
Paper Structure (25 sections, 39 theorems, 43 equations, 2 figures, 1 table)

This paper contains 25 sections, 39 theorems, 43 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. The modal logic setting
  3. Monotonicity
  4. Preservation under induced substructures
  5. Complete additivity
  6. Continuity
  7. Where we stand
  8. The first-order logic setting
  9. Bisimulation invariance and bisimulation safety
  10. Basic modal preservation operations on frames
  11. Generated subframes
  12. Disjoint unions
  13. Bounded morphic images
  14. Ultrafilter extensions
  15. Where we stand
  16. ...and 10 more sections

Key Result

Theorem 2.1

A modal formula is valid over arbitrary Kripke models if and only if it is valid over finite Kripke models.

Figures (2)

  • Figure 1: The structure $\mathfrak{A}_n$. In addition to the edges shown, there is an $R_3$-edge from $a_w$ to $a_u$ whenever $u$ is a proper prefix of $w$.
  • Figure 2: The frames $\mathfrak{F}_5$ and $\mathfrak{G}_5$.

Theorems & Definitions (65)

  • Theorem 2.1: Finite Model Property
  • Theorem 2.2: Kurtonina1997:simulating, cf. also Kurtonina1999:expressiveness
  • Proposition 2.3
  • Theorem 2.4: deRijkePhD
  • Proposition 2.5
  • Theorem 2.6: vBenthem1998:bisimulation
  • Proposition 2.7
  • proof
  • Theorem 2.8: Fontaine2008:continuous
  • Proposition 2.9
  • ...and 55 more