Conservative Extensions in Guarded and Two-Variable Fragments

TL;DR

This paper explores the decidability and complexity of conservative extensions in fragments of first-order logic, showing undecidability in most fragments and decidability with high complexity in a specific intersection.

Contribution

It establishes the boundaries of decidability for conservative extensions in guarded and two-variable first-order logic fragments.

Findings

Conservative extensions are undecidable in FO fragments containing FO$^2$ or GF.

Decidable and 2 ext{ExpTime}-complete in GF$^2$ (intersection of FO$^2$ and GF).

Abstract

We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpTime-complete in the intersection GF$^2$ of FO$^2$ and GF.

Equations

$$\forall \mathbf{y}(\alpha (\mathbf{x},\mathbf{y})\to \phi (\mathbf{x},\mathbf{y}))\exists \mathbf{y}(\alpha (\mathbf{x},\mathbf{y})\wedge \phi (\mathbf{x},\mathbf{y}))$$

$$\exists xSx\wedge \forall x(Sx\to (q_{0}x\wedge \neg \exists y{R}_{0}xy\wedge \neg \exists y{R}_{1}xy))$$

$$\begin{array}[]{rl}\forall x(q_{i}x\rightarrow\exists y(Nxy\wedge q_{j}y))&\text{ if }I_{i}=+(p,q_{j})\\[2.84526pt] \forall x((q_{i}x\wedge\neg\exists yR_{p}xy)\rightarrow\exists y(Nxy\wedge q_{j}y))&\text{ if }I_{i}=-(p,q_{j},q_{k})\\[2.84526pt] \forall x((q_{i}x\wedge\exists yR_{p}xy)\rightarrow\exists y(Nxy\wedge q_{k}y))&\text{ if }I_{i}=-(p,q_{j},q_{k})\end{array}$$

$$\exists x(Sx\wedge Px)\wedge \forall x(Px\to \exists y(Nxy\wedge Py))$$

$$\begin{array}[]{l}\exists x\exists y\,\big{(}Nxy\wedge\displaystyle\big{(}\bigvee_{I_{i}=+(p,q_{j})}(q_{i}x\wedge q_{j}y\wedge(D^{+}_{p}xy\vee D^{=}_{1-p}xy))\\[17.07164pt] \hskip 82.51299pt\displaystyle\vee\,\bigvee_{I_{i}=-(p,q_{j},q_{k})}(q_{i}x\wedge q_{k}y\wedge(D^{-}_{p}xy\vee D^{=}_{1-p}xy))\\[17.07164pt] \hskip 82.51299pt\displaystyle\vee\,\bigvee_{I_{i}=-(p,q_{j},q_{k})}(q_{i}x\wedge q_{j}y\wedge(D^{=}_{p}xy\vee D^{=}_{1-p}xy))\big{)}\big{)}\\[17.07164pt] \wedge\,\forall x\forall y\,(D^{+}_{p}xy\rightarrow(\neg\exists z\,R_{p}yz\vee(\neg\exists z\,R_{p}xz\wedge\exists z\,(R_{p}yz\wedge\exists xR_{p}zx))\\[5.69054pt] \hskip 82.51299pt\vee\,\exists z(H_{1}^{+}xyz\wedge R_{p}xz\wedge\exists x(H_{2}^{+}xzy\wedge R_{p}yx\wedge D^{+}_{p}zx)).\end{array}$$

$$\displaystyle\varphi_{2}\wedge\exists x\big{(}t(x)\wedge\bigwedge_{\lambda\in T}\exists y\,\lambda(x,y)\wedge\forall y\,\bigvee_{R\in\mathsf{sig}(\varphi_{2})}((Rxy\vee Ryx)\rightarrow\bigvee_{\lambda\in T}\lambda(x,y))\big{)}$$

$$\begin{array}[]{l}\{q_{0},q_{\bot}\}\cup\mathsf{TP}_{0}\cup\{t,t^{?},t_{\uparrow},t_{\downarrow},t_{\&},t^{i},t^{i}_{\uparrow},t^{i}_{\downarrow}\mid t\in\mathsf{TP}_{1},\;i\in\{0,1\}\}\,\cup\\[2.84526pt] \{\lambda,\lambda_{\uparrow},\lambda^{i},\lambda^{i}_{\uparrow}\mid\lambda\in\mathsf{TP}_{2},\;i\in\{0,1\}\},\end{array}$$

$$\begin{array}[]{rcll}\delta_{2}(q_{0},\sigma)&=&\displaystyle\bigvee_{s\in\mathsf{TP}_{0}}\big{(}s\wedge\bigwedge_{\exists x\,\varphi(x)\in s}\bigvee_{\begin{subarray}{c}t\in\mathsf{TP}_{1}\mid\\ s\cup\{\varphi(x)\}\subseteq t\end{subarray}}t^{?}\big{)}\\[14.22636pt] \delta_{2}(s,\sigma)&=&\Box s\wedge\displaystyle\bigvee_{\begin{subarray}{c}t\in\mathsf{TP}_{1},s\subseteq t\end{subarray}}t&\\[14.22636pt] \delta_{2}(t^{?},\sigma)&=&\langle-1\rangle t^{?}\vee\Diamond t^{?}\vee t^{0}\end{array}$$

$$\begin{array}[]{rcll}\delta_{2}(t,(\tau,M))&=&t_{\uparrow}\wedge\Box t_{\downarrow}\wedge\displaystyle\bigvee_{T\mid t\approx T}\bigwedge_{\lambda\in T}(\Diamond\lambda\vee\lambda_{\uparrow})&\text{if }\tau_{y}=_{\Sigma}t\end{array}$$

$$\begin{array}[]{rcll}\delta_{2}(t,(\tau,M))&=&\mathsf{false}&\text{if }\tau_{y}\not=_{\Sigma}t\\[5.69054pt] \delta_{2}(t_{\downarrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t_{\downarrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda}\lambda_{y}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(t_{\uparrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t_{\uparrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda^{-}}[-1]\lambda_{y}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda,(\tau,M))&=&\lambda_{y}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda\\ \delta_{2}(\lambda,(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda\\ \delta_{2}(\lambda,(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda_{\uparrow},(\tau,M))&=&\langle-1\rangle\lambda_{y}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda_{\uparrow},(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda_{\uparrow},(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\end{array}$$

$$A=\{0,\dots ,k\}\cup \{a_j^i\mid 0<i\le k,0<j<n_i\}\cup \{b_j^i\mid 0<i\le k,0<j<m_i\}$$

$$\begin{array}[]{rcl}N^{\mathfrak{A}}&=&\{(i,i+1)\mid i<k\}\\[2.84526pt] R_{1}^{\mathfrak{A}}&=&\bigcup_{i\leq k}\{(i,a_{1}^{i}),(a_{1}^{i},a_{2}^{i}),\ldots,(a_{n_{i}-2}^{i},a_{n_{i}-1}^{i})\}\\[2.84526pt] R_{2}^{\mathfrak{A}}&=&\bigcup_{i\leq k}\{(i,b_{1}^{i}),(b_{1}^{i},b_{2}^{i}),\ldots,(b_{m_{i}-2}^{i},b_{m_{i}-1}^{i})\}\\[2.84526pt] S^{\mathfrak{A}}&=&\{0\}\\[2.84526pt] q^{\mathfrak{A}}&=&\{i\mid q_{i}=q\}\text{ for any }q\in Q.\end{array}$$

$$\begin{array}[]{l}\displaystyle\forall x\big{(}Gx\rightarrow\bigvee_{T\in\mathfrak{T}}(Tx\wedge\bigwedge_{T^{\prime}\in\mathfrak{T},\;T^{\prime}\not=T}\neg T^{\prime}x)\big{)}\\[14.22636pt] \displaystyle\forall x\big{(}Gx\rightarrow\bigwedge_{T\in\mathfrak{T}}\big{(}Tx\rightarrow(\bigvee_{(T,T^{\prime})\in H}\forall y(R_{h}xy\rightarrow T^{\prime}y)\wedge\bigvee_{(T,T^{\prime})\in V}\forall y(R_{v}xy\rightarrow T^{\prime}y))\big{)}\big{)}.\end{array}$$

$$\begin{array}[]{l}\forall x\big{(}Gx\wedge B_{\rightarrow}x\rightarrow\big{(}\neg\exists yR_{h}xy\wedge\forall y(R_{v}xy\rightarrow B_{\rightarrow}y)\wedge\forall y(R_{v}yx\rightarrow B_{\rightarrow}y)\big{)}\big{)}\\[5.69054pt] \forall x\big{(}Gx\wedge\neg B_{\rightarrow}x\rightarrow\exists yR_{h}xy\big{)}\end{array}$$

$$\exists x(Ox\wedge B_{\leftarrow }x\wedge B_{\downarrow }x).$$

$$\forall x\big{(}Ox\rightarrow Gx),\quad\forall x(Gx\rightarrow\forall y(R_{h}xy\rightarrow Gy)),\quad\forall x(Gx\rightarrow\forall y(R_{v}xy\rightarrow Gy)).$$

$$\forall x(B_{\to }x\to \underset{T\in \mathsf{Right}}{\bigvee }T(x)).$$

$$\forall x\big{(}Qx\rightarrow\big{(}\exists y(R_{h}xy\wedge Qy)\vee\exists y(R_{v}xy\wedge Qy)\vee\varphi_{D}x\big{)}\big{)}$$

$$\varphi_{D}x=\exists y\big{(}R_{h}xy\wedge\forall x(R_{v}yx\rightarrow Px)\big{)}\wedge\exists y\big{(}R_{v}xy\wedge\forall x(R_{h}yx\rightarrow\neg Px)\big{)}$$

$$\begin{array}[]{rcl}\psi&=&\forall x\,(Gx\rightarrow\bigvee_{i,j}P_{i,j}x)\\[2.84526pt] &&\displaystyle\wedge\;\bigwedge_{(i,j)\neq(i^{\prime},j^{\prime})}\forall x\,\neg(P_{i,j}x\wedge P_{i^{\prime},j^{\prime}}x)\\[2.84526pt] &&\wedge\;\forall x\forall y\,(R_{h}xy\leftrightarrow\bigvee_{i,j}P_{i,j}x\wedge P_{i+1,j}y)\\[2.84526pt] &&\wedge\;\forall x\forall y\,(R_{v}x,y\leftrightarrow\bigvee_{i,j}P_{i,j}x\wedge P_{i,j+1}y)\\[2.84526pt] &&\wedge\;\forall x\,(Ox\rightarrow P_{0,0}x).\end{array}$$

$$Q_1=\{q_{\phi (x)}\mid \phi (x)\in \mathsf{cl}({\phi }_1)\}\cup \{q_{\phi (x,\underline{y})},q_{\phi (\underline{x},y)}\mid \phi (x,y)\in \mathsf{cl}({\phi }_1)\}$$

$$\begin{array}[]{r@{\;}c@{\;}l}\delta_{1}(q_{Az},\sigma)&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Ay\in\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[8.53581pt] \delta_{1}(q_{\neg Az},\sigma)&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Ay\notin\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[8.53581pt] \delta_{1}(q_{\varphi(z)\circ\psi(z)},\sigma)&=&q_{\varphi(z)}\circ q_{\psi(z)}\\[2.84526pt] \delta_{1}(q_{\exists z(z=z\wedge\psi(z))})&=&\displaystyle q_{\psi(z)}\vee\langle-1\rangle q_{\exists z(z=z\wedge\psi(z))}\vee\Diamond q_{\exists z(z=z\wedge\psi(z))}\\[2.84526pt] \delta_{1}(q_{\forall z(z=z\rightarrow\psi(z))})&=&\displaystyle q_{\psi(z)}\wedge[-]q_{\forall z(z=z\rightarrow\psi(z))}\wedge\Box q_{\forall z(z=z\rightarrow\psi(z))}\\[2.84526pt] \delta_{1}(q_{\exists z^{\prime}\,\varphi(z,z^{\prime})},\sigma)&=&\Diamond q_{\varphi(z,\underline{z}^{\prime})}\vee q_{\varphi(z^{\prime},\underline{z})}\\[2.84526pt] \delta_{1}(q_{\forall z^{\prime}\,\varphi(z,z^{\prime})},\sigma)&=&\Box q_{{\varphi(z,\underline{z}^{\prime})}}\wedge q_{{\varphi(z^{\prime},\underline{z})}}\end{array}$$

$$\begin{array}[]{r@{\;}c@{\;}l}\delta_{1}(q_{Rz\underline{z}^{\prime}},\sigma))&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Rxy\in\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[11.38109pt] \delta_{1}(q_{R\underline{z}z^{\prime}},\sigma))&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Ryx\in\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[11.38109pt] \delta_{1}(q_{\neg Rz\underline{z}^{\prime}},\sigma))&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Rxy\notin\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[11.38109pt] \delta_{1}(q_{\neg R\underline{z}z^{\prime}},\sigma))&=&\left\{\begin{array}[]{ll}\mathsf{true}&\text{if }Ryx\notin\tau\\ \mathsf{false}&\text{otherwise}\end{array}\right.\\[11.38109pt] \delta_{1}(q_{\varphi(z,\underline{z}^{\prime})\circ\psi(z,\underline{z}^{\prime})},\sigma)&=&q_{\varphi(z,\underline{z}^{\prime})}\circ q_{\psi(z,\underline{z}^{\prime})}\\[2.84526pt] \delta_{1}(q_{\varphi(z,\underline{z}^{\prime})\circ\psi(z)},\sigma)&=&q_{\varphi(z,\underline{z}^{\prime})}\circ\langle-1\rangle q_{\psi(z)}\\[2.84526pt] \delta_{1}(q_{\varphi(z,\underline{z}^{\prime})\circ\psi(z^{\prime})},\sigma)&=&q_{\varphi(z,\underline{z}^{\prime})}\circ q_{\psi(z^{\prime})}\\[2.84526pt] \delta_{1}(q_{\varphi(z)\circ\psi(z^{\prime})},\sigma)&=&\langle-1\rangle q_{\varphi(z)}\circ q_{\psi(z^{\prime})}\end{array}$$

$$\begin{array}[]{rcll}\delta_{2}(t^{0},(\tau,M))&=&t^{0}_{\uparrow}\wedge\Box t^{0}_{\downarrow}\wedge\displaystyle\bigvee_{T\mid t\approx T}\bigwedge_{\lambda\in T}(\Diamond\lambda^{0}\vee\lambda^{0}_{\uparrow})&\text{if }\tau_{y}=_{\Sigma}t\\ \delta_{2}(t^{0},(\tau,M))&=&\mathsf{false}&\text{if }\tau_{y}\not=_{\Sigma}t\\[5.69054pt] \delta_{2}(t^{0}_{\downarrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t^{0}_{\downarrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda}\lambda_{y}^{0}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(t^{0}_{\uparrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t^{0}_{\uparrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda^{-}}[-1]\lambda_{y}^{M}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda^{0},(\tau,M))&=&\lambda_{y}^{0}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda\\ \delta_{2}(\lambda^{0},(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda\\ \delta_{2}(\lambda^{0},(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda^{0}_{\uparrow},(\tau,M))&=&\langle-1\rangle(\lambda_{y})_{\&}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda^{0}_{\uparrow},(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda^{0}_{\uparrow},(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\\ \delta_{2}(t_{\&},(\tau,M))&=&t^{M}\end{array}$$

$$\begin{array}[]{rcl@{\;}l}\delta_{2}(t^{1},(\tau,1))&=&\big{(}t^{?}\wedge t^{1}_{\uparrow}\wedge\Box t^{1}_{\downarrow}\wedge\displaystyle\bigvee_{T\mid t\approx T}\bigwedge_{\lambda\in T}(\Diamond\lambda^{1}\vee\lambda^{1}_{\uparrow})\big{)}&\text{if }\tau_{y}=_{\Sigma}t\\ &&\vee\;(t^{?}\wedge\langle-1\rangle q_{\bot})\\[5.69054pt] \delta_{2}(t^{1},(\tau,0))&=&\big{(}t^{?}\wedge t^{1}_{\uparrow}\wedge\Box t^{0}_{\downarrow}\wedge\displaystyle\bigvee_{T\mid t\approx T}\bigwedge_{\lambda\in T}(\Diamond\lambda^{0}\vee\lambda^{1}_{\uparrow})\big{)}&\text{if }\tau_{y}=_{\Sigma}t\\ &&\vee\;(t^{?}\wedge\langle-1\rangle q_{\bot})\\[5.69054pt] \delta_{2}(t^{1},(\tau,M))&=&\langle-1\rangle q_{\bot}&\text{if }\tau_{y}\not=_{\Sigma}t\\ \delta_{2}(q_{\bot},(\tau,0))&=&\mathsf{false}\\ \delta_{2}(q_{\bot},(\tau,1))&=&\mathsf{true}\\[5.69054pt] \delta_{2}(t^{1}_{\downarrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t^{1}_{\downarrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda}\lambda_{y}^{1}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(t^{1}_{\uparrow},(\tau,M))&=&\mathsf{true}&\text{if $\tau$ is not $\Sigma$-guarded}\\ \delta_{2}(t^{1}_{\uparrow},(\tau,M))&=&\displaystyle\bigvee_{\lambda\mid t\approx\lambda\wedge\tau=_{\Sigma}\lambda^{-}}[-1]\lambda_{y}^{1}&\text{if $\tau$ is $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda^{1},(\tau,M))&=&\lambda_{y}^{1}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda\\ \delta_{2}(\lambda^{1},(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda\\ \delta_{2}(\lambda^{1},(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\\[5.69054pt] \delta_{2}(\lambda^{1}_{\uparrow},(\tau,M))&=&\langle-1\rangle\lambda_{y}^{1}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda^{1}_{\uparrow},(\tau,M))&=&\mathsf{false}&\text{if }\lambda\text{ is $\Sigma$-guarded and }\tau\not=_{\Sigma}\lambda^{-}\\ \delta_{2}(\lambda^{1}_{\uparrow},(\tau,M))&=&\lambda_{y}^{?}&\text{if $\lambda$ is not $\Sigma$-guarded}\end{array}$$

$$\forall x(Px\to {\phi }_{C=0}(x))$$

$$\displaystyle\forall x\big{(}\varphi_{C<2^{n}-1}(x)\rightarrow\big{(}\exists yNxy\wedge\forall y(Nxy\rightarrow\varphi_{C{+}{+}}(x,y)\big{)}\big{)}$$

$$\displaystyle\forall x\big{(}\varphi_{C=2^{n}-1}(x)\rightarrow(\exists yLxy\wedge\forall y(Lxy\rightarrow\varphi_{C=0}(y))\wedge\exists yRxy\wedge\forall y(Rxy\rightarrow\varphi_{C=0}(y)))\big{)}$$

$$\displaystyle\forall x\big{(}(Px\rightarrow Fx)\wedge\forall y(Nxy\rightarrow Fy)\big{)}$$

$$\displaystyle\forall x\bigvee_{\alpha\in\Gamma\cup(Q\times\Gamma)}\big{(}S_{\alpha}x\wedge\bigwedge_{\beta\in(\Gamma\cup(Q\times\Gamma))\setminus\{\alpha\}}\neg S_{\beta}x\big{)}$$

$$\displaystyle\forall x\bigvee_{\alpha\in\Gamma\cup(Q\times\Gamma)}\big{(}S^{p}_{\alpha}x\wedge\bigwedge_{\beta\in(\Gamma\cup(Q\times\Gamma))\setminus\{\alpha\}}\neg S^{p}_{\beta}x\big{)}$$

$$\displaystyle\forall x\big{(}(Fx\wedge\varphi_{C=0}(x))\rightarrow S_{q_{0},a_{0}}x\big{)}$$

$$\displaystyle\forall x\big{(}(Fx\wedge\varphi_{C=i}(x))\rightarrow S_{a_{i}}x\big{)}\qquad\text{ for }1\leq i<n$$

$$\displaystyle\forall x\big{(}(Fx\wedge\varphi_{C\geq n}(x))\rightarrow S_{\Box}x\big{)}$$

Full text

1 Introduction

Conservative extensions are a fundamental notion in logic. In mathematical logic, they provide an important tool for relating logical theories, such as theories of arithmetic and theories that emerge in set theory [38, 34]. In computer science, they come up in diverse areas such as software specification [14], higher order theorem proving [18], and ontologies [27]. In these applications, it would be very useful to decide, given two sentences $\varphi_{1}$ and $\varphi_{2}$, whether $\varphi_{1}\wedge\varphi_{2}$ is a conservative extension of $\varphi_{1}$. As expected, this problem is undecidable in first-order logic (FO). In contrast, it has been observed in recent years that conservative extensions are decidable in many modal and description logics [16, 29, 30, 7]. This observation is particularly interesting from the viewpoint of ontologies, where conservative extensions have many natural applications including modularity and reuse, refinement, versioning, and forgetting [11, 27].

Regarding decidability, conservative extensions thus seem to behave similarly to the classical satisfiability problem, which is also undecidable in FO while it is decidable for modal and description logics. In the case of satisfiability, the aim to understand the deeper reasons for this discrepancy and to push the limits of decidability to more expressive fragments of FO has sparked a long line of research that identified prominent decidable FO fragments such as the two-variable fragment FO2 [37, 32], its extension with counting quantifiers C2 [22], the guarded fragment GF [1], and the guarded negation fragment GNF [4], see also [6, 19, 36, 26] and references therein. These fragments have sometimes been used as a replacement for the modal and description logics that they generalize, and in particular the guarded fragment has been proposed as an ontology language [3]. Motivated by this situation, the aim of the current paper is to study the following two questions:

Are conservative extensions decidable in relevant fragments of FO such as FO2, C2, GF, and GNF? 2. 2.

What are the deeper reasons for decidability of conservative extensions in modal and description logics and how far can the limits of decidability be pushed?

To be more precise, we concentrate on deductive conservative extensions, that is, $\varphi_{1}\wedge\varphi_{2}$ is a conservative extension of $\varphi_{1}$ if for every sentence $\psi$ formulated in the signature of $\varphi_{1}$, $\varphi_{1}\wedge\varphi_{2}\models\psi$ implies $\varphi_{1}\models\psi$. There is also a model-theoretic notion of conservative extension which says that $\varphi_{1}\wedge\varphi_{2}$ is a conservative extension of $\varphi_{1}$ if every model of $\varphi_{1}$ can be extended to a model of $\varphi_{2}$ by interpreting the additional symbols in $\varphi_{2}$. Model-theoretic conservative extensions imply deductive conservative extensions, but the converse fails unless one works with a very expressive logic such as second-order logic [27]. In fact, model-theoretic conservative extensions are undecidable even for some very inexpressive description logics that include neither negation nor disjunction [28]. Deductive conservative extensions, as studied in this paper, are closely related to other important notions in logic, such as uniform interpolation [33, 40, 5]. For example, in logics that enjoy Craig interpolation, a decision procedure for conservative extensions can also be used to decide whether a given sentence $\varphi_{2}$ is a uniform interpolant of a given sentence $\varphi_{1}$ regarding the symbols used in $\varphi_{2}$.

Instead of concentrating only on conservative extensions, we also consider two related reasoning problems that we call $\Sigma$-entailment and $\Sigma$-inseparability, where $\Sigma$ denotes a signature. The definitions are as follows: a sentence $\varphi_{1}$ $\Sigma$-entails a sentence $\varphi_{2}$ if for every sentence $\psi$ formulated in $\Sigma$, $\varphi_{2}\models\psi$ implies $\varphi_{1}\models\psi$. This can be viewed as a more relaxed notion of conservative extension where it is not required that one sentence actually extends the other as in the conjunction $\varphi_{1}\wedge\varphi_{2}$ used in the definition of conservative extensions. Two sentences $\varphi_{1},\varphi_{2}$ are $\Sigma$-inseparable if they $\Sigma$-entail each other. We generally prove lower bounds for conservative extensions and upper bounds for $\Sigma$-entailment, in this way obtaining the same decidability and complexity results for all three problems.

Our first main result is that conservative extensions are undecidable in FO2 and (the three-variable fragment of) GF, and in fact in all fragments of FO that contain at least one of the two; note that the latter is not immediate because the separating sentence $\psi$ in the definition of conservative extensions ranges over all sentences from the considered fragment, giving greater separating power when we move to a larger fragment. The proofs are by reductions from the halting problem for two-register machines and a tiling problem, respectively. We note that undecidability of conservative extensions also implies that there is no extension of the logic in question in which consequence is decidable and that has effective uniform interpolation (in the sense that uniform interpolants exist and are computable). We then show as our second main result that, in the two-variable guarded fragment GF2, $\Sigma$-entailment is decidable in 2ExpTime. Regarding the satisfiability problem, GF2 behaves fairly similarly to modal and description logics. It is thus suprising that deciding $\Sigma$-entailment (and conservative extensions) in GF2 turns out to be much more challenging than in most modal and description logics. There, the main approach to proving decidability of $\Sigma$-entailment is to first establish a suitable model-theoretic characterization based on bisimulations which is then used as a foundation for a decision procedure based on tree automata [30, 7]. In GF2, an analogous characterization in terms of appropriate guarded bisimulation fails. Instead, one has to demand the existence of $k$-bounded (guarded) bisimulations, for all $k$, and while tree automata can easily handle bisimulations, it is not clear how they can deal with such an infinite family of bounded bisimulations. We solve this problem by a very careful analysis of the situation and by providing another characterization that can be viewed as being ‘half way’ between a model-theoretic characterization and an automata-encoding of $\Sigma$-entailment.

We also observe that a 2ExpTime lower bound from [16] for conservative extensions in description logics can be adapted to GF2, and consequently our upper bound is tight. It is known that GF2 enjoys Craig interpolation and thus our results are also relevant to deciding uniform interpolants and to a stronger version of conservative extensions in which the separating sentence $\psi$ can also use ‘helper symbols’ that occur neither in $\varphi_{1}$ nor in $\varphi_{2}$.

2 Preliminaries

We introduce the fragments of classical first-order logic (FO) that are relevant for this paper. We generally admit equality and disallow function symbols and constants. With FO2, we denote the two-variable fragment of FO, obtained by fixing two variables $x$ and $y$ and disallowing the use of other variables [37, 32]. In FO2 and fragments thereof, we generally admit only predicates of arity one and two, which is without loss of generality [20]. In the guarded fragment of FO, denoted GF, quantification is restricted to the pattern

[TABLE]

where $\varphi(\bf{x},\bf{y})$ is a GF formula with free variables among $\bf{x},\bf{y}$ and $\alpha(\bf{x},\bf{y})$ is an atomic formula $R\mathbf{x}\mathbf{y}$ or an equality $x=y$ that in either case contains all variables in $\bf{x},\bf{y}$ [1, 19]. The formula $\alpha$ is called the guard of the quantifier. The $k$-variable fragment of GF, defined in the expected way, is denoted GF${}^{\,k}$. Apart from the logics introduced so far, in informal contexts we shall also mention several related description logics. Exact definitions are omitted, we refer the reader to [2].

A signature $\Sigma$ is a finite set of predicates. We use GF$(\Sigma)$ to denote the set of all GF-sentences that use only predicates from $\Sigma$ (and possibly equality), and likewise for GF${}^{2}(\Sigma)$ and other fragments. We use $\mathsf{sig}(\varphi)$ to denote the set of predicates that occur in the FO formula $\varphi$. Note that we consider equality to be a logical symbol, rather than a predicate, and it is thus never part of a signature. We write $\varphi_{1}\models\varphi_{2}$ if $\varphi_{2}$ is a logical consequence of $\varphi_{1}$. The next definition introduces the central notions studied in this paper.

Definition 2.1**.**

Let $F$ be a fragment of FO, $\varphi_{1},\varphi_{2}$ $F$-sentences and $\Sigma$ a signature. Then

$\varphi_{1}$* $\Sigma$-entails $\varphi_{2}$, written $\varphi_{1}\models_{\Sigma}\varphi_{2}$, if for all $F(\Sigma)$-sentences $\psi$, $\varphi_{2}\models\psi$ implies $\varphi_{1}\models\psi$;* 2. 2.

$\varphi_{1}$* and $\varphi_{2}$ are $\Sigma$-inseparable if $\varphi_{1}$ $\Sigma$-entails $\varphi_{2}$ and vice versa;* 3. 3.

$\varphi_{1}\wedge\varphi_{2}$* is a conservative extension of $\varphi_{1}$ if $\varphi_{1}$ $\mathsf{sig}(\varphi_{1})$-entails $\varphi_{1}\wedge\varphi_{2}$.*

Note that $\Sigma$-entailment could equivalently be defined as follows when $F$ is closed under negation: $\varphi_{1}$ $\Sigma$-entails $\varphi_{2}$ if for all $F(\Sigma)$-sentences $\psi$, satisfiability of $\varphi_{1}\wedge\psi$ implies satisfiability of $\varphi_{2}\wedge\psi$. If $\varphi_{1}$ does not $\Sigma$-entail $\varphi_{2}$, there is thus an $F(\Sigma)$-sentence $\psi$ such that $\varphi_{1}\wedge\psi$ is satisfiable while $\varphi_{2}\wedge\psi$ is not. We refer to such $\psi$ as a witness sentence for non-$\Sigma$-entailment.

Example 2.2**.**

(1) $\Sigma$-entailment is a weakening of logical consequence, that is, $\varphi_{1}\models\varphi_{2}$ implies $\varphi_{1}\models_{\Sigma}\varphi_{2}$ for any $\Sigma$. The converse is true when $\mathsf{sig}(\varphi_{2})\subseteq\Sigma$.

(2) Consider the GF2 sentences $\varphi_{1}=\forall x\exists yRxy$ and $\varphi_{2}=\forall x(\exists y(Rxy\wedge Ay)\wedge\exists y(Rxy\wedge\neg Ay))$ and let $\Sigma=\{R\}$. Then $\psi=\forall xy(Rxy\rightarrow x=y)$ is a witness for $\varphi_{1}\not\models_{\Sigma}\varphi_{2}$. If $\varphi_{1}$ is replaced by $\varphi_{1}^{\prime}=\forall x\exists y(Rxy\wedge x\not=y)$ we obtain $\varphi_{1}^{\prime}\models_{\Sigma}\varphi_{2}$ since GF2 cannot count the number of $R$-successors.

It is important to note that different fragments $F$ of FO give rise to different notions of $\Sigma$-entailment, $\Sigma$-inseparability and conservative extensions. For example, if $\varphi_{1}$ and $\varphi_{2}$ belong to GF2, then they also belong to GF and to FO2, but it might make a difference whether witness sentences range over all GF2-sentences, over all GF-sentences, or over all FO2-sentences. If we want to emphasize the fragment $F$ in which witness sentences are formulated, we speak of $F(\Sigma)$-entailment instead of $\Sigma$-entailment and write $\varphi_{1}\models_{F(\Sigma)}\varphi_{2}$, and likewise for $F(\Sigma)$-inseparability and $F$-conservative extensions.

Example 2.3**.**

Let $\varphi_{1}^{\prime}$, $\varphi_{2}$, and $\Sigma=\{R\}$ be from Example 2.2 (2). Then $\varphi_{1}^{\prime}$ GF${}^{2}(\Sigma)$-entails $\varphi_{2}$ but $\varphi_{1}^{\prime}$ does not FO$(\Sigma)$-entail $\varphi_{2}$; a witness is given by $\forall xy_{1}y_{2}((Rxy_{1}\wedge Rxy_{2})\rightarrow y_{1}=y_{2})$.

Note that conservative extensions and $\Sigma$-inseparability reduce in polynomial time to $\Sigma$-entailment (with two calls to $\Sigma$-entailment required in the case of $\Sigma$-inseparability). Moreover, conservative extensions reduce in polynomial time to $\Sigma$-inseparability. We thus state our upper bounds in terms of $\Sigma$-entailment and lower bounds in terms of conservative extensions.

There is a natural variation of each of the three notions in Definition 2.1 obtained by allowing to use additional ‘helper predicates’ in witness sentences. For a fragment $F$ of FO, $F$-sentences $\varphi_{1},\varphi_{2}$, and a signature $\Sigma$, we say that $\varphi_{1}$ strongly $\Sigma$-entails $\varphi_{2}$ if $\varphi_{1}$ $\Sigma^{\prime}$-entails $\varphi_{2}$ for any $\Sigma^{\prime}$ with $\Sigma^{\prime}\cap\textup{{sig}}(\varphi_{2})\subseteq\Sigma$. Strong $\Sigma$-inseparability and strong conservative extensions are defined accordingly. Strong $\Sigma$-entailment implies $\Sigma$-entailment, but the converse may fail.

Example 2.4**.**

GF$(\Sigma)$-entailment does not imply strong GF$(\Sigma)$-entailment. Let $\varphi_{1}$ state that the binary predicate $R$ is irreflexive and symmetric and let $\varphi_{2}$ be the conjunction of $\varphi_{1}$ and $\forall x(Ax\rightarrow\forall y(Rxy\rightarrow\neg Ay))\wedge\forall x(\neg Ax\rightarrow\forall y(Rxy\rightarrow Ay))$. Thus, an $\{R\}$-structure satisfying $\varphi_{1}$ can be extended to a model of $\varphi_{2}$ if it contains no $R$-cycles of odd length. Now observe that any satisfiable GF$(\{R\})$ sentence is satisfiable in a forest $\{R\}$-structure (see Section 4 for a precise definition). Hence, if a GF$(\{R\})$-sentence is satisfiable in an irreflexive and symmetric structure then it is satisfiable in a structure without odd cycles and so $\varphi_{1}$ GF$(\{R\})$-entails $\varphi_{2}$. In contrast, for the fresh ternary predicate $Q$ and $\psi=\exists x_{1}x_{2}x_{3}(Qx_{1}x_{2}x_{3}\wedge Rx_{1}x_{2}\wedge Rx_{2}x_{3}\wedge Rx_{3}x_{1})$ we have $\varphi_{2}\models\neg\psi$ but $\varphi_{1}\not\models\neg\psi$ and so $\psi$ witnesses that $\varphi_{1}$ does not GF$(\{R,Q\})$-entail $\varphi_{2}$.

The example above is inspired by proofs that GF does not enjoy Craig interpolation [24, 13]. This is not accidental, as we explain next. Recall that a fragment $F$ of FO has Craig interpolation if for all $F$-sentences $\psi_{1},\psi_{2}$ with $\psi_{1}\models\psi_{2}$ there exists an $F$-sentence $\psi$ (called an $F$-interpolant for $\psi_{1},\psi_{2}$) such that $\psi_{1}\models\psi\models\psi_{2}$ and $\textup{{sig}}(\psi)\subseteq\textup{{sig}}(\psi_{1})\cap\textup{{sig}}(\psi_{2})$. $F$ has uniform interpolation if one can always choose an $F$-interpolant that does not depend on $\psi_{2}$, but only on $\psi_{1}$ and $\textup{{sig}}(\psi_{1})\cap\textup{{sig}}(\psi_{2})$. Thus, given $\psi_{1}$, $\psi$ and $\Sigma$ with $\psi_{1}\models\psi$ and $\textup{{sig}}(\psi)\subseteq\Sigma$, then $\psi$ is a uniform $F(\Sigma)$-interpolant of $\psi_{1}$ iff $\psi$ strongly $F(\Sigma)$-entails $\psi_{1}$. Both Craig interpolation and uniform interpolation have been investigated extensively, for example for intuitionistic logic [33], modal logics [40, 12, 31], guarded fragments [13], and description logics [30]. The following observation summarizes the connection between (strong) $\Sigma$-entailment and interpolation.

Theorem 2.5**.**

Let $F$ be a fragment of FO that enjoys Craig interpolation. Then $F(\Sigma)$-entailment implies strong $F(\Sigma)$-entailment. In particular, if $\varphi_{2}\models\varphi_{1}$ and $\textup{{sig}}(\varphi_{1})\subseteq\Sigma$, then $\varphi_{1}$ is a uniform $F(\Sigma)$-interpolant of $\varphi_{2}$ iff $\varphi_{1}$ $F(\Sigma)$-entails $\varphi_{2}$.

Proof 2.6**.**

Assume $\varphi_{1}$ does not strongly $F(\Sigma)$-entail $\varphi_{2}$. Then there is an $F$-sentence $\psi$ with $\textup{{sig}}(\psi)\cap\textup{{sig}}(\varphi_{2})\subseteq\Sigma$ such that $\varphi_{2}\models\psi$ and $\varphi_{1}\wedge\neg\psi$ is satisfiable. Let $\chi$ be an interpolant for $\varphi_{2}$ and $\psi$ in $F$. Then $\neg\chi$ witnesses that $\varphi_{1}$ does not $F(\Sigma)$-entail $\varphi_{2}$.

The uniform interpolant recognition problem for $F$ is the problem to decide whether a sentence $\psi$ is a uniform $F(\Sigma)$-interpolant of a sentence $\psi^{\prime}$. It follows from Theorem 2.5 that in any fragment $F$ of FO that enjoys Craig interpolation, this problem reduces in polynomial time to $\Sigma$-inseparability in $F$ and that, conversely, conservative extension in $F$ reduces in polynomial time to the uniform interpolant recognition problem in $F$. Neither GF nor FO2 nor description logics with role inclusions enjoy Craig interpolation [24, 10, 27], but GF2 does [24]. Thus, our decidability and complexity results for $\Sigma$-entailment in GF2 also apply to strong $\Sigma$-entailment and the uniform interpolant recognition problem.

3 Undecidability

We prove that conservative extensions are undecidable in GF3 and in FO2, and consequently so are $\Sigma$-entailment and $\Sigma$-inseparability (as well as strong $\Sigma$-entailment and the uniform interpolant recognition problem). These results hold already without equality and in fact apply to all fragments of FO that contain at least one of GF3 and FO2 such as the guarded negation fragment [4] and the two-variable fragment with counting quantifiers [22].

We start with the case of GF3, using a reduction from the halting problem of two-register machines. A (deterministic) two-register machine (2RM) is a pair $M=(Q,P)$ with $Q=q_{0},\dots,q_{\ell}$ a set of states and $P=I_{0},\dots,I_{\ell-1}$ a sequence of instructions. By definition, $q_{0}$ is the initial state, and $q_{\ell}$ the halting state. For all $i<\ell$,

• •

either $I_{i}=+(p,q_{j})$ is an incrementation instruction with $p\in\{0,1\}$ a register and $q_{j}$ the subsequent state;

• •

or $I_{i}=-(p,q_{j},q_{k})$ is a decrementation instruction with $p\in\{0,1\}$ a register, $q_{j}$ the subsequent state if register $p$ contains 0, and $q_{k}$ the subsequent state otherwise.

A configuration of $M$ is a triple $(q,m,n)$, with $q$ the current state and $m,n\in\mathbbm{N}$ the register contents. We write $(q_{i},n_{1},n_{2})\Rightarrow_{M}(q_{j},m_{1},m_{2})$ if one of the following holds:

• •

$I_{i}=+(p,q_{j})$, $m_{p}=n_{p}+1$, and $m_{1-p}=n_{1-p}$;

• •

$I_{i}=-(p,q_{j},q_{k})$, $n_{p}=m_{p}=0$, and $m_{1-p}=n_{1-p}$;

• •

$I_{i}=-(p,q_{k},q_{j})$, $n_{p}>0$, $m_{p}=n_{p}-1$, and $m_{1-p}=n_{1-p}$.

The computation of $M$ on input $(n,m)\in\mathbbm{N}^{2}$ is the unique longest configuration sequence $(p_{0},n_{0},m_{0})\Rightarrow_{M}(p_{1},n_{1},m_{1})\Rightarrow_{M}\cdots$ such that $p_{0}=q_{0}$, $n_{0}=n$, and $m_{0}=m$. The halting problem for 2RMs is to decide, given a 2RM $M$, whether its computation on input $(0,0)$ is finite (which implies that its last state is $q_{\ell}$).

We show how to convert a given 2RM $M$ into GF3-sentences $\varphi_{1}$ and $\varphi_{2}$ such that $M$ halts on input $(0,0)$ iff $\varphi_{1}\wedge\varphi_{2}$ is not a conservative extension of $\varphi_{1}$. Let $M=(Q,P)$ with $Q=q_{0},\dots,q_{\ell}$ and $P=I_{0},\dots,I_{\ell-1}$. We assume w.l.o.g. that $\ell\geq 1$ and that if $I_{i}=-(p,q_{j},q_{k})$, then $q_{j}\neq q_{k}$. In $\varphi_{1}$, we use the following set $\Sigma$ of predicates:

• •

a binary predicate $N$ connecting a configuration to its successor configuration;

• •

binary predicates $R_{1}$ and $R_{2}$ that represent the register contents via the length of paths;

• •

unary predicates $q_{0},\ldots,q_{\ell}$ representing the states of $M$;

• •

a unary predicate $S$ denoting points where a computation starts.

We define $\varphi_{1}$ to be the conjunction of several GF2-sentences. First, we say that there is a point where the computation starts:222The formulas that are not syntactically guarded can easily be rewritten into such formulas.

[TABLE]

And second, we add that whenever $M$ is not in the final state, there is a next configuration. For $0\leq i<\ell$:

[TABLE]

The second sentence $\varphi_{2}$ is constructed so as to express that either $M$ does not halt or the representation of the computation of $M$ contains a defect, using the following additional predicates:

• •

a unary predicate $P$ used to represent that $M$ does not halt;

• •

binary predicates $D^{+}_{p},D_{p}^{-},D_{p}^{=}$ used to describe defects in incrementing, decrementing, and keeping register $p\in\{0,1\}$;

• •

ternary predicates $H_{1}^{+},H_{2}^{+},H_{1}^{-},H_{2}^{-},H_{1}^{=},H_{2}^{=}$ used as guards for existential quantifiers.

In fact, $\varphi_{2}$ is the disjunction of two sentences. The first sentence says that the computation does not terminate:

[TABLE]

while the second says that registers are not updated properly:

[TABLE]

In this second sentence, additional conjuncts that implement the desired behaviour of $D^{=}_{p}$ and $D^{-}_{p}$ are also needed; they are constructed analogously to the last three lines above (but using guards $H^{-}_{j}$ and $H^{=}_{j}$), details are omitted. The following is proved in the appendix of this paper.

Lemma 3.1**.**

If $M$ halts, then $\varphi_{1}\wedge\varphi_{2}$ is not a $\text{GF}^{\,2}$-conservative extension of $\varphi_{1}$. 2. 2.

If there exists a $\Sigma$-structure that satisfies $\varphi_{1}$ and cannot be extended to a model of $\varphi_{2}$ (by interpreting the predicates in $\mathsf{sig}(\varphi_{2})\setminus\mathsf{sig}(\varphi_{1})$), then $M$ halts.

In the proof of Point 1, the sentence that witnesses non-conservativity describes a halting computation of $M$, up to global GF${}^{2}(\Sigma)$-bisimulations. This can be done using only two variables. The following result is an immediate consequence of Lemma 3.1.

Theorem 3.2**.**

In any fragment of FO that extends the three-variable guarded fragment GF 3, the following problems are undecidable: conservative extensions, $\Sigma$-inseparability, $\Sigma$-entailment, and strong $\Sigma$-entailment.

Since Point 1 of Lemma 3.1 ensures GF2-witnesses, Theorem 3.2 can actually be strengthened to say that GF2-conservative extensions of GF3-sentences are undecidable.

Our result for FO2 is proved by a reduction of a tiling problem that asks for the tiling of a rectangle (of any size) such that the borders are tiled with certain distinguished tiles. Because of space limitations, we defer details to the appendix and state only the obtained result.

Theorem 3.3**.**

In any fragment of FO that extends FO2, the following problems are undecidable: conservative extensions, $\Sigma$-inseparability, $\Sigma$-entailment, and strong $\Sigma$-entailment.

It is interesting to note that the proof of Theorem 3.3 also shows that FO2-conservative extensions of $\mathcal{ALC}$-TBoxes are undecidable while it follows from our results below that GF2-conservative extensions of $\mathcal{ALC}$-TBoxes are decidable.

4 Characterizations

The undecidability results established in the previous section show that neither the restriction to two variables nor guardedness alone are sufficient for decidability of conservative extensions and related problems. In the remainder of the paper, we show that adopting both restrictions simultaneously results in decidability of $\Sigma$-entailment (and thus also of conservative extensions and of inseparability). We proceed by first establishing a suitable model-theoretic characterization and then use it as the foundation for a decision procedure based on tree automata. We in fact establish two versions of the characterization, the second one building on the first one.

We start with some preliminaries. An atomic 1-type for $\Sigma$ is a maximal satisfiable set $\tau$ of atomic GF${}^{2}(\Sigma)$-formulas and their negations that use the variable $x$, only. We use $\text{at}_{\mathfrak{A}}^{\Sigma}(a)$ to denote the atomic 1-type for $\Sigma$ realized by the element $a$ in the structure $\mathfrak{A}$. An atomic 2-type for $\Sigma$ is a maximal satisfiable set $\tau$ of atomic GF${}^{2}(\Sigma)$-formulas and their negations that use the variables $x$ and $y$, only, and contains $\neg(x=y)$. We say that $\tau$ is guarded if it contains an atom of the form $Rxy$ or $Ryx$, $R$ a predicate symbol. We use $\text{at}_{\mathfrak{A}}^{\Sigma}(a,b)$ to denote the atomic 2-type for $\Sigma$ realized by the elements $a,b$ in the structure $\mathfrak{A}$. A relation ${\sim}\subseteq A\times B$ is a GF${}^{2}(\Sigma)$-bisimulation between $\mathfrak{A}$ and $\mathfrak{B}$ if the following conditions hold whenever $a\sim b$:

$\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$; 2. 2.

for every $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ is guarded, there is a $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})=\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ and $a^{\prime}\sim b^{\prime}$ (forth condition); 3. 3.

for every $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ is guarded, there is an $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})=\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ and $a^{\prime}\sim b^{\prime}$ (back condition).

We write $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ and say that $(\mathfrak{A},a)$ and $(\mathfrak{B},b)$ are GF${}^{\,2}(\Sigma)$-bisimilar if there is a GF${}^{2}(\Sigma)$-bisimulation $\sim$ between $\mathfrak{A}$ and $\mathfrak{B}$ with $a\sim b$. If the domain and range of $\sim$ coincide with $A$ and $B$, respectively, then $\sim$ is called a global GF${}^{\,2}(\Sigma)$-bisimulation.

We next introduce a bounded version of bisimulations. For $k\geq 0$, we write $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$ and say that $(\mathfrak{A},a)$ and $(\mathfrak{B},b)$ are $k$-GF${}^{\,2}(\Sigma)$-bisimilar if there is a ${\sim}\subseteq A\times B$ such that the first condition for bisimulations holds and the back and forth conditions can be iterated up to $k$ times starting from $a$ and $b$; a formal definition is in the appendix. It is straightforward to show the following link between $k$-GF2-bisimilarity and GF2-sentences of guarded quantifier depth $k$ (defined in the obvious way).

Lemma 4.1**.**

Let $\mathfrak{A}$ and $\mathfrak{B}$ be structures, $\Sigma$ a signature, and $k\geq 0$. Then the following conditions are equivalent:

for all $a\in A$ there exists $b\in B$ with $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$ and vice versa; 2. 2.

$\mathfrak{A}$* and $\mathfrak{B}$ satisfy the same GF*${}^{\,2}(\Sigma)$-sentences of guarded quantifier depth at most $k$.

The corresponding lemma for GF${}^{2}(\Sigma)$-sentences of unbounded guarded quantifier depth and GF${}^{2}(\Sigma)$-bisimulations holds if $\mathfrak{A}$ and $\mathfrak{B}$ satisfy certain saturation conditions (for example, if $\mathfrak{A}$ and $\mathfrak{B}$ are $\omega$-saturated). It can then be proved that an FO-sentence $\varphi$ is equivalent to a GF2 sentence iff its models are preserved under global GF${}^{2}(\textup{{sig}}(\varphi))$-bisimulations [21, 17]. In modal and description logic, global $\Sigma$-bisimulations can often be used to characterize $\Sigma$-entailment in the following natural way [30]: $\varphi_{1}$ $\Sigma$-entails $\varphi_{2}$ iff every for every (tree) model $\mathfrak{A}$ of $\varphi_{1}$, there exists a (tree) model $\mathfrak{B}$ of $\varphi_{2}$ that is globally $\Sigma$-bisimilar to $\mathfrak{A}$. Such a characterization enables decision procedures based on tree automata, but does not hold for GF2.

Example 4.2**.**

Let $\varphi_{1}=\forall x\exists yRxy$ and let $\varphi_{2}=\varphi_{1}\wedge\exists xBx\wedge\forall x(Bx\rightarrow\exists y(Ryx\wedge By))$. Let $\mathfrak{A}$ be the model of $\varphi_{1}$ that consists of an infinite $R$-path with an initial element. Then there is no model of $\varphi_{2}$ that is globally GF${}^{2}(\{R\})$-bisimilar to $\mathfrak{A}$ since any such model has to contain an infinite $R$-path with no initial element. Yet, $\varphi_{2}$ is a conservative extension of $\varphi_{1}$ which can be proved using Theorem 4.3 below.

We give our first characterization theorem that uses unbounded bisimulations in one direction and bounded bisimulations in the other.

Theorem 4.3**.**

Let $\varphi_{1},\varphi_{2}$ be $GF_{2}$-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every model $\mathfrak{A}$ of $\varphi_{1}$ of finite outdegree, there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$ there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every $b\in B$ and every $k\geq 0$, there is an $a\in A$ such that $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$.

The direction ($\Leftarrow$) follows from Lemma 4.1 and ($\Rightarrow$) can be proved using compactness and $\omega$-saturated structures. Because of the use of $k$-bounded bisimulations (for unbounded $k$), it is not clear how to use Theorem 4.3 to find a decision procedure based on tree automata. In the following, we formulate a more ‘operational’ but also more technical characterization that no longer mentions bounded bisimulations. It additionally refers to forest models $\mathfrak{A}$ of $\varphi_{1}$ (of finite outdegree) instead of unrestricted models, but we remark that Theorem 4.3 also remains true under this modification.

A structure $\mathfrak{A}$ is a forest if its Gaifman graph is a forest. Thus, a forest admits cycles of length one and two, but not of any higher length. A ($\Sigma$-)tree in a forest structure $\mathfrak{A}$ is a maximal ($\Sigma$)-connected substructure of $\mathfrak{A}$. When working with forest structures $\mathfrak{A}$, we will typically view them as directed forests rather than as undirected ones. This can be done by choosing a root for each tree in the Gaifman graph of $\mathfrak{A}$, thus giving rise to notions such as successor, descendant, etc. Which node is chosen as the root will always be irrelevant. Note that the direction of binary relations does not need to reflect the successor relation. When speaking of a path in a forest structure $\mathfrak{A}$, we mean a path in the directed sense; when speaking of a subtree, we mean a tree that is obtained by choosing a root $a$ and restricting the structure to $a$ and its descendants. We say that $\mathfrak{A}$ is regular if it has only finitely many subtrees, up to isomorphism.

To see how we can get rid of bounded bisimulations, reconsider Theorem 4.3. The characterization is still correct if we pull out the quantification over $k$ in Point 2 so that the theorem reads ‘…iff for every model $\mathfrak{A}$ of $\varphi_{1}$ of finite outdegree and every $k\geq 0$, there is…’. In fact, this modified version of Theorem 4.3 is even closer to the definition of $\Sigma$-entailment. It also suggests that we add a marking $A_{\bot}\subseteq A$ of elements in $\mathfrak{A}$, representing ‘break-off points’ for bisimulations, and then replace $k$-bisimulations with bisimulations that stop whenever they have encountered the second marked element on the same path—in this way, the distance between marked elements (roughly) corresponds to the bound $k$ in $k$-bisimulations. However, we would need a marking $A_{\bot}$, for any $k\geq 0$, such that there are infinitely many markers on any infinite path and the distance between any two markers in a tree is at least $k$. It is easy to see that such a marking may not exist, for example when $k=3$ and $\mathfrak{A}$ is the infinite full binary tree. We solve this problem as follows. First, we only demand that the distance between any two markers on the same path is at least $k$. And second, we use the markers only when following bisimulations upwards in a tree while downwards, we use unbounded bisimulations. This does not compromise correctness of the characterization.

We next introduce a version of bisimulations that implement the ideas just explained. Let $\mathfrak{A}$ and $\mathfrak{B}$ be forest models, $\Sigma$ a signature, and $A_{\bot}\subseteq A$. Two relations ${\sim}^{A_{\bot},0}_{\Sigma},{\sim}^{A_{\bot},1}_{\Sigma}\subseteq A\times B$ form an $A_{\bot}$-delimited GF${}^{\,2}(\Sigma)$-bisimulation between $\mathfrak{A}$ and $\mathfrak{B}$ if the following conditions are satisfied:

if $(\mathfrak{A},a)\sim^{A_{\bot},0}_{\Sigma}(\mathfrak{B},b)$, then $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and

1. (a)

for every $a^{\prime}\neq a$ with $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ guarded, there is a $b^{\prime}\not=b$ such that $(\mathfrak{A},a^{\prime})\sim^{A_{\bot},i}_{\Sigma}(\mathfrak{B},b^{\prime})$ where $i=1$ if $a^{\prime}$ is the predecessor of $a$ and $a^{\prime}\in A_{\bot}$, and $i=0$ otherwise; 2. (b)

for every $b^{\prime}\neq b$ with $\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ guarded, there is an $a^{\prime}\not=a$ such that $(\mathfrak{A},a^{\prime})\sim^{A_{\bot},i}_{\Sigma}(\mathfrak{B},b^{\prime})$ where $i=1$ if $a^{\prime}$ is the predecessor of $a$ and $a^{\prime}\in A_{\bot}$, and $i=0$ otherwise; 2. 2.

if $(\mathfrak{A},a)\sim^{A_{\bot},1}_{\Sigma}(\mathfrak{B},b)$ and the predecessor of $a$ in $\mathfrak{A}$ is not in $A_{\bot}$, then $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and

1. (a)

for every $a^{\prime}\neq a$ with $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ guarded, there is a $b^{\prime}\not=b$ such that $(\mathfrak{A},a^{\prime})\sim^{A_{\bot},i}_{\Sigma}(\mathfrak{B},b^{\prime})$ where $i=0$ if $a$ is the predecessor of $a^{\prime}$ and $a\in A_{\bot}$, and $i=1$ otherwise; 2. (b)

for every $b^{\prime}\neq b$ with $\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ guarded, there is an $a^{\prime}\not=a$ such that $(\mathfrak{A},a^{\prime})\sim^{A_{\bot},i}_{\Sigma}(\mathfrak{B},b^{\prime})$ where $i=0$ if $a$ is the predecessor of $a^{\prime}$ and $a\in A_{\bot}$, and $i=1$ otherwise.

Then $(\mathfrak{A},a)$ and $(\mathfrak{B},b)$ are $A_{\bot}$-delimited GF${}^{\,2}(\Sigma)$-bisimilar, in symbols $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},b)$, if there exists an $A_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulation ${\sim}^{A_{\bot},0}_{\Sigma},{\sim}^{A_{\bot},1}_{\Sigma}$ between $\mathfrak{A}$ and $\mathfrak{B}$ such that $(\mathfrak{A},a)\sim^{A_{\bot},0}_{\Sigma}(\mathfrak{B},b)$.

Let $\varphi$ be a GF2-sentence. We use $\mathsf{cl}(\varphi)$ to denote the set of all subformulas of $\varphi$ closed under single negation and renaming of free variables (using only the available variables $x$ and $y$). A $1$-type for $\varphi$ is a subset $t\subseteq\mathsf{cl}(\varphi)$ that contains only formulas of the form $\psi(x)$ and such that $\varphi\wedge\exists x\,\bigwedge t(x)$ is satisfiable. For a model $\mathfrak{A}$ of $\varphi$ and $a\in A$, we use $\mathsf{tp}_{\mathfrak{A}}(a)$ to denote the $1$-type $\{\psi(x)\in\mathsf{cl}(\varphi)\mid\mathfrak{A}\models\psi(a)\}$, assuming that $\varphi$ is understood from the context. We say that the $1$-type $t$ is realized in $\mathfrak{A}$ if there is an $a\in A$ with $\mathsf{tp}_{\mathfrak{A}}(a)=t$. We are now ready to formulate our final characterizations.

Theorem 4.4**.**

Let $\varphi_{1},\varphi_{2}$ be GF 2-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree and for every set $A_{\bot}\subseteq A$ with $A_{\bot}\cap\rho$ infinite for any infinite $\Sigma$-path $\rho$ in $\mathfrak{A}$, there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$, there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$; 2. 2.

for every 1-type $t$ for $\varphi_{2}$ that is realized in $\mathfrak{B}$, there are $a\in A$ and $b\in B$ such that $\mathsf{tp}_{\mathfrak{B}}(b)=t$ and $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},b)$.

Regularity and finite outdegree are used in the proof of Theorem 4.4 given in the appendix, but it follows from the automata constructions below that the theorem is still correct when these qualifications are dropped.

5 Decidability and Complexity

We show that $\Sigma$-entailment in GF2 is decidable and 2ExpTime-complete, and thus so are conservative extensions and $\Sigma$-inseparability. The upper bound is based on Theorem 4.4 and uses alternating parity automata on infinite trees. Since Theorem 4.4 does not provide us with an obvious upper bound on the outdegree of the involved tree models, we use alternating tree automata which can deal with trees of any finite outdegree, similar to the ones introduced by Wilke [41], but with the capability to move both downwards and upwards in the tree.

A tree is a non-empty (and potentially infinite) set of words $T\subseteq(\mathbb{N}\setminus 0)^{*}$ closed under prefixes. We generally assume that trees are finitely branching, that is, for every $w\in T$, the set $\{i\mid w\cdot i\in T\}$ is finite. For any $w\in(\mathbb{N}\setminus 0)^{*}$, as a convention we set $w\cdot 0:=w$. If $w=n_{0}n_{1}\cdots n_{k}$, we additionally set $w\cdot-1:=n_{0}\cdots n_{k-1}$. For an alphabet $\Theta$, a $\Theta$-labeled tree is a pair $(T,L)$ with $T$ a tree and $L:T\rightarrow\Theta$ a node labeling function.

A two-way alternating tree automata (2ATA) is a tuple $\mathcal{A}=(Q,\Theta,q_{0},\delta,\Omega)$ where $Q$ is a finite set of states, $\Theta$ is the input alphabet, $q_{0}\in Q$ is the initial state, $\delta$ is a transition function as specified below, and $\Omega:Q\to\mathbb{N}$ is a priority function, which assigns a priority to each state. The transition function maps a state $q$ and some input letter $\theta\in\Theta$ to a transition condition $\delta(q,\theta)$ which is a positive Boolean formula over the truth constants $\mathsf{true}$ and $\mathsf{false}$ and transitions of the form $q$, $\langle-\rangle q$, $[-]q$, $\Diamond q$, $\Box q$ where $q\in Q$. The automaton runs on $\Theta$-labeled trees. Informally, the transition $q$ expresses that a copy of the automaton is sent to the current node in state $q$, $\langle-\rangle q$ means that a copy is sent in state $q$ to the predecessor node, which is then required to exist, $[-]q$ means the same except that the predecessor node is not required to exist, $\Diamond q$ means that a copy is sent in state $q$ to some successor, and $\Box q$ that a copy is sent in state $q$ to all successors. The semantics is defined in terms of runs in the usual way, we refer to the appendix for details. We use $L(\mathcal{A})$ to denote the set of all $\Theta$-labeled trees accepted by $\mathcal{A}$. It is standard to verify that 2ATAs are closed under complementation and intersection. We show in the appendix that the emptiness problem for 2ATAs can be solved in time exponential in the number of states.

We aim to show that given two GF2-sentences $\varphi_{1}$ and $\varphi_{2}$ and a signature $\Sigma$, one can construct a 2ATA $\mathcal{A}$ such that $L(\mathcal{A})=\emptyset$ iff $\varphi_{1}\models_{\text{GF}^{2}(\Sigma)}\varphi_{2}$. The number of states of the 2ATA $\mathcal{A}$ is polynomial in the size of $\varphi_{1}$ and exponential in the size of $\varphi_{2}$, which yields the desired 2ExpTime upper bounds.

Let $\varphi_{1}$, $\varphi_{2}$, and $\Sigma$ be given. Since the logics we are concerned with have Craig interpolation, we can assume w.l.o.g. that $\Sigma\subseteq\mathsf{sig}(\varphi_{1})$. With $\Theta$, we denote the set of all pairs $(\tau,M)$ where $\tau$ is an atomic 2-type for $\mathsf{sig}(\varphi_{1})$ and $M\in\{0,1\}$. For $p=(\tau,M)\in\Theta$, we use $p^{1}$ to denote $\tau$ and $p^{2}$ to denote $M$. A $\Theta$-labeled tree $(T,L)$ represents a forest structure $\mathfrak{A}_{(T,L)}$ with universe $A_{(T,L)}=T$ and where $w\in A^{\mathfrak{A}_{(T,L)}}$ if $A(y)\in L(w)$ and $(w,w^{\prime})\in R^{\mathfrak{A}_{(T,L)}}$ if one of the following conditions is satisfied: (1) $w=w^{\prime}$ and $Ryy\in L(w)^{1}$; (2) $w^{\prime}$ is a successor of $w$ and $Rxy\in L(w^{\prime})^{1}$; (3) $w$ is a successor of $w^{\prime}$ and $Ryx\in L(w)^{1}$. Thus, the atoms in a node label that involve only the variable $y$ describe the current node, the atoms that involve both variables $x$ and $y$ describe the connection between the predecessor and the current node, and the atoms that involve only the variable $x$ are ignored. The $M$-components of node labels are used to represent a set of markers $A_{\bot}=\{w\in A_{(T,L)}\mid L(w)^{2}=1\}$. It is easy to see that, conversely, for every tree structure $\mathfrak{A}$ over $\Sigma$, there is a $\Theta$-labeled tree $(T,L)$ such that $\mathfrak{A}_{(T,L)}=\mathfrak{A}$.

To obtain the desired 2ATA $\mathcal{A}$, we construct three 2ATAs $\mathcal{A}_{1},\mathcal{A}_{2},\mathcal{A}_{3}$ and then define $\mathcal{A}$ so that it accepts $L(\mathcal{A}_{1})\cap\overline{L(\mathcal{A}_{2})}\cap L(\mathcal{A}_{3})$. The 2ATA $\mathcal{A}_{3}$ only makes sure that the set $A_{\bot}\subseteq A_{(T,L)}$ is such that for any infinite $\Sigma$-path $\rho$, $A_{\bot}\cap\rho$ is infinite (as required by Theorem 4.4), we omit details. We construct $\mathcal{A}_{1}$ so that it accepts a $\Theta$-labeled tree $(T,L)$ iff $\mathfrak{A}_{(T,L)}$ is a model of $\varphi_{1}$. The details of the construction, which is fairly standard, can be found in the appendix. The number of states of $\mathcal{A}_{1}$ is polynomial in the size of $\varphi_{1}$ and independent of $\varphi_{2}$. The most interesting automaton is $\mathcal{A}_{2}$.

Lemma 5.1**.**

There is a 2ATA $\mathcal{A}_{2}$ that accepts a $\Theta$-labeled tree $(T,L)$ iff there is a model $\mathfrak{B}$ of $\varphi_{2}$ s.t. Conditions 1 and 2 from Theorem 4.4 are satisfied when $\mathfrak{A}$ is replaced with $\mathfrak{A}_{(T,L)}$.

The general idea of the construction of $\mathcal{A}_{2}$ is to check the existence of the desired model $\mathfrak{B}$ of $\varphi_{2}$ by verifying that there is a set of 1-types for $\varphi_{2}$ from which $\mathfrak{B}$ can be assembled, represented via the states that occur in a successful run. Before we can give details, we introduce some preliminaries.

A [math]-type $s$ for $\varphi_{2}$ is a maximal set of sentences $\psi()\in\mathsf{cl}(\varphi_{2})$ such that $\varphi_{2}\wedge s$ is satisfiable. A $2$-type $\lambda$ for $\varphi_{2}$ is a maximal set of formulas $\psi(x,y)\in\mathsf{cl}(\varphi_{2})$ that contains $\neg(x=y)$ and such that $\varphi_{2}\wedge\exists xy\,\lambda(x,y)$ is satisfiable. If a 2-type $\lambda$ contains the atom $Rxy$ or $Ryx$ for at least one binary predicate $R$, then it is guarded. If additionally $R\in\Sigma$, then it is $\Sigma$-guarded. Note that each $1$-type contains a (unique) [math]-type and each $2$-type contains two (unique) $1$-types. Formally, we use $\lambda_{x}$ to denote the 1-type obtained by restricting the 2-type $\lambda$ to the formulas that do not use the variable $y$, and likewise for $\lambda_{y}$ and the variable $x$. We use $\mathsf{TP}_{n}$ to denote the set of $n$-types for $\varphi_{2}$, $n\in\{0,1,2\}$. For $t\in\mathsf{TP}_{1}$ and a $\lambda\in\mathsf{TP}_{2}$, we say that $\lambda$ is compatible with $t$ and write $t\approx\lambda$ if the sentence $\varphi_{2}\wedge\exists xy(t(x)\wedge\lambda(x,y))$ is satisfiable; for $t\in\mathsf{TP}_{1}$ and $T\subseteq\mathsf{TP}_{2}$ a set of guarded 2-types, we say that $T$ is a neighborhood for $t$ and write $t\approx T$ if the sentence

[TABLE]

is satisfiable. Note that each of the mentioned sentences is formulated in GF2 and at most single exponential in size (in the size of $\varphi_{1}$ and $\varphi_{2}$), thus satisfiability can be decided in 2ExpTime.

To build the automaton $\mathcal{A}_{2}$ from Lemma 5.1, set $\mathcal{A}_{2}=(Q_{2},\Theta,q_{0},\delta_{2},\Omega_{2})$ where $Q_{2}$ is

[TABLE]

$\Omega_{2}$ assigns two to all states except for those of the form $t^{?}$, to which it assigns one.

The automaton begins by choosing the [math]-type $s$ realized in the forest model $\mathfrak{B}$ of $\varphi_{2}$ whose existence it aims to verify. For every $\exists x\varphi(x)\in s$, it then chooses a 1-type $t$ in which $\varphi(x)$ is realized in $\mathfrak{B}$ and sends off a copy of itself to find a node where $t$ is realized. To satisfy Condition 1 of Theorem 4.4, at each node it further chooses a 1-type that is compatible with $s$, to be realized at that node. This is implemented by the following transitions:

[TABLE]

where $s$ ranges over $\mathsf{TP}_{0}$. When a state of the form $t$ is assigned to a node $w$, this is an obligation to prove that there is a GF${}^{2}(\Sigma)$-bisimulation between the element $w$ in $\mathfrak{A}_{(T,L)}$ and an element $b$ of type $t$ in $\mathfrak{B}$. A state of the form $t^{0}$ represents the obligation to verify that there is an $A_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulation between $w$ and an element of type $t$ in $\mathfrak{B}$. We first verify that the former obligations are satisfied. This requires to follow all successors of $w$ and to guess types of successors of $b$ to be mapped there, satisfying the back condition of bisimulations. We also need to guess successors of $b$ in $\mathfrak{B}$ (represented as a neighborhood for $t$) to satisfy the existential demands of $t$ and then select successors of $a$ to which they are mapped, satisfying the “back” condition of bisimulations. Whenever we decide to realize a 1-type $t$ in $\mathfrak{B}$ that does not participate in the bisimulation currently being verified, we also send another copy of the automaton in state $t^{?}$ to guess an $a\in A_{(T,L)}$ that we can use to satisfy Condition 2 from Theorem 4.4:

[TABLE]

[TABLE]

where $\tau_{y}=_{\Sigma}t$ means that the atoms in $\tau$ that mention only $y$ are identical to the $\Sigma$-relational atoms in $t$ (up to renaming $x$ to $y$), $\tau=_{\Sigma}\lambda$ means that the restriction of $\lambda$ to $\Sigma$-atoms is exactly $\tau$, and $\lambda^{-}$ is obtained from $\lambda$ by swapping $x$ and $y$. We need further transitions to satisfy the obligations represented by states of the form $t^{0}$, which involves checking $A_{\bot}$-delimited bisimulations. Details are given in the appendix where also the correctness of the construction is proved.

Theorem 5.2**.**

In GF 2, $\Sigma$-entailment and conservative extensions can be decided in time $2^{2^{p(|\varphi_{2}|\cdot\log|\varphi_{1}|)}}$, for some polynomial $p$. Moreover, $\Sigma$-inseparability is in 2ExpTime.

Note that the time bound for conservative extensions given in Theorem 5.2 is double exponential only in the size of $\varphi_{2}$ (that is, the extension). In ontology engineering applications, $\varphi_{2}$ will often be small compared with $\varphi_{1}$.

A matching lower bound is proved using a reduction of the word problem of exponentially space-bounded alternating Turing machines, see the appendix for details. The construction is inspired by the proof from [16] that conservative extensions in the description logic ${\cal ALC}$ are 2ExpTime-hard, but the lower bound does not transfer directly since we are interested here in witness sentences that are formulated in GF2 rather than in ${\cal ALC}$.

Theorem 5.3**.**

In any fragment of FO that contains GF 2, the problems $\Sigma$-entailment, $\Sigma$-inseparability, conservative extensions, and strong $\Sigma$-entailment are 2ExpTime-hard.

6 Conclusion

We have shown that conservative extensions are undecidable in (extensions of) GF and FO2, and that they are decidable and 2ExpTime-complete in GF2. It thus appears that decidability of conservative extensions is linked even more closely to the tree model property than decidability of the satisfiability problem: apart from cycles of length at most two, GF2 enjoys a ‘true’ tree model property while GF only enjoys a bounded treewidth model property and FO2 has a rather complex regular model property that is typically not even made explicit. As future work, it would be interesting to investigate whether conservative extensions remain decidable when guarded counting quantifiers, transitive relations, equivalence relations, or fixed points are added, see e.g. [35, 25, 23]. It would also be interesting to investigate a finite model version of conservative extensions.

Appendix A Proofs for Section 3

We split the proof of Lemma 3.1 into two parts.

Lemma A.1**.**

If $M$ halts then $\varphi_{1}\wedge\varphi_{2}$ is not a GF2-conservative extension of $\varphi_{1}$.

Proof A.2**.**

Assume that $M$ halts. We define a witness $\psi$ for non-conservativity. It says that every element participates in a substructure that represents the computation of $M$ on input $(0,0)$, that is: if the computation is $(q_{0},n_{0},m_{0}),\dots,(q_{k},n_{k},m_{k})$, then there is an $N$-path of length $k$ (but not longer) such that any object reachable in $i\leq k$ steps from the beginning of the path is labeled with $q_{i}$, has an outgoing $R_{0}$-path of length $n_{i}$ and no longer outgoing $R_{0}$-path, and likewise for $R_{1}$ and $m_{i}$. In more detail, consider the $\Sigma$-structure $\mathfrak{A}$ with

[TABLE]

in which

[TABLE]

Then let $\psi$ be a $GF^{2}(\Sigma)$-sentence that describes $\mathfrak{A}$ up to global GF${}^{2}(\Sigma)$-bisimulations. Clearly $\mathfrak{A}$ satisfies $\varphi_{1}\wedge\psi$. It thus remains to show that $\varphi_{1}\wedge\varphi_{2}\wedge\psi$ is unsatisfiable. But this is clear as there are no $N$-paths of length $>k$ in any model of $\psi$ and since there are no defects in register updates in any model of $\psi$.

Lemma A.3**.**

If there exists a $\Sigma$-structure that satisfies $\varphi_{1}$ and cannot be extended to a model of $\varphi_{2}$, then $M$ halts.

Proof A.4**.**

Let $\mathfrak{A}$ be a $\Sigma$-structure satisfying $\varphi_{1}$ that cannot be extended to a model of $\varphi_{2}$. Then $S^{\mathfrak{A}}\not=\emptyset$ and there exists an $N$-path labeled with states in $Q$ starting in $S$. Since $\mathfrak{A}$ cannot be extended to a model of $\varphi_{2}$ the computation starting from $S$ is finite. Moreover, one can readily prove by induction that no register update defects occur since otherwise $\varphi_{2}$ can be satisfied.

We now prove Theorem 3.3 using a reduction of an undecidable tiling problem.

Definition A.5**.**

A tiling system $\mathfrak{D}=(\mathfrak{T},H,V,{\sf Right},{\sf Left},{\sf Top},{\sf Bottom})$ consists of a finite set $\mathfrak{T}$ of tiles, horizontal and vertical matching relations $H,V\subseteq\mathfrak{T}\times\mathfrak{T}$, and subsets ${\sf Right}$, ${\sf Left}$, ${\sf Top}$, and ${\sf Bottom}$ of $\mathfrak{T}$ containing the right tiles, left tiles, top tiles, and bottom tiles, respectively. A solution to $\mathfrak{D}$ is a triple $(n,m,\tau)$ where $n,m\in\mathbb{N}$ and $\tau:\{0,\ldots,n-1\}\times\{0,\ldots,m-1\}\rightarrow\mathfrak{T}$ such that the following hold:

$(\tau(i,j),\tau(i+1,j))\in H$, for all $i<n$ and $j\leq m$; 2. 2.

$(\tau(i,j),\tau(i,j+1))\in V$, for all $i\leq n$ and $j<m$; 3. 3.

$\tau(0,j)\in{\sf Left}$* and $\tau(n,j)\in{\sf Right}$, for all $j\leq m$;* 4. 4.

$\tau(i,0)\in{\sf Bottom}$* and $\tau(i,m)\in{\sf Top}$, for all $i\leq n$.*

We show how to convert a tiling system $\mathfrak{D}$ into FO2-sentences $\varphi_{1}$ and $\varphi_{2}$ such that $\mathfrak{D}$ has a solution iff $\varphi_{1}\wedge\varphi_{2}$ is not a conservative extension of $\varphi_{1}$. In particular, models of witness sentences will define solutions of $\mathfrak{D}$.

Let $\mathfrak{D}=(\mathfrak{T},H,V,{\sf Right},{\sf Left},{\sf Top},{\sf Bottom})$ be a tiling system. The formula $\varphi_{1}$ uses the following set $\Sigma$ of predicates:

• •

binary predicates $R_{h}$ and $R_{v}$ (representing a grid) and $S_{h}$ and $S_{v}$ (for technical reasons),

• •

unary predicates $T$ for every $T\in\mathfrak{T}$, $G$ (for the domain of the grid), $O$ (for the lower left corner of the grid), $B_{\rightarrow}$, $B_{\leftarrow}$, $B_{\uparrow}$, and $B_{\downarrow}$ (for the borders of the grid).

Then $\varphi_{1}$ is the conjunction of the following sentences:

Every position in the $n\times m$ grid is labeled with exactly one tile and the matching conditions are satisfied:

[TABLE] 2. 2.

The predicates $B_{\rightarrow}$, $B_{\leftarrow}$, $B_{\uparrow}$, and $B_{\downarrow}$ mark the borders of the grid:

[TABLE]

and similarly for $B_{\leftarrow}$, $B_{\uparrow}$, and $B_{\downarrow}$. 3. 3.

There is a grid origin:

[TABLE] 4. 4.

The grid elements are marked by $G$:

[TABLE] 5. 5.

The tiles on border positions are labeled with appropriate tiles:

[TABLE]

and similarly for $B_{\leftarrow}$, $B_{\uparrow}$, and $B_{\downarrow}$. 6. 6.

The predicates $S_{h}$ and $S_{v}$ occur in $\varphi_{1}$: any FO2-tautology using them.

This finishes the definition of $\varphi_{1}$. The sentence $\varphi_{2}$ introduces two new unary predicates $Q$ and $P$ and is the conjuntion of $\exists x(Ox\wedge Qx)$ and

[TABLE]

where

[TABLE]

Thus, $\varphi_{D}$ describes a defect in the grid: there exist an $R_{h}$-successor $y_{1}$ and an $R_{v}$-successor $y_{2}$ of $x$ such that every $R_{v}$-successor of $y_{1}$ is labeled with $P$ and every $R_{h}$-successor of $y_{2}$ is labeled with $\neg P$. Informally, we can satisfy $\varphi_{2}$ only if from some element of $O$, there is an infinite $R_{h}/R_{v}$-path or a non-closing grid cell can be reached by a finite such path. To make this precise, we introduce some notation. Let $\Sigma^{\prime}\supseteq\Sigma$ and let $\mathfrak{B}$ be a $\Sigma^{\prime}$-structure. Then the $\Sigma$-structure $\mathfrak{A}$ obtained from $\mathfrak{B}$ by removing the interpretation of predicates in $\Sigma^{\prime}\setminus\Sigma$ is called the $\Sigma$-reduct of $\mathfrak{B}$ and $\mathfrak{B}$ is called a $\Sigma^{\prime}\setminus\Sigma$-extension of $\mathfrak{A}$. For a $\Sigma$-structure $\mathfrak{A}$, we say that $a\in A$ is the root of a non-closing grid cell if there are $(a,b_{1})\in R_{h}^{\mathfrak{A}}$ and $(a,b_{2})\in R_{v}^{\mathfrak{A}}$ such that there does not exist a $c\in A$ with $(b_{1},c)\in R_{v}^{\mathfrak{A}}$ and $(b_{2},c)\in R_{h}^{\mathfrak{A}}$. Now, it is straightforward to show the following characterization of $\varphi_{2}$.

Lemma A.6**.**

$\varphi_{2}$* can be satisfied in a $\{Q,P\}$-extension of a $\Sigma$-structure $\mathfrak{A}$ iff there exists an element of $O^{\mathfrak{A}}$ that starts an infinite $R_{h}/R_{v}$-path or a finite $R_{h}/R_{v}$-path to a root of a non-closing grid cell.*

We now argue that $\mathfrak{D}$ has a solution iff $\varphi_{1}\wedge\varphi_{2}$ is not a conservative extension of $\varphi_{1}$.

Lemma A.7**.**

If $\mathfrak{D}$ has a solution then $\varphi_{1}\wedge\varphi_{2}$ is not a FO2-conservative extension of $\varphi_{1}$.

Proof A.8**.**

Assume that $\mathfrak{D}$ has a solution $(n,m,\tau)$. We define a witness $\psi$, first using additional fresh unary predicates and then argueing that these can be removed. Thus introduce fresh unary predicates $P_{i,j}$ for all $i<n$ and $j<m$. Intuitively, $P_{i,j}$ identifies grid position $(i,j)$. Set

[TABLE]

We first show that $\varphi_{1}\wedge\psi$ is satisfiable. As the model, simply take the standard $n\times m$-grid in which all positions are labeled with $P_{i,j}$, $G$, $O$, $B_{\rightarrow}$ etc in the expected way, and that is tiled according to $\tau$. It is easily verified that this structure satisfies both $\varphi_{1}$ and $\psi$. It thus remains to show that $\varphi_{1}\wedge\varphi_{2}\wedge\psi$ is unsatisfiable. By Lemma A.6 it suffices to show that there is no model $\mathfrak{A}$ of $\varphi_{1}\wedge\psi$ in which there exists an element of $O^{\mathfrak{A}}$ starting an infinite $R_{h}/R_{v}$-path or a finite $R_{h}/R_{v}$-path leading to a root of a non-closing grid cell. Assume for a proof by contradiction that there exists such a model $\mathfrak{A}$ and $a\in O^{\mathfrak{A}}$. Then we find a sequence $a_{0}R^{\mathfrak{A}}_{z_{0}}a_{1}R^{\mathfrak{A}}_{z_{1}}a_{2}\cdots$ with $a_{0}=a$ and $z_{i}\in\{x,y\}$ such that either some $a_{h}$ is the root of a non-closing grid cell or the sequence is infinite. By $\varphi_{1}$ and the first conjunct of $\psi$ for each $a_{k}$ there exists $P_{i,j}$ with $a_{k}\in P_{i,j}^{\mathfrak{A}}$. By the last conjunct of $\psi$, $a_{0}\in P_{0,0}^{\mathfrak{A}}$. By the remaining conjuncts of $\psi$ we have $k\geq i+j$ if $a_{k}\in P_{i,j}^{\mathfrak{A}}$ and it follows that there is no $a_{k}$ with $k>n+m$. Thus, assume some $a_{k}$ is the root of a non-closing grid. Then we have $(a_{k},b_{1})\in R_{h}^{\mathfrak{A}}$ and $(a_{k},b_{2})\in R_{v}^{\mathfrak{A}}$ such that there is no $c\in A$ with $(b_{1},c)\in R_{v}^{\mathfrak{A}}$ and $(b_{2},c)\in R_{h}^{\mathfrak{A}}$. By $\psi$, there are $i,j$ with $b_{1}\in P_{i+1,j}^{\mathfrak{A}}$ and $b_{2}\in P_{i,j+1}^{\mathfrak{A}}$. By the second set of conjuncts of $\varphi_{1}$ there exists $(b_{1},c)\in R_{v}^{\mathfrak{A}}$. By $\psi$, $c\in P_{i+1,j+1}^{\mathfrak{A}}$. But then again using $\psi$ we obtain that $(b_{2},c)\in R_{h}^{\mathfrak{A}}$ and we have derived a contradiction.

As announced, we now show how to remove the additional predicates $P_{i,j}$. To this end, we use the binary predicates $S_{h},S_{v}$. In the sentence $\psi$, we replace every occurrence of $P_{i,j}(x)$ with a formula saying: there is an outgoing $S_{h}$-path of length $i$, but not of length $i+1$ and an outgoing $S_{v}$-path of length $j$, but not of length $j+1$. When we build a model of $\varphi_{1}\wedge\psi$, we now need to introduce additional elements for the “counting paths”. We make the predicate $G$ false on all those elements and true everywhere on the grid.

Lemma A.9**.**

If there exists a $\Sigma$-structure that satisfies $\varphi_{1}$ and cannot be extended to a model of $\varphi_{2}$, then $\mathfrak{D}$ has solution.

Proof A.10**.**

Take a $\Sigma$-structure $\mathfrak{A}$ satisfying $\varphi_{1}$ that cannot be extended to a model of $\varphi_{2}$. By the conjunct of $\varphi_{1}$ given in Item 3, $O^{\mathfrak{A}}\cap B_{\leftarrow}^{\mathfrak{A}}\cap B_{\downarrow}^{\mathfrak{A}}\not=\emptyset$. Take $a\in O^{\mathfrak{A}}\cap B_{\leftarrow}^{\mathfrak{A}}\cap B_{\downarrow}^{\mathfrak{A}}$. By Lemma A.6, $a$ does not start an infinite $R_{h}/R_{v}$-path or a finite $R_{h}/R_{v}$-path leading to the root of a non-closing grid cell. Using the conjuncts of $\varphi_{1}$ it is now straightforward to read off a tiling from $\mathfrak{A}$.

Theorem 3.3 is an immediate consequence of Lemmas A.7 and A.9.

Note that the sentences $\varphi_{1}$ and $\varphi_{2}$ can be replaced by equivalent $\mathcal{ALC}$-TBoxes: in $\varphi_{2}$, we can replace the conjunct $\exists x(Ox\wedge Qx)$ which cannot be expressed in $\mathcal{ALC}$ by the concept inclusion $\top\sqsubseteq\exists S.(O\sqcap Q)$ with $S$ a fresh binary predicate. Consequently, FO${}^{2}(\Sigma)$-inseparability of $\mathcal{ALC}$-TBoxes is undecidable.

Appendix B Preliminaries on Bisimulations

We first show that GF${}^{2}(\Sigma)$-bisimulations characterize the expressive power of GF${}^{2}(\Sigma)$. The proofs are standard [21, 17, 1]. We start by giving a precise definition of $k$-GF${}^{2}(\Sigma)$ bisimilarity. Let $\mathfrak{A}$ and $\mathfrak{B}$ be structures, $a\in A$, and $b\in B$. The definition is by induction on $k\geq 0$. Then $(\mathfrak{A},a)\sim^{0}_{\Sigma}(\mathfrak{B},b)$ iff $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and $(\mathfrak{A},a)\sim^{k+1}_{\Sigma}(\mathfrak{B},b)$ iff $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and

for every $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ is guarded there exists $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})=\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ and $(\mathfrak{A},a^{\prime})\sim^{k}_{\Sigma}(\mathfrak{B},b^{\prime})$ 2. 2.

for every $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ is guarded there exists $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})=\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ and $(\mathfrak{A},a^{\prime})\sim^{k}_{\Sigma}(\mathfrak{B},b^{\prime})$.

Denote by openGF2 the fragment of GF2 consisting of all GF2 formulas with one free variable in which equality is not used as a guard and which do not contain a subformula that is a sentence. It is not difficult to prove the following result.

Lemma B.1**.**

Every GF 2 sentence is equivalent to a Boolean combination of sentences of the form $\forall x\varphi(x)$, where $\varphi(x)$ is a openGF 2 formula.

A structure $\mathfrak{A}$ is $\omega$-saturated if for every finite set $\{a_{1},\ldots,a_{n}\}\subseteq A$ and every set $\Gamma(x)$ of FO formulas using elements of $\{a_{1},\ldots,a_{n}\}$ as constants the following holds: if every finite subset of $\Gamma(x)$ is satisfiable in the structure $(\mathfrak{A},a_{1},\ldots,a_{n})$, then $\Gamma(x)$ is satisfiable in $(\mathfrak{A},a_{1},\ldots,a_{n})$. For every structure $\mathfrak{A}$ there exists an elementary extension $\mathfrak{A}^{\prime}$ of $\mathfrak{A}$ that is $\omega$-saturated [9]. Mostly we only require a weaker form of saturation. A structure $\mathfrak{A}$ is successor-saturated if for any $a\in A$ and set $\Gamma(x)$ of openGF2 formulas the following holds for any atomic guarded binary type $\tau$: if for any finite subset $\Gamma^{\prime}$ of $\Gamma$ there exists $a^{\prime}\not=a$ with $\text{at}_{\mathfrak{A}}(a,a^{\prime})=\tau$ and $\mathfrak{A}\models\psi(a^{\prime})$ for all $\psi\in\Gamma^{\prime}$, then there exists $b^{\prime}\not=a$ with $\text{at}_{\mathfrak{A}}(a,b^{\prime})=\tau$ and $\mathfrak{A}\models\psi(b^{\prime})$ for all $\psi\in\Gamma$. Observe that structures of finite outdegree and $\omega$-saturated structures are successor-saturated.

The depth of a GF2 formula $\varphi$ is the number of nestings of guarded quantifications in $\varphi$. We first characterize openGF2. The proof is standard and omitted.

Lemma B.2**.**

Let $\mathfrak{A}$ and $\mathfrak{B}$ be structures, $\Sigma$ a signature, and $a\in A$, $b\in B$.

The following conditions are equivalent for all $k\geq 0$:

• •

$\mathfrak{A}\models\varphi(a)$* iff $\mathfrak{B}\models\varphi(b)$ holds for all openGF*${}^{2}(\Sigma)$* formulas $\varphi(x)$ of depth $k$;*

• •

$(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$. 2. 2.

If $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$, then $\mathfrak{A}\models\varphi(a)$ iff $\mathfrak{B}\models\varphi(b)$ holds for all openGF${}^{2}(\Sigma)$* formulas $\varphi(x)$. The converse direction holds if $\mathfrak{A}$ and $\mathfrak{B}$ are successor-saturated. *

We also require the following link between bounded bisimulations and unbounded bisimulations which follows from Lemma B.2.

Lemma B.3**.**

*Let $\mathfrak{A}$ and $\mathfrak{B}$ be successor-saturated structures, $a\in A$, and $b\in B$. If $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$ for all $k\geq 0$, then $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$. *

We now consider ‘global’ versions of the bounded bisimulations introduced above to characterize GF2. Call structures $\mathfrak{A}$ and $\mathfrak{B}$ globally $k$-GF${}^{2}(\Sigma)$-bisimilar if for all $a\in A$ there exists $b\in B$ such that $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$ and, conversely, for every $b\in B$ there exists $a\in A$ with $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$. $\mathfrak{A}$ and $\mathfrak{B}$ are globally finitely GF${}^{2}(\Sigma)$-bisimilar iff they are globally $k$-GF${}^{2}(\Sigma)$-bisimilar for all $k\geq 0$. The following characterization result now follows from Lemma B.1 and Lemma B.2.

Lemma B.4**.**

Let $\mathfrak{A}$ and $\mathfrak{B}$ be structures and $\Sigma$ a signature.

The following conditions are equivalent:

• •

$\mathfrak{A}\models\varphi$* iff $\mathfrak{B}\models\varphi$ holds for all GF*${}^{2}(\Sigma)$* sentences $\varphi$;*

• •

$\mathfrak{A}$* and $\mathfrak{B}$ are globally finitely GF*${}^{2}(\Sigma)$-bisimilar. 2. 2.

If $\mathfrak{A}$ and $\mathfrak{B}$ are globally GF${}^{2}(\Sigma)$-bisimilar, then $\mathfrak{A}\models\varphi$ iff $\mathfrak{B}\models\varphi$ holds for all GF${}^{2}(\Sigma)$* sentences $\varphi$. The converse direction holds if $\mathfrak{A}$ and $\mathfrak{B}$ are $\omega$-saturated. *

Observe that in Lemma B.4 we cannot replace $\omega$-saturation by successor-saturation or finite outdegree.

Appendix C Proofs for Section 4

Based on the results presented in the previous section we prove the following characterization of $\Sigma$-entailment in FO2.

Theorem 4.3 Let $\varphi_{1},\varphi_{2}$ be GF2-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every model $\mathfrak{A}$ of $\varphi_{1}$ of finite outdegree, there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$ there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every $b\in B$ and every $k\geq 0$, there is an $a\in A$ such that $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$.

Proof C.1**.**

“if”. Assume that for every model $\mathfrak{A}$ of $\varphi_{1}$ of finite outdegree, there is a model $\mathfrak{B}$ of $\varphi_{2}$ as described in Theorem 4.3. Take a $\Sigma$-sentence $\psi$ such that $\varphi_{1}\wedge\psi$ is satisfiable. We have to show that $\varphi_{2}\wedge\psi$ is satisfiable. We find a model $\mathfrak{A}$ of $\varphi_{1}\wedge\psi$ that has finite outdegree. By assumption, there is a model $\mathfrak{B}$ of $\varphi_{2}$ that satisfies Conditions 1 and 2 of Theorem 4.3. It suffices to show that $\mathfrak{B}$ satisfies $\psi$. But this follows from Lemma B.4.

“only if”. Assume that $\varphi_{1}\models_{\Sigma}\varphi_{2}$. Let $\mathfrak{A}$ be a model of $\varphi_{1}$ of finite outdegree. Let $\Gamma$ denote the set of all GF${}^{2}(\Sigma)$ sentences $\psi$ with $\mathfrak{A}\models\psi$. Then $\varphi_{1}\wedge\bigwedge\Gamma^{\prime}$ is satisfiable for every finite subset $\Gamma^{\prime}$ of $\Gamma$. As $\varphi_{1}\models_{\Sigma}\varphi_{2}$, $\varphi_{2}\wedge\bigwedge\Gamma^{\prime}$ is satisfiable for every finite subset $\Gamma^{\prime}$ of $\Gamma$. By compactness $\{\varphi_{2}\}\cup\Gamma$ is satisfiable. Then there exists an $\omega$-saturated model $\mathfrak{B}$ of $\{\varphi_{2}\}\cup\Gamma$. By $\omega$-saturatedness, for every $a\in A$ there exists $b\in B$ such that $\mathfrak{A}\models\varphi(a)$ iff $\mathfrak{B}\models\varphi(b)$ holds for all formulas $\varphi(x)$ in openGF${}^{2}(\Sigma)$. By Lemma B.2, we have $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$, as required for Condition 1. Condition 2 follows from Lemma B.2.

Before we come to the proof of Theorem 4.4 we prove another characterization of $\Sigma$-entailment in GF2. If $\mathfrak{A}$ is a forest structure with $a,a^{\prime}\in A$, then we write $a\prec a^{\prime}$ iff $a$ and $a^{\prime}$ are part of the same $\Sigma$-tree in $\mathfrak{A}$ and $a$ is a ancestor of $a^{\prime}$ (recall that a $\Sigma$-tree in a forest structure $\mathfrak{A}$ is a maximal $\Sigma$-connected substructure of $\mathfrak{A}$ and that we always assume a fixed root in trees within forest structures). For $\mathfrak{A}$ and $\mathfrak{B}$ structures and $a_{\bot}\in A$, an $a_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulation between $\mathfrak{A}$ and $\mathfrak{B}$ is defined like a GF${}^{2}(\Sigma)$-bisimulation except that Conditions 2 and 3 are not required to hold when $a=a_{\bot}$. We indicate the existence of an $a_{\bot}$-delimited bisimulation by writing $(\mathfrak{A},a)\sim^{a_{\bot}}_{\Sigma}(\mathfrak{B},b)$. This requires $a_{\bot}\preceq a$. We now give a characterization of $\Sigma$-entailment using forest models in which we replace the bounded backward condition by an unbounded condition.

Theorem C.2**.**

Let $\varphi_{1},\varphi_{2}$ be GF2-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$ there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every $b\in B$, one of the following holds:

1. (a)

there is an $a\in A$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$; 2. (b)

there are $a_{\bot},a_{0},a_{1},\dots,a^{\prime}_{0},a^{\prime}_{1},\dots\in A$ such that $a_{\bot}\prec a_{0}\prec a_{1}\prec\cdots$ and, for all $i\geq 0$, $a_{i}\prec a^{\prime}_{i}$ and $(\mathfrak{A},a_{i}^{\prime})\sim^{a_{\bot}}_{\Sigma}(\mathfrak{B},b)$.

Proof C.3**.**

Using the proof of Theorem 4.3, the fact that every (successor-saturated/finite outdegree) structure $\mathfrak{A}$ can be unfolded into a globally GF${}^{2}(\Sigma)$-bisimilar (successor saturated/finite outdegree) forest model $\mathfrak{B}$, and the fact that, consequently, every satisfiable GF2 formula is satisfiable in a regular forest model of finite outdegree one can easily prove the following variant of Theorem 4.3 based on forest models:

Fact 1.* Let $\varphi_{1},\varphi_{2}$ be GF2-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree there is a (successor saturated) forest model $\mathfrak{B}$ of $\varphi_{2}$ such that*

for every $a\in A$ there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every $b\in B$ and every $k\geq 0$, there is an $a\in A$ such that $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$.

To show Theorem C.2 it therefore suffices to show that for every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree and every successor-saturated forest model $\mathfrak{B}$ of $\varphi_{2}$, Condition 2 in Fact 1 is equivalent to Condition 2 of Theorem C.2.

Thus, let $\mathfrak{A}$ and $\mathfrak{B}$ be as described. The interesting direction is to prove that if Condition 2 in Fact 1 holds then Condition 2 of Theorem C.2 holds. Thus, assume that Condition 2 in Fact 1 holds. Take $b\in B$. We may assume it is a root $b$ of a $\Sigma$-tree in $\mathfrak{B}$. Then there are $a_{0},a_{1},\dots\in A$ such that for all $k$, $(\mathfrak{A},a_{k})\sim^{k}_{\Sigma}(\mathfrak{B},b)$. If infinitely many of the $a_{i}$ are identical, then there is an $a\in A$ such that $(\mathfrak{A},a)\sim^{k}_{\Sigma}(\mathfrak{B},b)$ for all $k\geq 0$, thus $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ by Lemma B.3 and we are done. Therefore, assume that there are infinitely many distinct $a_{i}$. By ‘skipping’ elements in the sequence $a_{0},a_{1},\dots$, we can then achieve that the $a_{i}$ are all distinct.

Two nodes $a,a^{\prime}\in A$ are downwards isomorphic, written $a\sim_{\downarrow}a^{\prime}$, if they are the roots of isomorphic subtrees. For a forest structure $\mathfrak{A}$, $a\in A$, and $i\geq 0,$ we denote by $\mathfrak{A}|^{\uparrow i}_{a}$ the path structure obtained by restricting $\mathfrak{A}$ to those elements that can be reached from $a$ by traveling at most $i$ steps towards the root of the tree in $\mathfrak{A}$ that $a$ is part of (including $a$ itself). For $a,a^{\prime}\in A$ and $i\geq 0$, we write $a\approx_{i}a^{\prime}$ if there is an isomorphism $\iota$ from $\mathfrak{A}|^{\uparrow i}_{a}$ to $\mathfrak{A}|^{\uparrow i}_{a^{\prime}}$ with $\iota(a)=a^{\prime}$ such that $c\sim_{\downarrow}\iota(c)$ for all $c$. Since $\mathfrak{A}$ is regular, $\mathfrak{A}$ contains only finitely many equivalence classes for each $\approx_{i}$. By skipping $a_{i}$’s, we can thus achieve that

• ($*$)

$a_{i}\approx_{k}a_{j}$* for all $i,k,j$ with $k\leq i$ and $j>i$.*

This also implies that each $a_{i}$ is at least $i$ steps away from the root of the tree in $\mathfrak{A}$ that it is in (since there are infinitely many $a_{i}$, they must be unboundedly deep in their respective tree, and it remains to apply ($*$)). Let $c_{i}$ denote the element of $A$ reached from $a_{i}$ by traveling $i$ steps towards the root. Since $\mathfrak{A}$ is regular, there must be an infinite subsequence $a_{\ell_{0}},a_{\ell_{1}},\dots$ of $a_{0},a_{1},\dots$ such that $c_{\ell_{i}}\sim_{\downarrow}c_{\ell_{j}}$ for all $i,j$.

Choose some $a_{\bot}\in A$ with $a_{\bot}\sim_{\downarrow}c_{\ell_{i}}$ for all $i$ (equivalently: for some $i$). We can assume w.l.o.g. that each $a_{\ell_{i}}$ is in the subtree rooted at $a_{\bot}$ and that when traveling ${\ell_{i}}$ steps from $a_{\ell_{i}}$ towards the root of the subtree that $a_{\bot}$ is in, then we reach exactly $a_{\bot}$.

Let $\mathfrak{A}^{*}$ be the structure obtained in the limit of the neighborhoods $\mathfrak{A}|^{0}_{a_{\ell_{0}}},\mathcal{A}|^{1}_{a_{\ell_{1}}},\dots$. That is, we start with the subtree of $\mathfrak{A}$ rooted at $a_{\ell_{0}}$, renaming $a_{\ell_{0}}$ to $a^{*}$, and then proceed as follows: after the $i$-th step, the constructed structure is isomorphic to the subtree of $\mathfrak{A}$ rooted at $a_{\bot}$ via an isomorphism that maps $a^{*}$ to $a_{\ell_{i}}$ and the root to $a_{\bot}$; by ($*$), we can thus add a path of predecessor to the root of the structure constructed so far, and then add additional subtrees to the nodes on the path as additional successors, making sure that the obtained structure is isomorphic to the subtree of $\mathfrak{A}$ rooted at $a_{\bot}$ via an isomorphism that maps $a^{*}$ to $a_{\ell_{i+1}}$ and the new root to $a_{\bot}$. By construction, $(\mathfrak{A}^{*},a^{*})\sim_{\Sigma}^{k}(\mathfrak{B},b)$ for all $k\geq 0$ and thus Lemma B.3 yields $(\mathfrak{A}^{*},a^{*})\sim_{\Sigma}(\mathfrak{B},b)$.

Take some $a_{\ell_{i}}$. We aim to show that $(\mathfrak{A},a_{\ell_{i}})\sim^{a_{\bot}}_{\Sigma}(\mathfrak{B},b)$. Let $c$ be the element reached from $a^{*}$ in $\mathfrak{A}^{*}$ by traveling $\ell_{i}$ steps upwards and recall that $a_{\bot}$ is the element reached from $a_{\ell_{i}}$ in $\mathfrak{A}$ by traveling $\ell_{i}$ steps upwards. By construction of $\mathfrak{A}^{*}$, we find an isomorphism from the subtree in $\mathfrak{A}^{*}$ rooted at $c$ to the subtree in $\mathfrak{A}$ rooted at $a_{\bot}$ that takes $c$ to $a_{\bot}$ and $a^{*}$ to $a_{i}$. From $(\mathfrak{A}^{*},a^{*})\sim_{\Sigma}(\mathfrak{B},b)$, we thus obtain the desired $a_{\bot}$-delimited $\Sigma$-bisimulation that witnesses $(\mathfrak{A},a_{i})\sim_{\Sigma}^{a_{\bot}}(\mathfrak{B},b)$.

It remains to show the existence of the required elements $a^{\prime}_{0},a^{\prime}_{1},\dots$, that is, to show that there is a path through the subtree of $\mathfrak{A}$ rooted at $a_{\bot}$ such that each $a_{\ell_{i}}$ is either on the path or can be reached by branching off at a different point of the path. This can be done in the following straightforward way. Starting at $a_{\bot}$, we define the path step by step. In every step, there must be at least one successor which is the root of a subtree that contains infinitely many $a_{\ell_{i}}$’s since $\mathfrak{A}$ has finite outdegree. We always proceed by choosing such a successor. This almost achieves the desired result, except that not all $a_{\ell_{i}}$ are reachable from a distinct node on the path by traveling downwards. However, there are infinitely many nodes on the path from which at least one $a_{\ell_{i}}$ can be reached by traveling downwards, so the problem can be cured by skipping $a_{\ell_{i}}$’s.

We are now in a position to prove Theorem 4.4. We require the following extended version of $k$-GF2-bisimilarity which respects the successor relation in forest structures. Let $\mathfrak{A}$ and $\mathfrak{B}$ be forest structures, $a\in A$, and $b\in B$. The definition is by induction on $k\geq 0$. Then $(\mathfrak{A},a)\sim^{0,\text{succ}}_{\Sigma}(\mathfrak{B},b)$ iff $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and $(\mathfrak{A},a)\sim^{k+1,\text{succ}}_{\Sigma}(\mathfrak{B},b)$ iff $\text{at}_{\mathfrak{A}}^{\Sigma}(a)=\text{at}_{\mathfrak{B}}^{\Sigma}(b)$ and

for every $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})$ is guarded there exists $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(a,a^{\prime})=\text{at}_{\mathfrak{B}}^{\Sigma}(b,b^{\prime})$ and $b^{\prime}$ is a successor of $b$ in $\mathfrak{B}$ iff $a^{\prime}$ is a successor of $a$ in $\mathfrak{A}$ and $(\mathfrak{A},a^{\prime})\sim^{k,\text{succ}}_{\Sigma}(\mathfrak{B},b^{\prime})$ 2. 2.

for every $b^{\prime}\not=b$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(b,b^{\prime})$ is guarded there exists $a^{\prime}\not=a$ such that $\text{at}_{\mathfrak{A}}^{\Sigma}(b,b^{\prime})=\text{at}_{\mathfrak{B}}^{\Sigma}(a,a^{\prime})$ and $a^{\prime}$ is a successor of $a$ in $\mathfrak{A}$ iff $b^{\prime}$ is a successor of $b$ in $\mathfrak{B}$ and $(\mathfrak{A},a^{\prime})\sim^{k,\text{succ}}_{\Sigma}(\mathfrak{B},b^{\prime})$.

Theorem 4.4 Let $\varphi_{1},\varphi_{2}$ be GF2-sentences and $\Sigma$ a signature. Then $\varphi_{1}\models_{\Sigma}\varphi_{2}$ iff for every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree and every set $A_{\bot}\subseteq A$ with $A_{\bot}\cap\rho$ infinite for any infinite $\Sigma$-path $\rho$ in $\mathfrak{A}$ there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$, there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every 1-type $t$ for $\varphi_{2}$ that is realized in $\mathfrak{B}$, there are $a\in A$ and $b\in B$ such that $\mathsf{tp}_{\mathfrak{B}}(b)=t$ and $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},b)$.

Proof C.4**.**

($\Leftarrow$) It suffices to show that for every $m>0$ and every regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree there exists a model $\mathfrak{B}$ of $\varphi_{2}$ such that $\mathfrak{A}$ and $\mathfrak{B}$ are globally $m$-GF${}^{2}(\Sigma)$-bisimilar. Assume $m>0$ and a regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree is given. Let $m^{\prime}$ be the maximum of $m$ and the guarded quantifier depth of $\varphi_{2}$. Then $f(m,\varphi_{2})$ denotes the maximal number of nodes in any $\Sigma\cup{\sf sig}(\varphi_{2})$-forest model $\mathfrak{C}$ which are pairwise $\sim^{m^{\prime},\text{succ}}$-incomparable. Define $A_{\bot}\subseteq A$ on every $\Sigma$-tree with root $r$ in $\mathfrak{A}$ in such a way that $a\in A_{\bot}$ iff the distance between $r$ and $a$ is $kf(m,\varphi_{2})$ for some $k\geq 0$. Let $\mathfrak{B}$ be a forest shaped model of $\varphi_{2}$ satisfying the conditions of Theorem 4.4. One can easily modify $\mathfrak{B}$ in such a way that in addition to the conditions given in the theorem

$(\ast)$* every 1-type $t$ for $\varphi_{2}$ that is realized in $\mathfrak{B}$ is realized in the root of a $\Sigma$-tree in $\mathfrak{B}$ and for every root $r$ of a $\Sigma$-tree in $\mathfrak{B}$ there exists $a\in A$ such that $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},r)$.*

To show $(\ast)$ first pick for every $a\in A$ a $b\in B$ with $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$. Let $S_{1}$ be the set of $b$’s just picked and let $\mathfrak{B}_{1}$ be the disjoint union of the structures induced in $\mathfrak{B}$ by the $\Sigma$-trees whose roots are in $S_{1}$. Next pick for every 1-type $t$ for $\varphi_{2}$ that is realized in $\mathfrak{B}$ a $b\in B$ that realizes $t$. Let $S_{2}$ be the set of $b$’s just picked and let $\mathfrak{B}_{2}$ be the disjoint union of the structures induced in $\mathfrak{B}$ by the $\Sigma$-trees whose roots are in $S_{2}$. Finally, we add (recursively) witnesses for guarded existential quantifiers not involving binary predicates from $\Sigma$ to the disjoint union $\mathfrak{B}^{\prime}$ of $\mathfrak{B}_{1}$ and $\mathfrak{B}_{2}$. In detail, take for any $b$ in $\mathfrak{B}^{\prime}$ its copy $b^{\prime}$ in $\mathfrak{B}$ and assume $c^{\prime}$ in $\mathfrak{B}$ is such that $\{R\mid(b^{\prime},c^{\prime})\in R^{\mathfrak{B}}$ or $(c^{\prime},b^{\prime})\in R^{\mathfrak{B}}\}$ is non-empty and contains no predicate in $\Sigma$. Then add to $\mathfrak{B}^{\prime}$ a copy of the $\Sigma$-tree in $\mathfrak{B}^{\prime}$ whose root $c$ realizes the same 1-type for $\varphi_{2}$ as $c^{\prime}$ and connect $c$ to $b$ by adding for all binary predicates $R$ the pair $(b,c)$ to the extension of $R$ if $(b^{\prime},c^{\prime})\in R^{\mathfrak{B}}$ and the pair $(c,b)$ to the extension of $R$ if $(c^{\prime},b^{\prime})\in R^{\mathfrak{B}}$. We apply this procedure recursively to the new structure (in a fair way) and obtain the desired structure as the limit of the resulting sequence of structures.

We now modify $\mathfrak{B}$ in such a way that the resulting structure is still a model of $\varphi_{2}$ but in addition globally $m$-GF${}^{2}(\Sigma)$-bisimilar to $\mathfrak{A}$. Consider the structure $\mathfrak{B}_{r}$ induced by the $\Sigma$-tree with root $r$ in $\mathfrak{B}$. If there exists an $a\in A$ with $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},r)$ then we do not modify $\mathfrak{B}_{r}$ and set $\mathfrak{B}_{r}^{u}=\mathfrak{B}_{r}$. If no such $a$ exists, then we modify $\mathfrak{B}_{r}$ in such a way that every $b$ in the resulting $\Sigma$-tree is $m$-GF${}^{2}(\Sigma)$-bisimilar to some $a\in A$. Note that we only know that there exists $a\in A$ such that $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},r)$. By construction of $A_{\bot}$ this implies that $(\mathfrak{A},a)$ and $(\mathfrak{B},r)$ are $f(m,\varphi_{2})$-GF${}^{2}(\Sigma)$-bisimilar. Thus, it suffices to modify $\mathfrak{B}_{r}$ in such a way that every node $b$ in the $\Sigma$-tree becomes $m$-GF${}^{2}(\Sigma)$-bisimilar to some $b^{\prime}$ in the original $\mathfrak{B}_{r}$ with distance $\leq f(m,\varphi_{2})-m$ from $r$. To ensure that $\varphi_{2}$ is still satisfied we make sure that the following stronger condition holds: every node $b$ in the $\Sigma$-tree rooted at $r$ is $m^{\prime}$-GF2-bisimilar to some $b^{\prime}$ in the original $\mathfrak{B}_{r}$ with distance $\leq f(m,\varphi_{2})-m^{\prime}$ from $r$. The construction is by a standard pumping argument. For $a,b\in B$ we say that $a$ blocks $b$ if $a\prec b$ and $(\mathfrak{B},a)\sim^{m^{\prime},\text{succ}}(\mathfrak{B},b)$ and there is no $b^{\prime}\prec b$ such that there is an $a^{\prime}$ with $a^{\prime}\prec b^{\prime}$ and $(\mathfrak{B},a^{\prime})\sim^{m^{\prime},\text{succ}}(\mathfrak{B},b^{\prime})$. The universe $B_{r}^{u}$ of $\mathfrak{B}_{r}^{u}$ is the set of words $a_{0}\cdots a_{n}$ with $a_{0},\ldots,a_{n}$ in $\mathfrak{B}_{r}^{u}$ and $a_{0}=r$ such that either $a_{i+1}$ is a successor of $a_{i}$ or there is a successor $b_{i+1}$ of $a_{i}$ such that $a_{i+1}$ blocks $b_{i+1}$. Let $\text{tail}(a_{0}\ldots a_{n})=a_{n}$. For every unary $R$ and $w\in A_{r}^{u}$ we set $w\in R^{\mathfrak{A}_{r}^{u}}$ if $\text{tail}(w)\in R^{\mathfrak{A}}$ and for every binary $R$ we set for $w\in A_{r}^{u}$: $(w,w)\in R^{\mathfrak{A}_{r}^{u}}$ if $(\text{tail}(w),\text{tail}(w))\in R^{\mathfrak{A}}$ and for $wb\in A_{r}^{u}$:

• •

$(w,wb)\in R^{\mathfrak{A}_{r}^{u}}$* if $(\text{tail}(w),b)\in R^{\mathfrak{A}}$ or there is an $a$ such that $b$ blocks $a$ and $(\text{tail}(w),a)\in R^{\mathfrak{A}}$;*

• •

$(wb,w)\in R^{\mathfrak{A}_{a}^{u}}$* if $(b,\text{tail}(w))\in R^{\mathfrak{A}}$ or there is an $a$ such that $b$ blocks $a$ and $(a,\text{tail}(w))\in R^{\mathfrak{A}}$.*

We now replace $\mathfrak{B}_{r}$ by $\mathfrak{B}_{r}^{u}$ in $\mathfrak{B}$. In more detail, take the disjoint union $\mathfrak{B}^{d}$ of all $\mathfrak{B}_{r}^{u}$, $r$ the root of a $\Sigma$-tree in $\mathfrak{B}$. Then add (recursively) witnesses for guarded existential quantifiers not involving binary predicates from $\Sigma$ to $\mathfrak{B}^{d}$: take for any $w$ in $\mathfrak{B}_{r}^{u}$ and any 1-type $t$ for $\varphi_{2}$ that is realized in some node $c$ in $\mathfrak{B}$ such that $\{R\mid(\text{tail}(w),c)\in R^{\mathfrak{B}}$ or $(c,\text{tail}(w))\in R^{\mathfrak{B}}\}$ is non-empty and contains no predicate in $\Sigma$ the root $r^{\prime}$ of a structure $\mathfrak{B}_{r^{\prime}}^{u}$ such that $r^{\prime}$ realizes $t$ in $\mathfrak{B}_{r^{\prime}}^{u}$. Then add to $\mathfrak{B}^{d}$ a new copy of $\mathfrak{B}_{r^{\prime}}^{u}$ and connect $r^{\prime}$ to $b$ by adding for any binary predicate $R$ the pair $(r,r^{\prime})$ to $R^{\mathfrak{B}_{d}}$ if $(\text{tail}(w),c)\in R^{\mathfrak{B}}$ and the pair $(r^{\prime},r)$ to $R^{\mathfrak{B}_{d}}$ if $(c,\text{tail}(w))\in R^{\mathfrak{B}}$. We apply this procedure recursively to the new structure (in a fair way) and obtain the desired structure $\mathfrak{B}^{\prime}$ as the limit of the resulting sequence of structures.

($\Rightarrow$) Assume that $\varphi_{1}\models_{\Sigma}\varphi_{2}$. Let $\mathfrak{A}$ be a regular forest model $\mathfrak{A}$ of $\varphi_{1}$ that has finite outdegree and let $A_{\bot}\subseteq A$ be such that $A_{\bot}\cap\rho$ is infinite for any maximal infinite $\Sigma$-path $\rho$ in $\mathfrak{A}$. By Theorem C.2, there is a model $\mathfrak{B}$ of $\varphi_{2}$ such that

for every $a\in A$ there is a $b\in B$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ 2. 2.

for every $b\in B$, one of the following holds:

1. (a)

there is an $a\in A$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$; 2. (b)

there are $a_{\bot},a_{0},a_{1},\dots,a^{\prime}_{0},a^{\prime}_{1},\dots\in A$ such that $a_{\bot}\prec a_{0}\prec a_{1}\prec\cdots$ and, for all $i\geq 0$, $a_{i}\prec a^{\prime}_{i}$ and $(\mathfrak{A},a_{i}^{\prime})\sim^{a_{\bot}}_{\Sigma}(\mathfrak{B},b)$.

Let $t$ be a 1-type for $\varphi_{2}$ realized by some $b\in B$. We have to find an $a\in A$ such that $(\mathfrak{A},a)\sim^{A_{\bot}}_{\Sigma}(\mathfrak{B},b)$. If there is an $a\in A$ such that $(\mathfrak{A},a)\sim_{\Sigma}(\mathfrak{B},b)$ then we are done as $(\mathfrak{A},a)\sim_{\Sigma}^{A_{\bot}}(\mathfrak{B},b)$ follows. Otherwise there are $a_{\bot},a_{0},a_{1},\dots,a^{\prime}_{0},a^{\prime}_{1},\dots\in A$ such that $a_{\bot}\prec a_{0}\prec a_{1}\prec\cdots$ and, for all $i\geq 0$, $a_{i}\prec a^{\prime}_{i}$ and $(\mathfrak{A},a_{i}^{\prime})\sim^{a_{\bot}}_{\Sigma}(\mathfrak{B},b)$. Then let $\rho$ be a $\Sigma$-path containing $a_{\bot},a_{0},a_{1},\ldots$. $A_{\bot}\cap\rho$ is infinite and so we can choose an $a_{i}^{\prime}$ such that there are at least two elements of $A_{\bot}$ on the path from $a_{\bot}$ to $a_{i}^{\prime}$. It follows from the definition of $\sim^{A_{\bot}}_{\Sigma}$ that $(\mathfrak{A},a_{i}^{\prime})\sim^{A_{\bot}}_{\Sigma}(\mathfrak{B},b)$, as required.

Appendix D Proofs for Section 5

We construct the required 2ATAs.

Lemma D.1**.**

*Let $\varphi_{1}$ be a GF2-sentence. There is a 2ATA $\mathcal{A}_{1}$ that accepts a $\Theta$-labeled tree $(T,L)$ iff $\mathfrak{A}_{(T,L)}$ is a model of $\varphi_{1}$. *

We assume that in all subformulas of $\varphi_{1}$ of the form $\exists\mathbf{y}(\alpha(\mathbf{x},\mathbf{y})\wedge\varphi(\mathbf{x},\mathbf{y}))$ and $\forall\mathbf{y}(\alpha(\mathbf{x},\mathbf{y})\rightarrow\varphi(\mathbf{x},\mathbf{y}))$, $\mathbf{y}$ consists of exactly one variable and $\alpha(\mathbf{x},\mathbf{y})$ is a relational atom with two variables or an equality atom. This can be done w.l.o.g. because each sentence $\exists xy\varphi(x,y)$ can be rewritten into $\exists x(x=x\wedge\exists y\varphi(x,y))$, each sentence $\exists x(\alpha(x)\wedge\varphi(x))$ with $\alpha$ a relational atom can be rewritten into $\exists x(x=x\wedge\alpha(x)\wedge\varphi(x))$, and likewise for universal quantifiers. We further assume that $\varphi_{1}$ has no subformulas of the form $\exists x(x=y\wedge\varphi(x,y))$ with $x\neq y$; such formulas are equivalent to $\varphi[y/x]$, that is, the result of replacing in $\varphi$ all occurrences of $x$ with $y$. The result of these assumptions is that each formula $\exists\mathbf{y}(\alpha(\mathbf{x},\mathbf{y})\wedge\varphi(\mathbf{x},\mathbf{y}))$ takes the form $\exists x(x=x\wedge\psi(x))$ or $\exists x\psi(x,y)$, and likewise for universally quantified formulas. We define $\mathcal{A}_{1}=(Q_{1},\Theta,q_{\varphi_{1}},\delta_{1},\Omega_{1})$ where

[TABLE]

and $\Omega_{1}$ assigns two to all states except those of the form $q_{\exists x(x=x\wedge\psi(x))}$, to which it assigns one. The underlining in states of the form $q_{\varphi(x,\underline{y})}$ and $q_{\varphi(\underline{x},y)}$ serves as a marking of the variable that is bound to the tree node to which the state is assigned. We define the transition function $\delta_{1}$ as follows, for each $\sigma=(\tau,M)$:

[TABLE]

[TABLE]

where $\sigma$ ranges over $\Theta$, $z,z^{\prime}$ range over $\{x,y\}$, and $\circ$ ranges over $\{{\wedge},{\vee}\}$. With $\varphi(z^{\prime},z)$, we mean the result of exchanging in $\varphi(z,z^{\prime})$ the variables $z$ and $z^{\prime}$, and $\overline{\varphi(z,z^{\prime})}$ denotes the negation normal form of the negation of $\varphi(z,z^{\prime})$.

We now complete the construction of the 2ATA $\mathcal{A}_{2}$. It remains to implement the obligation represented by states of the form $t^{0}$, that is, the existence of $A_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulations. Recall that such a bisimulation consists of two relations $\sim^{A_{\bot},0}_{\Sigma}$ and $\sim^{A_{\bot},1}_{\Sigma}$, each of which behaves essentially like a GF${}^{2}(\Sigma)$-bisimulation except in some special cases that pertain to the $A_{\bot}$-marking of one of the involved structures, which in this case is the structure $\mathfrak{A}_{(T,L)}$. To deal with $\sim^{A_{\bot},0}_{\Sigma}$ and $\sim^{A_{\bot},1}_{\Sigma}$, we take copies $q^{0}$ and $q^{1}$ of every state $q$ that is of the form $t$, $t_{\downarrow}$, $t_{\uparrow}$, $\lambda$, and $\lambda_{\uparrow}$, and also copies of the above block of transitions, modified in a suitable way to take care of the special cases. This is implemented for $\sim^{A_{\bot},0}_{\Sigma}$ by the following transitions:

[TABLE]

The transitions for $\sim^{A_{\bot},1}_{\Sigma}$ are as follows:

[TABLE]

Lemma D.2**.**

$\mathcal{A}_{2}$* satisfies the condition from Lemma 5.1.*

Proof D.3**.**

“$\Leftarrow$”. Let $(T,L)$ be a $\Theta$-labeled tree and let $\mathfrak{B}$ be a model of $\varphi_{2}$ such that Conditions 1 and 2 of Theorem 4.4 are satisfied when $\mathfrak{A}$ is replaced with $\mathfrak{A}_{(T,L)}$ (and when $A_{\bot}$ is the set described by the second component of the $L$-labels). We argue that $\mathfrak{B}$ can be used to guide a run of $\mathcal{A}_{2}$ on $(T,L)$ so that it is accepting.

In this run, $\mathcal{A}_{2}$ starts with choosing the [math]-type $s$ realized by $\mathfrak{B}$. Then, for each $\exists x\varphi(x)\in s$, we guide $\mathcal{A}_{2}$ to proceed in state $t^{?}$, where $t$ is the $1$-type of some element $b\in B$ with $\mathfrak{B}\models\varphi(b)$. By Condition 2 of Theorem 4.4, there is a $w\in A_{(T,L)}$ such that $\mathsf{tp}_{\mathfrak{B}}(b)=t$ and $(\mathfrak{A}_{(T,L)},w)\sim^{A_{\bot}}(\mathfrak{B},b)$. In the search state $t^{?}$, we guide the run to reach $w$ and switch to state $t^{0}$ there. The automaton also sends a copy in state $s$ to each node $w\in A_{(T,L)}$. By Condition 1 of Theorem 4.4, there is a $b\in B$ such that $(\mathfrak{A}_{(T,L)},w)\sim_{\Sigma}(\mathfrak{B},b)$. We guide the run to proceed in state $t$, the 1-type of $b$.

At this point, the automaton needs to satisfy two kinds of obligations:

states $t$ true at a node $w\in A_{(T,L)}$ representing the obligation to verify that there is a $b\in B$ with 1-type $t$ and such that $(\mathfrak{A}_{(T,L)},w)\sim_{\Sigma}(\mathfrak{B},b)$ and 2. 2.

states $t^{0}$ true at a node $w\in A_{(T,L)}$ representing the obligation to verify that there is a $b\in B$ with 1-type $t$ and such that $(\mathfrak{A}_{(T,L)},w)\sim^{A_{\bot}}_{\Sigma}(\mathfrak{B},b)$.

Note that we have guided the run so that the required bisimulations indeed exist and therefore we can use them to further guide the run. We only consider Case 1 above, thus concentrating on states of the form $t$, $t_{\downarrow}$, $t_{\uparrow}$, $\lambda$, and $\lambda_{\uparrow}$. Suppose the automaton is in state $t$ at node $w$. By the way in which we guide the run, there is then a $b\in B$ with 1-type $t$ and such that $(\mathfrak{A}_{(T,L)},w)\sim_{\Sigma}(\mathfrak{B},b)$. We guide the run to select as $T$ the set of all guarded 2-types $\lambda$ such that $\mathfrak{B}\models(\exists y\lambda(x,y))(b)$. For each such $\lambda$, there must be a $b^{\prime}\in B$ and a $v\in A_{(T,L)}$ with $\mathfrak{B}\models\lambda(b,b^{\prime})$ and $(\mathfrak{A}_{(T,L)},v)\sim_{\Sigma}(\mathfrak{B},b^{\prime})$ where $v$ is either the predecessor of $w$ or a successor of it. In the former case, we guide the automaton to switch to state $\lambda_{\uparrow}$ and in the latter, we guide it to execute $\Diamond\lambda$. When the automaton was sent in state $t_{\downarrow}$ to a successor $v$ of $w$, then there must be a $b^{\prime}\in B$ such that $(\mathfrak{A}_{(T,L)},v)\sim_{\Sigma}(\mathfrak{B},b^{\prime})$ and $\mathfrak{B}\models\lambda(b,b^{\prime})$ for some guarded 2-type $\lambda$. Guide the run to choose $\lambda$. The decision to be taken for states $t_{\uparrow}$ is handled very similarly.

“$\Rightarrow$”. Let $(T,L)$ be a $\Theta$-labeled tree that is accepted by $\mathcal{A}_{2}$. Then there is an accepting run $(T_{r},r)$ of $\mathcal{A}_{2}$ on $(T,L)$. We show how to use $(T_{r},r)$ to construct a model $\mathfrak{B}$ of $\varphi_{2}$ such that Conditions 1 and 2 of Theorem 4.4 are satisfied when $\mathfrak{A}$ is replaced with $\mathfrak{A}_{(T,L)}$. Along with $\mathfrak{B}$, we construct the following objects:

• •

a GF${}^{2}(\Sigma)$-bisimulation $\sim$ between $\mathfrak{A}_{(T,L)}$ and $\mathfrak{B}$ which witnesses that Condition 1 of Theorem 4.4 is satisfied,

• •

two relations $\sim^{A_{\bot},0}$ and $\sim^{A_{\bot},1}$ that form an $A_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulation between $\mathfrak{A}_{(T,L)}$ and $\mathfrak{B}$, where $A_{\bot}\subseteq\mathfrak{A}_{(T,L)}$ is the subset defined by the second component of $L$, and which witness that Condition 2 of Theorem 4.4 is satisfied, and

• •

a function $\mu$ that assigns to each element of $\mathfrak{B}$ the 1-type that we aim to realize there.

Throughout the construction, we make sure that the following invariants are satisfied:

if $(w,b)\in{\sim}$, then the label $(w,\mu(b))$ occurs in $(T_{r},r)$; 2. 2.

if $(w,b)\in{\sim^{A_{\bot},i}}$, $i\in\{0,1\}$, then the label $(w,\mu(b)^{0})$ occurs in $(T_{r},r)$.

The start of the construction is as follows:

• •

for each label $(w,t)$ that occurs in $(T_{r},r)$, introduce an element $b$ of $B$, add $(w,b)$ to $\sim$, and set $\mu(b)=t$;

• •

for each label $(w,t^{0})$ that occurs in $(T_{r},r)$, introduce an element $b$ of $B$, add $(w,b)$ to $\sim^{A_{\bot},0}$, and set $\mu(b)=t$.

We then iteratively extend $\mathfrak{B}$, $\sim$, $\sim^{A_{\bot},0}$, $\sim^{A_{\bot},1}$, and $\mu$, obtaining the desired structure and bisimulations in the limit. In each step, process every $b\in B$ that has not been processed in a previous round. There are three cases.

Case (a)**. There is a $(w,b)\in{\sim}$. By Invariant 1, we find a node $x\in T_{r}$ such that $r(x)=(w,\mu(b))$. We perform two steps:

• •

For every predecessor or successor $v$ of $w$ in $T$ with $\text{at}_{\mathfrak{A}_{(T,L)}}^{\Sigma}(w,v)$ guarded, there must be a 2-type $\lambda$ such that $\mu(b)\approx\lambda$, $(v,\lambda_{y})$ occurs as a label in $(T_{r},r)$, and $\text{at}_{\mathfrak{A}_{(T,L)}}^{\Sigma}(w,v)=_{\Sigma}\lambda$. Extend $\mathfrak{B}$ with a new element $b^{\prime}$, extend the interpretation of the predicates in $\mathfrak{B}$ such that $\text{at}_{\mathfrak{B}}^{\Sigma}(w,v)=_{\Sigma}\lambda$, set $\mu(b^{\prime})=\lambda_{y}$, and extend $\sim$ with $(v,b^{\prime})$.

• •

There must be a set $T$ of guarded 2-types such that $t\approx T$ and for every $\lambda\in T$, there is a predecessor or successor $v$ of $w$ in $T$ such that $\mu(b)\approx\lambda$, $(v,\lambda_{y})$ occurs as a label in $(T_{r},r)$, and $\text{at}_{\mathfrak{A}_{(T,L)}}^{\Sigma}(w,v)=_{\Sigma}\lambda$. Extend $\mathfrak{B}$ with a new element $b^{\prime}$ (for every $\lambda$), extend the interpretation of the predicates in $\mathfrak{B}$ such that $\text{at}_{\mathfrak{B}}^{\Sigma}(w,v)=_{\Sigma}\lambda$, set $\mu(b^{\prime})=\lambda_{y}$, and extend $\sim$ with $(v,b^{\prime})$.

Case (b)**. There is a $(w,b)\in{\sim^{A_{\bot},0}}$. By Invariant 2, we find a node $x\in T_{r}$ such that $r(x)=(w,\mu(b)^{0})$. We can now proceed exactly as in Case (a) except that, in both subcases, we add $(v,b^{\prime})$ to $\sim^{A_{\bot},1}$ if $v$ is a predecessor of $w$ and $v\in A_{\bot}$, and to $\sim^{A_{\bot},0}$ otherwise.

Case (c)**. There is a $(w,b)\in{\sim^{A_{\bot},1}}$. By Invariant 2, we find a node $x\in T_{r}$ such that $r(x)=(w,\mu(b)^{1})$. If the predecessor of $w$ is not in $A_{\bot}$, then we again proceed as in Case (a) except that, in both subcases, we add $(v,b^{\prime})$ to $\sim^{A_{\bot},0}$ if $v$ is a sucessor of $w$ and $w\in A_{\bot}$, and to $\sim^{A_{\bot},1}$ otherwise. If the predecessor of $w$ is in $A_{\bot}$, then we we also proceed as in Case (a), but do not add $(v,b^{\prime})$ to any of the constructed bisimulations.

Case (d)**. None of the above cases applies. Then we proceed as in Case (a), again not adding $(v,b^{\prime})$ to any of the constructed bisimulations.

It can be verified that, as intended the structure $\mathfrak{B}$ obtained in the limit is a model of $\varphi_{2}$, that the relation $\sim$ is a GF${}^{2}(\Sigma)$-bisimulation, and that $\sim^{A_{\bot},0},\sim^{A_{\bot},1}$ form an $A_{\bot}$-delimited GF${}^{2}(\Sigma)$-bisimulation.

Recall that we define the overall 2ATA $\mathcal{A}$ so that it accepts $L(\mathcal{A}_{1})\cap\overline{L(\mathcal{A}_{2})}\cap L(\mathcal{A}_{3})$. Using Theorem 4.4, it can be verified that, as intended, $\varphi_{1}\models_{\text{GF}^{2}(\Sigma)}\varphi_{2}$ iff $L(\mathcal{A})=\emptyset$. Note that for the “only if” direction, we have to show that $L(\mathcal{A})\neq\emptyset$ implies that there is a regular forest model of $\varphi_{1}$ that satisfies the negation of the conditions in Theorem 4.4. As is the case for other kinds of tree automata, also for the 2ATA $\mathcal{A}$ it can be shown that $L(\mathcal{A})\neq\emptyset$ implies that $\mathcal{A}$ accepts a regular $\Theta$-labeled tree $(T,L)$. The corresponding structure $\mathfrak{A}_{(T,L)}$ must then also be regular.

We show that $\Sigma$-entailment, $\Sigma$-inseparability, and conservative extensions in GF2 are 2ExpTime-hard. The proof is by reduction of the word problem for exponentially space bounded alternating Turing machines (ATMs). An ATM is of the form $M=(Q,\Theta,\Gamma,q_{0},\Delta)$. The set of states $Q=Q_{\exists}\uplus Q_{\forall}\uplus\{q_{a}\}\uplus\{q_{r}\}$ consists of existential states from $Q_{\exists}$, universal states from $Q_{\forall}$, an accepting state $q_{a}$, and a rejecting state $q_{r}$; $\Theta$ is the input alphabet and $\Gamma\supset\Theta$ the work alphabet that contains a blank symbol $\square\notin\Theta$; $q_{0}\in Q_{\exists}$ is the starting state; and the transition relation $\Delta$ is of the form $\Delta\;\subseteq\;Q\times\Gamma\times Q\times\Gamma\times\{L,R\}.$ We write $\Delta(q,a)$ for $\{(q^{\prime},b,M)\mid(q,a,q^{\prime},b,M)\in\Delta\}$ and assume that $\Delta(q,b)=\emptyset$ for all $q\in\{q_{a},q_{r}\}$ and $b\in\Gamma$.

A configuration of an ATM is a word $wqw^{\prime}$ with $w,w^{\prime}\in\Gamma^{*}$ and $q\in Q$. The intended meaning is that the one-side infinite tape contains the word $ww^{\prime}$ with only blanks behind it, the machine is in state $q$, and the head is on the symbol just after $w$. The successor configurations of a configuration $wqw^{\prime}$ are defined in the usual way in terms of the transition relation $\Delta$. A halting configuration (resp. accepting configuration) is of the form $wqw^{\prime}$ with $q\in\{q_{a},q_{r}\}$ (resp. $q=q_{a}$).

A computation tree of an ATM $M$ on input $w$ is a tree whose nodes are labeled with configurations of $M$ on $w$, such that the descendants of any non-leaf labeled by a universal (resp. existential) configuration include all (resp. one) of the successor configurations of that configuration. A computation tree is accepting if the root is labeled with the initial configuration $q_{0}w$ for $w$ and all leaves with accepting configurations. An ATM $M$ accepts input $w$ if there is a computation tree of $M$ on $w$.

Take an exponentially space bounded ATM $M$ whose word problem is 2ExpTime-hard [8]. We may w.l.o.g. assume that the length of every computation path of $M$ on $w\in\Theta^{n}$ is bounded by $2^{2^{n}}$. We can also assume that for each $q\in Q_{\forall}\cup Q_{\exists}$ and each $a\in\Gamma$, the set $\Delta(q,a)$ has exactly two elements. We assume that these elements are ordered, i.e., $\Delta(q,a)$ is an ordered pair $((q_{L},b_{L},M_{L}),(q_{R},b_{R},M_{R}))$. Furthermore, we assume that $M$ never attempts to move left on the left-most tape cell.

Let $w=a_{0}\cdots a_{n-1}\in\Theta^{*}$ be an input to $M$. In the following, we construct GF2 sentences $\varphi_{1}$ and $\varphi_{2}$ such that $\varphi_{1}\wedge\varphi_{2}$ is a conservative extension of $\varphi_{1}$ if and only if $M$ does not accept $w$. Informally, the main idea is to construct $\varphi_{1}$ and $\varphi_{2}$ such that models of sentences that witness non-conservativity describe an accepting computation tree of $M$ on $w$. In such models, each domain element represents a tape cell of a configuration of $M$, the binary predicate $N$ indicates moving to the next tape cell in the same configuration, and the binary predicates $L$ and $R$ indicate moving to left and right successor configurations in accepting configuration trees. Thus, each node of the computation tree (that is, each configuration) is spread out over a sequence of nodes in the model. We actually assume that every non-halting configuration has two successor configurations, also when its state is existential. This can of course easily be achieved by duplicating subtrees in computation trees. The following predicates are used in $\varphi_{1}$:

• •

a unary predicate $P$ to mark the root of computation trees;

• •

binary predicates $N$, $R$, $L$, as explained above;

• •

unary predicates $C_{0},\dots,C_{n-1}$ that represent the bits of a binary counter which identifies tape positions;

• •

a unary predicate $F$ that marks the topmost configuration in the configuration tree;

• •

unary predicates $S_{a}$, $a\in\Gamma$, to represent the tape content of cells that are not under the head;

• •

unary predicates $S_{q,a}$, $q\in Q$ and $a\in\Gamma$, to represent the state of a configuration, the head position, and the tape content of the cell that is under the head;

• •

unary predicates $S^{p}_{a}$ and $S^{p}_{q,a}$, with the ranges of $q$ and $a$ as above, to represent the same information, but for the previous configuration in the tree instead of for the current one;

• •

unary predicates $Y_{L,q,a,M}$ and $Y_{R,q,a,M}$, $q\in Q$, $a\in\Gamma$, $M\in\{L,R\}$, to record the transition to be executed in the subsequent configurations;

• •

unary predicates $Y_{q,a,M}$, with the ranges of $q,a,M$ as above, to record the transition executed to reach the current configuration.

The sentence $\varphi_{2}$ uses some additional unary predicates, including $C^{\prime}_{0},\dots,C^{\prime}_{n-1}$ to implement another counter whose purpose is explained below.

The sentences $\varphi_{1}$ and $\varphi_{2}$ are shown in Figures 1 and 2, respectively, where $q$ and $q^{\prime}$ range over $Q$, $a,b,b^{\prime}$ over $\Gamma$, $M$ and $P$ over $\{L,R\}$, $T,T_{L},T_{R}$ over $Q\times\Gamma\times\{L,R\}$, and $\alpha$ over $\Gamma\cup(Q\times\Gamma)$. The formula $\varphi_{C=i}(x)$, which is easily worked out in detail, expresses that the value of the binary counter implemented by $C_{0},\dots,C_{n-1}$ has value exactly $i$ at $x$, and likewise for $\varphi_{C<i}(x)$ and $\varphi_{C\geq i}(x)$, and for the primed versions in $\varphi_{2}$ which refer to the counter implemented by $C^{\prime}_{0},\dots,C^{\prime}_{n-1}$. The formula $\varphi_{C{+}{+}}(x,y)$ expresses that the counter value at $y$ is obtained from the counter value at $x$ by incrementation modulo $2^{n}$. Again, we omit the details.

Let us walk through $\varphi_{1}$ and $\varphi_{2}$ and give some intuition of what the various conjuncts are good for. In $\varphi_{1}$, Lines (1) to (4) ensure that at an element that satisfies $P$, there is an infinite tree of the expected pattern: first $2^{n}-1$ $N$-edges without branching, then a binary branching of an $L$-edge and an $R$-edge, then $2^{n}-1$ $N$-edges without branching, and so on, ad infinitum. Of course, a computation tree will be represented using only a finite initial piece of this infinite tree. These conjuncts also set up the counter $C$ so that it identifies the position of tape cells and the marker $F$ so that it identifies the topmost configuration in the tree. Line (5) says that every cell is labeled with exactly one symbol and that the state is unique (locally to one cell; there is no need to express the same globally for the entire configuration), and Line (6) says the same for the representation of the previous configuration. Lines (7) to (9) make sure that the topmost configuration in the infinite tree is the initial configuration of $M$ on input $w$. Lines (10) and (11) choose transitions to execute and Lines (12) to (14) propagate this choice down to the subsequent configurations. Assume that the predicates of the $S^{p}_{a}$ and $S^{p}_{q,a}$ indeed represent the previous configuration, Lines (15) to (20) then implement the chosen transitions. Line (21) says that we do never see a rejecting halting configuration.

Now for $\varphi_{2}$. Essentially, we want to achieve that a sentence is a witness for non-conservativity if and only if it expresses that its models contain (a representation of) an accepting computation tree of $M$ on $w$ whose root is labeled with $P$. This is achieved by designing $\varphi_{2}$ so that, whenever a tree model of $\varphi_{1}$ contains only instances of $P$ that are not the root of such a computation tree, then this model can be extended to a model of $\varphi_{2}$ by assigning an interpretation to the additional predicates in $\varphi_{2}$. Note that $\varphi_{1}$ already enforces that, below any instance of $P$, there is a tree that satisfies almost all of the required conditions of an accepting computation tree. In fact, the only way in which that tree cannot be an accepting configuration tree is that the predicates $S^{p}_{a}$ and $S^{p}_{q,a}$ do not behave in the expected way, that is, there is a configuration and a cell in this configuration that is labeled with $S_{\alpha}$, $\alpha\in\Gamma\cup(Q\times\Gamma)$, and in one of the two subsequent configurations the same cell is not labeled with $S^{p}_{\alpha}$. We thus design $\varphi_{2}$ so that it can be made true whenever the model contains such a defect. In Line (22), we select the place where the defect is. Line (23) ensures that the counter $C^{\prime}$ starts counting with value zero at that place, and that the marker $M$ is set there, too. Line (24) memorizes the content $\alpha$ of the cell in the upper configuration involved in the defect. Lines (25) to (27) propagate downwards the memorized content and make sure that, at the corresponding cell of at least one subsequent configuration (which is identified using the counter $C^{\prime}$), we do not find $S^{p}_{\alpha}$.

Lemma D.4**.**

If $M$ accepts $w$, then $\varphi_{1}\wedge\varphi_{2}$ is not a GF2*-conservative extension of $\varphi_{1}$.* 2. 2.

If there exists a $\textup{{sig}}(\varphi_{1})$-structure that satisfies $\varphi_{1}$ and cannot be extended to a model of $\varphi_{1}\wedge\varphi_{2}$, then $M$ does not accept $w$.

Proof D.5**.**

(sketch) For Point 1 assume that $M$ accept $w$. Then there is an accepting computation tree of $M$ on $w$. Let $\Sigma=\textup{{sig}}(\varphi_{1})$. We can find a GF${}^{2}(\Sigma)$-sentence $\psi_{1}$ which expresses that the model contains a (homomorphic image of a) finite tree which represents this configuration tree and whose root is labeled with $P$. We can also find a GF${}^{2}(\Sigma)$-sentence $\psi_{2}$ which expresses that nowhere in the model there is a defect situation. It can be verified that $\psi_{1}\wedge\psi_{2}$ is satisfiable w.r.t. $\varphi_{1}$, but not w.r.t. $\varphi_{2}$ because $\varphi_{2}$ requires the existence of a defect situation whenever the extension of $P$ is non-empty.

For Point 2 assume that $\mathfrak{A}$ is a $\textup{{sig}}(\varphi_{1})$-structure that satisfies $\varphi_{1}$. If $P^{\mathfrak{A}}=\emptyset$, then the desired model $\mathfrak{B}$ is obtained from $\mathfrak{A}$ by interpreting all predicates in $\mathsf{sig}(\varphi_{2})\setminus\mathsf{sig}(\varphi_{1})$ as empty. Otherwise, take some $a\in P^{\mathfrak{A}}$. We can follow the existential quantifiers in $\varphi_{1}$ to identify a homomorphic image of an infinite tree in $\mathfrak{A}$ with root $a$ whose edges follow the expected pattern and that is labeled in the expected way by the counter $C$. Since $\mathfrak{A}$ is a model of $\varphi_{1}$, an initial piece of the identified tree represents an accepting computation tree of $M$ on $w$ provided that the predicates $S^{p}_{\alpha}$ behave as expected, that is, if there is no defect of the form described above. Since $M$ does not accept $w$, there must thus be such a defect, that is a path of length $2^{n}$ that links a cell of a configuration with the corresponding cell of a subsequent configuration such that the former is labeled with $S_{\alpha}$, but the latter is not labeled with $S^{p}_{\alpha}$. All the elements of the path (with the possible exception of the start point and the end point) are labeled with a different value of the counter $C$ and must thus be distinct. Consequently, we can interpret the counter $C^{\prime}$ and the other symbols in $\varphi_{2}$ to extend $\mathfrak{A}$ to a model of $\varphi_{2}$, as desired.

It follows directly from Lemma D.4 that $\Sigma$-entailment, $\Sigma$-inseparability, and conservative extensions in GF2, are 2ExpTime-hard.

Appendix E 2ATAs and Their Emptiness Problem

The aim of this section is to show that the emptiness problem for 2ATAs can be solved in time exponential in the number of states. For proving this, we reduce it to the emptiness problem of the standard two-way alternating tree automata over trees of fixed outdegree [39].

We start with making precise the semantics of 2ATAs. Let $\mathcal{A}=(Q,\Theta,q_{0},\delta,\Omega)$ be a 2ATA and $(T,L)$ a $\Theta$-labeled tree. A run for $\mathcal{A}$ on $(T,L)$ is a $T\times Q$-labeled tree $(T_{r},r)$ such that:

• •

$\varepsilon\in T_{r}$ and $r(\varepsilon)=(\varepsilon,q_{0})$;

• •

For all $y\in T_{r}$ with $r(y)=(x,q)$ and $\delta(q,L(x))=\varphi$, there is an assignment $v$ of truth values to the transitions in $\varphi$ such that $v$ satisfies $\varphi$ and:

• –

if $v(p)=1$, then $r(y^{\prime})=(x,p)$ for some successor $y^{\prime}$ of $y$ in $T_{r}$;

• –

if $v(\langle-\rangle p)=1$, then $x\neq\varepsilon$ and there is a successor $y^{\prime}$ of $y$ in $T_{r}$ with $r(y^{\prime})=(x\cdot-1,p)$;

• –

if $v([-]p)=1$, then $x=\varepsilon$ or there is a successor $y^{\prime}$ of $y$ in $T_{r}$ such that $r(y^{\prime})=(x\cdot-1,p)$;

• –

if $v(\Diamond p)=1$, then there is a successor $x^{\prime}$ of $x$ in $T$ and a successor $y^{\prime}$ of $y$ in $T_{r}$ such that $r(y^{\prime})=(x^{\prime},p)$;

• –

if $v(\Box p)=1$, then for every successor $x^{\prime}$ of $x$ in $T$, there is a successor $y^{\prime}$ of $y$ in $T_{r}$ such that $r(y^{\prime})=(x^{\prime},p)$.

Let $\gamma=i_{0}i_{1}\cdots$ be an infinite path in $T_{r}$ and denote, for all $j\geq 0$, with $q_{j}$ the state such that $r(i_{0}\cdots i_{j})=(x,q_{j})$. The path $\gamma$ is accepting if the largest number $m$ such that $\Omega(q_{j})=m$ for infinitely many $j$ is even. A run $(T_{r},r)$ is accepting, if all infinite paths in $T_{r}$ are accepting. Finally, a tree is accepted if there is some accepting run for it.

We next introduce strategy trees similar to [39, Section 4]. A strategy tree for a 2ATA $\mathcal{A}$ is a tree $(T,\tau)$ where $\tau$ labels every node in $T$ with a subset $\tau(x)\subseteq 2^{Q\times(\mathbb{N}\cup\{-1\})\times Q}$, that is, with a graph with nodes from $Q$ and edges labeled with natural numbers or $-1$. Intuitively, $(q,i,p)\in\tau(x)$ expresses that, if we reached node $x$ in state $q$, then we should send a copy of the automaton in state $p$ to $x\cdot i$. For each label $\zeta$, we define $\mathsf{state}(\zeta)=\{q\mid(q,i,q^{\prime})\in\zeta\}$, that is, the set of sources in the graph $\zeta$. A strategy tree is on an input tree $(T^{\prime},L)$ if $T=T^{\prime}$, $q_{0}\in\mathsf{state}(\tau(\varepsilon))$, and for every $x\in T$, the following conditions are satisfied:

if $(q,i,p)\in\tau(x)$, then $x\cdot i\in T$; 2. 2.

if $(q,i,p)\in\tau(x)$, then $p\in\mathsf{state}(\tau(x\cdot i))$; 3. 3.

if $q\in\mathsf{state}(\tau(x))$, then the truth assignment $v_{q,x}$ defined below satisfies $\delta(q,L(x))$:

1. (a)

$v_{q,x}(p)=1$ iff $(q,0,p)\in\tau(x)$; 2. (b)

$v_{q,x}(\langle-\rangle p)=1$ iff $(q,-1,p)\in\tau(x)$; 3. (c)

$v_{q,x}([-]p)=1$ iff $x=\varepsilon$ or $(q,-1,p)\in\tau(x)$; 4. (d)

$v_{q,x}(\Diamond p)=1$ iff there is some $i$ with $(q,i,p)\in\tau(x)$; 5. (e)

$v_{q,x}(\Box p)=1$ iff $(q,i,p)\in\tau(x)$, for all $x\cdot i\in T$;

A path $\beta$ in a strategy tree $(T,\tau)$ is a sequence $\beta=(u_{1},q_{1})(u_{2},q_{2})\cdots$ of pairs from $T\times Q$ such that for all $\ell>0$, there is some $i$ such that $(q_{\ell},i,q_{\ell+1})\in\tau(u_{\ell})$ and $u_{\ell+1}=u_{\ell}\cdot i$. Thus, $\beta$ is obtained by following moves prescribed by the strategy tree. We say that $\beta$ is accepting if the largest number $m$ such that $\Omega(q_{i})=m$, for infinitely many $i$, is even. A strategy tree $(T,\tau)$ is accepting if all infinite paths in $(T,\tau)$ are accepting.

Lemma E.1**.**

A 2ATA accepts a $\Theta$-labeled tree $(T,L)$ iff there is an accepting strategy tree for $\mathcal{A}$ on $(T,L)$.

Proof E.2**.**

The “if”-direction is immediate: just read off an accepting run from the accepting strategy tree.

For the “only if”-direction, we observe that acceptance of an input tree can be defined in terms of a parity game between Player 1 (trying to show that the input is accepted) and Player 2 (trying to challenge that). The initial configuration is $(\varepsilon,q_{0})$ and Player 1 begins. Consider a configuration $(x,q)$. Player 1 chooses a satisfying truth assignment $v$ of $\delta(q,L(x))$. Player 2 chooses a transition $\alpha$ with $v(\alpha)=1$ and the next configuration is determined as follows:

• •

if $\alpha=p$, then the next configuration is $(x,p)$,

• •

if $\alpha=\langle-\rangle p$, then the next configuration is $(x\cdot-1,p)$ unless $x=\varepsilon$ in which case Player 1 loses immediately.

• •

if $\alpha=[-]p$, then the next configuration is $(x\cdot-1,p)$ unless $x=\varepsilon$ in which case Player 2 loses immediately;

• •

if $\alpha=\Diamond p$, then Player 1 chooses some $i$ with $x\cdot i\in T$ (and loses if no such $i$ exists) and the next configuration is $(x\cdot i,p)$;

• •

if $\alpha=\Box p$, then Player 2 chooses some $i$ with $x\cdot i\in T$ (and loses if no such $i$ exists) and the next configuration is $(x\cdot i,p)$.

Player 1 wins an infinite play $(x_{0},q_{0})(x_{1},q_{1})\cdots$ if the largest number $m$ such that $\Omega(q_{i})=m$, for infinitely many $i$, is even. It is not difficult to see that Player 1 has a winning strategy on an input tree iff $\mathcal{A}$ accepts the input tree. Observe now that the defined game is a parity game and thus Player 1 has a winning strategy iff she is has a memoryless winning strategy [15]. It remains to observe that a memoryless winning strategy is nothing else than an accepting strategy tree.

Based on the previuos lemma, we show that, if $L(\mathcal{A})$ is not empty, then it contains a tree of small outdegree.

Lemma E.3**.**

If $L(\mathcal{A})\neq\emptyset$, then there is a $(T,L)\in L(\mathcal{A})$ such that the outdegree of $T$ is bounded by the number of states in $\mathcal{A}$.

Proof E.4**.**

Let $(T,L)$ be a $\Theta$-labeled tree and $\tau$ an accepting strategy tree on $T$. We construct a tree $T^{\prime}\subseteq T$ and an accepting strategy tree $\tau^{\prime}$ on $(T^{\prime},L^{\prime})$ where $L^{\prime}$ is the restriction of $L$ to $T^{\prime}$. Start with $T^{\prime}=\{\varepsilon\}$ and $\tau^{\prime}$ the empty mapping. Then exhaustively repeat the following step. Select an $x\in T^{\prime}$ with $\tau^{\prime}(x)$ undefined, in a fair way. Then construct $\tau^{\prime}(x)$ as follows:

for every $(q,i,p)\in\tau(x)$ with $i\in\{-1,0\}$, include $(q,i,p)$ in $\tau^{\prime}(x)$; 2. 2.

for every $p\in Q$, choose an $i$ such that $(q,i,p)\in\tau(x)$ for some $q$, if existant. Then add $x\cdot i$ to $T^{\prime}$ and include $(q^{\prime},i,p)$ in $\tau^{\prime}(x)$ for all $(q^{\prime},j,p)\in\tau(x)$; 3. 3.

further include $(q,i,p)$ in $\tau^{\prime}(x)$ whenever $x\cdot i\in T^{\prime}$ and $(q,j,p)\in\tau(x)$ for all $j$ with $x\cdot j\in T$.

Clearly, $T^{\prime}$ has the desired outdegree. It remains to show that $\tau^{\prime}$ is an accepting strategy tree on $(T^{\prime},L^{\prime})$. Observe that the following properties hold for all $x\in T^{\prime}$, and $p,q\in Q$:

• (i)

$(q,i,p)\in\tau(x)$* iff $(q,i,p)\in\tau^{\prime}(x)$, for $i\in\{-1,0\}$;*

• (ii)

$(q,i,p)\in\tau(x)$* for some $i>0$ with $x\cdot i\in T$ iff $(q,j,p)\in\tau^{\prime}(x)$ for some $j>0$ with $x\cdot j\in T$.*

Observe that we have $q_{0}\in\mathsf{state}(\tau^{\prime}(\varepsilon))$, by Points (i) and (ii) and since $q_{0}\in\mathsf{state}(\tau(\varepsilon))$. It can be verified that Conditions 1 and 2 of a strategy tree being on an input tree are satisfied due to the construction of $T^{\prime}$ and $\tau^{\prime}$. For Condition 3, take any $x\in T^{\prime}$ and $q\in\mathsf{state}(\tau^{\prime}(x))$. As $q\in\mathsf{state}(\tau(x))$, we know that the truth assignment $v_{q,x}$ defined for $\tau$ satisfies $\delta(q,V(x))$. Let $v^{\prime}_{q,x}$ be the truth assignment for $\tau^{\prime},q,x$. It suffices to show that, for all transitions $\alpha$, $v_{q,x}(\alpha)=1$ implies $v^{\prime}_{q,x}(\alpha)=1$. By Point (i), this is the case for transitions of the form $p,\langle-\rangle p,[-]p$. For $\alpha=\Diamond p$, we know that there is some $i,p$ with $(q,i,p)\in\tau(x)$. By Point (ii), we know that $(q,i^{\prime},p)\in\tau^{\prime}(x)$ for some $i^{\prime}$ with $x\cdot i^{\prime}\in T^{\prime}$, and thus, $v_{q,x}^{\prime}(\alpha)=1$. For $\alpha=\Box p$, we know that $(q,i,p)\in\tau(x)$ for all $i$ with $x\cdot i\in T$. By construction if $\tau^{\prime}$, it follows that $(q,i,p)\in\tau(x)$ for all $i$ with $x\cdot i\in T^{\prime}$, as required.

We finally argue that $\tau^{\prime}$ is also accepting. Let $\beta=(u_{1},q_{1})(u_{2},q_{2})\cdots$ be an infinite path in $(T^{\prime},\tau^{\prime})$. We construct an infinite path $\beta^{\prime}=(u_{1}^{\prime},q_{1})(u_{2}^{\prime},q_{2})(u_{3}^{\prime},q_{3})\cdots$ in $(T,\tau)$ as follows:

• •

$u_{1}^{\prime}=u_{1}$;

• •

if $u_{i+1}=u_{i}\cdot\ell$ with $\ell\in\{-1,0\}$, then $u_{i+1}^{\prime}=u_{i}^{\prime}\cdot\ell$.

• •

if $u_{i+1}=u_{i}\cdot\ell$ for some $\ell\geq 0$ with $(q_{i},\ell,q_{i+1})\in\tau^{\prime}(x)$, then, by Point (ii), there is some $\ell^{\prime}$ with $(q_{i},\ell^{\prime},q_{i+1})\in\tau(x)$ and $x\cdot\ell^{\prime}\in T^{\prime}$. Set $u_{i+1}=u_{i}\cdot\ell^{\prime}$.

Since every infinite path in $(T,\tau)$ is accepting, so is $\beta^{\prime}$, and thus $\beta$.

We are now reduce to reduce the emptiness problem of 2ATAs to the emptiness of alternating automata running on trees of fixed outdegree [39], which we recall here. A tree $T$ is $k$-ary if every node has exactly $k$ successors. A two-way alternating tree automaton over $k$-ary trees (2ATAk) that are $\Theta$-labeled is a tuple $\mathcal{A}=(Q,\Theta,q_{0},\delta,\Omega)$ where $Q$ is a finite set of states, $\Theta$ is the input alphabet, $q_{0}\in Q$ is an initial state, $\delta$ is the transition function, and $\Omega:Q\to\mathbb{N}$ is a priority function. The transition function maps a state $q$ and some input letter $\theta$ to a transition condition $\delta(q,\theta)$, which is a positive Boolean formula over the truth constants $\mathsf{true}$, $\mathsf{false}$, and transitions of the form $(i,q)\in[k]\times Q$ where $[k]=\{-1,0,\ldots,k\}$. A run of $\mathcal{A}$ on a $\Theta$-labeled tree $(T,L)$ is a $T\times Q$-labeled tree $(T_{r},r)$ such that

$r(\varepsilon)=(\varepsilon,q_{0})$; 2. 2.

for all $x\in T_{r},r(x)=(w,q)$, and $\delta(q,\tau(w))=\varphi$, there is a (possibly empty) set $\mathcal{S}=\{(m_{1},q_{1}),\ldots,(m_{n},q_{n})\}\subseteq[k]\times Q$ such that $\mathcal{S}$ satisfies $\varphi$ and for $1\leq i\leq n$, we have $x\cdot i\in T_{r}$, $w\cdot m_{i}$ is defined, and $\tau_{r}(x\cdot i)=(w\cdot m_{i},q_{i})$.

Accepting runs and accepted trees are defined as for 2ATAs. The emptiness problem for 2ATAks can be solved in time exponential in the number of states [39].

Theorem E.5**.**

The emptiness problem for 2ATAs can be solved in time exponential in the number of states.

Proof E.6**.**

Let $\mathcal{A}=(Q,\Theta,q_{0},\delta,\Omega)$ be a 2ATA with $n$ states. We transform $\mathcal{A}$ into a 2ATAn $\mathcal{A}^{\prime}=(Q^{\prime},\Theta^{\prime},q_{0}^{\prime},\delta^{\prime},\Omega)$, running over $n$-ary $\Theta^{\prime}$-labeled trees, where $Q^{\prime}=Q\uplus\{q_{0}^{\prime},q^{\prime},q_{r}\}$ and $\Theta^{\prime}=\Theta\times\{0,1\}$. The extended alphabet and the extra states $q_{0}^{\prime},q^{\prime},q_{r}$ are used to simulate transitions of the form $[-]p$. We make sure that the additional component labels the root node with 1 and all other nodes with 0, and based on this use $q_{r}$ to check whether we are at the root of the input tree.

Formally, we proceed as follows. For all $q\in Q$, $\theta\in\Theta$, and $b\in\{0,1\}$ obtain $\delta^{\prime}(q,(\theta,b))$ from $\delta(q,\theta)$ by replacing $q$ with $(0,q)$, $\langle-\rangle q$ with $(-1,q)$, $[-]q$ with $(0,q_{r})\vee(-1,q)$, $\Diamond q$ with $\bigvee_{i=1}^{n}(i,q)$, and $\Box q$ with $\bigwedge_{i=1}^{n}(i,q)$. To enforce the intended labeling in the second component and the correct behaviour for $q_{r}$, we set:

[TABLE]

Using Lemma E.3 it is straightforward to verify that $L(\mathcal{A})\neq\emptyset$ iff $L(\mathcal{A}^{\prime})\neq\emptyset$. Since the translation can be done in polynomial time and the emptiness problem for 2ATAks is in ExpTime, also emptiness for 2ATAs is in ExpTime.