Craig Interpolation for Decidable First-Order Fragments

Abstract

We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, we show that the smallest extension of the two-variable fragment ($\textrm{FO}^2$), and of the forward fragment (FF) with Craig interpolation, is full first-order logic. Similarly, we also show that all extensions of $\textrm{FO}^2$and of the fluted fragment (FL) with Craig interpolation are undecidable.

1 Introduction

The study of decidable fragments of first-order logic (FO) is a topic with a long history, dating back to the early 1900s ([40, 52], cf. also [16]), and more actively pursued since the 1990s. Inspired by Vardi [55], who asked “what makes modal logic so robustly decidable?” and Andreka et al. [1], who asked “what makes modal logic tick?” many decidable fragments have been introduced and studied over the last 25 years that take inspiration from modal logic (ML), which itself can be viewed as a fragment of FO that features a restricted form of quantification. These include the following fragments, each of which naturally generalizes modal logic in a different way: the two-variable fragment ($\textrm{FO}^2$) [42], the guarded fragment (GFO) [1], and the unary negation fragment (UNFO) [22]. Further decidable extensions of these fragments were subsequently identified, including the two-variable fragment with counting quantifiers ($\textrm{C}^2$) [29] and the guarded negation fragment (GNFO) [4]. The latter can be viewed as a common generalization of GFO and UNFO. Many decidable logics used in computer science and AI, including various description logics and rule-based languages, can be translated into GNFO and/or $\textrm{C}^2$. In this sense, GNFO and $\textrm{C}^2$are convenient tools for explaining the decidability of other logics. Extensions of GNFO have been studied that push the decidability frontier even further (for instance with fixed-point operators and using clique-guards), but these fall outside the scope of this paper.

In an earlier line of investigation, Quine identified the decidable fluted fragment (FL) [51], the first of several ordered logics which have been the subject of recent interest [44, 47,48,49,50]. The idea behind ordered logics is to restrict the order in which variables are allowed to occur in atomic formulas and quantifiers. Another recently introduced decidable fragment that falls in this family is the forward fragment (FF), whose syntax strictly generalizes that of FL. Both FL and FF have the finite model property (FMP) [44] and embed ML [34], but are incomparable in expressive power to GFO [45], $\textrm{FO}^2$, and UNFO.¹

Fig. 1.

Landscape of decidable fragments of FO with () and without () CIP. The inclusion marked $(*)$ holds only for sentences and self-guarded formulas.

Ideally, an FO-fragment is not only decidable, but also model-theoretically well behaved. A particularly important model-theoretic property of logics is the Craig Interpolation Property (CIP). It states that, for all formulas $\varphi , \psi$, if $\varphi \models \psi$, then there exists a formula $\vartheta$ such that $\varphi \models \vartheta$ and $\vartheta \models \psi$, and such that all non-logical symbols occurring in $\vartheta$ occur both in $\varphi$ and in $\psi$. Craig [24] proved in 1957 that FO itself has this property (hence the name). Several refinements of Craig’s result have subsequently been obtained (e.g., [10, 43]). These have found applications in various areas of computer science and AI, including formal verification, modular hard/software specification and automated deduction [18, 31, 41], and are emerging as a new prominent technology in databases [12, 53] and knowledge representation [21, 37, 39]. While we have described CIP here as a model theoretic property, it also has a proof-theoretic interpretation. Indeed, it has been argued that CIP is an indicator for the existence of nice proof systems [32].

Turning our attention to the decidable fragments of FO we mentioned earlier, it turns out that, although GFO is in many ways model-theoretically well-behaved [1], it lacks CIP [33]. Likewise, $\textrm{FO}^2$lacks CIP [23] and the same holds for $\textrm{C}^2$([35, Example 2] yields a counterexample). Both FF and FL lack CIP [7]. On the other hand, UNFO and GNFO have CIP [3, 22]. Figure 1 summarizes these known results. Note that we restrict attention to relational signatures without constant symbols and function symbols. Some of the results depend on this restriction. Other known results not reflected in Figure 1 (to avoid clutter) are that the intersection of GFO and $\textrm{FO}^2$(also known as $\textrm{GFO}^2$) has CIP [33]. Similarly, the intersection of FF with GFO and the intersection of FL with GFO (known as $\textrm{G}_\textrm{FF}$and $\textrm{G}_\textrm{FL}$, respectively) have CIP [7].

When a logic L lacks CIP, the question naturally arises as to whether there exists a more expressive logic $L'$ that has CIP. If such an $L'$ exists, then, in particular, interpolants for valid L-implications can be found in $L'$. This line of analysis is sometimes referred to as Repairing Interpolation [2]. If $L'$ is an FO-fragment, and our aim is to repair interpolation by extension, then there is a trivial solution: FO itself is an extension of L satisfying CIP. We will instead consider the following refinement of the question: can a natural extension $L'$ of L be identified which satisfies CIP while retaining decidability? We will answer this question for three of the fragments depicted in Figure 1 that lack CIP, by identifying the minimal natural extension $L'$ of L satisfying CIP. Our main results can be stated informally as follows:

• 1. The smallest logic extending GFO that has CIP is GNFO.

• 2. The smallest logic extending $\textrm{FO}^2$that has CIP is FO, and no decidable extension of $\textrm{FO}^2$has CIP.

• 3. The smallest logic extending FF that has CIP is FO, and no decidable extension of FL has CIP.

The precise statements of these results will be given in the respective sections. They involve some natural closure assumptions on the logics in question, and, for the undecidability results, some assumptions regarding the effective computability of the translation between the extension and the logic that it extends.

These results give us a clear sense of where, in the larger landscape of decidable fragments of FO, we may find logics that enjoy CIP. What makes the above results remarkable is that, from the definition of the Craig interpolation property, it doesn’t appear to follow that a logic without CIP would have a unique minimal extension with CIP. Note that a valid implication may have many possible interpolants, and the Craig interpolation property merely requires the existence of one such interpolant. Nevertheless, the above results show that, in the case $\textrm{FO}^2$, GFO, and FF, such a unique minimal extension indeed exists (assuming suitable closure properties, which will be spelled out in detail in the next sections).

Related Work. Several other approaches have been proposed for dealing with logics that lack CIP. One approach is to weaken CIP. For example, it was shown in [33] that GFO satisfies a weak, “modal” form of Craig interpolation, where, roughly speaking, only the relation symbols that occur in non-guard positions in the interpolant are required to occur both in the premise and the conclusion. As it turns out, this weakening of CIP is strong enough to entail the (non-projective) Beth Definability Property, which is one important use case of CIP. See also Section 7 for further discussion of weak forms of CIP.

Another recent approach [35] is to develop algorithms for testing whether an interpolant exists for a given entailment. That is, rather than viewing Craig interpolation as a property of logics, the existence of interpolants is studied as an algorithmic problem at the level of individual entailments. The interpolant existence problem turns out to be indeed decidable (although of higher complexity than the satisfiability problem) for both GFO and $\textrm{FO}^2$ [35].

Additional results are known for UNFO and GNFO beyond the fact that they have CIP. In particular, CIP holds for their fixed-point extensions [8, 9], interpolants can be constructed effectively, and tight bounds are known on the size of interpolants and the computational complexity of computing them [11].

Our paper can be viewed as an instance of abstract model theory for fragments of FO. One large driving force behind the development of abstract model theory was the identification of extensions of FO which satisfy desirable model-theoretic properties, such as the compactness theorem, the Löwenheim-Skolem, and Craig interpolation. One takeaway from this line of research is that CIP is scarce among many “reasonable” FO-extensions. An early result of Lindström showed that FO-extensions with finitely many generalized quantifiers and satisfying the downward Löwenheim-Skolem property do not have the Beth property (and hence fail to satisfy CIP) [38]. Similarly, Caicedo [17], generalizing an early result by Friedman [26], established a strong negative CIP result that applies to arbitrary proper FO-extensions with monadic generalized quantifiers. For a survey of negative interpolation results among FO-extensions, see [54]. These negative results not only show that CIP is scarce among extensions of FO, they also provide clues as to where, within the space of all extensions, one may hope to find logics with CIP. Our results can be viewed similarly, except that they pertain to (extensions of) fragments of FO.

Our results can also be appreciated as characterizations of GNFO and of FO. While traditional Lindström-style characterizations are maximality theorems (e.g., FO is a maximal logic having the compactness and Löwenheim-Skolem properties), our results can be viewed as minimality theorems (e.g., GNFO is the minimal logic extending GFO and having CIP).

Some prior work exists that studies abstract model theory for (extensions of) fragments of FO. Most closely related is [19], which studies modal logics and hybrid logics. Among other things, it was shown in [19] that the smallest extension of modal logic with the difference operator (ML(D)) which satisfies CIP is full first-order logic. Additionally, in [28], the authors identified minimal extensions of various fragments of propositional linear temporal logic (PLTL) with CIP. Furthermore, it was shown in [19] that every abstract logic extending GFO with CIP can express all FO sentences and formulas with one free variable, and is thus undecidable. A crucial difference between this result and ours is that [19] assumes signatures with constant symbols and concerns a stronger version of CIP, interpolating not only over relation symbols but also over constant symbols. In contrast, we only consider purely relational signatures without constant symbols. Other prior work on abstract model theory for fragments of FO are [13, 15, 27]. Repairing interpolation has also been pursued in the context of quantified modal logics, which typically lack CIP; in [2], the authors showed that CIP can be repaired for such logics by adding nominals, @-operators and the $\downarrow$-binder.

Outline. Section 2 introduces the abstract model-theoretic framework. In Sections 3, 4, and 5, we repair interpolation for $\textrm{FO}^2$, GFO, and FF, respectively. In Section 6, we provide results showing that, even with weak expressive assumptions, extensions of $\textrm{FO}^2$and FL with CIP are undecidable. In Section 7, we discuss the implications and limitations of our results, and future directions.

2 Preliminaries

We assume familiarity with the syntax and semantics of FO. Signatures are denoted by $\sigma$ and $\tau$, and are assumed to be relational and finite. If $\varphi$ contains only relation symbols occurring in $\sigma$, then we write $M, g \models \varphi$ to denote that a $\sigma$-structure M satisfies $\varphi$ under the variable assignment g. We write $x_i, y_i, z_i, u_i$ to denote variables, and $\overline{x}, \overline{y}, \overline{z}, \overline{u}$ to denote tuples of variables. We write $a_i,b_i,c_i$ to denote elements of structures and $\overline{a},\overline{b},\overline{c}$ to denote tuples of such elements. Given a tuple of elements $\overline{a} = a_1,\ldots ,a_n$ in a structure M, a tuple of variables $\overline{x} = x_1,\ldots ,x_n$, and a variable assignment g, we write $g[\overline{x} / \overline{a}]$ to denote the variable assignment which is the same as g except that $g(x_i) = a_i$ for each $i \le n$. In order to state our main results precisely, we must formally define what we mean by extensions $L'$ of L (where L is some fragment of FO that lacks CIP). One option is to let $L'$ range over fragments of FO that syntactically include L. However, as it turns out, our main results apply even to extensions that are not themselves contained in FO. We therefore opt, instead, to work with an abstract definition of logics, as typically used in abstract model theory.

Abstract Logics. An abstract logic (or logic) is a pair $(L,\models _L)$, where L is a map from relational signatures $\sigma$ to collections of formulas, and $\models _L$ is a ternary satisfaction relation. A formula of an abstract logic $(L,\models _L)$ is an element of $L(\sigma )$ for some finite relational signature $\sigma$. L must be monotone: if $\sigma \subseteq \tau$, then $L(\sigma ) \subseteq L(\tau )$. Each formula $\varphi$ has an associated finite set of free variables $\textrm{free}(\varphi )$, and we write $\varphi (\overline{x})$ or $\varphi (x_1,\dots ,x_k)$ to denote that the free variables of $\varphi$ are exactly those in the tuple $\overline{x} = x_1,\ldots ,x_k$. As in the case of FO, a formula $\varphi$ is a sentence if $\textrm{free}(\varphi ) = \emptyset$. We write $\textrm{sig}(\varphi )$ to denote the least signature $\sigma$ such that $\varphi \in L(\sigma )$. The ternary satisfaction relation $\models _L$ is defined over triples $(M,g,\varphi )$, where $\varphi$ is an L-formula, M is a $\tau$-structure such that $\textrm{sig}(\varphi ) \subseteq \tau$, and g is a variable assignment with $\textrm{free}(\varphi ) \subseteq \textrm{dom}(g)$; we write $M, g \models _L \varphi$ if this relation holds between these objects. The notions of logical consequence and logical equivalence for abstract logics are defined completely analogously to FO. In later sections, we will prefer to suppress the subscript L in the notation for the satisfaction relation and write L to denote an abstract logic $(L,\models _L)$. Furthermore, we often write $\varphi \in L$ rather than $\varphi \in L(\sigma )$, leaving the signature implicit.

All abstract logics L are assumed to satisfy the reduct property and the renaming property. The reduct property states that if $\sigma \subseteq \tau$, then for all $\varphi \in L(\sigma )$, all $\tau$-structures M, and all assignments g, if $M,g \models _L \varphi$, then $M \upharpoonright \sigma , g \models _L \varphi$. In other words, the truth of a formula of an abstract logic L in a structure depends only on the interpretations of the symbols in the signature of that formula. The renaming property states that if $\rho : \sigma \rightarrow \tau$ is an injective map preserving the arity of relation symbols, then for each formula $\varphi \in L(\sigma )$, there is a formula $\psi \in L(\tau )$ such that for all $\tau$-structures M, we have that $M, g \models _L \psi$ if and only if $\rho ^{-1}[M], g \models _L \varphi$, where $\rho ^{-1}[M]$ is the $\sigma$-structure with the same domain as M where, for each $R \in \sigma$, we have that $R^{\rho ^{-1}[M]} = \rho (R)^M$. Intuitively, the renaming property states that if a formula over a signature $\sigma$ can be expressed in a logic L, then the formula obtained by renaming all of its relation symbols can also be expressed in L.

For arbitrary abstract logics L, the Craig interpolation property states that if $\varphi \models _L \psi$ for L-formulas $\varphi$ and $\psi$, then there exists a formula $\vartheta \in L(\textrm{sig}(\varphi ) \cap \textrm{sig}(\psi ))$ with $\textrm{free}(\vartheta ) = \textrm{free}(\varphi ) \cap \textrm{free}(\psi )$ such that $\varphi \models _L \vartheta$ and $\vartheta \models _L \psi$.

We say a formula $\varphi$ of a logic L expresses a formula $\psi$ of a logic $L'$ if $\textrm{free}(\varphi ) = \textrm{free}(\psi )$, $\textrm{sig}(\varphi ) = \textrm{sig}(\psi )$, and for all structures M and assignments g, we have that $M, g \models _L \varphi$ if and only if $M, g \models _{L'} \psi$. We say that a logic $L'$ is an extension of a logic L (notation: $L \preceq L'$) if $L'$ can express all formulas of L. An FO-fragment can then be precisely defined, without reference to syntax, as a logic of which FO is an extension. We say that $L'$ is a sentential extension of L (notation: $L \preceq _{sent} L'$) if $L'$ can express all sentences of L.

Let L be a logic and $\psi (x_1,\ldots ,x_n)$ be an L-formula. We write $\llbracket \psi \rrbracket ^M$ for the collection of tuples $(a_1,\ldots ,a_n) \in M^n$ such that there exists an assignment g where $M, g \models \psi$ and $g(x_i) = a_i$ for each $i \le n$. Given formulas $\psi _1,\ldots ,\psi _k \in L(\sigma )$, a $\sigma$-structure M, and relation symbols $R_1,\ldots ,R_k \in \sigma$ with $|\textrm{free}(\psi _i) |= \textrm{arity}(R_i)$ for each $i \le k$, we define $M[R_1/\psi _1,\ldots ,R_k/\psi _k]$ to be the $\sigma$-structure with the same domain as M and such that $R_i^{M[R_1/\psi _1,\ldots ,R_k/\psi _k]} = \llbracket \psi _i \rrbracket ^M$ for each $i \le k$. We now describe a syntax-free notion of uniform substitution for formulas of an abstract logic.

Definition 2.1

Let L be a logic and $\varphi \in L(\sigma )$ with $R_1,\ldots ,R_k \in \textrm{sig}(\varphi )$, where for each $i \le k$, we have that $R_i$ is a $k_i$-ary relation symbol. Furthermore, let $\psi _1,\ldots ,\psi _k \in L(\sigma )$ be formulas with $|\textrm{free}(\psi _i) |= k_i$ for each $i \le k$. We say that L expresses the substitution of $\psi _1,\ldots ,\psi _k$ for $R_1,\ldots ,R_k$ in $\varphi$ if there exists a formula $\chi \in L(\sigma )$ such that, for every $\sigma$-structure M,

$$M, g \models \chi \iff M[R_1/\psi _1,\ldots ,R_k/\psi _k], g \models \varphi .$$

Most studies in abstract logic assume that the logics under study are regular, roughly meaning that they can express atomic formulas, Boolean connectives, and existential quantification. In other words, to study regular logics is to study extensions of FO. Since we are interested in a more fine-grained view of logics including FO-fragments, these assumptions are too strong. As a result, the first step of studying extensions of FO-fragments from the perspective of abstract logic is to identify natural expressive assumptions for those extensions which are strictly weaker than regularity. We do this in the respective sections.

Some of our proofs will use second-order quantification (for expository reasons only), and we recall the semantics of these quantifiers here. Given a formula $\varphi \in L(\sigma \cup \{P\})$ of some abstract logic L, we can form new formulas $\exists P \varphi$ and $\forall P \varphi$ with signature $\sigma$ and the same free variables as $\varphi$. Given a $\sigma$-structure M and an assignment g, the semantics of these formulas are defined as follows:

$$\begin{aligned} M,g \models \exists P \varphi ~~&\text {if there is a}~ \sigma \cup \{P\}\text {-expansion}~ M' ~\text {of}~ M \\ &\text {such that}~ M', g \models \varphi , ~\text {and} \\ M,g \models \forall P \varphi ~~&\text {if for all}~ \sigma \cup \{P\}\text {-expansions}~ M' ~\text {of}~ M, \\ &\text {we have that}~ M', g \models \varphi . \end{aligned}$$

If L itself does not allow second-order quantification, we can view $\exists P \varphi$ and $\forall P \varphi$ as elements of $L'(\sigma )$ for a suitable extension $L'$ of L. In particular, if $\varphi$ is an FO-formula, then $\exists P \varphi$ and $\forall P \varphi$ are formulas of second-order logic (SO).

3 Repairing Interpolation for $\textrm{FO}^2$

The two-variable fragment ($\textrm{FO}^2$) consists of all FO-formulas containing only two variables, say, x and y, where we allow for nested quantifiers that reuse the same variable (as in $\exists xy (R(x,y)\wedge \exists x(R(y,x)))$, expressing the existence of a path of length 2). In this context, as is customary, we restrict attention to relations of arity at most 2. It is known that $\textrm{FO}^2$is decidable [42] but does not have CIP [23].

3.1 Natural Extensions of $\textrm{FO}^2$

While $\textrm{FO}^2$is restricted to only two variables and predicates of arity as most 2, it has no restriction on its connectives: it is fully closed under Boolean connectives and existential and universal quantification. Because of this fact, we will consider in this section those abstract logics which are strong extensions of $\textrm{FO}^2$.

Definition 3.1

We say that a logic $L'$ strongly extends a logic L if $L'$ extends L and, for each formula $\varphi \in L'$ with $R_1,\ldots ,R_k \in \textrm{sig}(\varphi )$, where $\varphi$ expresses some $\psi \in L$, and all formulas $\psi _1,\ldots ,\psi _k \in L'$, we have that $L'$ expresses the substitution of $\psi _1,\ldots ,\psi _k$ for $R_1,\ldots ,R_k$ in $\varphi$ (cf. Definition 2.1).

Intuitively, Definition 3.1 means that $L'$ can express uniform substitutions of its formulas into formulas of L. In other words, the notion of a strong extension is a syntax-free way to say that $L'$ extends L and is closed under the connectives of L. In particular, if L strongly extends $\textrm{FO}^2$, then L can express all of the usual first-order connectives: for $\psi _0$ and $\psi _1$ expressible in L, it must also be the case that $\lnot \psi _0$, $\psi _0 \wedge \psi _1$, and $\exists x \psi _0$ are expressible in L, under the usual semantics of these connectives. Clearly $\textrm{FO}^2$is the smallest strong extension of itself.

3.2 Finding the Minimal Extension of $\textrm{FO}^2$with CIP

Recall that we write $L \preceq _{sent} L'$ if every sentence of L is expressible in $L'$. Our main result in this section is the following.

Theorem 3.1

If L is a strong extension of $\textrm{FO}^2$with CIP, then $\textrm{FO} \preceq _{sent} L$.

Proof

We will show by induction on the complexity of formulas that, for every $\textrm{FO}$-formula $\varphi (x_1 \ldots , x_n)$ there is a sentence $\psi \in L$ over an extended signature containing additional unary predicates $P_1, \ldots , P_n$, that is equivalent to

$$\exists x_1\ldots x_n(\big (\!\!\!\bigwedge _{i=1\ldots n}\!\!\! P_i(x_i)\wedge \forall y(P_i(y)\rightarrow y=x_i)\big )\wedge \varphi (x_1, \ldots , x_n)).$$

In other words, $\psi$ is a sentence expressing that $\varphi$ holds under an assignment of its free variables to some tuple of elements which uniquely satisfy the $P_i$ predicates. In the case that $n=0$ (i.e., the case that $\varphi$ is a sentence), we then have that $\psi$ is equivalent to $\varphi$, which shows that $FO\preceq _{sent} L$.

The base case of the induction is straightforward (recall that we restrict attention to relations of arity at most 2). The induction step for the Boolean connectives is straightforward as well (using the fact that L is a strong extension of $\textrm{FO}^2$, and thus can express all connectives of $\textrm{FO}^2$). In fact, the only non-trivial part of the argument is the induction step for the existential quantifier. Let $\varphi (x_1,\ldots ,x_n)$ be of the form $\exists x_{n+1} \varphi '(x_1.\ldots ,x_n,x_{n+1})$. By the inductive hypothesis, there is an L-sentence $\psi$ with $\textrm{sig}(\psi ) = \textrm{sig}(\varphi ') \cup \{P_1,\ldots ,P_{n+1}\}$, where $P_1,\ldots ,P_{n+1}$ are unary predicates not in $\textrm{sig}(\varphi ')$, which is equivalent to

$$\exists x_1\ldots x_n\exists x_{n+1}(\big (\!\!\!\bigwedge _{i \le n+1}\!\!\! P_i(x_i)\wedge \forall y(P_i(y)\rightarrow y=x_i)\big )\wedge \varphi '(x_1, \ldots , x_n,x_{n+1})).$$

Now, let $\psi '$ be obtained from $\psi$ by replacing every occurrence of $P_{n+1}$ by $P'$ for some fresh unary predicate $P'$; this is expressible in L by the renaming property. Furthermore, let

$$ \begin{array}{ll} \gamma (x) &{}:= \psi \wedge P_{n+1}(x), ~\text {and}\\[2mm] \chi (x) &{}:= (P'(x)\wedge \forall y(P'(y)\rightarrow y=x)) \rightarrow \psi '. \end{array} $$

(where x is either of the two variables we have at our disposal; it does not matter which). Since L strongly extends $\textrm{FO}^2$, both can be written as an L-formula. Then

$$\gamma (x) \models \chi (x).$$

Let $\vartheta (x)\in L$ be an interpolant. Observe that since $P_{n+1}$ occurs only in $\gamma (x)$ and $P'$ only in $\chi (x)$, the following second-order entailment is also valid:

$$\exists P_{n+1}\gamma (x) \models \vartheta (x) \models \forall P' \chi (x).$$

It is not hard to see that $\exists P_{n+1} \gamma (x)$ and $\forall P' \chi (x)$ are equivalent. Indeed, both are satisfied in a structure M under an assignment g precisely if $M',g\models \varphi$, where $M'$ is the expansion of M in which $P_{n+1}$ denotes the singleton set $\{g(x_{n+1})\}$. It then follows that $\vartheta (x)$, being sandwiched between the two, is also equivalent to $\exists P_{n+1} \gamma (x)$. This implies that $\vartheta (x)$ is the unique interpolant (up to logical equivalence) of the entailment $\gamma (x) \models \chi (x)$, and so it is expressible in L. Then since L strongly extends $\textrm{FO}^2$, it can express $\exists x \vartheta (x)$. We claim that this sentence satisfies the requirement of our claim. To see this, observe that $\exists x \vartheta (x)$ is equivalent to $\exists x \exists P_{n+1} \gamma (x)$, which is equivalent to $\exists P_{n+1} \psi$, which clearly satisfies the requirement of our claim.    $\square$

4 Repairing Interpolation for GFO

The guarded fragment (GFO) [1] allows formulas in which all quantifiers are “guarded.” Formally, a guard for a formula $\varphi$ is an atomic formula $\alpha$ whose free variables include all free variables of $\varphi$. Following [30], we allow $\alpha$ to be an equality. More generally, by an $\exists$-guard for $\varphi$, we will mean a possibly-existentially-quantified atomic formula $\exists \overline{x}\beta$ whose free variables include all free variables of $\varphi$. The formulas of GFO are generated by the following grammar:

$$\varphi := \top \mid R(\overline{x}) \mid x = y \mid \varphi \wedge \psi \mid \varphi \vee \psi \mid \lnot \varphi \mid \exists \overline{x} (\alpha \wedge \varphi ),$$

where, in the last clause, $\alpha$ is a guard for $\varphi$. Note again that we do not allow constants and function symbols.

In the guarded-negation fragment (GNFO) [4], arbitrary existential quantification is allowed, but every negation is required to be guarded. More precisely, the formulas of GNFO are generated by the following grammar:

$$\varphi := \top \mid R(\overline{x}) \mid x = y \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \exists x \varphi \mid \alpha \wedge \lnot \varphi ,$$

where, in the last clause, $\alpha$ is a guard for $\varphi$.

As is customary, the above definitions are phrased in terms of ordinary guards $\alpha$. However, it is easy to see that if we allow for $\exists$-guards, this would not affect the expressive power (or computational complexity) of these logics in any way. This is because, when the variables in the tuple $\overline{x}$ do not occur free in $\varphi$, as is the case when $\exists \overline{x} \beta$ is an $\exists$-guard for $\varphi$, then we can write $\exists \overline{x}\beta \wedge \varphi$ equivalently as $\exists \overline{x}(\beta \wedge \varphi )$. In other words, an $\exists$-guard is as good as an ordinary guard. We call an FO-formula self-guarded if it is either a sentence or it is of the form $\alpha \wedge \varphi$ where $\alpha$ is an $\exists$-guard for $\varphi$.

In this section, we will require the notions of conjunctive queries (CQs) and unions of conjunctive queries (UCQs). A CQ is an FO-formula of the form

$$\varphi (x_1, \dots , x_n) := \exists y_1 \dots \exists y_m (\bigwedge _{i \in I} \alpha _i),$$

where each $\alpha _i$ is an atomic relation, possibly an equality, whose free variables are among $\{x_1, \dots , x_n, y_1, \dots , y_m\}$. The collection of all CQs is expressively equivalent to the fragment $\textrm{FO}_{\exists ,\wedge }$of first-order logic, which is generated by the following grammar:

$$\varphi := R(x_1, \dots , x_k) \mid x = y \mid \varphi \wedge \varphi \mid \exists x \varphi .$$

A UCQ is a finite disjunction of CQs. Importantly, GNFO can be alternatively characterized as the smallest logic which can express every UCQ and is closed under guarded negation [4]. This is made explicit in the following expressively equivalent grammar for GNFO:

$$\varphi := \top \mid R(\overline{x}) \mid x = y \mid \alpha \wedge \lnot \varphi \mid q[R_1 / \varphi _1, \dots , R_n / \varphi _n],$$

where q is a UCQ with relation symbols $R_1, \dots , R_n$ and $\varphi _1, \dots , \varphi _n$ are self-guarded formulas with the appropriate number of free variables and generated by the same recursive grammar. We refer to this as the UCQ syntax for GNFO.

4.1 Natural Extensions of GFO

Unlike $\textrm{FO}^2$, guarded fragments are peculiar in that they are not closed under substitution. For example, $\exists xy(R(x,y)\wedge \lnot S(x,y))$ belongs to GFO, but if we substitute $x=x \wedge y=y$ for R(x, y), we obtain $\exists xy(x=x\wedge y=y\wedge \lnot S(x,y))$, which does not belong to GFO (and is not even expressible in GNFO). GFO and GNFO are, however, closed under self-guarded substitution: we can uniformly substitute self-guarded formulas for atomic relations. We generalize the notion of a self-guarded formula to abstract logics L as follows: a formula $\varphi (\overline{x}) \in L(\sigma )$ with $\textrm{free}(\varphi ) = \{x_1,\ldots ,x_k\}$ is self-guarded if there is a n-ary relation symbol $G \in \sigma$, where $n \ge k$, and a tuple of variables $\overline{y}$ containing exactly the variables $\textrm{free}(\varphi ) \cup \{z_1,\ldots ,z_m\}$, such that for all $\sigma$-structures M and assignments g,

$$M, g \models \varphi \implies M, g \models \exists z_1 \ldots \exists z_m G(\overline{y}).$$

Intuitively, we can think of a self-guarded L-formula as a conjunction of the form $\alpha \wedge \psi$, where $\alpha$ is an $\exists$-guard for $\psi$. We can then capture the notion of self-guarded substitution for abstract logics by the following definition.

Definition 4.1

We say that an abstract logic L expresses self-guarded substitutions if, for each formula $\varphi \in L$ with $R_1,\ldots ,R_k \in \textrm{sig}(\varphi )$, and all self-guarded formulas $\psi _1,\ldots ,\psi _k \in L$, we have that L can express the substitution of $\psi _1,\ldots ,\psi _k$ for $R_1,\ldots ,R_k$ in $\varphi$ (cf. Definition 2.1).

It was shown in [4] that every self-guarded GFO-formula is expressible in GNFO. In particular, this applies to all GFO-sentences and GFO-formulas with at most one free variable (since all such formulas can be equivalently written as $x=x \wedge \varphi$). It is therefore common to treat GNFO as an extension of GFO. To make this precise, we say that $L'$ is a self-guarded extension of L if $L'$ can express all self-guarded formulas of L (notation: $L \preceq _{sg} L'$). In Figure 1, the line marked (*) indicates that GNFO extends GFO in this weaker sense. Furthermore, it is worth noting that GNFO is also not closed under implication, while GFO is. If it were, then GNFO would be able to express full negation (using formulas of the form $\varphi \rightarrow \bot$). However, GFO and GNFO both have disjunction and conjunction in common. We formalize all of these considerations into the following notion.

Definition 4.2

A guarded logic is a logic L such that

• 1. $\textrm{GFO} \preceq _{sg} L$,

• 2. L expresses self-guarded substitutions, and

• 3. L expresses conjunction and disjunction.

Clearly, GFO and GNFO are both guarded logics. Furthermore, observe that the smallest guarded logic consists of all conjunctions and disjunctions of self-guarded formulas of GFO.

4.2 Finding the Minimal Extension of GFO with CIP

Our main result in this section is the following.

Theorem 4.1

Let L be a guarded logic with CIP. Then $\textrm{GNFO} \preceq L$.

In other words, loosely speaking, GNFO is the smallest extension of GFO with CIP. It is based on similar ideas as the proof of Theorem 3.1, but the argument is more intricate. The main thrust of the argument will be to show that our abstract logic L can express all positive existential formulas, from which it will follow easily that L is able to express all formulas in the UCQ syntax for GNFO. Toward this end, the main technical result is the following proposition.

Proposition 4.1

Let L be a logic with CIP that can express atomic formulas, guarded quantification, conjunction, and unary implication. Then $\textrm{FO}_{\exists ,\wedge } \preceq L$.

Here, we say that a logic L can express guarded quantification if, whenever $\varphi \in L$ and $\alpha$ is a guard for $\varphi$, L can express $\exists \overline{x} (\alpha \wedge \varphi )$; we say that L can express unary implications if, whenever $\varphi \in L$ and $\alpha$ is an atomic formula with only one free variable, L can express $\alpha \rightarrow \varphi$.

The following definition is used in the proof of Proposition 4.1.

Definition 4.3

Let $\varphi$ be a formula in $\textrm{FO}_{\exists ,\wedge }$, let $\overline{y} = y_1, \dots , y_n$ be a tuple of distinct variables, and let $\overline{P}=P_1, \dots , P_n$ be a tuple of unary predicates of the same length. Then $\textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\varphi )$ is defined recursively as follows:

$$\begin{array}{ll} \textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\alpha ) &{}= \exists \overline{y} (\alpha \wedge \bigwedge _{1\le i\le n}P_i(y_i)) \\ \textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\phi \wedge \psi ) &{}= \textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\phi ) \wedge \textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\psi ) \\ \textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\exists z \psi ) &{}= \exists z (\textsf {BIND}_{\overline{y}\mapsto \overline{P}}(\psi )), \end{array}$$

where $\alpha$ is an atomic formula (possibly an equality).

The $\textsf {BIND}_{\overline{y}\rightarrow \overline{P}}$ operation applied to a formula $\varphi \in \textrm{FO}_{\exists ,\wedge }$ wraps each atomic subformula of $\varphi$ with quantifiers for the variables in $\overline{y}$, and adds additional unary predicates for these variables. Thus, the free variables of $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi )$, for $\overline{y}=y_1,\dots ,y_n$, are exactly $\textrm{free}(\varphi )\setminus \{y_1, \dots , y_n\}$, which justifies our use of the word “BIND”. The utility of this definition is due to the following fact: for any $\varphi \in \textrm{FO}_{\exists ,\wedge }$, whenever $M, g \models \textsf {BIND}_{\overline{y}\rightarrow \overline{P}}(\varphi )$, and the interpretation in M of each unary predicate $P_i$ in $\overline{P}$ is a singleton, then $M, g' \models \varphi$, where $g'$ is the extension of g which maps each $y_i$ to the unique element satisfying $P_i$ (cf. Propositions 4.3, 4.4). The following proposition is a simple consequence of the definition of $\textsf {BIND}$.

Proposition 4.2

For all $\textrm{FO}_{\exists ,\wedge }$-formulas $\varphi$ and for all $\overline{x}, \overline{y}$ and $\overline{P},\overline{Q}$, if $\overline{x}$ and $\overline{y}$ are disjoint, then $\textsf {BIND}_{\overline{xy} \mapsto \overline{PQ}}(\varphi ) \equiv \textsf {BIND}_{\overline{x} \mapsto \overline{P}}(\textsf {BIND}_{\overline{y} \mapsto \overline{Q}}(\varphi ))$.

A formula $\varphi$ is clean if no free variable of $\varphi$ also occurs bound in $\varphi$, and $\varphi$ does not contain two quantifiers for the same variable. Every FO-formula is equivalent to a clean FO-formula, and all subformulas of a clean formula are also clean. We now state two technical propositions, whose proofs can be found in the full version of this paper [20].

Proposition 4.3

For every clean $\textrm{FO}_{\exists ,\wedge }$-formula $\varphi$, for every tuple of distinct variables $\overline{y}=y_1, \dots , y_n$ (with each $y_i\in \textrm{free}(\varphi )$), and for every tuple of unary predicates $\overline{P}=P_1,\ldots ,P_n$, we have that

$$\big (\bigwedge _{i=1,\ldots ,n} P_i(y_i)\big )\models \varphi \rightarrow \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi ).$$

Proposition 4.4

For every clean $\textrm{FO}_{\exists ,\wedge }$-formula $\varphi (x,\overline{y})$ with $\overline{y}=y_1, \ldots , y_n$ distinct from x, and for every n-tuple of unary predicates $\overline{P}=P_1, \ldots , P_n$ not occurring in $\varphi$, we have that

$$\exists x\varphi (x,\overline{y}) \equiv \forall \overline{P}\Big (\big (\bigwedge _{i=1\ldots n} P_i(y_i)\big ) \rightarrow \exists x \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi (x,\overline{y}))\Big ).$$

The following lemma enables the proof of Proposition 4.1.

Lemma 4.1

Let L be an FO-fragment which can express atomic formulas and is closed under guarded quantification, conjunction, and unary implication. If L can express a formula $\varphi \in \textrm{FO}_{\exists ,\wedge }$ and all of its subformulas, then for all tuples $\overline{y}$ of variables, we have that L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi )$.

Proof

We show by strong induction on the complexity of clean $\textrm{FO}_{\exists ,\wedge }$-formulas $\varphi$ that this proposition holds.

Base Case

Suppose $\varphi$ is an atomic formula. Fix an arbitrary tuple $\overline{y}=y_1 \ldots , y_n$. Then

$$\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi ) \equiv \exists \overline{y} (\varphi \wedge \bigwedge _{1\le i\le n} P_i(y_i)),$$

which L can express by closure under conjunction and guarded quantification.

Inductive Step

Suppose inductively that, for all formulas $\psi$ of lesser complexity than $\varphi$, and all tuples $\overline{z}$ of variables, we have that L can express $\textsf {BIND}_{\overline{z} \mapsto \overline{P}}(\psi )$. Fix an arbitrary tuple $\overline{y}$ of variables.

Suppose that $\varphi = \psi _1 \wedge \psi _2$. Since L can express $\varphi$ and all of its subformulas, it can also express $\psi _1$, $\psi _2$, and all of their subformulas. Then by the inductive hypothesis, L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi _1)$ and $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi _2)$. Then by closure under conjunctions, L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi _1) \wedge \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi _2)$, which is the same as $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi )$ (cf. Definition 4.3).

Now suppose that $\varphi (\overline{x},\overline{y}) = \exists z \psi (\overline{x},\overline{y},z)$, where the (possibly empty) tuple $\overline{x}$ consists of all free variables of $\varphi$ not in the tuple $\overline{y}$. We need to show that L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\varphi (\overline{x},\overline{y}))$, which is the same as $\exists z (\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi (\overline{x},\overline{y},z)))$ (cf. Definition 4.3). Since L can express $\varphi$ and all of its subformulas, it can also express $\psi$ and all of its subformulas. Then, by the inductive hypothesis, L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$, whose free variables are those in the tuple $\overline{x}z$, as well as $\textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi )$, whose only free variable is z. Since L is closed under conjunction and guarded quantification, it follows that L can express

$$\gamma (\overline{x}) :=\exists z (G(\overline{x},z) \wedge \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )) \,\,\,\,\,\text {and}\,\,\,\,\, \exists z (z=z \wedge \textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi )),$$

where G is a fresh relation symbol not occurring in $\psi$. Then by closure under unary implications, we have that L can also express

$$\chi (\overline{x}) := \big (\bigwedge _{i} Q_i(x_i)\big ) \rightarrow \exists z (z=z \wedge \textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi )).$$

Claim: $\gamma (\overline{x})\models \chi (\overline{x})$

Proof of claim: By Proposition 4.2,

$$\begin{aligned} \textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi ) \equiv \textsf {BIND}_{\overline{x} \mapsto \overline{Q}}(\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )). \end{aligned}$$

(1)

Then by applying Proposition 4.3 and inverting the hypotheses, we have

$$\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi ) \models \big (\bigwedge _{i} Q_i(x_i)\big ) \rightarrow \textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi ).$$

From this, it follows (because z is distinct from $x_i$ variables) that

$$\exists z(\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )) \models \big (\bigwedge _{i} Q_i(x_i)\big ) \rightarrow \exists z\textsf {BIND}_{\overline{xy} \mapsto \overline{QP}}(\psi ),$$

and therefore $\gamma (\overline{x})\models \chi (\overline{x})$. This concludes the proof of the claim.

Since L can express both $\gamma (\overline{x})$ and $\chi (\overline{x})$, we have by the Craig interpolation property that L can express some Craig interpolant $\vartheta (\overline{x})$. Since G and the $Q_i$ predicates do not occur in $\varphi$, they do not occur in $\vartheta (\overline{x})$, and therefore, the following second-order implication is valid:

$$\exists G \gamma (\overline{x}) \models \vartheta (\overline{x}) \models \forall \overline{Q} \chi (\overline{x}).$$

It is easy to see that $\exists G \gamma (\overline{x}) \equiv \exists z \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$. Similarly, it follows from Proposition 4.4 and equation (1) that $\forall \overline{Q} \chi (\overline{x}) \equiv \exists z \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$. Therefore, $\vartheta (\overline{x}) \equiv \exists z \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$. In particular, $\exists z \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$ is expressible in L.    $\square$

We are now ready to prove Proposition 4.1, restated below.

Proposition 4.1. Let L be a logic with CIP that can express atomic formulas, guarded quantification, conjunction, and unary implication. Then $\textrm{FO}_{\exists ,\wedge } \preceq L$.

Proof

By strong induction on the complexity of $\textrm{FO}_{\exists ,\wedge }$-formulas. The base case is immediate, since L can express all atomic formulas. For the inductive step, if $\varphi := \psi _1 \wedge \psi _2$, then by the inductive hypothesis, L can express $\psi _1$ and $\psi _2$, and so by closure under conjunction, L can express $\varphi$. Now suppose $\varphi (\overline{y}) := \exists x(\psi (x,\overline{y}))$. By the inductive hypothesis, together with closure under guarded quantification, L can express

$$\begin{aligned} \gamma (\overline{y}) := \exists x (G(x, \overline{y}) \wedge \psi ). \end{aligned}$$

Furthermore, by Lemma 4.1, L can express $\textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$, and therefore, by closure under guarded quantification and unary implications, L can express

$$\begin{aligned} \chi (\overline{y}) := \big (\bigwedge _{i} P_i(y_i)\big ) \rightarrow \exists x(x=x\wedge \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )). \end{aligned}$$

Claim: $\gamma (\overline{y}) \models \chi (\overline{y})$.

Proof of claim: It is clear that $\gamma (\overline{y})\models \exists x \psi$. Furthermore, by Proposition 4.3, $\psi \models \big (\bigwedge _{i} P_i(y_i)\big ) \mapsto \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )$, from which it follows that $\exists x \psi \models \chi (\overline{y})$ (since the variable x is distinct from $y_1, \ldots , y_n$). Therefore, $\gamma (\overline{y}) \models \chi (\overline{y})$.

Let $\vartheta (\overline{y})$ be an interpolant for $\gamma (\overline{y}) \models \chi (\overline{y})$ in L. Since G and the predicates in $\overline{P}$ do not occur in $\psi$, the following second-order entailments are valid:

$$\exists G \exists x (G(x, \overline{y}) \wedge \psi ) \models \vartheta (\overline{y}) \models \forall \overline{P} ((\bigwedge _{i} P_i(y_i)) \rightarrow \exists x \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )).$$

It is easy to see that

$$\exists G \exists x (G(x, \overline{y}) \wedge \psi ) \equiv \exists x \psi .$$

Furthermore, by Proposition 4.4,

$$\psi \equiv \forall \overline{P} ((\bigwedge _{i} P_i(y_i)) \rightarrow \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )).$$

from which it follows (since x is distinct from $y_1, \ldots , y_n$) that

$$\exists x \psi \equiv \forall \overline{P} ((\bigwedge _{i} P_i(y_i)) \rightarrow \exists x \textsf {BIND}_{\overline{y} \mapsto \overline{P}}(\psi )).$$

Therefore, $\vartheta (\overline{y}) \equiv \varphi (\overline{y})$, and so we are done.    $\square$

Our main result follows easily from Proposition 4.1, the closure properties of guarded logics, and the UCQ characterization of GNFO.

Theorem 4.1. Let L be a guarded logic with CIP. Then $\textrm{GNFO} \preceq L$.

Proof

L can express self-guarded GFO-formulas, so it can express formulas of the form $\exists \overline{x} \beta$, where $\beta$ is an atomic formula. Then since L can express self-guarded substitution, L can express guarded quantification. Furthermore, L can express all self-guarded formulas of the form $\alpha \wedge \lnot \beta$, where $\alpha$ and $\beta$ are atomic formulas such that $\textrm{free}(\alpha ) = \textrm{free}(\beta )$. Furthermore, for every formula $\varphi$ expressible in L with $\textrm{free}(\varphi ) \subseteq \textrm{free}(\alpha )$, $\alpha \wedge \varphi$ is a self-guarded formula. Thus by expressibility of self-guarded substitution, L can also express $\alpha \wedge \lnot (\alpha \wedge \varphi )$, which is equivalent to $\alpha \wedge \lnot \varphi$; hence L can express guarded negation. If L can express $\varphi$, then by expressibility of guarded negation and disjunction, it can also express the formula $(x=x \wedge \lnot P(x)) \vee \varphi$, which is equivalent to $P(x) \rightarrow \varphi$. Hence L can express unary implications. Therefore, by Proposition 4.1, L can express all formulas in $\textrm{FO}_{\exists ,\wedge }$. Then by expressibility of disjunction, L can express all unions of conjunctive queries. The result then follows immediately from the UCQ-syntax for GNFO, by closure under self-guarded substitution.    $\square$

5 Repairing Interpolation for FF

The fluted fragment (FL) [51] is an ordered logic, in which all occurrences of variables in atomic formulas and quantifiers must follow a fixed order. In the context of ordered logics, we assume a fixed infinite sequence of variables $X = \langle x_i \rangle _{i \in \mathbb {Z}^+}$. A suffix n-atom is an atomic formula of the form $R(x_j,\dots ,x_n)$, where $x_j, \dots , x_n$ is a finite contiguous subsequence of X. FL is defined by the following recursion.

Definition 5.1

For each $n \in \mathbb {N}$, define collections of formulas $\textrm{FL} ^n$ as follows:

• 1. $\textrm{FL} ^n$ contains all suffix n-atoms,

• 2. $\textrm{FL} ^n$ is closed under Boolean combinations, and

• 3. If $\varphi$ is in $\textrm{FL} ^{n+1}$, then $\exists x_{n+1} \varphi$ and $\forall x_{n+1} \varphi$ are in $\textrm{FL} ^n$.

We set $\textrm{FL} = \bigcup _{n \in \mathbb {N}} \textrm{FL} ^n$.

The forward fragment (FF), introduced in [6], is a syntactic generalization of FL. We say that $R(x_j,\dots ,x_k)$ is an infix n-atom if $x_j, \dots , x_n$ is a finite contiguous subsequence of X and $k \le n$. FF is defined by the following recursion.

Definition 5.2

For each $n \in \mathbb {N}$, define collections of formulas $\textrm{FF} ^n$ as follows:

• 1. $\textrm{FF} ^n$ contains all infix n-atoms,

• 2. $\textrm{FF} ^n$ is closed under Boolean combinations, and

• 3. If $\varphi$ is in $\textrm{FF} ^{n+1}$, then $\exists x_{n+1} \varphi$ and $\forall x_{n+1} \varphi$ are in $\textrm{FF} ^n$.

We set $\textrm{FF} = \bigcup _{n \in \mathbb {N}} \textrm{FF} ^n$.

In contrast to the other logics we have seen, FL and FF do not allow the primitive equality symbol. It can be seen by a simple formula induction that every formula in $\textrm{FF} ^k$ can be expressed by a formula in $\textrm{FF} ^n$ for every $n > k$; it follows easily that FF can express arbitrary Boolean combinations of its formulas. However, FL cannot: $P(x_1)$ and $P(x_2)$ are in $\textrm{FL}$, but $P(x_1) \wedge P(x_2)$ is not expressible in FL. Although FF contains formulas which are not in FL, it is known that FF and FL are expressively equivalent at the level of sentences [7]. Furthermore, the satisfiability problems for FL and FF are decidable [7, 48].

5.1 Natural Extensions of FF

Given a formula $\varphi$, we write $gfv(\varphi )$ to denote the greatest $n \in \mathbb {Z}^+$ such that $x_n$ occurs free in $\varphi$; if $\varphi$ is a sentence, then we set $gfv(\varphi ) = 0$. We define forward logics to capture the notion of a natural extension of FF.

Definition 5.3

A forward logic is an abstract logic L such that

• 1. L can express all infix n-atoms for every $n \in \mathbb {Z}^+$,

• 2. L can express all Boolean combinations of its formulas, and

• 3. L can express $\exists x_n \varphi$ and $\forall x_n \varphi$ whenever L can express $\varphi$ and $n = gfv(\varphi )$.

We refer to the last property of a forward logic as expressibility of ordered quantification. Clearly FF is a forward logic, and every forward logic extends FF.

5.2 Finding the Minimal Extension of FF with CIP

Unlike the other fragments we have seen, one peculiar property of FF is that the logic is not closed under variable substitutions. This can be seen simply by considering relational atoms: for a 3-ary relational symbol R, the formula $R(x_1,x_2,x_3)$ is in FF, but the formula $R(x_3,x_1,x_2)$ is not. Before proving our main theorem, we prove the following lemma asserting that whenever a formula is expressible in a forward logic L satisfying CIP, the result of making arbitrary substitutions for the free variables of the formula is also expressible in L.

Lemma 5.1

Let L be a forward logic satisfying CIP, and let $\varphi (x_{i_1}, \dots , x_{i_k})$ be a formula of first-order logic expressible in L, where $x_{i_1}, \dots , x_{i_k}$ is not necessarily a contiguous subsequence of variables. Then for every map

$$\pi : \{i_1,\dots ,i_k\} \rightarrow \mathbb {Z}^+,$$

we have that L can also express $\varphi (x_{\pi (i_1)}, \dots , x_{\pi (i_k)})$. In other words, L is closed under renamings of free variables.

Proof

For brevity, let $\overline{x} = x_{i_1}, \dots , x_{i_k}$, and let $\pi (\overline{x}) = x_{\pi (i_1)}, \dots , x_{\pi (i_k)}$. Without loss of generality, assume that $i_1 \le \dots \le i_k$ (we can do this since the notation $\varphi (x_{i_1}, \dots , x_{i_k})$ only indicates that the variables occur free, but says nothing about where or in what order they occur in the formula). Since L can express $\varphi (\overline{x})$, it can evidently express the following formulas, by the definition of a forward logic:

$$\begin{aligned} \gamma (\overline{x}) &:= \bigwedge _{m \le k} G_m(x_{i_m}) \wedge \forall x_{i_1} \dots \forall x_{i_k} \left( \bigwedge _{m \le k} G_m(x_{\pi (i_m)}) \rightarrow \varphi (\overline{x}) \right) \\ \chi (\overline{x}) &:= \bigwedge _{m \le k} P_m(x_{i_m}) \rightarrow \exists x_{i_1} \dots \exists x_{i_k} \left( \varphi (\overline{x}) \wedge \bigwedge _{m \le k} P_m(x_{\pi (i_m)}) \right) \end{aligned}$$

Clearly $\gamma \models \chi$, and so there exists an interpolant $\vartheta$. Hence

$$\exists G_1 \ldots G_k \gamma \models \vartheta \models \forall P_1 \ldots P_k \chi $$

is a valid second-order entailment. Furthermore, it is easy to see that

$$\exists G_1 \ldots G_k \gamma \equiv \forall P_1 \ldots P_k \chi \equiv \varphi .$$

Therefore, $\varphi (x_{\pi (i_1)}, \dots , x_{\pi (i_k)})$ is expressible in L.    $\square$

We now prove our main theorem, which follows easily from Lemma 5.1.

Theorem 5.1

Let L be a forward logic satisfying CIP. Then $\textrm{FO} \preceq L$.

Proof

We proceed by formula induction on FO-formulas $\varphi$. For the base case, clearly L can express all atomic FO-formulas by applying Lemma 5.1 to an appropriate infix atom. For the inductive step, the Boolean cases are immediate since L can express all Boolean combinations. Hence the only interesting case is when $\varphi := \exists x_k \psi$ for some formula $\psi$. By the inductive hypothesis, L can express $\psi$. Applying Lemma 5.1, L can also express $\varphi '$, the result of substituting $x_{n+1}$ for all free occurrences of $x_k$, where $n = gfv(\varphi )$, and leaving all other free variables the same. Then by expressibility of ordered quantification, L can express $\exists x_{n+1} \varphi '$, which is equivalent to $\varphi$.    $\square$

6 Undecidability of Extensions of $\textrm{FO}^2$and FL with CIP

In Section 3, we showed that every strong extension of $\textrm{FO}^2$with CIP can express all sentences of FO, and in Section 5, we showed that every forward logic with CIP can express all formulas of FO. These results suggest the undecidability of the satisfiability problems for such logics. In this section, we formalize this idea, showing that extensions of $\textrm{FO}^2$and FL with CIP and satisfying very limited expressive assumptions are undecidable. These results rely primarily on known results on the undecidability of $\textrm{FO}^2$and FL with additional transitive relations.

Proposition 6.1

Every abstract logic L with CIP extending $\textrm{FO}^2$or FL can express the following formulas:

$$\begin{aligned} \psi _0(x_1) &:= \forall x_2 \forall x_3 (R(x_1,x_2) \wedge R(x_2,x_3) \rightarrow R(x_1,x_3)), ~\text {and} \\ \psi _1 &:= \lnot \forall x_1 \forall x_2 \forall x_3 (R(x_1,x_2) \wedge R(x_2,x_3) \rightarrow R(x_1,x_3)). \end{aligned}$$

The proof of Proposition 6.1 can be found in the full version of this paper [20]. We also need two additional definitions. First, an effective translation from a logic L to a logic $L'$ is a computable function which takes formula of $\varphi \in L$ as input and outputs an equivalent formula $\varphi ' \in L'$. Second, we say that a logic L has effective conjunction if there is a computable function taking formulas $\varphi , \psi \in L$ as input and outputting a formula $\chi \in L$ which is equivalent to $\varphi \wedge \psi$.

Theorem 6.1

Let L be an extension of FL which satisfies CIP. Suppose further that there is an effective translation from FL to L, and L has effective conjunction. The satisfiability problem for L is undecidable if either

• 1. L can express ordered quantification, or

• 2. L can express negation.

Proof

Let $\chi$ be the sentence asserting the transitivity of the relation R. Since L has CIP and extends FL, it can express both $\psi _0(x_1)$ and $\psi _1$ by Proposition 6.1. If L can express ordered quantification, it can express $\forall x_1 \psi _0(x_1)$, which is equivalent to $\chi$. If L can express negation, then it can express $\lnot \psi _1$, which is also equivalent to $\chi$. Since L, as an abstract logic, can express $\chi$ and is closed under predicate renamings, it can express that any number of binary relations are transitive. Let $\chi _1$, $\chi _2$, and $\chi _3$ be sentences expressing transitivity of binary relation symbols $R_1$, $R_2$, and $R_3$, respectively. Let tr be an effective translation from FL to L. Then a formula $\varphi$ of FL with three designated transitive relations is satisfiable if and only if $tr(\varphi ) \wedge \chi _1 \wedge \chi _2 \wedge \chi _3$ is satisfiable. Since tr is computable and L is effectively closed under conjunction, this reduction is computable. Since the satisfiability problem for FL with three transitive relations is undecidable [46], the satisfiability problem for L is undecidable.    $\square$

It is also known that satisfiability is undecidable for $FO^2$-formulas with two transitive relations [36]. Using this fact, along with Proposition 6.1, we obtain the following theorem, by a similar proof to that of Theorem 6.1.

Theorem 6.2

Let L be an extension of $\textrm{FO}^2$which satisfies CIP. Suppose further that there is an effective translation from $\textrm{FO}^2$to L, and L has effective conjunction. The satisfiability problem for L is undecidable if either

• 1. L can express universal quantification, or

• 2. L can express negation.

We remark that all forward logics and strong extensions of $\textrm{FO}^2$with CIP, assuming appropriate effective translations and effective conjunction, meet the requirements of Theorems 6.1 and 6.2, and hence are undecidable.

7 Discussion

In the introduction, we mentioned several results indicating the failure of CIP among many natural proper extension of FO. In [14], van Benthem points out that there is a similar scarcity among FO-fragments as well. Our results in Sections 3 and 5 may be interpreted as additional confirmation of this observation. Furthermore, one tends to study proper fragments of FO for their desirable computational properties, and so our broader undecidability results show that CIP fails for large swaths of decidable FO-fragments. However, there are a few notable fragments for which the determination of a minimal extension satisfying CIP is still open, such as FL and the quantifier prefix fragments.

One limitation of our methodology and results is their dependence on a definition of Craig interpolation which mandates the existence of interpolants between proper formulas, while many practical applications only require CIP for sentences. Throughout this paper, we have established expressibility of a formula $\vartheta$ in a logic L by induction (and by constructing two formulas $\varphi$ and $\psi$ such that $\varphi \models \psi$ and arguing that every interpolant is equivalent to $\vartheta$). In general, this method is difficult to apply unless free variables are allowed; it is not clear how to apply this type of inductive argument if we were only concerned with the existence of interpolants for sentences of the logic.

There are several well-studied properties strictly weaker than CIP. The $\varDelta$-interpolation property (also known as Suslin-Kleene interpolation) holds for a logic L if, whenever $\varphi \models \psi$, and (intuitively speaking) there is only one possible interpolant $\vartheta$ up to logical equivalence for this entailment, then L contains a formula equivalent to $\vartheta$ [5]. It is not hard to see that, unlike the Craig interpolation property, every logic L has a unique extension, denoted $\varDelta (L)$, satisfying the $\varDelta$-interpolation property. In fact, in our proofs we only rely on $\varDelta$-interpolation; every application of the assumption that some abstract logic L satisfies CIP yields a provably unique interpolant, up to logical equivalence. Therefore, all of our results hold also when CIP is replaced by $\varDelta$-interpolation.

Two additional weakenings of CIP are the projective and non-projective Beth definability properties. The projective Beth property states, roughly, that whenever a $\sigma \cup \tau \cup \{R\}$-theory $\varSigma$ implicitly defines a relation R in terms of the relations in $\sigma$, then $\varSigma$ entails an explicit definition of R in terms of $\sigma$ (the non-projective Beth property being the special case for $\tau =\emptyset$). Many practical applications of CIP in database theory and knowledge representation require only the projective Beth property. It is not immediately clear how to extend our methodology to a systematic study of the (projective) Beth property among decidable FO-fragments. Indeed, GFO already satisfies the non-projective Beth property [33]. Given their applications, an interesting avenue of future work is to map the landscape of FO-fragments satisfying these properties. In the other direction, minimal extensions of logics with uniform interpolation (a strengthening of CIP) were studied in [25], although with limited results so far (cf. [25, Thm. 14]). Some of the minimal extensions of PLTL fragments with CIP identified in [28], however, do satisfy uniform interpolation.