Finite Model Property and Bisimulation for LFD

TL;DR

This paper proves that the logic of functional dependence (LFD) is decidable with the finite model property and characterizes it via bisimulation invariance, connecting modal and first-order logic.

Contribution

It establishes the finite model property for LFD using Herwig's theorem and provides a bisimulation invariance characterization of the logic.

Findings

LFD has the finite model property.

Bisimulation invariance characterizes LFD.

LFD is both a modal and a first-order logic fragment.

Abstract

Recently, Baltag and van Benthem introduced a decidable logic of functional dependence (LFD) that extends the logic of Cylindrical Relativized Set Algebras (CRS) with atomic local dependence statements. Its semantics can be given in terms of generalised assignment models or their modal counterparts, hence the logic is both a first-order and a modal logic. We show that LFD has the finite model property (FMP) using Herwig's theorem on extending partial isomorphisms, and prove a bisimulation invariance theorem characterizing LFD as a fragment of first-order logic.