Finite Model Property and Bisimulation for LFD

Recently, Baltag and van Benthem arXiv:2103.14946 [cs.LO] introduced a new decidable logic of functional dependence (LFD) with local dependence formulas and dependence quantifiers. The language is interpreted over dependence models, which are pairs of first-order structures with a set of available variable assignments, also called a team. The team associated with a dependence model can be seen as a labelled transition system over which LFD becomes a modal logic, where the dependence quantifiers become modalities and local dependence formulas are treated as special atoms. In this paper, we introduce appropriate notions of bisimulation characterizing LFD (and some related logics) as a fragment of first order logic (FOL), and show it is equivalent to a notion of bisimulation along more standard lines proposed in arXiv:2102.10368 [cs.LO], yet more efficient for bisimilarity-checking. Our main result is that LFD has the finite model property (FMP), by a new application of Herwig's theorem on extending partial isomorphisms.