  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.
