Negation and Partial Axiomatizations of Dependence and Independence Logic Revisited

Abstract

In this paper, we axiomatize the negatable consequences in dependence and independence logic by extending the natural deduction systems of the logics given in [10, 20]. We give a characterization for negatable formulas in independence logic and negatable sentences in dependence logic, and identify an interesting class of formulas that are negatable in independence logic. Dependence and independence atoms, first-order formulas belong to this class.

Appendices

Appendix I

Proof

(of the direction “$\Longleftarrow$” of Theorem 4.3 ). It suffices to show by induction that $\varGamma \,\models \,\phi$ holds for each derivation D in the extended system with the conclusion $\phi$ and the hypotheses in $\varGamma$. We only give the proof for the induction step when the rule $\mathop {\mathop {\dot{\sim }} \textsf {Tr}}$ is applied. The case when the rule $\mathop {\mathop {\dot{\sim }} \textsf {E}}$ is applied can be proved similarly, and all the other cases follow from the arguments in [20] and in [10].

Assume that $D_2$ is a derivation for $\varDelta ,\exists \vec {x}(\psi \wedge \mathop {\dot{\sim }} \phi )\vdash _{\mathsf {L}}^*\bot$ and $D_1$ is a derivation for $\varPi \vdash _{\mathsf {L}}^*\psi$, where $\mathrm{Fv}(\varDelta )\cap \{x_1,\dots ,x_n\}=\emptyset$. We show that $\varDelta ,\varPi \,\models \,\phi$. By the induction hypothesis, we have $\varDelta ,\exists \vec {x}(\psi \wedge \mathop {\dot{\sim }} \phi )\,\models \,\bot$ and $\varPi \,\models \,\psi$. From the former and Lemma 4.2 we obtain $\varDelta ,\psi \wedge \mathop {\dot{\sim }} \phi \,\models \,\bot$, which is equivalent to $\varDelta ,\psi \,\models \,\phi$. Since $\varPi \,\models \,\psi$, we conclude $\varDelta ,\varPi \,\models \,\phi$, as desired.    $\square$

Appendix II

Fig. 1.

(a) A team X. (b) A team $X[F/\vec {w}]$

Fig. 2.

(a) A team X (b) A team $X[\vec {F_1}/\overrightarrow{w_1}]$ (c) A team $X[\vec {F_1}/\overrightarrow{w_1},\vec {F_2}/\overrightarrow{w_2}]$

Fig. 3.

(a) A team X (b) A team $X[\vec {F_1}/\overrightarrow{w_1}]$ (c) A team $X[\vec {F_1}/\overrightarrow{w_1},\vec {F_2}/\overrightarrow{w_2}]$

Appendix III

Lemma A

Let X be a nonempty team of a model M with $x_1,\dots ,x_m\in \mathrm{dom}(X)$.

• (i) Let $\gamma :X\rightarrow X$ be a choice function. Define inductively functions $F_1,\dots ,F_m$ to simulate assignments in $\gamma [X]$ restricted to $\vec {x}$ on a sequence $\vec {w}=\langle w_1,\dots ,w_m\rangle$ of new variables as follows:

  • –Define the function $F_1:X\rightarrow \wp (M)\setminus \{\emptyset \}$ as $F_1(t)=\{\gamma (t)(x_1)\}$.

  • – For each $2\le i\le m$, define the function $F_i:X[F_1/w_1,\dots ,F_{i-1}/w_{i-1}]\rightarrow \wp (M)\setminus \{\emptyset \}$ as $F_i(t)=\{\gamma (t)(x_i)\}$.

  We call $\vec {F}=\langle F_1,\dots ,F_m\rangle$ the sequence of simulating functions for $\gamma [X]\upharpoonright \vec {x}$ on $\vec {w}$. Let $Y=X[\vec {F}/\vec {w}]$ (see Fig. 1 in Appendix II for an example of such a team with a constant choice function $\gamma (t)=s$ for all $t\in X$, or Fig. 2(b) for another example with an obvious choice function). Then, $t(\vec {w})=\gamma (t)(\vec {x})$ for all $t\in Y$ and $M\models _Y \mathsf {inc}(\vec {w}; \vec {x})$.

  For a sequence $\varGamma =\langle \gamma _1,\dots ,\gamma _k\rangle$ of choice functions $\gamma _i:X\rightarrow X$,

  • – let $\vec {F_1}$ be the sequence of simulating functions for $\gamma _1[X]\upharpoonright \vec {x}$ on $\overrightarrow{w_1}$,

  • – and for each $2\le i\le k$, let $\vec {F_i}$ be the sequence of simulating functions for $\gamma _i[X[\overrightarrow{F_1}/\overrightarrow{w_1},\dots ,\overrightarrow{F_{i-1}}/\overrightarrow{w_{i-1}}]]\upharpoonright \vec {x}$ on $\overrightarrow{w_i}$.

  We call $\vec {F_1},\dots ,\vec {F_k}$ the group of simulating functions for $\varGamma [X]\upharpoonright \vec {x}$ on $\overrightarrow{w_1},\dots ,\overrightarrow{w_k}$, and the team $Y=X[\vec {F_1}/\overrightarrow{w_1},\dots ,\vec {F_{k}}/\overrightarrow{w_{k}}]$ its associated team (see Fig. 2 in Appendix II for examples of such teams). Then, $M\models _Y \mathsf {inc}(\overrightarrow{w_1},\dots ,\overrightarrow{w_k}; \vec {x})$.

• (ii) Define inductively functions $F_1,\dots ,F_m$ to duplicate assignments in X restricted to $\vec {x}$ on a sequence $\vec {w}=\langle w_1,\dots ,w_m\rangle$ of new variables as follows:

  • – Define the function $F_1:X\rightarrow \wp (M)\setminus \{\emptyset \}$ as $F_1(t)=\{s(x_1)\mid s\in X\}$.

  • – For each $2\le i\le m$, define the function $F_{i}:X[F_{1}/w_{1},\dots ,F_{i-1}/w_{i-1}]\rightarrow \wp (M)\setminus \{\emptyset \}$ as

    $$\begin{aligned} F_i(t)=\{s(x_i)\mid s\in X\text { and } s\upharpoonright \{x_1,\dots ,x_{i-1}\}=t\upharpoonright \{w_1,\dots ,w_{i-1}\}\}. \end{aligned}$$

  We call $\vec {F}=\langle F_1,\dots ,F_m\rangle$ the sequence of duplicating functions for $X\upharpoonright \vec {x}$ on $\vec {w}$. (see Fig. 3(b) in Appendix II for an example of a team $X[\vec {F}/\vec {w}]$). For a team X,

  • – let $\vec {F_1}$ be the sequence of duplicating functions for $X\upharpoonright \vec {x}$ on $\overrightarrow{w_1}$,

  • – and for each $i=2,\dots ,k$, let $\vec {F_i}$ be the sequence of duplicating functions for $X[\overrightarrow{F_1}/\overrightarrow{w_1},\dots ,\overrightarrow{F_{i-1}}/\overrightarrow{w_{i-1}}]\upharpoonright \vec {x}$ on $\overrightarrow{w_i}$.

  We call $\vec {F_1},\dots ,\vec {F_k}$ the group of duplicating functions for $X\upharpoonright \vec {x}$ on $\overrightarrow{w_1},\dots ,\overrightarrow{w_k}$. and the team $Y=X[\vec {F_1}/\overrightarrow{w_1},\dots ,\vec {F_{k}}/\overrightarrow{w_{k}}]$ its associated team (see Fig. 3 in Appendix II for examples of such teams). Then, $M\models _Y \mathsf {pro}(\vec {y};\vec {x};\overrightarrow{w_1},\dots ,\overrightarrow{w_k})$ for any sequence $\vec {y}$ of variables in $\mathrm{dom}(X)$ that has no variable in common with $\vec {x}$ and $\overrightarrow{w_1},\dots ,\overrightarrow{w_k}$, and for any $t\in Y$, there exist $s_1,\dots ,s_k\in X$ such that $s_1(\vec {x})=t(\overrightarrow{w_1}),\dots ,s_k(\vec {x})=t(\overrightarrow{w_k})$.

Proof

We only give the detailed proof for $M\models _Y \mathsf {pro}(\vec {y};\vec {x};\overrightarrow{w_1},\dots ,\overrightarrow{w_k})$ in the item (ii), i.e.,

$$\begin{aligned} M\models _Y\bigwedge _{i=1}^k(\vec {x}\subseteq \overrightarrow{w_i})\wedge \left( \bigwedge _{i=1}^{k} (\langle \overrightarrow{w_{j}}\mid j\ne i\rangle \perp \overrightarrow{w_{i}})\right) \wedge (\vec {y}\perp \overrightarrow{w_1}\dots \overrightarrow{w_k}) \end{aligned}$$

(7)

To show that Y satisfies the first conjunct of the formula in (7), it suffices to show that $M\models _{Y_i}\vec {x}\subseteq \overrightarrow{w_i}$ for each $1\le i\le k$ and $Y_i=X[\vec {F_1}/\overrightarrow{w_1},\dots ,\vec {F_{i}}/\overrightarrow{w_{i}}]$.

For any $t\in Y_i$, by the definition of $Y_i=Y_{i-1}[\vec {F_i}/\overrightarrow{w_i}]$, there exists $s\in X$ such that $s(\vec {x})=t(\vec {x})$, and

$$\begin{aligned} t'=s\cup \{(w_{i,1},s(x_1)),\dots ,(w_{i,m},s(x_{m}))\}\in Y_{i-1}[F_{i,1}/w_{i,1},\dots ,F_{i,m}/w_{i,m}] \end{aligned}$$

Thus, $t'(\overrightarrow{w_i})=s(\vec {x})=t(\vec {x})$, as required.

To prove that Y satisfies the second and the third conjuncts of the formula in (7), we prove a more general property that $M\models _Y\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}}\perp \overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}v_1\dots v_c$ holds for any disjoint subsequences $\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}}$ and $\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}$ of $\overrightarrow{w_1}\dots \overrightarrow{w_k}$ and any variables $v_1\dots v_c\in \mathrm{dom}(X)$. Assume that $\{\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}},\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}\}=\{\overrightarrow{w_{l_1}}\dots \overrightarrow{w_{l_d}}\}$ with $l_1<\dots <l_d$.

Let $s,s'\in Y$ be arbitrary. We need to find an $s''\in Y$ such that $s''(\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}})=s(\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}})$ and $s''(\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}v_1\dots v_c)=s'(\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}v_1\dots v_c)$. Let f be a function satisfying

$$\begin{aligned} f(\overrightarrow{w_{l_\xi }})={\left\{ \begin{array}{ll} s(\overrightarrow{w_{l_\xi }})&{} \text {if }l_\xi \in \{i_1,\dots ,i_a\}\\ s'(\overrightarrow{w_{l_\xi }})&{}\text { if }l_\xi \in \{j_1,\dots ,j_b\} \end{array}\right. } \end{aligned}$$

There exists $s_1\in X$ such that $s_1(\vec {x})=f(\overrightarrow{w_{l_1}})$. Put $Y_{l_1-1}=X[\overrightarrow{F_1}/\overrightarrow{w_1},\dots ,\overrightarrow{F_{l_1-1}}/\overrightarrow{w_{l_1-1}}]$ and $t=s'\upharpoonright \mathrm{dom}(Y_{l_1-1})$. By the construction,

$$\begin{aligned} t_{l_1}=t\cup \{(w_{l_1,1},s_1(x_1)),\dots ,(w_{l_1,m},s_1(x_m))\}\in Y_{l_1-1}[\overrightarrow{F_{l_1}}/\overrightarrow{w_{l_1}}]=Y_{l_1}. \end{aligned}$$

Thus

$$\begin{aligned} t_{l_1}(\overrightarrow{w_{l_1}})=s_1(\vec {x})=f(\overrightarrow{w_{l_1}})\text { and }t_{l_1}(\vec {v})=t(\vec {v})=s'(\vec {v}). \end{aligned}$$

Repeat the same argument for $f(\overrightarrow{w_{l_2}}),\dots ,f(\overrightarrow{w_{l_d}})$, we can find $t_{l_d}\in Y_{l_d}$ such that

$$\begin{aligned} t_{l_d}(\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}})=s(\overrightarrow{w_{i_1}}\dots \overrightarrow{w_{i_a}})\text { and }t_{l_d}(\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}v_1\dots v_c)=s'(\overrightarrow{w_{j_1}}\dots \overrightarrow{w_{j_b}}v_1\dots v_c). \end{aligned}$$

Finally, by the construction of Y, there exists $s''\in Y$ such that $s''\upharpoonright \mathrm{dom}(Y_{l_d})=t_{l_d}$. Hence, $s''$ is the desired assignment.    $\square$