Epistemic Logic with Partial Dependency Operator

TL;DR

This paper introduces a new partial dependency operator into epistemic logic, enhancing its expressivity to reason about partial dependencies in Kripke models, with formal properties and axiomatization.

Contribution

It presents a novel partial dependency modality in epistemic logic, along with its formal properties, examples, bisimulation analysis, and a complete axiomatization.

Findings

The logic can express partial dependency relationships.

The logic has desirable properties like bisimulation invariance.

A sound and complete axiomatization is provided for a sub-language.

Abstract

In this paper, we introduce $\textit{partial}$ dependency modality $\mathcal{D}$ into epistemic logic so as to reason about $\textit{partial}$ dependency relationship in Kripke models. The resulted dependence epistemic logic possesses decent expressivity and beautiful properties. Several interesting examples are provided, which highlight this logic's practical usage. The logic's bisimulation is then discussed, and we give a sound and strongly complete axiomatization for a sub-language of the logic.

Equations

$$\phi ::=\top \mid p\mid \neg \phi \mid (\phi \wedge \phi )\mid \mathcal{K}\phi \mid \mathcal{A}\phi \mid {\mathcal{D}}_g(X,Y)\mid {\mathcal{D}}_l(X,Y)$$

$${\mathcal{D}}_g(X,Y)\leftrightarrow \neg \mathcal{A}\neg {\mathcal{D}}_l(X,Y)$$

$$\phi ::=\top \mid p\mid \neg \phi \mid (\phi \wedge \phi )\mid \mathcal{K}\phi \mid \mathcal{A}\phi \mid {\mathcal{D}}_g(X,Y)$$

$${\mathcal{D}}_g(X,Y)⟺\exists \overrightarrow{w_1}\overrightarrow{x_1}\overrightarrow{y_1}\exists \overrightarrow{w_2}\overrightarrow{x_2}\overrightarrow{y_2}(\overrightarrow{w_1}\overrightarrow{x_1}\overrightarrow{y_1}\subseteq (V\backslash (X\cup Y))XY\wedge$$

$$\overrightarrow{w_2}\overrightarrow{x_2}\overrightarrow{y_2}\subseteq (V\backslash (X\cup Y))XY\wedge \overrightarrow{w_1}=\overrightarrow{w_2}\wedge \neg \overrightarrow{x_1}=\overrightarrow{x_2}\wedge \neg \overrightarrow{y_1}=\overrightarrow{y_2})$$

$$s:p,q,r$$

$$x=1$$

$$s:a,\neg b,c$$

$$s:a,b,c$$

$$\displaystyle\Delta(u,v)=\left\{\begin{array}[]{cc}\{x\mid x\in\mathbb{V},U(u,x)\neq U(v,x)\},&\text{ if }(V\backslash\mathbb{V})_{u}=(V\backslash\mathbb{V})_{v}\\ \emptyset,&\text{otherwise}\\ \end{array}\right.$$

$${\mathfrak{P}}_g(s)=\{\text{nonempty finite set }\Delta (u,v)\mid u,v\in S,u\approx v\approx s\}$$

$${\mathfrak{P}}_l(s)=\{\text{nonempty finite set }\Delta (t,s)\mid t\in S,t\approx s\}$$

$$\mathfrak{G}(s)=\{W\mid W\text{ is generative from }\mathfrak{P}(s)\}$$

$$\mathcal{D}(X,Y)\to \mathcal{D}(X^{\prime },Y)\text{, given }X\subseteq X^{\prime }\text{ (Weakening Rule)}$$

$$\displaystyle\mathcal{Q}(W)::=\left\{\begin{array}[]{cc}\mathcal{D}(W,W),&|W|=1\\ \bigwedge\limits_{Z\subset W,Z\neq\emptyset}\mathcal{D}(Z,W\backslash Z),&|W|\geqslant 2\\ \end{array}\right.$$

Full text

1 Introduction

Following some previous fundamental work on “knowing value” [15, 16, 10, 4, 2], recent years have seen an abundance of interest in this novel kind of non-standard epistemic logic. There has been epistemic logic with functional dependency operator [3], which can help us reason about knowing that the value of certain variable is functionally decided by some other variables. For instance, the agent knows that $y=x^{2}$, so he knows that $y$ functionally depends on $x$ even if without knowing the exact values of $x$ or $y$.

Nevertheless, the real world is never so ideal as a simple parabola. As a matter of fact, in a lot of practical cases, the value of a dependent variable $y$ is usually influenced by thousands of independent factors as $x_{1}$, $x_{2}$, $\ldots$ in a quite complicated way, such that it is virtually impossible to obtain a detailed function to precisely determine the value of $y$. Therefore, in both scientific and social study, the method of control variable gets widely used. We often set the values of all the other variables rigid, only change the value of an independent variable $x$ and observe the change of the dependent variable $y$. If the value of $y$ varies with the value of $x$, then we conclude that $y$ partially depends on $x$. In this paper, we introduce modality $\mathcal{D}$ in order to express this kind of partial dependency relationship.

There have also been dependence and independence logics dealing with dependency relationship between variables [13, 9, 8, 6], and we will discuss our logic’s connection to them in Remark 2. A similar definition for dependency relationship also appears in Halpern’s recent book, pp. 14-19. [11] However, the start point of our work is epistemic logic as well as the Kripke model, and we would like to incorporate partial dependency relationship between variables into the agent’s knowledge so that we shall obtain an epistemic logic of “knowing dependency”, which is hence named as dependence epistemic logic. This dependence epistemic logic proves to possess further affluent expressivity as well as rather straightforward properties.

In the Kripke model for our dependence epistemic logic, besides a usual $\sim_{i}$ S5 equivalence relation representing the agent’s knowledge, i.e., all the possible worlds that the agent cannot distinguish, there also exists another $\approx$ S5 equivalence relation representing the physical probability, i.e., all the possible worlds that share the same set of physical laws with the current world. Generally speaking, these two equivalence relations do not have to have any correlation, and thus in the language, the former is characterized by an S5 modality $\mathcal{K}$, while the latter is characterized by another independent S5 modality $\mathcal{A}$. This kind of framework is first introduced by another recent work [14], and so readers who get confused with the conception of two independent equivalence relations in the model are strongly recommended to refer to that paper.

Then the partial dependency relationship is valuated in the $\approx$ equivalence class, since dependency relationship between variables is in fact related to some universal physical law and thus concerns not only the current exact world but also all the other worlds that are physically potentially possible. Actually, we introduce two different modalities $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$ to characterize partial dependency relationship. Their respective semantics is both based on the discussion in the beginning about what modality $\mathcal{D}$ should be like, except for that, the former $\mathcal{D}_{g}$ is valuated globally in a whole $\approx$ equivalence class, while the latter $\mathcal{D}_{l}$ fixes one reference point as the current exact world and so is valuated locally. Readers will soon become clear about what $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$ mean respectively through the following Section 2 on preliminaries including the language, model and semantics, and the correlation between these two modalities also gets discussed in Remark 1. Examples in Section 3 illustrate that $\mathcal{D}_{g}$ is helpful in analyzing universal physical laws while $\mathcal{D}_{l}$ is useful in expressing counterfactual assumptions, in surprising accordance with our very intuition as well as commonsense, so the practicality of $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$ counts to why we introduce both modalities.

The rest of the paper is organized as follows. We lay out the basics of the language and the semantics in Section 2. Several interesting examples are illustrated in Section 3. A bisimulation notion for this dependence epistemic logic then gets thoroughly discussed in Section 4, followed by a sound and strongly complete axiomatization for a sub-language in Section 5. We finally conclude this paper and propose future research directions in Section 6.

2 Preliminaries

Definition 1 (Language EDL)

For a fixed countable set of propositions $\mathbb{P}$, and a fixed countable set of variables $\mathbb{V}$, the language EDL of dependence epistemic logic is defined recursively as:

[TABLE]

where $p\in\mathbb{P}$, and $X$ as well as $Y$ are finite subsets of $\mathbb{V}$. $\mathcal{D}_{g}(X,Y)$ reads as $Y$ depends on $X$ globally, while $\mathcal{D}_{l}(X,Y)$ reads as $Y$ depends on $X$ locally. We define $\bot$, $\lor$ and $\to$ as usual.

Important Notation

In the following parts of this paper, when some property applies to both $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$, we will simply omit the subscript and write down only one theorem, lemma, axiom, etc. concerning $\mathcal{D}$ for convenience, and the omitting is also similar for other notations derived from $\mathcal{D}$.

If $X=\{x\}$, we will also denote $\mathcal{D}(\{x\},Y)$ as $\mathcal{D}(x,Y)$ for simplicity, and likely for $Y$ if $Y=\{y\}$.

Definition 2 (Model)

A dependence epistemic model $\mathcal{M}$ is $\langle S,T,V,U,\sim_{i},\approx\rangle$:

• •

$S$ is a set of possible worlds.

• •

$T$: $S\times\mathbb{P}\to\{0,1\}$.

• •

$V\supseteq\mathbb{V}$ is a countable set of variable objects.

• •

$U$: $S\times V\to\mathbb{N}$.

• •

$\sim_{i}$ is an equivalence relation over $S$.

• •

$\approx$ is an equivalence relation over $S$.

As the convention in first-order logic, while $\mathbb{V}$ in the language are names for variables, $V$ in the model interpret each name with a concrete object and also may consist of other variable objects whose names are not included in the language. Since the language EDL excludes the equal sign $=$, every name in $\mathbb{V}$ can be managed to be interpreted differently in $V$, so we simply let $V\supseteq\mathbb{V}$ and do not make explicit distinctions between names and objects in the following without causing any confusion. Then $U$ is the function that assigns each variable on each possible world with a (countably possible) value, which is supposed to be uniformly numbered by $\mathbb{N}$ for convenience.

Sometimes we apply another extra stipulation on the model in order to satisfy our practical needs: for any proposition $p\in\mathbb{P}$, it may have its corresponding variable ${\overline{p}}\in\mathbb{V}$. If so, we then stipulate that $\forall s\in S$, $U(s,{\overline{p}})=T(s,p)$. The following Subsections 3.1 and 3.3 present examples of this kind.

Definition 3 (Semantics)

We define that $\forall s,t\in S$, $\forall$ subset $X\subseteq V$, $X_{s}=X_{t}$ iff $\forall x\in X,U(s,x)=U(t,x)$, while of course, $X_{s}\neq X_{t}$ iff $\exists x\in X,U(s,x)\neq U(t,x)$. A pointed model $\mathcal{M},s$ is a dependence epistemic model $\mathcal{M}$ with a possible world $s\in S$.

[TABLE]

When it is not that $\mathcal{M},s\vDash\varphi$, we denote it as $\mathcal{M},s\nvDash\varphi$.

Remark 1 (Expressivity of $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$)

We are able to perceive through Definition 3 that $\mathcal{D}_{g}$ is actually definable using $\neg$, $\mathcal{A}$ and $\mathcal{D}_{l}$, demonstrated as the following:

[TABLE]

In fact, $\mathcal{D}_{l}$ is strictly more expressive than $\mathcal{D}_{g}$, which will become clear to readers through our discussion for bisimulation in Section 4. Nevertheless, due to $\mathcal{D}_{g}$’s simplicity and usefulness, we will take the language with $\mathcal{D}_{g}$ but without $\mathcal{D}_{l}$ as a sub-language of EDL.

Definition 4 (Language EDG)

For a fixed countable set of propositions $\mathbb{P}$, and a fixed countable set of variables $\mathbb{V}$, the language EDG is defined recursively as:

[TABLE]

where $p\in\mathbb{P}$, and $X$ as well as $Y$ are finite subsets of $\mathbb{V}$.

The model and semantics are the same.

Remark 2 (Connection to Independence Logic)

If the total set of variables $V$ is finite and explicitly known, then modality $\mathcal{D}_{g}$ can be expressed in inclusion logic, a sub-language of independence logic [5], as the following:111As for the notation, we prefer to use $X$ and $Y$ instead of $\overrightarrow{x}$ or $\overrightarrow{y}$. Anyway, their respective meanings in this specific context should be clear to readers.

[TABLE]

However, this form puts too many restrictions and becomes too lengthy, while we actually want the total set $V$ to be clear from our language so that we can reason with simple and compact logic. In fact, the team model on which independence logic is based is quite different from the Kripke possible world model [12], both in technique and in philosophical explanation, and hence they are very unlike logics. While independence logic, inherited from first order logic, always reasons globally, epistemic logic, rooted from modal logic, usually reasons locally, which is demonstrated by this obvious fact that local modality $\mathcal{D}_{l}$ can surely not be defined in independence logic.

3 Examples

3.1 An Open Door

Let $p$ denote that the door of the room is open now, $q$ denote that the agent possesses the key of the door, and $r$ denote that the agent is able to enter the room. Let us suppose that the agent has perfect knowledge, so $\sim_{i}$ relation is only reflexive. Then we have:222When drawing all these figures in this paper, for brevity we will omit some relation lines which can be deduced from S5 equivalence class requirements.

[TABLE]

It is not difficult to observe that $\mathcal{M},s\vDash\mathcal{K}\mathcal{D}_{g}({\overline{p}},{\overline{r}})$ and $\mathcal{M},s\vDash\mathcal{K}\neg\mathcal{D}_{l}({\overline{p}},{\overline{r}})$. The former says that the agent knows whether he is able to enter the room is somewhat related to whether the door is open now – if he did not possess the key. And the latter says that under the present situation, since the agent does possess the key, he surely knows that if this precondition is kept unchanged, then he was still able to open the door to enter the room even if the door was now closed. Namely, whether he is able to enter the room does not depend on whether the door is open now, which provides us with a fancy way to express counterfactual assumptions.

3.2 Error-included Experiment

Suppose we are carrying out an experiment, and we know from theory that there are two independent variables $x$ and $y$ which may influence the value of the dependent variable $z$, where the value of $x$ is well under control but $y$ represents some random experimental error, and so of course, we cannot control or even measure the value of $y$. The only thing we know about $y$ is that it will be either $1$ or $2$ during every experiment.

Now we have done this experiment twice. When $x=1$, $z=1$. When $x=2$, $z=2$. By combining all kinds of possibilities, we can have the model as:

[TABLE]

Can we be confident that $z$ depends on $x$? Certainly not, because the change of $z$ may be brought about by the change of $y$. As a matter of fact, on every possible world $s$ there is $\mathcal{M},s\nvDash\mathcal{K}\mathcal{D}_{g}(x,z)$.

However, if we have further done the third experiment, and when $x=3$, $z=3$. Now can we be confident that $z$ depends on $x$? Indeed we can. This fact can be easily observed through the following huge model, where $\mathcal{M},s\vDash\mathcal{K}\mathcal{D}_{g}(x,z)$ on every possible world $s$:

[TABLE]

Whatever values $y$ may be in the three experiments, there must be at least two experiments in which $y$ is the same, so we can only explain the difference between $z$ in these two experiments as caused by the difference between the value of $x$. This scenario clearly explains why in all the natural science experiments, despite the universal existence of errors, we can still manage to obtain useful conclusions concerning our interested variables, by multiple experiments with relatively large data range.

3.3 Judging a Case

We have seen that global modality $\mathcal{D}_{g}$ can help us analyze complicated experimental results, while local modality $\mathcal{D}_{l}$ is very helpful in expressing counterfactual assumptions. And there are still trickier things worth examining. Until now, we have only proposed examples including modality $\mathcal{D}$ affecting solely on singletons. It may seem by intuitive guess that $\mathcal{D}(\{a,b\},c)$ tells very similar thing as $\mathcal{D}(a,c)\lor\mathcal{D}(b,c)$. Nevertheless, these two expressions are not exactly the same, and in fact, they may result in quite opposite epistemic consequences, as demonstrated by the following scenario.

Unfortunately, Charles got killed in a tragedy ($c$), which was related to Alan having done something ($a$) and/or Bob having done something ($b$). Firstly, let us suppose that either $a$ or $b$ could happen so as to cause $c$, and only one of them could have happened to be $c$’s indeed cause. However, on the current world $s$ we are yet not sure whether $a$ or $b$ actually happened to be the exact cause of $c$. This can be modeled as the following:

[TABLE]

It is not difficult to observe that $\mathcal{M},s\vDash\mathcal{K}\mathcal{D}_{l}(\{{\overline{a}},{\overline{b}}\},{\overline{c}})\land\mathcal{K}(\mathcal{D}_{l}({\overline{a}},{\overline{c}})\lor\mathcal{D}_{l}({\overline{b}},{\overline{c}}))$. This is to say, it is within our knowledge that not only the whole group event $\{a,b\}$ is related to $c$, but also either $a$ or $b$ itself is alone related to $c$, namely, their influences on $c$ can be separated in concept. Hence, unless we obtain further evidence to pin down our knowledge in order to determine whether Alan or Bob was the real criminal, by presumption of innocence neither of them can be sentenced guilty for Charles’ death.

Now let us turn to a second phenomenon, where $b$’s happening was a direct consequence of $a$’s happening. For instance, let $b$ denote that Bob killed Charles, and $a$ denote that Alan compelled Bob to kill Charles, either by threatening that he would have killed Bob otherwise or by Alan’s mind control over Bob through magic or science fiction. In other words, we restrict ourselves to only consider possible worlds on which $a\rightarrow b$ holds in our Kripke model. Under this circumstance, we can model our knowledge as the following:

[TABLE]

At present, even physically speaking $b$ should be the only direct cause of $c$, which is demonstrated by $\mathcal{A}(b\leftrightarrow c)$ holding throughout the model, to our little surprise $\mathcal{K}\mathcal{D}_{l}({\overline{b}},{\overline{c}})$ does not hold on the current world $s$. As a matter of fact, we have $\mathcal{M},s\vDash\mathcal{K}\mathcal{D}_{l}(\{{\overline{a}},{\overline{b}}\},{\overline{c}})\land\mathcal{K}(\neg\mathcal{D}_{l}({\overline{a}},{\overline{c}})\land\neg\mathcal{D}_{l}({\overline{b}},{\overline{c}}))$, a direct contrast against the former scene. This time we not only know that $c$ locally depends on $\{a,b\}$ as a whole, but also know that this dependency relationship should be viewed as an entirety instead of conceptually separable, and therefore, both Alan and Bob should be responsible for Charles’ death. Further considering that $\mathcal{K}\mathcal{A}(a\rightarrow b)$ holds on $s$, a legal and rational sentence ought to be that Alan is the principal criminal while Bob is the coerced criminal, which precisely captures the meanings of all the formulae mentioned above.

4 Bisimulation

Definition 5 ($\Delta(u,v)$)

For any two possible worlds $u,v\in S$, we define:

[TABLE]

Definition 6 (Evidence)

For any three sets $W$, $X$ and $Y$, $W$ is called an evidence of $\langle X,Y\rangle$, iff $W\cap X\neq\emptyset$, $W\cap Y\neq\emptyset$, and $W\subseteq X\cup Y$.

Compared with the original semantics defined in Definition 3, we manage to rewrite part of it in an equivalent form as the following:

Lemma 1 (Evidence Lemma I)

[TABLE]

Proof

Directly from the semantics defined in Definition 3.

Definition 7 ($\mathfrak{P}(s)$)

For any possible world $s\in S$, we define:

[TABLE]

It is obvious that $\forall s\in S$, $\mathfrak{P}_{l}(s)\subseteq\mathfrak{P}_{g}(s)\subseteq\{$nonempty finite set $W\mid W\subseteq\mathbb{V}\}$.

We again manage to rewrite part of the semantics in another equivalent form as the following, making use of the newly defined $\mathfrak{P}(s)$:

Lemma 2 (Evidence Lemma II)

[TABLE]

Proof

By Lemma 1.

Definition 8 (Generative)

$\forall s\in S$, any nonempty finite set $W\subseteq\mathbb{V}$ is called generative from $\mathfrak{P}(s)$, iff for any two finite sets $X,Y\subseteq\mathbb{V}$, such that $W$ is an evidence of $\langle X,Y\rangle$, there exists $W^{\prime}\in\mathfrak{P}(s)$, such that $W^{\prime}$ is also an evidence of $\langle X,Y\rangle$.

Theorem 4.1 (Equivalence Theorem I)

For any two pointed models $\mathcal{M},s$ and $\mathcal{M}^{\prime},s^{\prime}$, they satisfy exactly the same $\mathcal{D}(X,Y)$ formulae for any two finite sets $X,Y\subseteq\mathbb{V}$ iff:

• •

Zig: $\forall W\in\mathfrak{P}(s),W\text{ is generative from }\mathfrak{P}(s^{\prime})$.

• •

Zag: $\forall W\in\mathfrak{P}(s^{\prime}),W\text{ is generative from }\mathfrak{P}(s)$.

Proof

For the direction from left to right, we first concentrate on the Zig condition. If there exists $W\in\mathfrak{P}(s)$, such that $W$ is not generative from $\mathfrak{P}(s^{\prime})$, then by definition, there exist two finite sets $X,Y\subseteq\mathbb{V}$, such that $W$ is an evidence of $\langle X,Y\rangle$, but there does not exist $W^{\prime}\in\mathfrak{P}(s^{\prime})$, such that $W^{\prime}$ is an evidence of $\langle X,Y\rangle$. By Lemma 2, this is equivalent to that $\mathcal{M},s\vDash\mathcal{D}(X,Y)$ but $\mathcal{M}^{\prime},s^{\prime}\nvDash\mathcal{D}(X,Y)$, a contradiction. The Zag condition follows by symmetry.

The other direction can also be verified similarly and easily.

Definition 9 ($\mathfrak{G}(s)$)

For any possible world $s\in S$, we define:

[TABLE]

It is obvious that $\forall s\in S$, $\mathfrak{G}_{l}(s)\subseteq\mathfrak{G}_{g}(s)\subseteq\{$nonempty finite set $W\mid W\subseteq\mathbb{V}\}$.

Theorem 4.2 (Equivalence Theorem II)

For any two pointed models $\mathcal{M},s$ and $\mathcal{M}^{\prime},s^{\prime}$, they satisfy exactly the same $\mathcal{D}(X,Y)$ formulae for any two finite sets $X,Y\subseteq\mathbb{V}$ iff $\mathfrak{G}(s)=\mathfrak{G}(s^{\prime})$.

Proof

Similar to the proof of Theorem 4.1.

Actually, the set $\mathfrak{G}(s)$ is the existent and the only greatest generative set from the original $\mathfrak{P}(s)$ while keeping satisfying the same formulae for modality $\mathcal{D}$. Therefore, it is worthwhile investigating what characteristics $\mathfrak{G}(s)$ possesses, since it precisely determines the modal property of the pointed model $\mathcal{M},s$. In the following theorem, we manage to express the generative condition for a nonempty finite set $W$ from $\mathfrak{P}(s)$ in several different equivalent forms.

Theorem 4.3 (Generative Theorem)

$\forall s\in S$, for any nonempty finite set $W\subseteq\mathbb{V}$, we define $\Sigma(s,W)=\{W^{\prime}\mid W^{\prime}\in\mathfrak{P}(s),W^{\prime}\subseteq W\}$, then:

[TABLE]

Proof

Let us concentrate on the following crucial lemma, from which the proof of this theorem follows not difficultly.

Lemma 3 (Generative Lemma)

$\forall s\in S$, for any nonempty finite set $W\subseteq\mathbb{V}$, $W$ is generative from $\mathfrak{P}(s)$ iff:

• •

if $|W|=1$, then $W\in\mathfrak{P}(s)$.

• •

if $|W|\geqslant 2$, then $\forall Z\subset W$ such that $Z\neq\emptyset$, $\exists W^{\prime}\in\mathfrak{P}(s)$ such that $W^{\prime}$ is an evidence of $\langle Z,W\backslash Z\rangle$.

Proof

The direction from left to right is immediate. For the direction from right to left, we only have to make use of one simple fact about evidence:

• •

If $W$ is an evidence of $\langle X,Y\rangle$ and $X\subseteq X^{\prime}$, then $W$ is an evidence of $\langle X^{\prime},Y\rangle$.

which, as a matter of fact, can be correspondingly written into a sound axiom regarding modality $\mathcal{D}$:

[TABLE]

Full axiomatization will later be discussed in the following Section 5.

The last equivalent condition in Theorem 4.3 is to say, we can construct an undirected graph over $\mathfrak{P}(s)$ by its elements’ intersection relation, and all the generative sets are exactly union of some connected nonempty finite subgraph. This provides us with a clear picture and an intuitive understanding about where every generative set comes from and what $\mathfrak{G}(s)$ looks like. Hence given $\mathfrak{P}(s)$, there is an explicit algorithm to calculate all the generative nonempty finite sets $W\subseteq\mathbb{V}$ so as to obtain $\mathfrak{G}(s)$.

Finally, taking into account all the modalities including $\mathcal{K}$, $\mathcal{A}$, $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$, we are able to define the full bisimulation relation between two models $\mathcal{M}$ and $\mathcal{M}^{\prime}$:

Definition 10 (Bisimulation)

A nonempty binary relation $B\subseteq S\times S^{\prime}$ is called a bisimulation between two models $\mathcal{M}$ and $\mathcal{M}^{\prime}$ iff:

• •

If $sBs^{\prime}$, then $\forall p\in\mathbb{P}$, $T(s,p)=T(s^{\prime},p)$.

• •

If $sBs^{\prime}$, then $\mathfrak{G}_{g}(s)=\mathfrak{G}_{g}(s^{\prime})$.

• •

If $sBs^{\prime}$, then $\mathfrak{G}_{l}(s)=\mathfrak{G}_{l}(s^{\prime})$.

• •

Zig for $\mathcal{K}$: if $sBs^{\prime}$ and $s\sim_{i}t$, then $\exists t^{\prime}\in S^{\prime}$ such that $tBt^{\prime}$ and $s^{\prime}\sim_{i}t^{\prime}$.

• •

Zig for $\mathcal{A}$: if $sBs^{\prime}$ and $s\approx t$, then $\exists t^{\prime}\in S^{\prime}$ such that $tBt^{\prime}$ and $s^{\prime}\approx t^{\prime}$.

• •

Zag for $\mathcal{K}$: if $sBs^{\prime}$ and $s^{\prime}\sim_{i}t^{\prime}$, then $\exists t\in S$ such that $tBt^{\prime}$ and $s\sim_{i}t$.

• •

Zag for $\mathcal{A}$: if $sBs^{\prime}$ and $s^{\prime}\approx t^{\prime}$, then $\exists t\in S$ such that $tBt^{\prime}$ and $s\approx t$.

When $B$ is a bisimulation between two models $\mathcal{M}$ and $\mathcal{M}^{\prime}$, we write $B:\mathcal{M}\ \underline{\leftrightarrow}\ \mathcal{M}^{\prime}$. Furthermore if $sBs^{\prime}$, we write $B:\mathcal{M},s\ \underline{\leftrightarrow}\ \mathcal{M}^{\prime},s^{\prime}$. If there is a bisimulation $B$ such that $B:\mathcal{M},s\ \underline{\leftrightarrow}\ \mathcal{M}^{\prime},s^{\prime}$, we write $\mathcal{M},s\ \underline{\leftrightarrow}\ \mathcal{M}^{\prime},s^{\prime}$.

We write $\mathcal{M},s\leftrightsquigarrow\mathcal{M}^{\prime},s^{\prime}$, when for any EDL-formula $\varphi$, $\mathcal{M},s\vDash\varphi$ iff $\mathcal{M}^{\prime},s^{\prime}\vDash\varphi$.

Theorem 4.4 (Hennessy-Milner Theorem)

For any two m-saturated models $\mathcal{M}$ and $\mathcal{M}^{\prime}$, $\forall s\in S$, $\forall s^{\prime}\in S^{\prime}$, $\mathcal{M},s\ \underline{\leftrightarrow}\ \mathcal{M}^{\prime},s^{\prime}$ iff $\mathcal{M},s\leftrightsquigarrow\mathcal{M}^{\prime},s^{\prime}$.

Proof

See [1]. The definition of m-saturated models also appears as Definition 2.53 in that book. It is only the cases for modalities $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$ that are added, which just follow from Theorem 4.2.

5 Axiomatization

We only provide a sound and strongly complete axiomatization for language EDG. Nevertheless, the same as the assumed routine in this paper, axioms without subscripts attached to $\mathcal{D}$ are sound with respect to both $\mathcal{D}_{g}$ and $\mathcal{D}_{l}$.

To start with, we may notice some obviously sound axioms to characterize the properties of modality $\mathcal{D}$:

$\mathcal{D}(\emptyset,X)\leftrightarrow\bot$ (Empty Set Rule) 2. 2.

$\mathcal{D}(X,Y)\leftrightarrow\mathcal{D}(Y,X)$ (Symmetry Rule) 3. 3.

$\mathcal{D}(X,Y)\to\mathcal{D}(X^{\prime},Y)$, given $X\subseteq X^{\prime}$ (Weakening Rule) 4. 4.

$\mathcal{D}(X,Y)\leftrightarrow\mathcal{D}(X\backslash Y,Y)\lor\mathcal{D}(X\cap Y,Y)$ (Separation Rule)

Although these naïve axioms indeed look very similar to those in independence logic [7], pitifully in our dependence epistemic logic, they alone are away from being complete. The good news is that, we can instead find some conciser axioms, which entirely grasp the full properties of modality $\mathcal{D}$ itself, and from which all the above sound axioms can surely be deduced.

For brevity, let us first define an auxiliary notation:

Definition 11 ($\mathcal{Q}(W)$)

For any nonempty finite set $W\subseteq\mathbb{V}$, we define:

[TABLE]

Recall Lemma 3, readers should be aware that this $\mathcal{Q}(W)$ precisely depicts the minimum necessary $\mathcal{D}(X,Y)$ formulae, such that $W$ is an evidence of $\langle X,Y\rangle$. Taking advantage of this notation, we can write down rather concise sound axioms about modality $\mathcal{D}$ so as to obtain a complete axiomatization, as the following Q and E Axioms for $\mathcal{D}$ in Theorem 5.1:

Theorem 5.1 (Axiomatization)

The following proof system is sound and strongly complete with respect to language EDG.

[TABLE]

Proof

We only show completeness. The proof is almost routine, so we concentrate on how the canonical model is built and on the Truth Lemma for modality $\mathcal{D}_{g}$. Notice that the Axiom of Choice has to be made use of in the proof.

Definition 12 (Canonical Model)

For a fixed language with a set of propositions $\mathbb{P}$ and a set of variables $\mathbb{V}$, we first expand this language to $\mathbb{P}^{C}$ and $\mathbb{V}^{C}$, such that $\mathbb{P}^{C}=\mathbb{P}$, $\mathbb{V}^{C}\supseteq\mathbb{V}$, and that $\mathbb{V}^{C}$ is countably infinite. Obviously, if an MCS is satisfied in the canonical model of the expanded language, its restriction down to the original language will also be satisfied in the same model.

The canonical dependence epistemic model $\mathcal{M}^{C}$ is $\langle S^{C},T^{C},V^{C},U^{C},\sim_{i}^{C},\approx^{C}\rangle$:

• •

$S^{C}$ is the set of all MCSs.

• •

$T^{C}:S^{C}\times\mathbb{P}^{C}\to\{0,1\}$. $\forall s\in S^{C}$, $\forall p\in\mathbb{P}^{C}$, $T^{C}(s,p)=1$ iff $p\in s$.

• •

$V^{C}=\mathbb{V}^{C}$.

• •

$\sim_{i}^{C}$ is an equivalence relation over $S^{C}$. $\forall s,t\in S^{C}$, $s\sim_{i}^{C}t$ iff $\{\mathcal{K}\varphi\mid\mathcal{K}\varphi\in s\}=\{\mathcal{K}\varphi\mid\mathcal{K}\varphi\in t\}$.

• •

$\approx^{C}$ is an equivalence relation over $S^{C}$. $\forall s,t\in S^{C}$, $s\approx^{C}t$ iff $\{\mathcal{A}\varphi\mid\mathcal{A}\varphi\in s\}=\{\mathcal{A}\varphi\mid\mathcal{A}\varphi\in t\}$.

• •

$U^{C}:S^{C}\times V^{C}\to\mathbb{N}$. For each fixed $\approx^{C}$ equivalence class $S_{\approx}\subseteq S^{C}$, we assign $V^{C}$’s values on every possible world $s\in S_{\approx}$ as the following procedure:

By the 4 Axiom for $\mathcal{D}_{g}$ in Theorem 5.1, it is easy to see that if $s\approx^{C}t$, then $\{\mathcal{D}_{g}(X,Y)\mid\mathcal{D}_{g}(X,Y)\in s\}$ = $\{\mathcal{D}_{g}(X,Y)\mid\mathcal{D}_{g}(X,Y)\in t\}$. So suppose arbitrary $s\in S_{\approx}$, $W_{\approx}=\{\text{nonempty finite set }W\mid W\subset\mathbb{V}^{C},\mathcal{Q}_{g}(W)\in s\}$ is a well defined set, regardless of which possible world $s$ we choose from $S_{\approx}$.

Claim

$W_{\approx}$ is countable. Therefore, we can suppose a well order $<_{W}\cong\omega$ on it.

We define a constant function $f_{0}:V^{C}\to\mathbb{N}$, $\forall x\in V^{C}$, $f_{0}(x)=0$.

Lemma 4 (Canonical Assignment)

For every $W\in W_{\approx}$, we can simultaneously find two corresponding functions $f_{1}^{W}:V^{C}\to\mathbb{N}$ and $f_{2}^{W}:V^{C}\to\mathbb{N}$ such that:

• •

$\{f_{1}^{W}(x)\neq f_{2}^{W}(x)\mid x\in V^{C}\}=W$;

• •

if $W_{1},W_{2}\in W_{\approx}$, $W_{1}\neq W_{2}$, then $\{f_{i}^{W_{1}}(x)\neq f_{j}^{W_{2}}(x)\mid x\in V^{C}\}$ is countably infinite, $i,j\in\{1,2\}$;

• •

$\{f_{i}^{W}(x)\neq f_{0}(x)\mid x\in V^{C}\}$* is countably infinite, $i\in\{1,2\}$.*

Proof

Noticing that there are countably infinite variables in $V^{C}$ which can be assigned to countably infinite values, while $W_{\approx}$ is also countable and all the sets $W\in W_{\approx}$ are finite, we are sure that these requirements can be satisfied. For example, we manage to designate $f_{1}^{W}$ and $f_{2}^{W}$ for every $W\in W_{\approx}$ one by one, along the well order $<_{W}$. Since every $W$ is finite, to satisfy the first requirement, the ranges of $f_{1}^{W}$ and $f_{2}^{W}$ can be controlled to be both finite. For the second requirement, if $W_{1}<_{W}W_{2}$, we let the ranges of $f_{i}^{W_{2}}$ and $f_{j}^{W_{1}}$ not intersect. For the third requirement, we let [math] not be in $f_{i}^{W}$’s range.

We collect all these functions as $F_{\approx}=\{f_{i}^{W}\mid W\in W_{\approx},i\in\{1,2\}\}\cup\{f_{0}\}$.

Claim

$F_{\approx}$ is countable. Therefore, we can suppose a well order $<_{F}$ on it.

Then by the Well-ordering Theorem, we can also suppose a well order $<_{S}$ on $S_{\approx}$. By correlating these two well orders $<_{F}$ and $<_{S}$, we can use function $f\in F_{\approx}$ to assign $V^{C}$’s values on possible world $s\in S_{\approx}$, such that $\forall x\in V^{C}$, $U^{C}(s,x)=f(x)$. As any two well orders can be compared, during this correlating procedure, one and only one of the following three conditions will occur:

• •

If $<_{F}\cong<_{S}$, done.

• •

If we first run out of functions from $F_{\approx}$, then we use $f_{0}$ to assign $V^{C}$’s values for all the other left possible worlds in $S_{\approx}$.

• •

If we first run out of possible worlds from $S_{\approx}$, then we arbitrarily choose one possible world $s\in S_{\approx}$, and copy it many times so as to match all the other left functions in $F_{\approx}$. All these copies of $s$, along with the original one, of course share the same $T^{C}$, and are in the same $\sim_{i}^{C}$ and $\approx^{C}$ equivalence classes. Obviously, this copy will not cause any unpleasant consequences.

Lemma 5 (Truth Lemma for Modality $\mathcal{D}_{g}$)

$\forall s\in S^{C}$, $\forall$ finite subsets $X,Y\subset\mathbb{V}^{C}$, $\mathcal{D}_{g}(X,Y)\in s\iff\mathcal{M}^{C},s\vDash\mathcal{D}_{g}(X,Y)$.

Proof

The cases when $X=\emptyset$ or $Y=\emptyset$ follow immediately from the E Axiom for $\mathcal{D}$ in Theorem 5.1, so we concentrate on the situations when $X\neq\emptyset$ and $Y\neq\emptyset$. By Lemma 1, $\mathcal{M}^{C},s\vDash\mathcal{D}_{g}(X,Y)\iff\exists u,v\in S^{C}$, $u\approx^{C}v\approx^{C}s$, such that $\Delta(u,v)$ is an evidence of $\langle X,Y\rangle$.

For the direction from right to left, from the above assignment procedure of $U^{C}$ in the canonical model, we have $\mathcal{Q}_{g}(\Delta(u,v))\in s$. Since $\Delta(u,v)$ is an evidence of $\langle X,Y\rangle$, by making use of the Weakening Rule it is not difficult to reason that $\mathcal{D}_{g}(X,Y)\in s$.

For the direction from left to right, considering the Q Axiom for $\mathcal{D}$ in Theorem 5.1, at least one of the $\mathcal{Q}_{g}(X^{\prime}\cup Y^{\prime})$ in the big disjunction is in $s$, and thus from the above assignment procedure of $U^{C}$ in the canonical model, $\exists u,v\in S^{C}$, $u\approx^{C}v\approx^{C}s$, such that $\Delta(u,v)=X^{\prime}\cup Y^{\prime}$. Since $X^{\prime}\subseteq X,Y^{\prime}\subseteq Y,X^{\prime},Y^{\prime}\neq\emptyset$, obviously $X^{\prime}\cup Y^{\prime}$ is just an evidence of $\langle X,Y\rangle$ and hence $\mathcal{M}^{C},s\vDash\mathcal{D}_{g}(X,Y)$.

6 Conclusions and Future Work

In this paper, we come up with dependence epistemic logic in order to reason about partial dependency relationship between variables under an epistemic scenario. Several interesting examples are proposed, which demonstrate our language’s affluent expressivity and practical usage. Besides that, the essential properties of the logic are straightforward to understand, and hence we further discuss its bisimulation relation and manage to provide a sound and strongly complete axiomatization system for the simpler sub-language EDG.

Nevertheless, there still remains much work to be done in the future. The axiomatization of the full language EDL is yet unknown. It will also be helpful to elaborate on other computational properties of this logic, such as decidability. Besides, as we only deal with the presence of a single agent in this paper, extending this dependence epistemic logic to cases with multiple agents may result in more interesting results. Moreover, it seems to be an exciting idea to add other modalities into this framework so that we will be able to reason about knowing dependency, knowing value, knowing how as well as many other epistemic assertions all together.

Acknowledgements

The author would like to thank Yanjing Wang for proposing the $\approx$ equivalence relation as well as a lot of other useful comments and suggestions on this paper.

The author would like to thank Fan Yang for coming up with the formula in Remark 2.

The author would also like to thank all the teachers and students who have been taking part in the epistemic logic course, from discussions with whom a lot of inspirations have been stimulated.