Finite Model Property and Bisimulation for LFD

Recently, Baltag & van Benthem introduced a decidable logic of functional dependence (LFD) that extends the logic of Cylindrical Relativized Set Algebras (CRS) [2] with atomic dependence statements. The semantics is given in terms of dependence models¹¹1These are just the generalised assignment models known from [2][5]., which are pairs $(M,A)$ of a first-order structure $M$ together with a fixed set of variable assignments (or ’team’) $A\subseteq M^{V}$ on $M$, where $V$ is some (possibly finite) ambient set of variables. Formulas are evaluated at individual assignments $s\in A$; in particular the dependence atoms get the following semantics: $s\models D_{X}y$ if for all $t\in A$, $s\restriction X=t\restriction X$ implies $s(y)=t(y)$. This is in contrast with logics based on team semantics, where dependence formulas are evaluated at teams and this team is dynamically changed over the course of evaluation. Whereas most logics based on team semantics are undecidable, non-classical and have expressive going beyond FOL, LFD is decidable with a classical semantics and can be considered a fragment of FOL.

Many interesting notions of dependence (such as lineair dependence in vector spaces, temporal dependence in dynamical systems and strategic interaction in a multi-player game) can be formalized in LFD [3]. Moreover, LFD invites a natural epistemic interpretation where (sets of) variables may represent (groups of) agents, (joint) questions or objects.[3] The dependence modalities then capture distributed knowledge or the interrogative modality, while the dependence atoms capture epistemic superiority or inquisitive implication (or other ’mixed’ notions). More spectacularly, [4] introduces a complete and decidable dynamic-epistemic logic based on LFD with so-called ’reading events’ as well as a notion of ’common distributed knowledge’ that combines features of common knowledge and distributed knowledge.

Dependence models are closely related to relational databases: assignments are rows in the table and each variable represents a column, or attribute. Here is a simple numerical example of a dependence model, viewed as a database:

In this table we see that e.g. $y$ locally depends on $x$ in the first row, because the second row, which agrees on $x$ with the first, also agrees on $y$ with it (and no other rows agree on $x$ with the first row). In fact, this dependence holds at all rows, in which case we say that $y$ globally depends on $x$. Conversely, $x$ does not depend globally on $y$ because it does not locally depend on $y$ at the first row: both $1$ and $2$ occur as $x$-values of rows that share the current $y$-value $0$. Finally, because the fourth row is the only row with $z$-value $2$, all other variables locally depend on $z$ there.

The foregoing example witnesses the close connection between LFD and the study of dependence in databases, and indeed the Projection and Transitivity axioms of LFD recapture Armstrong’s Axioms for functional dependence [3]. Deeper connections with database theory as well as team semantics might arise by introducing dynamics on the level of teams, generalizing the semantics to dependence universes, i.e. families of dependence models [3]. In particular, dependence models

The decidability proof in [3] uses completeness of LFD w.r.t a purely syntactic ’type semantics’ resembling the ’quasi-models’ studied in connection with the Guarded Fragment [5][2]. The question whether LFD has the finite model property (FMP) w.r.t. dependence models remained an open problem [3]. Our main result is that LFD has the FMP, by a new application of Herwig’s theorem on extending partial isomorphisms. Moreover, we define dependence bisimulations and show that LFD can be characterized as the fragment of FOL that is invariant under this notion. Independently, another notion of bisimulation for LFD along more standard lines has been proposed in [6]. We show that these notions are equivalent, but that dependence bisimulations suggest a more efficient procedure for checking bisimilarity.

We first introduce the language LFD, dependence models and type models. A pair $(V,\tau)$, where $V$ is set of variables and $\tau$ is a relational language is called a vocabulary. When both $V$ and $\tau$ are finite, we say that $(V,\tau)$ is a finite vocabulary. We write $FOL[V,\tau]$ for the set of first-order formulas with variables in $V$ (both free and bound) and predicates in $\tau$, and similarly for $LFD[V,\tau]$. We assume that each vocabulary becomes equipped with an arity map $ar:\tau\to\mathbb{N}$.

Moreover, we let $V_{\varphi}$ denote the set of variables occurring in $\varphi$. This is in general a superset of the free of variables, i.e. $V_{D_{X}y}=X\cup\{y\}$. Further, we say that $\tau_{\varphi}:=\{P\in\tau\;|\;P\;\textrm{occurs in}\;\varphi\}$.

Where $s(\mathbf{x})$ denotes the tuple $(s(x_{1}),...,s(x_{m}))$ for $\mathbf{x}=(x_{1},...,x_{m})$. Clearly, for every dependence model $(M,A)$ and assignments $s,t\in A$, there is a unique set $V^{s,t}:=\{v\in V\;|\;s=_{v}t\}$ that is the maximal set of variables on which $s,t$ agree. An important feature of the semantics is LFD satisfies Locality.

Next to dependence models, LFD is weakly complete w.r.t. a non-standard type semantics.[3] In other words, only LFD over finite vocabularies is complete for this semantics. Type models were used in [3] as a technical auxiliary to prove completeness and decidability. Types are defined relative to closures. We obtain the closure $\Psi:=Cl(\psi)$ of a formula $\psi$ by adding to $\{\psi\}$ all formulas $D_{X}y$ for $X\cup\{y\}\subseteq V_{\psi}$ and closing the resulting set under subformulas and single negation. ⁴⁴4For every non-negated formula $\varphi$ (i.e. a formula whose principal connective is not $\neg$) we add $\neg\varphi$ to the closure, and for negated formulas we we do nothing. The resulting closure set will not contain any formulas with double negations.

For $X\subseteq V_{\psi}$, we define a relation $\sim_{X}$ on types $\Sigma,\Delta\subseteq\Psi$:

where $D^{\Sigma}_{X}=\{y\in V_{\varphi}\;|\;D_{X}y\in\Sigma\}$ is the dependence-closure of $X$ w.r.t and $\Sigma$. Observe that $\Sigma\sim_{X}\Delta$ implies $D^{\Sigma}_{X}=D^{\Delta}_{X}$ as $Free(D_{X}y)=X$.

The original paper [3] left finding a bisimulation-invariance theorem characterizing LFD as an open problem. precisely which formulas in $FOL[V\cup V^{\prime},\tau\cup\{A\}]$ are equivalent to the $tr$-translation of an LFD-formula over standard structures.⁷⁷7There is also a modal translation of LFD into FOL that extends the well-known standard translation of modal logic into the 2-variable fragment of FOL. A similar characterization theorem can be proved via this translation and the relational semantics for LFD, as our notion of bisimulation as well as the one proposed in [6] are naturally formulated on dependence models as well as their modal counterparts. The following notion of dependence bisimulation exactly characterizes $LFD$ as the largest fragment of $FOL$ invariant under this notion. Say that a set of variables $X$ is dependence-closed at $s^{\prime}$ if $D^{s^{\prime}}_{X}:=\{y\in V\;|\;;s^{\prime}\models D_{X}y\}=X$, or equivalently if $s^{\prime}\models D_{X}y$ implies $y\in X$.

Dependence bisimulations are always total; every state is related to another by the bisimulation.

Dependence bisimulations in fact characterize LFD as a fragment of FOL. This can be shown by formulating an analogue of dependence bisimulations for structures of the form $T(\mathbb{M})$, and showing that on $\omega$-saturated structures of this form, LFD-equivalence implies dependence-bisimilarity.

Independently, another notion of bisimulation characterizing LFD has been proposed in [6] that treats dependence atoms like ordinary relational atoms. That is, instead of the dependence-closed condition they simply require that ”$s\models D_{X}y$ iff $s^{\prime}\models D_{X}y$” holds for all $X\cup\{y\}\subseteq V$. It follows that proposition 3.1 shows that dependence bisimulations are also bisimulations in their sense. Conversely, ”$s\models D_{X}y$ iff $s^{\prime}\models D_{X}y$” clearly implies the dependence-closed condition, hence the two notions are equivalent. It follows that the proof given in [6] also shows that LFD is the dependence bisimulation-invariant fragment of FOL.

Dependence bisimulations suggest a more efficient way to implement a bisimilarity-checking algorithm for LFD compared to the definition in [6]. For what proposition 3.1 shows is that, given $(M,A),(M^{\prime},A^{\prime})$ with $s\in A,s^{\prime}\in A^{\prime}$, it actually suffices to check that ”$s\models D_{X}y$ iff $s^{\prime}\models D_{X}y$ for all $y\in V$” holds for all $X\in\{V^{s,t}\subseteq V\;|\;t\in A\}\cup\{V^{s^{\prime},t^{\prime}}\subseteq V\;|\;t^{\prime}\in A^{\prime}\}$ in order to conclude that ”$s\models D_{X}y$ iff $s^{\prime}\models D_{X}y$ for all $y\in V$” holds for all $X\subseteq V$. This could be used to avoid an exponential blow-up in $|V|$.

Dependence bisimulations generalise naturally to extensions of LFD. For instance, we can extend $LFD$ with the equality relation $=$, yielding the logic $LFD^{=}$ which was shown to be a conservative reduction class of FOL and hence undecidable in [6]. Dependence bisimulations with an extended (Atom) clause that also ranges over equality can be shown to characterize $LFD^{=}$ as a fragment to FOL. Interestingly, over full dependence models (i.e. those $(M,A)$ with $A=M^{V}$, which are standard first-order structures repackaged as dependence models), dependence bisimulations (for LFD over a finite vocabulary $(V,\tau)$ with $|V|=k$) coincides with $k$-potential isomorphism, which characterizes first-order logic in $k$ variables.

We show that LFD has the FMP w.r.t the intended dependence model semantics, by an application of Herwig’s theorem similar to the one in [7]. Fix a satisfiable LFD-formula $\varphi$, and let $\Phi:=Cl(\{\varphi\})$. We let $(V,\tau):=(V_{\varphi},\tau_{\varphi})$ be the smallest vocabulary containing $\varphi$ and hence $\Phi$. Note that $(V,\tau)$ is a finite vocabulary, so let $|V|=k$. We know that there is a tree-like dependence model $\mathbb{M}=(M,A)$, with associated tree $T$ of good paths, satisfying $\varphi$ at the root assignment. Furthermore, the degree of $T$ is bounded by $m\times 2^{k}$, where $m$ is the number of distinct $\Phi$-types. Our strategy is as follows: we will cut the underlying $k$-tree $M$ to a finite structure, encode the dependence atoms in a richer language and finally use Herwig’s theorem to generate out of this a finite dependence model that is bisimilar to the original tree-model. Define a sub-team of $A$ by:

and let $M_{cut}$ be the submodel of $M$ induced by $\bigcup\{v_{\pi}[V]\subseteq M\;|\;v_{\pi}\in A_{cut}\}$; we call $\mathbb{M}_{cut}:=(M_{cut},A_{cut})$ the cut-off model. This is a finite model because the branching degree of $T$ is bounded and $V$ is finite. The truth lemma clearly no longer holds on this cut-off model, because some existential witnesses are missing for assignments of length 3.

We extend the language to include an $|X|$-ary relation $R^{X,y}$ for each $X\cup\{y\}\subseteq V$, and obtain the (still finite) richer language $\tau^{+}\supseteq\tau$. We will use these relations to encode the semantics of the dependence atoms. We expand the structure $M_{cut}$ underlying the cut-off model to a $\tau^{+}$ structure by putting:

so that $\mathbb{M}_{cut},v_{\pi}\models R^{X,y}\mathbf{x}$ iff $D_{X}y\in last(\pi)$. In the end, we want to show that $R^{x,y}\mathbf{x}\leftrightarrow D_{X}y$ holds on the Herwig extension, so that we can recover an appropriate dependence model from it. To show this, we will need the following restricted version of this claim on the cut-off model:

Herwig’s theorem on extending partial isomorphism [8] is a result about first-order relational languages. It tells us that any finite structure with some set of partial isomorphisms on it has a finite extension in which all these partial isomorphisms extend to automorphisms. This theorem has already been used to show the FMP of the Guarded Fragment (GF) [7].

where $\langle p_{1},...,p_{k}\rangle$ is the collection of all partial isomorphisms that can be obtained by composing the $p_{i}$ with their inverses. Note that $\langle p_{1},...,p_{k}\rangle$ is strictly speaking not a group as it need not be the case that $p\circ p^{-1}$ is the identity on $C$ (in general, it is the identity on a subset of $C$).

Condition (iii) is in need of further clarification. In words, it says that elements in the submodel $C$ are only mapped to each other by some $f\in\langle f_{1},...,f_{n}\rangle$ if this is forced given the choice of partial isomorphisms. Uniqueness of $p$ in this condition is ensured by the fact that the map $\widehat{(\;)}$ extends to a bijective map $\widehat{(\;)}:\langle p_{1},...,p_{k}\rangle\to\langle\widehat{p_{1}},...,\widehat{p_{k}}\rangle$ that commutes with the operations $\circ,(\;)^{-1}$ (and the identity $id$). By condition (i), $\widehat{(\;)}$ is defined on the subset $\{p_{1},...,p_{k}\}$. Set $\widehat{p^{-1}}:=\widehat{p}^{-1}$ and $\widehat{p\circ p^{\prime}}:=\widehat{p}\circ\widehat{p^{\prime}}$; so commutation follows by definition. It immediately follows that the map is injective. For surjectivity, let $f\in\langle\widehat{p_{1}},...,\widehat{p_{k}}\rangle$. By definition $f=\widehat{p_{i_{1}}}^{\epsilon_{1}}\circ...\circ\widehat{p_{i_{m}}}^{\epsilon_{m}}$ for some $\{i_{1},...,i_{m}\}\subseteq\{1,...,k\}$ and $\epsilon_{j}\in\{-1,1\}$ for each $j\leq m$. Define $p:=p_{i_{1}}^{\epsilon_{1}}\circ...\circ p_{i_{m}}^{\epsilon_{m}}\in\langle p_{1},...,p_{k}\rangle$. Now observe:

We proceed with specifying a choice of partial isomorphisms on the cut-off model. If $\pi$ is a good path of $lh(\pi)=3$ and $last(\pi)=\Delta$, then there is a partial isomorphism $p_{\pi}:v_{\pi}[V_{\varphi}]\to v_{\pi_{\Delta}}[V_{\varphi}]$ such that $p_{\pi}\circ v_{\pi}=v_{\pi_{\Delta}}$, where $\pi_{\Delta}:=\langle\Sigma_{0},\emptyset,\Delta\rangle$ so $lh(\pi_{\Delta})=2$. We pick the finite set of partial isomorphisms $\{p_{\pi}\;|\;\pi\;\textrm{good path of}\;lh(\pi)=3\}=\{p_{1},...,p_{k}\}$. The following proposition tells us what kind of partial isomorphisms are in $\langle p_{1},...,p_{k}\rangle$.

The associated first-order structure $T(\mathbb{M}_{cut})$ of the Herwig extension is a finite model in a finite relational language $\tau^{+}\cup\{A\}$, and $\{p_{1},...,p_{k}\}$ is a finite set of partial isomorphisms on it. Hence, by Herwig’s theorem, there exists a finite extension $T(\mathbb{M}_{cut})^{+}$ of this structure, the Herwig extension, satisfying conditions (i)-(iii) w.r.t $\{p_{1},...,p_{k}\}$. It is easy to see that the Herwig extension corresponds in the canonical way (i.e. see the first-order translation above) to a dependence model $\mathbb{M}_{cut}^{+}:=(M_{cut}^{+},A_{cut}^{+})$ such that $T(\mathbb{M}_{cut}^{+})=T(\mathbb{M}_{cut})^{+}$. Recall that we want to establish a bisimulation between the finite Herwig extension $\mathbb{M}_{cut}^{+}$ and the infinite tree model $\mathbb{M}$. To do this, we will need the following lemmas.