# Dependence logic ## Syntax >[!info] Definition - atomic formulas >Let $\tau$ be a vocabulary. $t,t_{i}\dots$ denote terms, $\bar{t},\bar{t}_{i}\dots$ denote tuples of $\tau$-terms, $R$ is a relation in $\tau$. >1. *First order literals* are formulas of the form $_{1}=t_{2} \mid R\bar{t} \mid \neg t_{1}=t_{2} \mid \neg R \bar{t}$ >2. A *dependence atom* is a formula of the form $=\!(\bar{t},t')$. > The formula $=\!(t')$ is called a *constancy atom*. > 2. An *inclusion atom* is a formula of the form $\bar{t}_{1} \subseteq \bar{t}_{2}$. > Here $\bar{t}_{1}, \bar{t}_{2}$ are of the same length. > 3. An *exclusion atom* is a formula of the form $\bar{t}_{1} \mid \bar{t}_{2}$. > 4. A *(conditional) independence atom* is a formula of the form $\bar{t}_{2} \bot_{\bar{t}_{1}} \bar{t}_{3}$. > If $\bar{t}_{1}=\varnothing$ we write $\bar{t}_{2} \bot \bar{t}_{3}$ and this is called a *pure independence atom*. >[!info] Definition >The set of $\tau$-formulas of *dependence logic* $\mathrm{FO(dep)}$ is defined as >$ > \phi ::=\quad =\!(\bar{t},t') \mid t_{1}=t_{2} \mid R\bar{t} \mid \neg t_{1}=t_{2} \mid \neg R \bar{t} \mid (\phi \land \phi) \mid (\phi \lor \phi) \mid \exists x \phi \mid \forall x \phi >$ >Similarly define *independence logic* $\mathrm{FO(ind)}$, *inclusion logic* $\mathrm{FO(inc)}$ and *exclusion logic* $\mathrm{FO(exc)}$. >[!note] Remark >Note that there is no general negation of formulas - only of first order atomic formulas. Adding Boolean negation extends the logic. >Similarly there is no basic notion of implication - several types of implication can be considered as extensions. ## Team semantics >[!info] Definition >Let $\mathcal{M}$ be a model and $V$ a set of variables. A *team* $X$ of $\mathcal{M}$ with domain $V$ is a set of assignments $s:V \to M$. >[!info] Definition - semantics of atomic formulas >Let $\tau$ be a vocabulary, $\mathcal{M}$ a $\tau$-model, $X$ a team of $\mathcal{M}$. > 1. $\mathcal{M}\models_{X} \ =\!(\bar{t},t')$ if for all $s,s' \in X$, if $s(\bar{t}) = s'(\bar{t})$ then $s(t')=s'(t')$. > 2. $\mathcal{M} \models_{X} \ \bar{t}_{1} \subseteq \bar{t}_{2}$ if for all $s \in X$ there is $s'\in X$ s.t. $s(\bar{t}_{1})= s'(\bar{t}_{2})$. > 3. $\mathcal{M} \models_{X} \ \bar{t}_{1} \mid \bar{t}_{2}$ if for all $s,s' \in X$, $s(\bar{t}_{1})\ne s'(\bar{t}_{2})$. > 4. $\mathcal{M} \models_{X} \ \bar{t}_{2} \bot_{\bar{t}_{1}} \bar{t}_{3}$ if for all $s,s' \in X$ s.t. $s(\bar{t}_{1}) = s'(\bar{t}_{1})$, there is $s''\in X$ s.t. > - $s''(\bar{t}_{1})=s(\bar{t}_{1})=s'(\bar{t}_{1})$, > - $s''(\bar{t}_{2})=s(\bar{t}_{2})$, > - $s''(\bar{t}_{3})=s'(\bar{t}_{3})$. >[!info] Definition >Let $\mathcal{M}$ be a model. Denote $\mathcal{P}^{+}(M)= \mathcal{P}(M)\smallsetminus \{\varnothing\}$. >Given a team $X$ and a function $F: X \to \mathcal{P}^{+}(M)$, define: > 1. The *supplement team of $X$ over $y$ with $F$*: $X(F/y)=\{ s(a/y) \mid s \in X, a \in F(s)\}$. > 2. The *duplicate team of $X$ over $y$*: $X(M/y)=\{ s(a/y) \mid s \in X, a \in M\}$. >[!info] Definition - Team semantics > Let $\mathcal{M}$ be a model, $X$ a team, $\phi$ a formula with $\mathrm{Fv}(\phi) \subseteq \mathrm{dom} X$. We define when $\mathcal{M}\models_{X} \phi$: > 1. $\phi$ is a first order literal: for all $s\in X$ $\mathcal{M}\models_{s} \phi$ > 2. $\phi$ is a non-first-order atom: see above > 3. $\phi=\psi_{1} \land \psi_{2}$: $\mathcal{M}\models_{X} \psi_{i}$ for $i=1,2$. > 4. $\phi = \psi_{1} \lor \psi_{2}$: there exists $Y,Z \subseteq X$ s.t. $Y \cup Z = X$, $\mathcal{M}\models_{Y} \psi_{1}$ and $\mathcal{M}\models_{Z} \psi_{2}$. > 5. $\phi = \exists x \psi$: There exists $F:X \to \mathcal{P}^{+}(M)$ s.t $\mathcal{M} \models_{X(F/x)} \psi$ > 6. $\phi = \forall x \psi$: $\mathcal{M} \models_{X(M/x)} \psi$ > [!info] Terminology > $\phi,\psi$ sentences, $\Gamma$ a set of sentences. > - $\phi$ is *true* in $\mathcal{M}$, $\mathcal{M}\models \phi$, if for all teams $X$, $\mathcal{M}\models_{X}\phi$ > - $\phi$ is *valid* if for all $\mathcal{M}$, $\mathcal{M}\models \phi$ > - $\phi$ is a *logical consequence* of $\Gamma$, $\Gamma \models \phi$, if for every $\mathcal{M},X$, $\mathcal{M}\models_{X}\Gamma$ implies $\mathcal{M}\models_{X}\phi$ > - $\phi,\psi$ are *logically equivalent*, $\phi \equiv \psi$, iff $\phi \models \psi$ and $\psi \models \phi$ **Theorem (Empty team property).** For every model $\mathcal{M}$ and formula $\phi$, $\mathcal{M} \models_{\varnothing} \phi$ **Theorem (Locality).** Let $\phi$ be a formula, $V \supseteq \mathrm{Fv}(\phi)$ an $\mathcal{M}$ a model. Then for all teams $X,Y$ s.t. $\mathrm{dom}(X),\mathrm{dox}(Y) \supseteq V$ and $X {\restriction}V = Y {\restriction}V$, $\mathcal{M} \models_{X}\phi \iff \mathcal{M}\models_{Y} \phi$. ### Closure properties >[!info] Definition >A formula $\phi$ is said to be: >1. *Closed downwards* if $\mathcal{M} \models_{X}\phi$ and $Y \subseteq X$ then $\mathcal{M}\models_{Y}\phi$; >2. *Closed under unions* if $\mathcal{M}\models_{X_{i}}$ for all $i\in I$ then $\mathcal{M}\models_{\bigcup_{i \in I}X_{i}}\phi$; >3. *Flat* if $\mathcal{M} \models_{X}\phi$ iff for all $s\in X$, $\mathcal{M} \models_{s} \phi$. >[!example] Anti-examples >1. $=\!(x,y)$ is not closed under unions >2. $x \subseteq y$ is not downward closed **Theorem.** A formula $\phi$ is flat iff it has the empty team property, is closed downwards, and is closed under unions. **Theorem.** 1. Formulas of $\mathrm{FO}(\mathrm{dep,exc})$ are downward closed 2. Formulas of $\mathrm{FO(inc)}$ are closed under unions 3. Formulas of $\mathrm{FO}$ are flat >[!warning] >Many of the usual rules of f.o. logic (e.g. de-Morgan laws, quantifier extraction etc) hold, but some depend on the closure properties of the formulas in question. In particular equivalences involving disjunction often work only for downward closed formulas. ### Prenex normal form **Theorem (Replacement/substitution).** Let $\theta$ be a formula in which $\phi$ occurs positively, and let $\theta[\psi/\phi]$ be the formula obtained by replacing $\phi$ by $\psi$ in $\theta$. If $\phi \vDash \psi$ then $\theta \vDash \theta[\psi/\phi]$. **Theorem.** Any formula can be put in prenex normal form. Remark. However there might be a need to add quantifiers. **Proposition.** If $\varphi$ is a formula of $\mathrm{FO(dep)}$, then $ \exists x \forall y \varphi(x,y,\bar{v}) \equiv \forall y \exists x (=\!(\bar{v},x)\land \varphi) $ **Proposition.** If $\varphi$ is a formula of $\mathrm{FO(inc)}$ then there is a quantifier free $\psi$ s.t. $\varphi \equiv \exists \bar{x} \forall y \psi$. >[!note] Remark >This means that quantifier alternation cannot measure the complexity of formulas. ### First order formulas **Lemma.** Let $\alpha\in \mathrm{FO}$. For any model $\mathcal{M}$ and assignment $s$ s.t. $\mathrm{Fv}(\alpha) \subseteq \mathrm{Dom}(s)$, $ \mathcal{M} \models_{\{s\}} \alpha \iff \mathcal{M}\models_{s} \alpha $ where on the left we have Team semantics and on the right ordinary Tarski semantics. **Corollary.** For $\Gamma \cup \{\alpha\} \subseteq \mathrm{FO}$, 1. $\mathcal{M}\models_{X}\alpha$ iff $\forall s \in X \ \mathcal{M}\models_{\{s\}}\alpha$ 2. $\Gamma \models_{Team} \alpha$ iff $\Gamma \models_{classic}\alpha$ >[!note] Notation >For first order $\alpha,\beta$, general $\phi,\psi$, we can define additional connectives: > - $\neg \alpha$ is defined as the formula $\alpha^{d}$ - the dual of $\alpha$ (obtained by the classical laws of pushing the negation inside). > - $\alpha \to \beta := \neg \alpha \lor \beta$ > - *Maximal implication*: $\mathcal{M}\models_{X} \phi \hookrightarrow \psi$ iff For any maximal subteam $Y \subseteq X$ with $\mathcal{M}\models_{Y}$, it holds that $\mathcal{M}\models_{Y} \psi$. **Lemma.** For first order $\alpha,\beta$, general $\phi,\psi$ 1. $\mathcal{M} \models_{X} \neg \alpha$ iff $\mathcal{M}\models_{s} \neg \alpha$ for all $s\in X$ iff $\mathcal{M} \not\models_{s} \alpha$ for every $s\in X$. 2. $\mathcal{M} \models_{X}\alpha \to \beta$ iff for all $s\in X$, $\mathcal{M}\models_{s}\alpha$ implies $\mathcal{M} \models_{s}\psi$. 3. $\alpha \hookrightarrow \psi \equiv \neg \alpha \lor (\alpha \land \psi)$ 4. If $\psi$ is flat then $\alpha \hookrightarrow \psi \equiv \neg \alpha \lor \psi$ ### Flattening **Theorem.** 1. $\mathcal{M}\models_{s}\ =\!(\bar{t},t')$, $\mathcal{M}\models_{s}\ \bar{t}_{2} \bot_{\bar{t}_{1}} \bar{t}_{3}$ always hold. 2. $\mathcal{M}\models_{s} \bar{t} \subseteq \bar{s} \iff \mathcal{M}\models_{s} \bar{t}=\bar{s}$ 3. $\mathcal{M}\models_{s} \bar{t}\mid \bar{s} \iff \mathcal{M}\models_{s} \neg \bar{t} = \bar{s}$