Proof The second “ $\iff $ ” follows from a straightforward inductive argument that uses directly the similarity of the team semantics of $\mathbf {FOT} $ -connectives and quantifiers and the Tarskian semantics of their counterparts in $\mathbf {FO} $ . We now prove the first “ $\iff $ ” by induction on $\alpha $ . We only give the detailed proof for the non-trivial cases.

If $\alpha =\beta \vee \gamma $ , then

(by empty team property) $$ \begin{align} M\models_{\{s\}}\beta\vee\gamma&\iff \exists Y,Z\subseteq \{s\}\text{ s.t. }X=Y\cup Z,~ M\models_Y\beta\text{ and }M\models_Z\gamma \nonumber \\ &\iff M\models_{\{s\}}\beta\text{ or }M\models_{\{s\}}\gamma \end{align} $$

(by induction hypothesis) $$ \begin{align} &\iff M\models_s\beta\vee\gamma. \end{align} $$

If $\alpha =\forall x\beta $ , then

(by flatness) $$ \begin{align} M\models_{\{s\}}\forall x\beta &\iff M\models_{\{s\}(M/x)}\beta\nonumber \\ &\iff M\models_{\{s(a/x)\}}\beta\text{ for all }a\in M \end{align} $$

(by induction hypothesis) $$ \begin{align} &\iff M\models_{s(a/x)}\beta\text{ for all }a\in M \\ &\iff M\models_{s}\forall x\beta. \notag \end{align} $$

If $\alpha =\exists x\beta $ , then

(by downward closure) $$ \begin{align} M\models_{\{s\}}\exists x\beta&\iff M\models_{\{s\}(F(s)/x)}\beta\text{ for some }F:\{s\}\to \wp^+(M) \nonumber\\ &\iff M\models_{\{s(a/x)\}}\beta\text{ for some }a\in M\end{align} $$

(by induction hypothesis) $$ \begin{align} &\iff M\models_{s(a/x)}\beta\text{ for some }a\in M \\ &\iff M\models_{s}\exists x\beta.\notag \end{align} $$

Proof We only give the detailed proof for item (i). We have that

(by definition of inclusion atom and flatness)

(by locality) $$ \begin{align} &\iff \text{for all sequences }\mathsf{a}\in\{s(\mathsf{x})\mid s\in X\},~ M\models_{\{\emptyset(\mathsf{a}/\mathsf{x})\}}\alpha^{\ast}(\mathsf{x})\qquad\qquad\qquad \nonumber \\ & \iff \text{for all } s \in X, ~M\models_{\{s\}}\alpha^{\ast}(\mathsf{x}) \end{align} $$

(by Lemma 2.1) $$ \begin{align} &\iff \text{for all } s \in X, ~M\models_{\{s\}}\alpha(\mathsf{x})\quad\qquad\quad\qquad\qquad\qquad\quad \ \end{align} $$

(by flatness) $$ \begin{align} &\iff M\models\alpha(\mathsf{x}).\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\quad\quad \ \end{align} $$

Proof We prove the theorem by proving a slightly more general claim: For any subformula $\theta (\mathsf {v},\mathsf {x})$ of $\phi (\mathsf {v})$ , there exists a first-order $\mathcal {L} (R)$ -formula $\gamma _{\theta }(R,\mathsf {x})$ such that for all $\mathcal {L} $ -models M, teams X, and sequences $\mathsf {a}$ of elements in M,

(4) $$ \begin{align} M \models_{X(\mathsf{a}/\mathsf{x})} \theta(\mathsf{v},\mathsf{x}) \iff (M, rel(X)) \models \gamma_{\theta}(R,\mathsf{x})(\mathsf{a}/\mathsf{x}). \end{align} $$

Define the formula $\gamma _{\theta }$ (found essentially in, e.g., [Reference Galliani15, Reference Yang41]) inductively as follows:

• • If $\theta (\mathsf {v},\mathsf {x})=\lambda (\mathsf {v},\mathsf {x})$ is a first-order atom, let $\gamma _{\theta }(R,\mathsf {x})=\forall \mathsf {v}(R\mathsf {v}\to \lambda (\mathsf {v},\mathsf {x}))$ .

• • If $\theta (\mathsf {v},\mathsf {x})=\neg \delta (\mathsf {v},\mathsf {x})$ for some quantifier-free and disjunction-free first-order formula $\delta $ , let $\gamma _{\theta }(R,\mathsf {x})=\forall \mathsf {v}(R\mathsf {v}\to \neg \delta (\mathsf {v},\mathsf {x}))$ .

• • If $\theta (\mathsf {v},\mathsf {x})=\rho (\mathsf {vx})\subseteq \sigma (\mathsf {vx})$ , where $\rho (\mathsf {vx})$ and $\sigma (\mathsf {vx})$ are two sequences of variables from $\mathsf {vx}$ , let $\gamma _{\theta }(R,\mathsf {x})=\forall \mathsf {u}\exists \mathsf {w}\big (R\mathsf {u}\to ( R\mathsf {w}\wedge \rho (\mathsf {ux})=\sigma (\mathsf {wx}))\big )$ , where $\mathsf {u}$ and $\mathsf {w}$ are two sequences of fresh variables.

• • If $\theta (\mathsf {v},\mathsf {x})=\theta _0(\mathsf {v},\mathsf {x})\wedge \theta _1(\mathsf {v},\mathsf {x})$ , let $\gamma _{\theta }(R,\mathsf {x})=\gamma _{\theta _0}(R,\mathsf {x})\wedge \gamma _{\theta _1}(R,\mathsf {x})$ .

• • If , let $\gamma _{\theta }(R,\mathsf {x})=\gamma _{\theta _0}(R,\mathsf {x})\vee \gamma _{\theta _1}(R,\mathsf {x})$ .

• • If $\theta (\mathsf {v},\mathsf {x})=\mathop {\dot \sim } \theta _0(\mathsf {v},\mathsf {x})$ , let $\gamma _{\theta }(R,\mathsf {x})= \forall \mathsf {v}\neg R\mathsf {v}\vee \neg \gamma _{\theta _0}(R,\mathsf {x})$ .

• • If $\theta (\mathsf {v},\mathsf {x})=\exists ^1 y\theta _0(\mathsf {v},\mathsf {x}y)$ , let $\gamma _{\theta }(R,\mathsf {x})=\exists y\gamma _{\theta _0}(R,\mathsf {x}y)$ .

• • If $\theta (\mathsf {v},\mathsf {x})=\forall ^1 y\theta _0(\mathsf {v},\mathsf {x}y)$ , let $\gamma _{\theta }(R,\mathsf {x})=\forall y\gamma _{\theta _0}(R,\mathsf {x}y)$ .

We only give the detailed proof of (4) for some nontrivial cases. If $\theta (\mathsf {v},\mathsf {x})=\lambda (\mathsf {v},\mathsf {x})$ is a first-order atom, then we have that

$$ \begin{align*} M\models_{X(\mathsf{a}/\mathsf{x})}\lambda(\mathsf{v},\mathsf{x})&{\iff} M\models_{s}\lambda(\mathsf{v},\mathsf{x})\text{ for all }s\in X(\mathsf{a}/\mathsf{x})\\ &{\iff} (M,rel(X))\!\models_{s(\mathsf{a}/\mathsf{x})}\! R\mathsf{v}{\to} \lambda(\mathsf{v},\mathsf{x})\text{ for all }s:\{v_1,\dots,v_k\}{\to} M\\ &{\iff} (M,rel(X))\models \forall \mathsf{v}(R\mathsf{v}\to \lambda(\mathsf{v},\mathsf{x}))(\mathsf{a}/\mathsf{x}). \end{align*} $$

If $\theta =\mathop {\dot \sim } \theta _0$ , then we have that

(by induction hypothesis) $$ \begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\mathop{\dot\sim}\theta_0&\iff X(\mathsf{a}/\mathsf{x})=\emptyset \text{ or }M\not\models_{X(\mathsf{a}/\mathsf{x})}\theta_0 \nonumber \\ &\iff (M,rel(X))\models\forall \mathsf{v}\neg R\mathsf{v}\text{ or }(M, rel(X)) \not\models \gamma_{\theta_0}(R,\mathsf{x})(\mathsf{a}/\mathsf{x}) \\ &\iff (M, rel(X)) \models \forall \mathsf{v}\neg R\mathsf{v}\ \vee \neg \gamma_{\theta_0}(R,\mathsf{x})(\mathsf{a}/\mathsf{x}).\notag \end{align} $$

If $\phi =\exists ^1 y\theta _0(\mathsf {v},\mathsf {x}y)$ , then we have that

(by induction hypothesis) $$ \begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\exists^1 y\theta_0(\mathsf{v},\mathsf{x}y)&\iff M\models_{X(\mathsf{a}b/\mathsf{x}y)}\theta_0(\mathsf{v},\mathsf{x}y)\text{ for some }b\in M \nonumber \\ &\iff (M, rel(X)) \models \gamma_{\theta_0}(R,\mathsf{x}y)(\mathsf{a}b/\mathsf{x}y)\text{ for some }b\in M \\ &\iff (M,rel(X))\models\exists y\gamma_{\theta_0}(R,\mathsf{x})(\mathsf{a}/\mathsf{x}).\notag \end{align} $$

Proof We may assume w.l.o.g. that the first-order sentence $\gamma (R)$ is in prenex normal form $Q_1x_1\dots Q_nx_n\alpha (\mathsf {x})$ , where $Q_i\in \{\forall ,\exists \}$ , $\alpha $ is quantifier-free and in negation normal form (i.e., negation occurs only in front of atomic formulas), and every occurrence of R is of the form $R\mathsf {x}_i$ for some sequence $\mathsf {x}_i$ of bound variables (for $R\mathsf {t}\equiv \exists \mathsf {y}(\mathsf {y}=\mathsf {t}\wedge R\mathsf {y})$ ). Define the translation $\phi _{\gamma }(\mathsf {v}):=Q_1^1x_1\dots Q_n^1x_n\phi _{\alpha }(\mathsf {x},\mathsf {v})$ , where $Q_i^1=\forall ^1 $ if $Q_i=\forall $ , $Q_i^1=\exists ^1 $ if $Q_i=\exists $ , and $\phi _{\alpha }(\mathsf {x},\mathsf {v})$ is obtained from $\alpha (\mathsf {x})$ by first taking the corresponding formula $\alpha ^{\ast }(\mathsf {x})$ in $\mathbf {FOT} $ and then replacing every first-order atom of the form $R\mathsf {x}_i$ by $\mathsf {x}_i\subseteq \mathsf {v}$ . We show by induction that for any quantifier-free formula $\alpha (\mathsf {x})$ , any nonempty team X over $\{v_1,\dots ,v_k\}$ and $a_1,\dots ,a_n\in M$ ,

(5) $$ \begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\phi_{\alpha}(\mathsf{x},\mathsf{v})\iff (M,rel(X))\models\alpha(\mathsf{a}/\mathsf{x}). \end{align} $$

We only give the detailed proof for the nontrivial cases. If $\alpha =\lambda (\mathsf {x})$ is an atomic formula in which R does not occur, then $\phi _{\lambda }=\lambda (\mathsf {x})$ and

(since X≠∅ and R does not occur in λ) $$\begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\lambda(\mathsf{x})&\iff M\models_{X}\lambda(\mathsf{a}/\mathsf{x}) \nonumber \\ &\iff M\models_{s}\lambda(\mathsf{a}/\mathsf{x})\text{ for all }s\in X \nonumber \\ &\iff M\models\lambda(\mathsf{a}/\mathsf{x}) \\ &\iff (M,rel(X))\models\lambda(\mathsf{a}/\mathsf{x}).\notag \end{align} $$

If $\alpha =R\mathsf {x}_{i}$ , then $\phi _{\alpha }=\mathsf {x}_i\subseteq \mathsf {v}$ and

(since X≠∅) $$\begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\mathsf{x}_{i}\subseteq \mathsf{v} {\iff}& \text{for all }s{\,\in\,} X(\mathsf{a}/\mathsf{x}),\text{ there exists }s'{\,\in\,} X(\mathsf{a}/\mathsf{x})\text{ s.t. }s(\mathsf{x}_{i})=s'(\mathsf{v}) \nonumber \\ \iff& \mathsf{a}_{i}\in rel(X)=\{s'(\mathsf{v})\mid s'\in X\} \\ \iff& (M,rel(X))\models R\mathsf{x}_{i}(\mathsf{a}/\mathsf{x}).\notag \end{align} $$

If $\alpha =\neg \lambda (\mathsf {x})$ , then $\phi _{\alpha } = \mathop {\dot \sim } \phi _{\lambda }(\mathsf {x},\mathsf {v})$ and

(since X (a/x) ≠ ∅) $$\begin{align} M\models_{X(\mathsf{a}/\mathsf{x})}\mathop{\dot\sim}\phi_{\lambda}(\mathsf{x},\mathsf{v})&\iff M\not\models_{X(\mathsf{a}/\mathsf{x})}\phi_{\lambda}(\mathsf{x},\mathsf{v})\end{align}$$

(by induction hypothesis) $$ \begin{align} &\iff (M,rel(X))\not\models{\lambda}(\mathsf{a}/\mathsf{x}) \\ &\iff (M,rel(X))\models\neg{\lambda}(\mathsf{a}/\mathsf{x}).\notag \end{align} $$

Finally, we have that

(by 5) $$ \begin{align} &M\models_X Q_1^1x_1\dots Q_n^1x_n\phi_{\alpha}(\mathsf{x},\mathsf{v}) \nonumber \\ \iff& Q_1a_1\in M\dots Q_n a_n\in M:~M\models_{X(\mathsf{a}/\mathsf{x})}\phi_{\alpha}(\mathsf{x},\mathsf{v})\nonumber \\ \iff& Q_1a_1\in M\dots Q_n a_n\in M:~(M,rel(X))\models\alpha(\mathsf{a}/\mathsf{x}) \\ \iff& (M,rel(X))\models Q_1x_1\dots Q_nx_n\alpha(\mathsf{x}).\notag \end{align} $$

This completes the proof for the translation into $\mathbf {FOT} $ . Now, if R occurs only negatively in $\gamma $ (thus also in $\alpha $ ), we can define alternatively the translation into $\mathbf {FOT}^{\downarrow } $ by redefining the following two cases:

If $\alpha =\neg R\mathsf {x}_{i}$ , define alternatively $\phi _{\alpha }:=\mathsf {x}_{i}\neq \mathsf {v}$ (which is defined as $\neg \bigwedge _{j\in J}\,x_{ij}=v_j)$ , and we have that

$$ \begin{align*} M\models_{X(\mathsf{a}/\mathsf{x})}\mathsf{x}_{i}\neq\mathsf{v}&\iff \text{for all }s\in X(\mathsf{a}/\mathsf{x}),~s(\mathsf{x}_{i})\neq s(\mathsf{v})\\ &\iff \text{for all }s\in X,~\mathsf{a}_{i}\neq s(\mathsf{v})\\ &\iff \mathsf{a}_{i}\notin rel(X)=\{s(\mathsf{v})\mid s\in X\}\\ &\iff (M,rel(X))\models\neg R\mathsf{x}_{i}(\mathsf{a}/\mathsf{x}). \end{align*} $$

If $\alpha :=\delta (\mathsf {x})$ is a literal (atomic or negated atomic formula) that does not contain R, define alternatively $\phi _{\alpha }=\delta (\mathsf {x})$ . It is easy to verify that (5) still holds.

Proof “ $\Longleftarrow $ ”: Suppose $\alpha $ is a first-order $\mathcal {L} (R)$ -sentence in which the k-ary predicate R occurs only negatively, and we assume w.l.o.g. that $\alpha $ is in negation normal form. We can show by induction that $\alpha $ is downward closed with respect to R. The only nontrivial case is when $\alpha =\neg R\mathsf {t}$ . In this case, for any model M, any $A\subseteq B\subseteq M^k$ , and any assignment s,

$$\begin{align*}(M,B)\models_s \neg R\mathsf{t}\Longrightarrow s(\mathsf{t}^M)\notin B\Longrightarrow s(\mathsf{t}^M)\notin A\Longrightarrow (M,A)\models_s \neg R\mathsf{t}. \end{align*}$$

“ $\Longrightarrow $ ”: Suppose that $\alpha $ is a first-order $\mathcal {L} (R)$ -sentence that is downward closed with respect to R. It is easy to see that $\alpha \equiv \exists S(\alpha (S/R)\wedge \forall \mathsf {x}(R\mathsf {x}\to S\mathsf {x})),$ where $\alpha (S/R)$ is obtained from $\alpha $ by replacing every occurrence of R by S. Put $\gamma =\alpha (S/R)\wedge \forall \mathsf {x}(R\mathsf {x}\to S\mathsf {x})$ , and note that R occurs only negatively in $\gamma $ . Then $\gamma \models \alpha $ . Now, by Lyndon’s Interpolation Theorem, there is a first-order $\mathcal {L} (R)$ -sentence $\beta (R)$ such that $\gamma (R,S)\models \beta (R)$ and $\beta (R)\models \alpha (R)$ , and moreover, R occurs only negatively in $\beta $ . It remains to show $\alpha \models \beta $ . For any $\mathcal {L} (R)$ -model $(M,A)$ such that $(M,A)\models \alpha (R)$ , the $\mathcal {L} (R,S)$ -model $(M,A,A)$ clearly satisfies $(M,A,A)\models \alpha (S/R)\wedge \forall \mathsf {x}(R\mathsf {x}\to S\mathsf {x})$ , i.e., $(M,A,A)\models \gamma (R,S)$ . Since $\gamma \models \beta $ , we conclude $(M,A,A)\models \beta (R)$ , thereby $(M,A)\models \beta (R)$ .

Proof Let $\mathcal {L} $ be the vocabulary of $\Gamma $ and $\mathsf {Fv}(\Gamma )=\{v_n\mid n\in \mathbb {N}\}$ . By assumption, for every $\phi \in \Gamma $ , there is an $\mathcal {L} (R_{\phi })$ -sentence $\gamma _{\phi }(R_{\phi })$ in $\mathbf {ESO} $ with a fresh $|\mathsf {Fv}(\phi )|$ -ary relation symbol $R_{\phi }$ such that for every $\mathcal {L} $ -model M and team X over the domain $\mathsf {Fv}(\phi )$ ,

(6) $$ \begin{align} M \models_X \phi\iff (M,rel(X)) \models \gamma_{\phi}(R_{\phi}). \end{align} $$

We may assume that the $\mathbf {ESO} $ -sentence $\gamma _{\phi }(R_{\phi })$ is of the form $\exists R_{\phi }^1\dots \exists R_{\phi }^{m_{\phi }}\alpha _{\phi }$ , where $\alpha _{\phi }$ is a first-order sentence with the relation symbol $R_{\phi }$ , and each relation symbol $R_{\phi }^i$ is fresh. For every $n\in \mathbb {N}$ , let

$$\begin{align*}\Gamma_n=\{\phi\in \Gamma\mid \textsf{Fv}(\phi)\subseteq \{v_1,\dots,v_n\}\}\end{align*}$$

be the set of formulas in $\Gamma $ whose free variables are among $v_1,\dots ,v_n$ , and introduce a $|\textsf {Fv}(\Gamma _n)|$ -ary fresh relation symbol $S_n$ . Clearly, $\Gamma _n\subseteq \Gamma _{n+1}$ and $\Gamma =\bigcup _{n\in \mathbb {N}}\Gamma _n$ . Consider the set $\Gamma '=\{\alpha _{\phi }\mid \phi \in \Gamma \}\cup \Delta $ of first-order sentences, where $\alpha _{\phi }(R_{\phi },R_{\phi }^1,\dots , R_{\phi }^{m_{\phi }})$ is the first-order part of the $\mathbf {ESO} $ -translation of the formula $\phi $ ,

$$ \begin{align*} \Delta=\big\{\exists \mathsf{v}R_{\phi}\mathsf{v},~\forall \mathsf{v}(R_{\phi}\mathsf{v}\to \exists \mathsf{u}S_n\mathsf{vu}),\forall &\mathsf{v}\big(S_n\mathsf{v}\to R_{\phi}\sigma_{\phi}(\mathsf{v})\big),\\ &\forall \mathsf{v}(S_n\mathsf{v}\to \exists \mathsf{u}S_{n+1}\mathsf{vu})\mid n\in\mathbb{N},~\phi\in \Gamma_n\big\}, \end{align*} $$

lists the free variables in $\phi (\mathsf {v})$ , and we assume w.l.o.g. the variables are ordered as shown. Intuitively, the theory $\Delta $ ensures that the relation $S_n$ encodes the team over the domain $\textsf {Fv}(\Gamma _n)$ that glues all relations $R_{\phi }$ with $\phi \in \Gamma _n$ .

We now show that every finite subset $\Gamma _0'\subseteq \Gamma '$ has a model. Consider the corresponding finite subset $\Gamma _0=\{\psi \in \Gamma \mid \alpha _{\psi }\in \Gamma _0'\}$ of $\Gamma $ . By assumption, there is an $\mathcal {L} $ -model N and nonempty team Y such that $N\models _{Y} \Gamma _0$ , where, by locality, we assume that $\textsf {dom}(Y)=\textsf {Fv}(\Gamma )$ . For every $\psi \in \Gamma _0$ , we have that $N\models _{Y_{\psi }}\psi $ by the locality property, where $Y_{\psi }=Y\upharpoonright \mathsf {Fv}(\psi )$ is the restriction of Y over the free variables in $\psi $ . Thus, by (6) we know that $(N,rel(Y_{\psi }))$ is an $\mathcal {L} (R_{\psi })$ -model of $\gamma _{\psi }(R_{\psi })=\exists R_{\psi }^1\dots \exists R_{\psi }^{m_{\psi }}\alpha _{\psi }$ . It follows that some expansion $(N,rel(Y_{\psi }),\mathcal {R}_{\psi }^N)$ of the model $(N,rel(Y_{\psi }))$ in the vocabulary $\mathcal {L} _{\psi }=\mathcal {L} (R_{\psi },R_{\psi }^1\dots R_{\psi }^{m_{\psi }})$ is a model of the first-order sentence $\alpha _{\psi }$ , where $\mathcal {R}_{\psi }^N=\langle (R_{\psi }^1)^N,\dots ,(R_{\psi }^{m_{\psi }})^N\rangle .$ Consider the model $N'=(N,\langle R_{\phi }^{N}\rangle _{\phi \in \Gamma },\langle \mathcal {R}_{\psi }^N\rangle _{\psi \in \Gamma _0},\langle S_n^N\rangle _{n\in \mathbb {N}})$ in the vocabulary $\{R_{\phi }\mid \phi \in \Gamma \}\cup (\bigcup _{\psi \in \Gamma _0}\mathcal {L} _{\psi })\cup \{S_n\mid n\in \mathbb {N}\}$ , where $R_{\phi }^{N}=rel(Y\upharpoonright \textsf {Fv}(\phi ))$ for every $\phi \in \Gamma $ , and $S_n^N=rel(Y\upharpoonright \textsf {Fv}(\Gamma _n))$ . It is not hard to verify that $N'\models \Delta $ (as $S_n$ ’s and $R_{\phi }$ ’s are interpreted according to the nonempty team Y). On the other hand, since $N'$ is an expansion of $(N,rel(Y_{\psi }),\mathcal {R}_{\psi }^N)$ for every $\psi \in \Gamma _0$ , we have that $N'\models \{\alpha _{\psi }\mid \psi \in \Gamma _0\}$ . Hence $N'\models \Gamma _0'$ .

Now, by compactness of first-order logic, $\Gamma '$ has a model $M'$ in the vocabulary $\mathcal {L} '=\bigcup _{\psi \in \Gamma }\mathcal {L} _{\psi }\cup \{S_n\mid n\in \mathbb {N}\}$ . For every $\phi \in \Gamma $ , let $(M,R_{\phi }^M)$ be the reduct of $M'$ to the vocabulary $\mathcal {L} (R_{\phi })$ . Since $M'\models \alpha _{\phi }$ , we have that $(M,R_{\phi }^M)\models \gamma _{\phi }(R_{\phi })$ , which by (6) implies that $M\models _{X_{\phi }}\phi $ for the team $X_{\phi }=\{s:\mathsf {Fv}(\phi )\to M\mid s(\mathsf {v})\in R_{\phi }^M\}$ of M over the finite domain $\mathsf {Fv}(\phi )$ , where $\mathsf {v}$ lists $\mathsf {Fv}(\phi )$ . Since $M'\models \exists \mathsf {v}R_{\phi }\mathsf {v}$ , we know that $X_{\phi }\neq \emptyset $ . Consider the team X over $\mathsf {Fv}(\Gamma )$ , defined as

$$\begin{align*}X=\{s:\mathsf{Fv}(\Gamma)\to M\mid s\upharpoonright \mathsf{Fv}(\phi)\in X_{\phi}\text{ for all }\phi\in \Gamma\}.\end{align*}$$

We claim that for every $\phi \in \Gamma $ , $X\upharpoonright \mathsf {Fv}(\phi )=X_{\phi }$ , which would then imply that $X\neq \emptyset $ and that $M\models _X\Gamma $ by locality, i.e., $\Gamma $ is satisfiable.

By definition, it suffices to show that $X_{\phi }\subseteq X\upharpoonright \mathsf {Fv}(\phi )$ . Let $s\in X_{\phi }$ . For every $n\in \mathbb {N}$ , put $X_{n}=\{t:\textsf {Fv}(\Gamma _n)\to M\mid t(\mathsf {v})\in S_n^{M'}\}$ , where $\mathsf {v}$ lists $\textsf {Fv}(\Gamma _n)$ ; that is, $X_n$ is the team associated with the relation $S_n^{M'}$ . Let $k\in \mathbb {N}$ be (the least number) such that $\phi \in \Gamma _k$ . For every $n\geq k$ , we find inductively an extension $s_n\in X_{n}$ of s over the domain $\textsf {Fv}(\Gamma _n)$ such that $s_n$ extends $s_{m}$ for all $k\leq m\leq n$ . This would then imply that $s_n\upharpoonright \textsf {Fv}(\psi )\in X_{\psi }$ for all $\psi \in \Gamma _n$ , since $M'\models \forall \mathsf {v}\big (S_{n}\mathsf {v}\to R_{\psi }\sigma _{\psi }(\mathsf {v})\big ).$ Therefore the assignment $\hat {s}=\bigcup _{n\geq k}s_n$ is in the team X, thereby $s\in X\upharpoonright \mathsf {Fv}(\phi )$ .

Now, since $M'\models \forall \mathsf {v}(R_{\phi }\mathsf {v}\to \exists \mathsf {u}S_k\mathsf {vu})$ , there exists an $s_k\in X_k$ over the domain $\textsf {Fv}(\Gamma _k)$ such that $s_k\upharpoonright \textsf {Fv}(\phi )=s\upharpoonright \textsf {Fv}(\phi )$ . Suppose $s_n\in X_n$ over $\textsf {Fv}(\Gamma _n)$ for $n\geq k$ has already been defined. Then, since $M'\models \forall \mathsf {v}(S_n\mathsf {v}\to \exists \mathsf {u}S_{n+1}\mathsf {vu}),$ there exists an $s_{n+1}\in X_{n+1}$ over $\textsf {Fv}(\Gamma _{n+1})$ such that $s_{n+1}\upharpoonright \textsf {Fv}(\Gamma _n)=s_n\upharpoonright \textsf {Fv}(\Gamma _n)$ .

Proof We only give detailed proof for the soundness of the nontrivial rules.

$\subseteq \!\textsf {Cmp} $ : It suffices to show that $\mathsf {x}\subseteq \mathsf {y},\alpha (\mathsf {y}/\mathsf {z})\models \alpha (\mathsf {x}/\mathsf {z})$ . Suppose that $M\models _X\mathsf {x}\subseteq \mathsf {y}$ and $M\models _X\alpha (\mathsf {y}/\mathsf {z})$ . Put $X[\mathsf {x}]=\{s(\mathsf {x})\mid s\in X\}$ . Consider $X_0=\{s\in X\mid s(\mathsf {y})\in X[\mathsf {x}]\}\subseteq X.$ Since $M\models _X\mathsf {x}\subseteq \mathsf {y}$ , it is easy to verify that $X[\mathsf {x}]=X_0[\mathsf {y}]$ . Now, since $\alpha $ is downward closed, we have that $M\models _{X_0}\alpha (\mathsf {y}/\mathsf {z})$ , which then implies that $M\models _X\alpha (\mathsf {x}/\mathsf {z})$ by locality (as free variables in the formula $\alpha (\mathsf {z})$ are among $\mathsf {z}$ ).

$\subseteq \!\textsf {W}_{\textsf {con}} $ : It suffices to show that $\mathop {=\!} (\mathsf {x}),\mathsf {y}\subseteq \mathsf {z}\models \mathsf {xy}\subseteq \mathsf {xz}$ . Suppose that $M\models _X\mathop {=\!} (\mathsf {x})$ and $M\models _X\mathsf {y}\subseteq \mathsf {z}$ . The latter implies that for any $s\in X$ , there exists $s'\in X$ such that

$s(\mathsf {y})=s'(\mathsf {z})$ . But since $M\models _X\mathop {=\!} (\mathsf {x})$ , we also have $s(\mathsf {x})=s'(\mathsf {x})$ . Thus $s(\mathsf {xy})= s'(\mathsf {xz})$ , thereby $M\models _X\mathsf {xy}\subseteq \mathsf {xz}$ .

$\subseteq \!\textsf {W}_{\exists ^1 } $ : It suffices to show that $\mathop {=\!} (\mathsf {x}),\mathsf {x}\subseteq \mathsf {y}\models \exists ^1 \mathsf {z}(\mathsf {zx}\subseteq \mathsf {wy})$ . Suppose that $M\models _X\mathop {=\!} (\mathsf {x})$ and $M\models _X\mathsf {x}\subseteq \mathsf {y}$ . Pick $s_0\in X$ . Then there exists $s^{\prime }_0\in X$ such that $s_0(\mathsf {x})=s^{\prime }_0(\mathsf {y})$ . Let $\mathsf {a}=s_0'(\mathsf {w})$ . We show that $M\models _{X(\mathsf {a}/\mathsf {z})}\mathsf {zx}\subseteq \mathsf {wy}$ . For any $s\in X(\mathsf {a}/\mathsf {z})$ , clearly $s^{\prime }_0(\mathsf {a}/\mathsf {z})\in X(\mathsf {a}/\mathsf {z})$ . Since $M\models _X\mathop {=\!} (\mathsf {x})$ , we have that $s(\mathsf {x})=s_0(\mathsf {x})$ . Thus $s(\mathsf {zx})=\mathsf {a}s_0(\mathsf {x})=s^{\prime }_0(\mathsf {w})s_0'(\mathsf {y})=s^{\prime }_0(\mathsf {a}/\mathsf {z})(\mathsf {wy}).$

$\subseteq \textsf {E} $ : Suppose $\Gamma \models \mathop {\dot \sim } \mathsf {x}\subseteq \mathsf {y}$ and $\Gamma ,\mathsf {c}\subseteq \mathsf {x},\mathop {\dot \sim } \mathsf {c}\subseteq \mathsf {y}\models \phi $ , and suppose that for some $\mathcal {L} $ -model M and nonempty team X, $M\models _X\Gamma $ . Then we have that $M\models _X\mathop {\dot \sim } \mathsf {x}\subseteq \mathsf {y}$ , which implies that there exists $s\in X$ such that for the $\mathcal {L} (\mathsf {c})$ -model $(M,s(\mathsf {x}))$ , we have $(M,s(\mathsf {x}))\models _X\mathsf {c}\subseteq \mathsf {x}\wedge \mathop {\dot \sim } \mathsf {c}\subseteq \mathsf {y}$ . Thus, by the assumption, $(M,s(\mathsf {x}))\models _X\phi $ , which gives $M\models _X\phi $ since constant symbols in $\mathsf {c}$ do not occur in $\phi $ .

$\lambda \textsf {E} $ : Suppose $\Gamma \models \mathop {\dot \sim } \lambda (\mathsf {x})$ and $\Gamma ,\mathsf {c}\subseteq \mathsf {x},\mathop {\dot \sim } \lambda (\mathsf {c})\models \phi $ , and suppose that for some $\mathcal {L} $ -model M and nonempty team X, $M\models _X\Gamma $ . Then we have that $M\models _X\mathop {\dot \sim } \lambda (\mathsf {x})$ , which implies that $M\not \models _X\lambda (\mathsf {x})$ . Since $\lambda (\mathsf {x})$ is flat, this means that there exists $s\in X$ such that for the $\mathcal {L} (\mathsf {c})$ -model $(M,s(\mathsf {x}))$ , $(M,s(\mathsf {x}))\not \models _X\lambda (\mathsf {c})$ , or $(M,s(\mathsf {x}))\models _X\mathop {\dot \sim } \lambda (\mathsf {c})$ . Clearly, we also have that $(M,s(\mathsf {x}))\models _X\mathsf {c}\subseteq \mathsf {x}$ . Hence, by assumption we conclude that $(M,s(\mathsf {x}))\models _X\phi $ , which gives $M\models _X\phi $ since $\mathsf {c}$ do not occur in $\phi $ .

$\subseteq \!\textsf {wI}_R $ : Suppose $\Gamma ,\phi (\mathsf {v})\not \models \bot $ , where the formulas in $\Gamma \cup \{\phi \}$ are in the vocabulary $\mathcal {L}$ with $R\notin \mathcal {L}$ . We may w.l.o.g. assume that $\phi (\mathsf {v})$ is in prenex and negation normal form (cf. Corollary 4.4). Then there exist an $\mathcal {L}$ -model M and a nonempty team X such that $M\models _X\Gamma $ and $M\models _X\phi (\mathsf {v})$ . Consider the $\mathbf {FO} $ -sentence $\phi _{\ast }(R)$ obtained from the inclusion atom-free $\mathbf {FOT} $ -sentence $\phi (R)$ by replacing every logical constant in $\mathbf {FOT} $ by its counterpart in FO, i.e., by replacing $\mathop {\dot \sim } $ by $\neg $ , by $\vee $ , $\forall ^1 $ by $\forall $ , and $\exists ^1 $ by $\exists $ . Now, by (the proof of) Theorem 3.2, we have $(M,rel(X))\models \phi _{\ast }(R)$ in $\mathbf {FO} $ . By Lemma 2.1, $(M,rel(X))\models _{\{\emptyset \}}\phi (R)$ in $\mathbf {FOT} $ follows. Since $\Gamma $ is a set of sentences in which R does not occur, we also have $(M,rel(X))\models _{\{\emptyset \}}\Gamma $ . Also, since $X\neq \emptyset $ , $(M,rel(X))\models \exists ^1 \mathsf {z}R\mathsf {z}$ . Hence, we conclude $\Gamma ,\exists ^1 \mathsf {z}R\mathsf {z},\phi (R)\not \models \bot $ .

Proof Item (i) follows easily from $\mathsf {con}\textsf {I} $ (the fact $\vdash \mathop {=\!} (c)$ in particular), $\forall ^1 $ E and $\exists ^1 $ I. The proofs for the other items are routine and thus left to the reader.

Proof Apply exhaustively Proposition 4.3(ii)–(v).

Proof Item (i) is proved by a routine inductive argument that uses Proposition 4.3 (i) in the cases for the quantifiers $\forall ^1 $ and $\exists ^1 $ . Item (ii) is proved easily by using Proposition 4.3 (iii).

Proof Item (i): For the right to left direction, we first derive by applying the rule $\subseteq \!\textsf {Pro} $ (which can be applied to add repeated arguments to an inclusion atom). Then, we apply the rules of identity to obtain .

For the left to right direction, follows from $\subseteq \!\textsf {Pro} $ . Next, by $\subseteq \!\textsf {Pro} $ and rules of identity, we have . Finally, viewing formula $\mathsf {v}=\mathsf {v}$ as $(\mathsf {x}=\mathsf {y})(\mathsf {vv}/\mathsf {xy})$ , we applying $\subseteq \!\textsf {Cmp} $ to conclude $\mathsf {x}\mathsf {y}\subseteq \mathsf {v}\mathsf {v},\mathsf {v}=\mathsf {v}\vdash \mathsf {x}=\mathsf {y}$ .

Item (ii): For the right to left direction, by Proposition 4.3 (iii) and (iv), it suffices to show the contrapositive $\mathop {\dot \sim } \xi \subseteq \eta \vdash \exists ^1 \mathsf {x}(\mathsf {x}\subseteq \xi \wedge \mathop {\dot \sim } \mathsf {x}\subseteq \eta )$ . For any sequence $\mathsf {c}$ of fresh constant symbols, we have $ \mathsf {c}\subseteq \xi ,\mathop {\dot \sim } \mathsf {c}\subseteq \eta \vdash \exists ^1 \mathsf {x}(\mathsf {x}\subseteq \xi \wedge \mathop {\dot \sim } \mathsf {x}\subseteq \eta )$ by Proposition 4.3 (i). Then the desired clause follows from $\subseteq \textsf {E} $ . For the other direction, by $\forall ^1 $ I, it suffices to show that for $\mathsf {c}$ a sequence of fresh constant symbols, which is further reduced to showing that $\xi \subseteq \eta , \mathsf {c}\subseteq \xi \vdash \mathsf {c}\subseteq \eta $ . But this follows from $\subseteq \!\textsf {Tr} $ .

Item (iii): We first show , which is equivalent to $\mathop {\mathop {=\!} } (\mathsf {z}),\mathsf {w}\xi \subseteq \mathsf {z}\eta \vdash \mathsf {w}=\mathsf {z}\wedge \xi \subseteq \eta $ . By $\subseteq \!\textsf {W}_{\textsf {con}} $ and $\subseteq \!\textsf {Pro} $ we have $\mathop {\mathop {=\!} } (\mathsf {z}),\mathsf {w}\subseteq \mathsf {z}\vdash \mathsf {w}\mathsf {z}\subseteq \mathsf {z}\mathsf {z}$ . By item (i), $\mathsf {w}\mathsf {z}\subseteq \mathsf {z}\mathsf {z}\vdash \mathsf {w}=\mathsf {z}$ . Hence, by $\subseteq \!\textsf {Pro} $ the desired clause follows. Next, we show $\mathop {\mathop {=\!} } (\mathsf {z}),\mathsf {w}=\mathsf {z}, \xi \subseteq \eta \vdash \mathsf {w}\xi \subseteq \mathsf {z}\eta $ . Again by $\subseteq \!\textsf {W}_{\textsf {con}} $ we have that $\xi \subseteq \eta ,\mathop {\mathop {=\!} } (\mathsf {z})\vdash \mathsf {z}\xi \subseteq \mathsf {z}\eta $ , and thus the desired clause follows from rules of identity.

Item (iv): The direction $\mathop {\mathop {=\!} } (\mathsf {x}),\mathsf {x}\subseteq \mathsf {v}\vdash \exists ^1 \mathsf {y}(\mathsf {x}\mathsf {y}\subseteq \mathsf {v}\mathsf {u})$ is given by $\subseteq \!\textsf {W}_{\exists ^1 }$ , and the other direction $\mathop {\mathop {=\!} } (\mathsf {x}),\exists ^1 \mathsf {y}(\mathsf {x}\mathsf {y}\subseteq \mathsf {v}\mathsf {u})\vdash \mathsf {x}\subseteq \mathsf {v}$ follows easily from $\subseteq \!\textsf {Pro} $ .

Item (v): We first show the left to right direction, which, by $\forall ^1 $ I, is reduced to for $\mathsf {c}$ a sequence of fresh constant symbols. But this follows from $\subseteq \!\textsf {Cmp} $ . Conversely, we show the contrapositive $\mathop {\dot \sim } \lambda (\mathsf {z})\vdash \exists ^1 \mathsf {w}(\mathsf {w}\subseteq \mathsf {z}\wedge \mathop {\dot \sim } \lambda (\mathsf {w}))$ . For any sequence $\mathsf {c}$ of fresh constant symbols, we have $ \mathsf {c}\subseteq \mathsf {z},\mathop {\dot \sim } \lambda (\mathsf {c})\vdash \exists ^1 \mathsf {w}(\mathsf {w}\subseteq \mathsf {z}\wedge \mathop {\dot \sim } \lambda (\mathsf {w}))$ by Proposition 4.3 (i). Then the desired clause follows from $\lambda \textsf {E} $ .

Proof By Proposition 4.3 (ii), $Q^1\textsf {I}$ , and $Q^1\textsf {E}$ , it is easy to prove that $Q^1 \mathsf {x}\theta (\mathsf {x},\mathsf {v})\dashv \vdash Q^1 \mathsf {x}(\theta (\mathsf {x},\mathsf {v})\wedge \mathop {\mathop {=\!} } (\mathsf {x})).$ We then push the formula $\mathop {\mathop {=\!} } (\mathsf {x})$ inside the quantifier-free formula $\theta $ in negation normal form all the way to the front of literals by using Replacement Lemma (Corollary 4.5(i)) and the (standard) equivalences $(\theta _0\wedge \theta _1)\wedge \mathop {\mathop {=\!} } (\mathsf {x})\dashv \vdash (\theta _0\wedge \mathop {\mathop {=\!} } (\mathsf {x}))\wedge (\theta _1\wedge \mathop {\mathop {=\!} } (\mathsf {x}))$

Proof By Corollary 4.4, we may assume that $\phi (\mathsf {v})$ is in prenex and negation normal form. Assume that the bound variables of $\phi (\mathsf {v})$ are among $\mathsf {x}$ . By Lemma 4.7 we may also assume that every literal $\mu (\mathsf {x},\mathsf {v})$ in $\phi $ is replaced by $\mu (\mathsf {x},\mathsf {v})\wedge \mathop {\mathop {=\!} } (\mathsf {x})$ (call such a formula a formula in constant normal form). Observe that now in $\phi (\mathsf {v})$ a generic first-order atom is of the form $\lambda (\mathsf {x},\mathsf {v})$ , and a generic inclusion atom is of the form $\eta \xi \rho \sigma \subseteq \eta '\xi '\rho '\sigma '$ (modulo permutation by $\subseteq \!\textsf {Pro} $ ), where $|\eta |=|\eta '|\geq 0$ , $|\xi |=|\xi '|\geq 0$ , $|\rho |=|\rho '|\geq 0$ , and $|\sigma |=|\sigma '|\geq 0$ :

• • $(\eta ,\eta ')=(\mathsf {x}_i,\mathsf {x}_j)$ for some bound variables $\mathsf {x}_i,\mathsf {x}_j$ from $\mathsf {x}$ ;

• • $(\xi ,\xi ')=(\mathsf {x}_i,\mathsf {v}_i)$ for some bound variables $\mathsf {x}_i$ from $\mathsf {x}$ , and free variables $\mathsf {v}_i$ from $\mathsf {v}$ ;

• • $(\rho ,\rho ')=(\mathsf {v}_i,\mathsf {x}_i)$ for some free variables $\mathsf {v}_i$ from $\mathsf {v}$ , and bound variables $\mathsf {x}_i$ from $\mathsf {x}$ ;

• • $(\sigma ,\sigma ')=(\mathsf {v}_i,\mathsf {v}_j)$ for some free variables $\mathsf {v}_i,\mathsf {v}_j$ from $\mathsf {v}$ .

To obtain the required normal form we have to transform every (first-order or inclusion) atom in $\phi $ to the required form. We achieve this in several steps.

In Step 1 of our transformation, we replace in $\phi (\mathsf {v})$ every inclusion atom of the form $\eta \xi \mathsf {v}_i\sigma \subseteq \eta '\xi '\mathsf {x}_i\sigma '$ by $\mathsf {v}_i=\mathsf {x}_i\wedge \eta \xi \sigma \subseteq \eta '\xi '\sigma '$ . Note that by Proposition 4.6 (iii), we have

$$\begin{align*}\mathop{\mathop{=\!}}(\mathsf{x}_i)\wedge\eta\xi\mathsf{v}_i\sigma\subseteq\eta'\xi'\mathsf{x}_i\sigma'\dashv\vdash\mathop{\mathop{=\!}}(\mathsf{x}_i)\wedge(\mathsf{v}_i=\mathsf{x}_i\wedge \eta\xi\sigma\subseteq\eta'\xi'\sigma')\end{align*}$$

$$\begin{align*}\text{and }\mathop{\mathop{=\!}}(\mathsf{x}_i)\wedge\mathop{\dot\sim}\eta\xi\mathsf{v}_i\sigma\subseteq\eta'\xi'\mathsf{x}_i\sigma'\dashv\vdash\mathop{\mathop{=\!}}(\mathsf{x}_i)\wedge\mathop{\dot\sim}(\mathsf{v}_i=\mathsf{x}_i\wedge \eta\xi\sigma\subseteq\eta'\xi'\sigma').\end{align*}$$

Hence, by Replacement Lemma (Corollary 4.5(i)), the resulting formula $\phi _1(\mathsf {v})$ is provably equivalent to $\phi $ . We further assume (here and also in the other steps) that $\phi _1(\mathsf {v})$ is turned into prenex, negation, and constant normal form by applying Corollary 4.4 and Lemma 4.7.

In Step 2, we replace in $\phi _1(\mathsf {v})$ every first-order atom $\lambda (\mathsf {x},\mathsf {v})$ by By Proposition 4.6 (v), the resulting formula $\phi _2(\mathsf {v})$ is provably equivalent to $\phi _1(\mathsf {v})$ . Up to now, every first-order atom in the formula is transformed to the required form. The steps afterwards will not generate first-order atoms not in normal form.

In Step 3, we apply Proposition 4.6 (ii) to replace in $\phi _2(\mathsf {v})$ every inclusion atom $\eta \xi \mathsf {v}_i\subseteq \eta '\xi '\mathsf {v}_j$ by and denote the resulting formula by $\phi _3(\mathsf {v})$ . In Step 4, we apply Proposition 4.6 (iii) to replace in $\phi _3(\mathsf {v})$ every inclusion atom $\mathsf {x}_i\mathsf {x}_k\subseteq \mathsf {x}_j\mathsf {v}_k$ by $\mathsf {x}_i=\mathsf {x}_j\wedge \mathsf {x}_k\subseteq \mathsf {v}_k$ , and denote the resulting formula by $\phi _4(\mathsf {v})$ . Up to now every inclusion atom in the formula is transformed to the form $\mathsf {x}_i\subseteq \mathsf {v}_i$ , where $\mathsf {x}_i$ are bound variables and $\mathsf {v}_i$ are free variables in $\phi _4(\mathsf {v})$ . Yet, $\mathsf {v}_i$ may contain repetitions, and it may be only a subsequence of $\mathsf {v}$ . Handling these requires two additional steps.

In Step 5, we remove repetitions on the right side of the inclusion atoms, by applying Proposition 4.6 (i) to replace in $\phi _4(\mathsf {v})$ every inclusion atom of the form $\mathsf {x}_i\mathsf {x}_j\mathsf {x}_k\subseteq \mathsf {v}_i\mathsf {v}_i\mathsf {v}_j$ by $\mathsf {x}_i=\mathsf {x}_j\wedge \mathsf {x}_i\mathsf {x}_k\subseteq \mathsf {v}_i\mathsf {v}_j$ . Denote the resulting formula by $\phi _5(\mathsf {v})$ . In Step 6, we extend the length of those shorter inclusion atoms. Assuming $\mathsf {v}=\mathsf {v}_i\mathsf {v}_j$ , we apply Proposition 4.6 (iv) to replace in $\phi _5(\mathsf {v})$ every inclusion atom of the form $\mathsf {x}_i\subseteq \mathsf {v}_i$ by $\exists ^1 \mathsf {y}(\mathsf {x}_i\mathsf {y}\subseteq \mathsf {v}_i\mathsf {v}_j)$ . Denote the resulting formula by $\phi _6(\mathsf {v})$ .

As before we assume that $\phi _6(\mathsf {v})$ is turned into prenex and negation normal form, but now we shall apply Lemma 4.7 in a reverse manner to remove the added constancy atoms for each literal in $\phi _6$ . Finally, the resulting provably equivalent formula is in the required normal form. Note that our transformation clearly terminates, because we have performed the steps of the transformation in such an order that each step will not generate new formulas for which the transformations in the previous steps apply.

Proof We prove that $\Delta \vdash _{\mathbf {FO}} \delta $ implies $\Delta ^{\ast }(\mathsf {c}/\mathsf {x})\vdash _{\mathbf {FOT}} \delta ^{\ast }(\mathsf {c}/\mathsf {x})$ by induction on the depth of the proof tree of $\Delta \vdash _{\mathbf {FO}} \delta $ . If the proof tree has depth 1, then either $\delta \in \Delta $ or $\delta $ is the identity axiom $t=t$ . In both cases $\Delta ^{\ast }(\mathsf {c}/\mathsf {x})\vdash _{\mathbf {FOT}} \delta ^{\ast }(\mathsf {c}/\mathsf {x})$ trivially holds.

If the proof tree has depth $>1$ , and the last step of the derivation of $\Delta \vdash _{\mathbf {FO}} \delta $ is an application of a rule for $\neg $ or $\wedge $ or $\vee $ in $\mathbf {FO} $ , then we derive $\Delta ^{\ast }(\mathsf {c}/\mathsf {x})\vdash _{\mathbf {FOT}} \delta ^{\ast }(\mathsf {c}/\mathsf {x})$ by directly applying the induction hypothesis and the corresponding (classical) rules for $\mathop {\dot \sim } $ or $\wedge $ or in our system for $\mathbf {FOT} $ .

If the last step of the derivation of $\Delta \vdash _{\mathbf {FO}} \delta $ is an application of the $\exists \textsf {I}$ rule:

where the free variables occurring in $\Delta (\mathsf {y})$ and $\exists x\alpha (x,\mathsf {y})$ are among $\mathsf {y}$ , and the variables and constant symbols occurring in the term t are, respectively, among $\mathsf {v}\mathsf {y}$ and $\mathsf {d}$ (denoted by $t(\mathsf {v}\mathsf {y},\mathsf {d})$ ), then the corresponding derivation in $\mathbf {FOT} $ is

where $\pi ^{\ast }$ is, by induction hypothesis, the derivation in $\mathbf {FOT} $ that corresponds to $\pi $ .

If the last step of the derivation of $\Delta \vdash _{\mathbf {FO}} \delta $ is an application of the $\exists \textsf {E}$ rule:

where $ v\notin \textsf {Fv}(\Delta \cup \{\alpha ,\delta \})$ and the free variables occurring in $\Delta ,\exists x\alpha ,\delta $ are among $\mathsf {y}$ , then the corresponding derivation in $\mathbf {FOT} $ is

where $\pi _1^{\ast },\pi _2^{\ast }$ are, by induction hypothesis, the derivations that correspond to $\pi _1,\pi _2$ in $\mathbf {FOT} $ respectively, and d is a fresh constant symbol.

If the last step of the derivation of $\Delta \vdash _{\mathbf {FO}} \delta $ is an application of the $\forall \textsf {I}$ rule:

where $ v\notin \textsf {Fv}(\Delta \cup \{\alpha \})$ and the free variables occurring in $\Delta ,\forall x\alpha $ are among $\mathsf {y}$ , then the corresponding derivation in $\mathbf {FOT} $ is

where d is a fresh constant symbol.

If the last step of the derivation of $\Delta \vdash _{\mathbf {FO}} \delta $ is an application of the $\forall \textsf {E}$ rule:

where the free variables occurring in $\Delta ,\forall x\alpha $ are among $\mathsf {y}$ and $t=t(\mathsf {vy},\mathsf {d})$ for some sequence $\mathsf {d}$ of constant symbols, then the corresponding derivation in FOT is

Proof Suppose that $\nvdash _{\mathbf {FOT}} \phi $ . By RAA we derive $\mathop {\dot \sim } \phi \nvdash _{\mathbf {FOT}} \bot $ , which is equivalent to $\psi (\mathsf {v})\nvdash _{\mathbf {FOT}} \bot $ , where $\psi (\mathsf {v})=Q^1\mathsf {x}\theta (\mathsf {x},\mathsf {v})$ is the formula $\mathop {\dot \sim } \phi $ in the normal form given by Lemma 4.8. Let R be a fresh relation symbol (which is assumed to be always available), and let $\psi (R)$ be the inclusion atom-free sentence obtained from $\psi (\mathsf {v})$ by replacing every inclusion atom $\mathsf {x}_i\subseteq \mathsf {v}$ by $R\mathsf {x}_i$ . By $\subseteq \!\textsf {wI}_R $ we have $\exists ^1 \mathsf {z}R\mathsf {z}, \psi (R)\nvdash _{\mathbf {FOT}} \bot $ . Consider the $\mathbf {FO} $ -formula $\psi _{\ast }(R)$ obtained from the $\mathbf {FOT} $ -formula $\psi (R)$ by replacing every logical constant in $\mathbf {FOT} $ by its counterpart in $\mathbf {FO} $ . It follows from Lemma 4.9 that $\exists \mathsf {z}R\mathsf {z},\psi _{\ast }(R)\nvdash _{\mathbf {FO}} \bot $ . Now, by the completeness theorem of $\mathbf {FO} $ , there exists a model $(M,R^M)$ such that $R^M\neq \emptyset $ and $(M,R^M)\models \psi _{\ast }(R)$ . It then follows from (the proof of) Theorem 3.2 that $M\models _{X_R}\psi (\mathsf {v})$ , where $X_R=\{s:\{v_1,\dots ,v_k\}\to M\mid s(\mathsf {v})\in R^M\}$ is the (nonempty) team associated with R. Hence $\mathop {\dot \sim } \phi \not \models \bot $ , thereby $\not \models \phi $ .

Proof Suppose $\Gamma \models \phi $ . Since $\Gamma ,\mathop {\dot \sim } \phi \models \bot $ and $\Gamma \cup \{\phi \}$ contains countably many free variables, by compactness of $\mathbf {FOT} $ (Theorem 3.8) we may assume that $\Gamma $ is a finite set. Now, we have that . Thus, by the weak completeness, we obtain , which, by E and $\mathop {\dot \sim } \mathsf {E}$ , implies $\Gamma \vdash _{\mathbf { FOT}} \phi $ .

Proof The “vice versa” direction is trivial. For the non-trivial direction, we show that for every $\mathbf {D} \oplus \mathbf {FOT}^{\downarrow } $ -formula $\phi (v_1,\dots ,v_k)$ in some vocabulary $\mathcal {L}$ , there exists an $\mathcal {L}(R)$ -sentence $\gamma _{\phi }(R)$ with a fresh k-ary relation symbol R occurring only negatively such that equivalence (3) from Theorem 3.1 holds for any $\mathcal {L}$ -model M and nonempty team X. This would then suffice for the following reasons: We know by [Reference Kontinen and Väänänen33, Theorem 4.9] that for every such existential second-order sentence $\gamma _{\phi }(R)$ , there exists an $\mathcal {L}$ -formula $\psi (v_1,\dots ,v_k)$ in $\mathbf {D} $ such that equivalence (3) from Theorem 3.1 with respect to $\psi $ holds for any $\mathcal {L}$ -model M and nonempty team X. This then implies that $\phi $ and $\psi $ are equivalent over arbitrary models and nonempty teams. Over the empty team, on the other hand, both $\phi $ and $\psi $ are satisfied (by the empty team property of the logics). Putting all these together, we would be able to conclude that $\phi \equiv \psi $ .

Now, to give the translation from $\mathbf {D} \oplus \mathbf {FOT}^{\downarrow } $ into existential second-order logic, we combine our translation from $\mathbf {FOT}^{\downarrow } $ into first-order logic as given in Theorem 3.1, and the translation from $\mathbf {D} $ into existential second-order logic as given in [Reference Väänänen39, Theorem 6.2]. If the $\mathbf {D} \oplus \mathbf {FOT}^{\downarrow } $ -formula $\phi (\mathsf {v})$ is a dependence atom, or if its main connective or quantifier is one from $\mathbf {D} $ , we define $\gamma _{\phi }(R)$ in the same way as in [Reference Väänänen39, Theorem 6.2]. For example, $\gamma _{\theta _0\vee \theta _1}(R,\mathsf {x})=\exists S_1\exists S_2(\forall \mathsf {u}(R\mathsf {u}\to S_1\mathsf {u}\vee S_2\mathsf {u})\wedge \gamma _{\theta _0}(S_1,\mathsf {x})\wedge \gamma _{\theta _1}(S_2,\mathsf {x}))$ , etc. If $\phi (\mathsf {v})$ is a first-order (negated) formula, or if its main connective or quantifier is or $\exists ^1 $ , we define $\gamma _{\phi }(R)$ in the same way as in Theorem 3.1. The formula $\gamma _{\phi }(R)$ is clearly existential second-order and it also satisfies equivalence (3) from Theorem 3.1.

Fact 5.2. $\mathbf {FO}(\forall ^1 ) $ -formulas are flat.

Proof Formulas $\phi $ of $\mathbf {FO}(\forall ^1 ) $ are clearly downward closed and satisfy the empty team property. It is then sufficient to show, by induction, that $\phi $ is closed under unions. For the only non-trivial case $\phi =\forall ^1 x\psi $ , suppose that $M\models _{X_i}\forall ^1 x\psi $ for any $i\in I\neq \emptyset $ . For any $a\in M$ , we have that $M\models _{X_i(a/x)}\psi $ . Thus, by induction hypothesis, $M\models _{X(a/x)}\psi $ for $X=\bigcup _{i\in I}X_i$ . Hence we conclude $M\models _{X}\forall ^1 x\psi $ .

Proof (i) This is proved by an inductive argument, for which most cases follow essentially from Lemma 2.1. We only illustrate two non-trivial cases. If $\theta =\mathop {=\!} (\mathsf {t},\mathsf {t}')$ , then both $M\models _{\{s\}}\mathop {=\!} (\mathsf {t},\mathsf {t}')$ and $M\models _{\{s\}}\top $ always hold. If $\theta =\forall x\eta $ where $\eta $ is in $\mathbf {FO}(\forall ^1 ) $ , then $\eta $ is flat (by Fact 5.2), and the rest of the proof is essentially the same as the corresponding case in Lemma 2.1.

(ii) Suppose $\Gamma \models \theta $ , and suppose $M\models _X\Gamma $ and $M\models _X\neg \theta _{\ast }$ . If $X\neq \emptyset $ , then for an arbitrary $s\in X$ , we have that $M\not \models _{\{s\}}\theta _{\ast }$ , which implies $M\not \models _{\{s\}}\theta $ by item (i). Hence, by the downward closure of $\theta $ , we conclude that $M\not \models _X\theta $ , which contradicts the assumption that $\Gamma \models \theta $ . Hence, $X=\emptyset $ and $M\models _X\bot $ .

Conversely, suppose $\Gamma ,\neg \theta _{\ast }\models \bot $ , and suppose $M\models _X\Gamma $ and $M\not \models _X\theta $ . We derive a contradiction. Let us first treat the case when $\theta $ is a pseudo-flat sentence with no free variable. By locality, $M\not \models _X\theta $ implies that $M\not \models _{\{\emptyset \}}\theta $ for the empty assignment $\emptyset $ . Thus, by item (i), we obtain $M\models _{\{\emptyset \}}\neg \theta _{\ast }$ . Observe that $\neg \theta _{\ast }$ is also a sentence with no free variable, thus $M\models _X\neg \theta _{\ast }$ , by locality again. Now, since $M\models _X\Gamma $ , by assumption we are forced to conclude that $M\models _X\bot $ , meaning that $X=\emptyset $ . But in view of the empty team property, this contradicts the assumption that $M\not \models _X\theta $ . Hence we are done.

Next, let us consider the case when $\theta $ is a (possibly open) $\mathbf {FO}(\forall ^1 ) $ -formula. Since now $\theta $ is flat (by Fact 5.2), we have that $M\not \models _{\{s\}}\theta $ for some $s\in X$ . This means, by item (i), that $M\models _{\{s\}}\neg \theta _{\ast }$ . Since formulas in $\Gamma $ are all downward closed, we then have that $M\models _{\{s\}}\Gamma $ . But then, the assumption $\Gamma ,\neg \theta _{\ast }\models \bot $ implies that $M\models _{\{s\}}\bot $ , which is not the case. Hence we are also done.

Proof Item (i) is easy to prove. We only give detailed proof for item (ii). Suppose . Then either $M\models _X\phi $ or $M\models _X\psi $ . Pick distinct $a,b\in M$ . Define functions $F:X\to \wp ^+(M)$ and $G:X(F/x)\to \wp ^+(M)$ as $F(s)=\{a\}$ , and $G(s)=\{a\}$ if $M\models _X\phi $ and $G(s)=\{b\}$ if $M\models _X\psi $ . Put $Y=X(F/x)(G/y)$ . It is easy to see that $M\models _Y\mathop {=\!} (x)\wedge \mathop {=\!} (y)$ , and $M\models _Yx=y\wedge \phi $ in case $M\models _X\phi $ , and $M\models _Yx\neq y\wedge \psi $ in case $M\models _X\psi $ .

Conversely, suppose there are suitable functions $F,G$ such that for the team $Y=X(F/x)(G/y)$ , $M\models _Y\mathop {=\!} (x)\wedge \mathop {=\!} (y)$ and $M\models _Y(x=y\wedge \phi )\vee (x\neq y\wedge \psi )$ . Since $x,y$ have constant values in Y, it must be that either $M\models _Yx=y\wedge \phi $ or $M\models _Yx\neq y\wedge \psi $ . Hence we conclude that . Since $x,y\notin \textsf {Fv}(\phi )\cup \textsf {Fv}(\psi )$ , we have by the locality property that .

Proof The second equivalence is clear. We only verify the first equivalence. Suppose $M\models _X\exists x\forall ^1 y\phi (x,y,\mathsf {z})$ , and we may w.l.o.g. assume also that $\textsf {dom}(X)=\mathsf {z}$ . Then there exists a function $F:X\to \wp ^+(M)$ such that for all $a\in M$ , $M\models _{X(F/x)(a/y)}\phi (x,y,\mathsf {z})$ . Since $\phi $ is downward closed, we may w.l.o.g. assume that $F(s)$ is a singleton for each $s\in X$ . Let $a\in M$ be arbitrary. We define a function $F':X(a/y)\to \wp ^+(M)$ as $F'(s)=F(s\upharpoonright \textsf {dom}(X)).$ Clearly, $M\models _{X(a/y)(F'/x)}\mathop {=\!} (\mathsf {z},x)$ . Observe that $X(a/y)(F'/x)=X(F/x)(a/y)$ . Thus $M\models _{X(a/y)(F'/x)}\phi $ , as required.

Conversely, suppose $M\models _X\forall ^1 y\exists x(\mathop {=\!} (\mathsf {z},x)\wedge \phi )$ . Pick $a\in M$ . By assumption, there exists a function $F_a:X(a/y)\to \wp ^+(M)$ such that $M\models _{X(a/y)(F_a/x)}\mathop {=\!} (\mathsf {z},x)\wedge \phi $ . Define a function $F':X\to \wp ^+(M)$ as $F'(s)=F_a(s(a/y))$ . For any $b\in M$ , it suffices to show that $M\models _{X(F'/x)(b/y)}\phi $ . Now, since $M\models _{X(b/y)(F_b/x)}\mathop {=\!} (\mathsf {z},x)$ , we have that for all $s_0\in X$ , $F_b(s_0(b/y))=F_a(s_0(a/y))$ is a singleton. We claim that $X(b/y)(F_b/x)=X(F'/x)(b/y)$ , which would then imply $M\models _{X(F'/x)(b/y)}\phi $ , since we have $M\models _{X(b/y)(F_b/x)}\phi $ by assumption. Indeed, if $s\in X(F'/x)(b/y)$ , then

$$\begin{align*}s(x)=F'(s\upharpoonright \textsf{dom}(X))=F_a((s\upharpoonright \textsf{dom}(X)(a/y))=F_b((s\upharpoonright \textsf{dom}(X)(b/y)),\end{align*}$$

which implies that $s\in X(b/y)(F_b/x)$ . The converse direction is symmetric.