Logics of Dependence and Independence: The Local Variants

TL;DR

This paper systematically extends local variants of dependence and independence logics, analyzing their model-theoretic properties, decidability, and complexity, revealing undecidability in certain cases.

Contribution

It introduces a systematic framework for localizing various dependency properties and studies their logical and computational characteristics.

Findings

Satisfiability of LFD without equality is decidable.

Satisfiability of LFD with equality is undecidable.

Complexity results for model checking of local dependence logics.

Abstract

Modern logics of dependence and independence are based on team semantics, which means that formulae are evaluated not on a single assignment of values to variables, but on a set of such assignments, called a team. This leads to high expressive power, on the level of existential second-order logic. As an alternative, Baltag and van Benthem have proposed a local variant of dependence logic, called logic of functional dependence (LFD). While its semantics is also based on a team, the formulae are evaluated locally on just one of its assignments, and the team just serves as the supply of the possible assignments that are taken into account in the evaluation process. This logic thus relies on the modal perspective of generalized assignments semantics, and can be seen as a fragment of first-order logic. For the variant of LFD without equality, the satisfiability problem is decidable. We extend the idea of localising logics of dependence and independence in a systematic way, taking into account local variants of standard atomic dependency properties: besides dependence and independence, also inclusion, exclusion, and anonymity. We study model-theoretic and algorithmic questions of the localised logics, and also resolve some of the questions that had been left open by Baltag and van Benthem. In particular, we study decidability issues of the local logics, and prove that satisfiability of LFD with equality is undecidable. Further, we establish characterisation theorems via appropriate notions of bisimulation and study the complexity of model checking problems for these logics.