Existential Fixed-Point Logic as a Fragment of Second-Order Logic

Abstract

The standard translation of existential fixed-point formulas into second-order logic produces strict universal formulas, that is, formulas consisting of universal quantifiers on relations (not functions) followed by an existential first-order formula. This form implies many of the pleasant properties of existential fixed-point logic, but not all. In particular, strict universal sentences can express some co-NP-complete properties of structures, whereas properties expressible by existential fixed-point formulas are always in P. We therefore investigate what additional syntactic properties, beyond strict universality, are enjoyed by the second-order translations of existential fixed-point formulas. In particular, do such syntactic properties account for polynomial-time model-checking?

To Yuri Gurevich, on the occasion of his $75\!{th}$ birthday.

Partially supported by NSF grant DMS-0653696

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In [3], Yuri Gurevich and I pointed out numerous pleasant properties of existential fixed-point logic ($\exists$FPL), the logic roughly described as first-order logic, minus universal quantification, plus the least-fixed-point operator for positive inductive definitions. (This and other concepts used in this introduction are explained in more detail in Sect. 2.) In that paper, we also showed that formulas of existential fixed-point logic can be translated into equivalent formulas in a fragment of second-order logic called “strict $\forall ^1_1$”. Many, but not all of the pleasant properties of $\exists$FPL formulas are consequences of this translation; that is, they are enjoyed not only by $\exists$FPL formulas but by all strict $\forall ^1_1$ formulas. The “not all” here refers particularly to PTime model-checking for all $\exists$FPL formulas; strict $\forall ^1_1$ formulas do not all enjoy this property unless P$=$NP.

This situation suggests that perhaps the second-order translations of $\exists$FPL formulas actually lie in a smaller fragment of second-order logic, a subset of the strict $\forall ^1_1$ fragment, such that the subset enjoys PTime model-checking. Of course, one could trivially define such a subset, namely the set of formulas that result from the standard translation procedure applied to $\exists$FPL formulas. The purpose of this paper¹ is to give a more detailed description of a subset with the desired properties.

We first show, in Sect. 3, that the model-checking problem for any $\exists$FPL sentence reduces to the propositional satisfiability problem for instances of a corresponding quantifier-free first-order formula. We describe the structure of these quantifier-free formulas and exploit that structure to transform these formulas, in Sects. 4 and 6, in a way that, on the one hand, does not alter the satisfiability of their instances but, on the other hand, ultimately leads to Horn formulas, so that satisfiability can be decided in polynomial time.

Along the way, the material in Sect. 5 presents an apparently new satisfiability-preserving transformation of propositional formulas in conjunctive normal form.

2 Preliminaries

2.1 Existential Fixed-Point Logic

In this subsection, we review the syntax and semantics of existential fixed-point logic.

A vocabulary for existential fixed-point logic ($\exists$FPL) consists of a vocabulary in the usual sense for first-order logic (predicate symbols and function symbols with specified natural numbers as arities) plus a specification, for each predicate symbol, whether it is positive or negatable. Terms and atomic formulas are defined as in first-order logic (without equality, for simplicity). Then $\exists$FPL formulas of a vocabulary L are defined by the following recursion, in which we omit some parentheses to improve readability.

• Atomic formulas of L are L-formulas.

• If $\varphi$ is an atomic L-formula whose predicate symbol is negatable, then $\lnot \varphi$ is an L-formula.

• If $\varphi$ and $\psi$ are L-formulas, then so are $\varphi \wedge \psi$ and $\varphi \vee \psi$.

• If $\varphi$ is an L-formula and x is a variable, then $\exists x\,\varphi$ is an L-formula.

• Let $L'=L\cup \{P_1,\dots ,P_k\}$ be a language obtained by adding to L some k new (i.e., not already in L) positive predicate symbols $P_i$, say of arities $r_i$. Let $\mathbf {x}_1,\dots ,\mathbf {x}_k$ be lists of distinct variables of lengths $r_i$, respectively. Let $\delta _1,\dots ,\delta _k$ and $\varphi$ be $L'$-formulas. Then

  $$\begin{aligned} \mathtt {Let\ }P_1(\mathbf {x}_1)\leftarrow \delta _1,\dots ,P_k(\mathbf {x}_k)\leftarrow \delta _k\mathtt {\ then\ }\varphi \end{aligned}$$

  is an L-formula. Formulas of this form are called fixed-point formulas, the predicate symbols $P_i$ are called the recursion variables, the $\delta _i$’s are called their defining formulas, and $\varphi$ is called the conclusion.

Free variables of a formula are defined as in first-order logic with the additional clause that a variable is free in the fixed-point formula

$$\begin{aligned} \mathtt {Let\ }P_1(\mathbf {x}_1)\leftarrow \delta _1,\dots ,P_k(\mathbf {x}_k)\leftarrow \delta _k\mathtt {\ then\ }\varphi \end{aligned}$$

if either it is free in some $\delta _i$ and is not in the list $\mathbf {x}_i$ or it is free in $\varphi$.

The semantics of $\exists$FPL is defined like that of first-order logic, with the following additional clause for fixed-point formulas. Let $\theta$ be the fixed-point formula displayed above. Let $\mathfrak {A}$ be an L-structure with underlying set A, and let values in A for the free variables of $\theta$ be given. Consider any k-tuple $(R_1,\dots ,R_k)$ of relations on A, where each $R_i$ is $r_i$-ary. Let $(\mathfrak {A},R_1,\dots ,R_k)$ be the $L'$-structure that agrees with $\mathfrak {A}$ as an L-structure and interprets the additional predicate symbols $P_i$ as the corresponding $R_i$. Each of the $L'$-formulas $\delta _j$ defines, in $(\mathfrak {A},R_1,\dots ,R_k)$, an $r_j$-ary relation $S_j$ on A. In detail, an $r_j$-tuple $\mathbf {a}$ of elements of A is in $S_j$ if $\delta _j$ is true in $(\mathfrak {A},R_1,\dots ,R_k)$ when the variables $\mathbf {x}_j$ are interpreted as $\mathbf {a}$ and the other free variables have their originally given interpretations. This construction $\mathbf {\Delta }$ sending k-tuples $(R_1,\dots ,R_k)$ to k-tuples $(S_1,\dots ,S_k)$ is a monotone operator on k-tuples of relations of arities $r_i$ on A. (Monotonicity is with respect to componentwise set-thoretic inclusion; it follows from the requirement that the $P_i$’s are positive in the $\delta _j$’s.) Let $\mathbf {\Delta }^\infty$ be the least fixed-point of this monotone operator. Then the interpretation of $\theta$ in $\mathfrak {A}$ is defined to be the interpretation of the conclusion $\varphi$ in $(\mathfrak {A},\mathbf {\Delta }^\infty )$.

Less formally, the “Let ... then ...” construction produces the least fixed-point of any definable positive operator on (tuples of) relations, and then uses that fixed-point in a further formula $\varphi$.

The absence of the universal quantifier would be meaningless if we allowed negation of arbitrary formulas, as one can simulate $\forall x$ with $\lnot \exists x\,\lnot$. This is why negation is allowed only on atomic formulas. The distinction between positive and negatable predicate symbols and the prohibition of negation on positive atomic formulas serve to ensure that the $\delta _i$ in the fixed-point formula $\theta$ above contain only positive occurrences of the recursion variables $P_j$ and thus define a monotone operator $\mathbf {\Delta }$. They also serve to ensure that the conclusion $\varphi$ in $\theta$ contains only positive occurrences of the predicates $P_j$; without such a restriction, we could surreptitiously introduce the negation of a positive predicate Q by writing $\mathtt {Let\ }P(x)\leftarrow Q(x)\mathtt {\ then\ }\lnot P(x)$, which would be equivalent to $\lnot Q(x)$.

The definition of $\exists$FPL formulas is a recursion involving all vocabularies simultaneously, because fixed-point formulas of one vocabulary L can have subformulas, like the $\delta _i$’s and $\varphi$ above, from a larger vocabulary $L'$. In effect, the additional symbols $P_i$ of $L'$ play the role of bound second-order variables. This connection with second-order logic will be clarified in the next subsection.

2.2 Translation to Second-Order Logic

In this subsection, we review the standard translation from $\exists$FPL formulas to strict $\forall ^1_1$ formulas of second-order logic. As mentioned in the introduction, these are formulas obtained from existential formulas of first-oder logic by prefixing them with a string (possibly an empty string) of universal second-order quantifiers over predicate symbols.²

Note that there is a symbiosis between the two requirements (1) that the second-order quantifiers apply to predicate symbols and not function symbols and (2) that the first-order part of the formula be purely existential. Each of these requirements alone would be meaningless. Specifically, if we imposed only requirement (1) but allowed arbitrary first-order parts, then we could use the first-order part to say that the universally quantified predicates are the graphs of functions, thereby making (1) pointless. If, on the other hand, we imposed only requirement (2) but allowed universal quantification of functions rather than predicates, then arbitrary first-order parts could be simulated by converting them to Herbrand normal form (the dual of Skolem normal form).

We now check, by induction on $\exists$FPL formulas $\varphi$, that they are equivalent to strict $\forall ^1_1$ formulas. This is obvious in the case of atomic or negated atomic formulas.

In the case of conjunctions and disjunctions, we write the conjuncts or disjuncts in strict $\forall ^1_1$ form using different bound second-order variables, combine them with $\wedge$ or $\vee$, and pull the second-order quantifiers out as a prefix using the usual prenexing rules.

In the case of existential quantification, we pull the second-order universal quantifiers out of the scope of the new existential first-order quantifier using the logical equivalence

$$\begin{aligned} (\exists x)(\forall P)\,\varphi (P(\dots ))\iff (\forall P')(\exists x)\,\varphi (P'(x,\dots )). \end{aligned}$$

Here the arity of $P'$ exceeds that of P by one, and every occurrence of P in the body of the formula is changed to an occurrence of $P'$ with the additional argument x.

Finally, in the case of fixed-point formulas, we use the fact that

$$\begin{aligned} \mathtt {Let\ }P_1(\mathbf {x}_1)\leftarrow \delta _1,\dots ,P_k(\mathbf {x}_k)\leftarrow \delta _k\mathtt {\ then\ }\varphi \end{aligned}$$

is equivalent to

$$\begin{aligned} (\forall P_1)\dots (\forall P_k)\,\left[ \left( \bigwedge _{i=1}^k(\forall \mathbf {x}_i)\,(\delta _i\implies P_i(\mathbf {x}))\right) \implies \varphi \right] . \end{aligned}$$

To see the equivalence, note that, since the $P_i$’s occur only positively in $\varphi$, if $\varphi$ holds for the intended interpretation $\mathbf {\Delta }^\infty$ of the $P_i$’s, then it also holds for all larger relations, and, in particular, for all relations closed under the operator $\mathbf {\Delta }$. And this is precisely what the second-order formula above says: $\varphi$ holds whenever the (interpretations of the) $P_i$ are closed under the operator $\mathbf {\Delta }$ given by the defining formulas $\delta _i$.

Now if we insert into this equivalent formula some strict $\forall ^1_1$ forms of the $\delta _i$’s and $\varphi$ and then apply standard prenex operations, the result is in strict $\forall ^1_1$ form, as desired. Note, in particular, that the universal first-order quantifiers $\forall \mathbf {x}_i$ are in the antecedent of an implication so the first-order part is existential.

The preceding proof, showing that $\exists$FPL formulas can be translated to equivalent strict $\forall ^1_1$ formulas, would become an algorithm for carrying out the translation if we added some unimportant details, such as the choice of bound variables and the order in which similar quantifiers are pulled out during prenex operations. We assume henceforth that these details have been supplied, and we refer to the resulting algorithm as the standard translation from $\exists$FPL to strict $\forall ^1_1$.

In [3] some semantical properties of $\exists$FPL formulas were established by showing that they actually hold for all strict $\forall ^1_1$ formulas. These properties include the facts that

• The set of valid $\exists$FPL sentences is a complete computably enumerable set.

• The set of satisfiable $\exists$FPL sentences is a complete computably enumerable set.³

• If a formula is satisfied by some elements in a structure, then this fact depends only on a finite part of the structure.

But at least one important property of $\exists$FPL formulas, namely PTime model-checking, does not (unless P=NP) hold for arbitrary strict $\forall ^1_1$ formulas. Specifically, on undirected graphs, regarded as structures with a single binary relation E of adjacency, the strict $\forall ^1_1$ formula

$$\begin{aligned} (\forall P_1)(\forall P_2)(\forall P_3)(\exists x)(\exists y)\,\left[ \bigwedge _{i=1}^3\lnot P_i(x)\vee \bigvee _{i=1}^3(E(x,y)\wedge P_i(x)\wedge P_i(y))\right] \end{aligned}$$

expresses that the graph is not 3-colorable, a co-NP-complete property.

This situation suggests that perhaps the second-order translations of $\exists$FPL formulas are not merely strict $\forall ^1_1$ but have some additional syntactic property that ensures their PTime decidability. The main purpose of this paper is to establish such an additional property.

3 Model-Checking

In this section, we discuss model-checking for strict $\forall ^1_1$ sentences. That is, we consider, for any fixed strict $\forall ^1_1$ sentence $\varphi$ in vocabulary L, the following decision problem:⁴ An instance is a finite L-structure $\mathfrak {A}$ and the question is whether $\mathfrak {A}\models \varphi$.

It is convenient to address this problem by considering the negation of $\varphi$ instead. It has a standard translation to a strict $\exists ^1_1$ sentence; that is, $\lnot \varphi$ can be put into the form

$$\begin{aligned} (\exists R_1)\dots (\exists R_m)\,\psi \end{aligned}$$

where the $R_i$ are predicate symbols and where $\psi$ is a universal first-order sentence of the vocabulary $L'=L\cup \{R_1,\dots ,R_m\}$. This strict $\exists ^1_1$ sentence is true in $\mathfrak {A}$ if and only if there are relations⁵ $R_i$ on the underlying set A such that all instances of $\psi$ are true for this interpretation of the existentially quantified predicate variables in $\lnot \varphi$. Here “instances of $\psi$” refers to all the formulas obtained by replacing the (universally) quantified first-order variables in $\psi$ by arbitrary elements of A.

This criterion for $\mathfrak {A}\models \lnot \varphi$ is essentially a question of propositional satisfiability. Indeed, consider the set $\varSigma$ of all instances of $\psi$. These are quantifier-free $L'(A)$-sentences, where $L'(A)$ is the language obtained from $L'=L\cup \{R_1,\dots ,R_m\}$ by adding (names for) all the elements of A as constant symbols. In these sentences, replace each atomic sentence that uses an L-predicate symbol (i.e., any predicate symbol other than the $R_i$’s) by its truth value in $\mathfrak {A}$. What remains is a set $\varSigma '$ of sentences that are Boolean combinations of instances of the $R_i$’s. Regard all these instances of $R_i$’s as propositional variables. Any truth assignment to these propositional variables amounts to a choice of relations $R_i$; the truth assignment satisfies $\varSigma '$ if and only if the $R_i$ relations satisfy $\psi$. Therefore $\lnot \varphi$ is true in $\mathfrak {A}$ if and only if $\varSigma '$ is (truth-functionally) satisfiable.

The process leading from $\varphi$ and $\mathfrak {A}$ to $\varSigma '$ can be summarized as follows.

• 1. Perform the standard translation of $\varphi$ to strict $\forall ^1_1$ form.

• 2. Negate the result and push the negation in past quantifiers and connectives, until only atomic formulas are negated; the result is the standard strict $\exists ^1_1$ form of $\lnot \varphi$.

• 3. Delete all quantifiers, but remember which predicate symbols were bound second-order variables.

• 4. Form all instances of the resulting formula, replacing the first-order variables by (names of) elements of $\mathfrak {A}$ in all possible ways.

• 5. In the resulting formulas, replace the atomic subformulas whose predicate symbols are in the vocabulary of $\mathfrak {A}$ (as opposed to the predicate symbols that were quantified second-order variables before step 3) by their truth values in $\mathfrak {A}$.

The resulting set of formulas is the propositional translation $\varSigma '$ of $\lnot \varphi$. Its propositional variables are of the form $R(\mathbf {a})$, where R was a bound second-order variable before step 3, and $\mathbf {a}$ is a tuple of elements of $\mathfrak {A}$.

Note that we have arranged the steps so that the input $\mathfrak {A}$ of our model-checking problem enters the process only at step 4.

The propositional translation has two key properties. First, $\mathfrak {A}\models \varphi$ if and only if the propositional translation of $\lnot \varphi$ is not satisfiable. Second, the propositional translation is, for fixed $\varphi$, computable in polynomial time from $\mathfrak {A}$. In particular, the size of the propositional translation of $\lnot \varphi$ is bounded by the product of

• $|A|^d$, where d is the number of universally quantified, first-order variables in the strict $\forall ^1_1$ translation of $\varphi$, because these are the variables that must be replaced, in all possible ways, by elements of A,

• $\log |A|$ to account for the length in bits of the names of the elements of A, and

• a constant, namely the length of the formula obtained in step 3 above, before $\mathfrak {A}$ entered the process.

Thus, we have a PTime reduction of the model-checking problem for a (fixed) $\exists$FPL sentence $\varphi$ to a propositional satisfiability problem. Our goal is to detect the special properties of the propositional translations of $\exists$FPL sentences that make their satisfiability decidable in PTime. For example, if the propositional translations always consisted of Horn formulas, then that would provide a PTime solution of the model-checking problem. We therefore turn our attention to the structure of the formulas that arise in the propositional translations of $\exists$FPL sentences.

Let us begin by disposing of a tempting error. When we translated $\exists$FPL formulas $\theta$ into second-order logic, the second-order variables originated from the recursion variables $P_i$ in the $P_i(\mathbf {x})\leftarrow \delta _i(\mathbf {x})$ parts of fixed-point formulas. Those $P_i$’s are positive predicate symbols. So they occur only positively in the strict $\forall ^1_1$ form of $\theta$, and therefore the resulting propositional variables occur only negatively in the propositional translation of $\lnot \varphi$. It is, of course, trivial to decide satisfiability of propositional formulas in which all the variables occur only negatively; just give them all the value “false” and see whether the formulas become true.

The error in the preceding paragraph is that, although the $P_i$ are positive predicate symbols and therefore occur only positively in the defining formulas $\delta _i$ and in the conclusion $\varphi$, they nevertheless acquire negative occurrences in the strict $\forall ^1_1$ translation. Specifically, the underlined occurrences in the translation

$$\begin{aligned} (\forall P_1)\dots (\forall P_k)\,\left[ \left( \bigwedge _{i=1}^k(\forall \mathbf {x}_i)\,(\delta _i\implies \underline{P_i(\mathbf {x})})\right) \implies \varphi \right] \end{aligned}$$

of a fixed-point formula are negative. So the situation is not so trivial as the preceding paragraph would suggest.

A better, but still incorrect approach involves rewriting the translation of a fixed-point formula exhibited above in the logically equivalent form

$$\begin{aligned} (\forall P_1)\dots (\forall P_k)\,\left[ \varphi \vee \bigvee _{i=1}^k\exists \mathbf {x}_i(\lnot P_i(\mathbf {x}_i)\wedge \delta _i) \right] . \end{aligned}$$

The negation, in strict $\exists ^1_1$ form, then looks like

$$\begin{aligned} (\exists P_1)\dots (\exists P_k)\,\left[ \lnot \varphi \wedge \bigwedge _{i=1}^k(\forall \mathbf {x}_i)\,(P_i(\mathbf {x}_i)\vee \lnot \delta _i) \right] . \end{aligned}$$

The first-order body of this formula is a conjunction of $k+1$ subformulas, each of which contains at most one positive occurrence of a $P_i$. When we form instances of this body, we get at most one positive literal in each conjunct. That is, we get only Horn clauses, and it is well-known that satisfiability of sets of Horn clauses is decidable in PTime.

There are two errors in this approach. The first is that $\exists$FPL formulas are not simply fixed-point formulas like the one under consideration here. In particular, we might have the conjunction of two (or more) such formulas. Then the propositional translation of the negation will be a disjunction of formulas like those here, and, when put into conjunctive normal form, will have two (or more) positive literals in some of its clauses. We shall address this conjunction problem in Sect. 4.

The second error in the argument above is that a conjunct $P_i(\mathbf {x})\vee \lnot \delta _i$ can have more positive occurrences of literals than just the visible $P_i(\mathbf {x})$. If the formula $\delta _i$ contains some fixed-point formulas as subformulas, then the second-order variables arising from those subformulas will have negative occurrences (analogous to the underlined $P_i$’s above) in $\delta _i$ and therefore positive occurrences in the conjunct $P_i(\mathbf {x})\vee \lnot \delta _i$ under consideration. So the conjunctive normal forms of our propositional translations need not be Horn formulas.

Notice that this error is relevant only when recursions are nested, that is, when the defining formula $\delta _i$ in a recursive clause $P_i(\mathbf {x}_i)\leftarrow \delta _i$ contains further fixed-point formulas. Accordingly, we call this the nesting problem; we shall address it in Sects. 5 and 6.

It is known that nesting of recursions is never really needed in $\exists$FPL. For example, the nested recursion

$$\begin{aligned} \mathtt {Let\ }P(x)\leftarrow [\mathtt {Let\ }Q(y)\leftarrow \delta (P,Q,x,y)\mathtt {\ then\ }\theta (P,Q,x)]\mathtt {\ then\ }\varphi (P) \end{aligned}$$

(where we have indicated which predicate symbols and bound variables are available in the subformulas) is equivalent to

$$\begin{aligned} \mathtt {Let\ }P(x)\leftarrow \theta (P,Q'_x,x),\ Q'(x,y)\leftarrow \delta (P,Q'_x,x,y)\mathtt {\ then\ }\varphi (P), \end{aligned}$$

where $Q'_x$ means the binary predicate symbol $Q'$ with x inserted as its first argument. For the general proof that unnested recursions suffice, see, for example, [5, Sect. 1.C].

One can similarly circumvent the conjunction problem, because conjunctions in $\exists$FPL formulas can be pushed inward to apply only to atomic and negated atomic formulas. For example, the conjunction

$$\begin{aligned} (\mathtt {Let\ }P(x)\leftarrow \delta (x)\mathtt {\ then\ }\varphi )\wedge (\mathtt {Let\ }P'(y)\leftarrow \delta '(y)\mathtt {\ then\ }\varphi ') \end{aligned}$$

is equivalent to

$$\begin{aligned} \mathtt {Let\ }P(x)\leftarrow \delta (x),P'(y)\leftarrow \delta '(y)\mathtt {\ then\ }\varphi \wedge \varphi ' \end{aligned}$$

(where we assume that bound variables have been renamed if necessary to avoid clashes).

In a sense, these observations explain, via the strict $\forall ^1_1$ translation, why $\exists$FPL has PTime model-checking. Explicitly: Given an $\exists$FPL sentence, rewrite it to avoid nested recursions and to avoid conjunctions of compound formulas. Then produce the propositional translation of the negation of the new $\exists$FPL sentence, using a conjunctive normal form of its matrix. The result consists of Horn clauses, for which satisfiability is decidable in PTime. (The use of the conjunctive normal form can exponentially increase the size of the formula, but this doesn’t matter as we are considering a single formula at a time and measuring complexity relative to the structure $\mathfrak {A}$.)

Unfortunately, this does not quite answer our original question, which concerned the direct translation of arbitrary $\exists$FPL formulas to strict $\forall ^1_1$ form, without pre-processing to eliminate nested recursions and non-trivial conjunctions.

Fortunately, the satisfiability problem for the sets of formulas that actually arise can be transformed, on the level of propositional logic, to an equivalent satisfiability problem for Horn formulas. In the following sections, we shall carry out this transformation. In Sect. 4, we show how to convert the formulas that actually arise to formulas that avoid the conjunction problem; the conversion preserves satisfiability. In Sects. 5 and 6, we do the same for the nesting problem. Section 5 isolates the relevant construction in general, not just for the formulas obtained by translating $\exists$FPL formulas; this general, satisfiability-preserving transformation seems to be of independent interest. The application of the general transformation to the nesting problem for translated $\exists$FPL formulas is described in Sect. 6.

Remark 1

The general theme of this paper is that model-checking for a certain class of second-order formulas is in polynomial time because it can be reduced to the propositional satisfiability problem for Horn formulas. The same theme occurs in a paper [4] of Erich Grädel. The class of second-order formulas considered there, called SO-HORN, is, however, quite different from the class arising here from $\exists$FPL. The appropriate comparison would be between SO-HORN and the strict $\exists ^1_1$ formulas arising from the negations of $\exists$FPL formulas. In both cases, the second-order quantifiers range only over relation variables, and in both cases the first-order matrix is required to be a universal formula, but the smiilarity ends there. SO-HORN allows both universal and existential second-order quantifiers, whereas strict $\exists ^1_1$ requires the second-order quantifiers to be existential. On the other hand, the quantifier-free parts of SO-HORN formulas are required to already be in Horn form (at least with regard to the quantified predicate symbols), whereas, as we have seen above, we must deal with non-Horn formulas. Indeed, the following sections are primarily devoted to the problem of converting our formulas to Horn form without altering the satisfiability of their instances.

4 Conjunctions

To avoid annoying distractions during our manipulations of formulas, we assume from now on that there are no clashes of variables in our $\exists$FPL formulas. That is, no (first-order) variable has both free and bound occurrences, nor is any such variable bound twice (by $\exists$ or by the fixed-point construction); also no predicate symbol occurs more than once as a recursion variable. This simplification can, of course, be achieved by renaming bound variables and recursion variables as necessary. We shall refer to this convention as the “no clashes” assumption.

We point out, for future reference, a consequence of the no clashes assumption. Suppose that, in some $\exists$FPL sentence $\varphi$, a certain variable x occurs in two or more fixed-point subformulas, say with recursion variables P and Q. Then the scope of that x must include both of those fixed-point subformulas. As a result, when one converts $\varphi$ to strict $\forall ^1_1$ form, the second-order quantifiers $\forall P$ and $\forall Q$ will be pulled out of the scope of an $\exists x$, and so the predicate symbols P and Q will have their arities increased and will have x inserted as an additional argument. Thus, if x occurs in two or more fixed-point subformulas of $\varphi$, then the recursion variables of those subformulas will, in the strict $\forall ^1_1$ translation of $\varphi$, have x among their arguments. We shall refer to this observation as “argument joining”.

As a first step in the solution of the conjunction problem, we describe carefully the class of formulas that arise from steps 1 to 3 in the process described above for obtaining $\varSigma '$ from $\varphi$ and $\mathfrak {A}$. As remarked there, these three steps do not involve $\mathfrak {A}$, which enters only at steps 4 and 5. So we are working with just an $\exists$FPL formula $\varphi$. We first produce the standard strict $\exists ^1_1$ form of $\lnot \varphi$, and then we delete all the quantifiers, obtaining a quantifier-free first-order formula in the vocabulary consisting of the vocabulary of $\varphi$ plus amplified recursion variables from $\varphi$. Here “amplified” refers to the extra argument places that recursion variables acquire when, in the production of the strict $\forall ^1_1$ form, they are pulled out of the scope of first-order existential quantifiers. By inspection of the definitions of $\exists$FPL formulas and of their standard translations to strict $\forall ^1_1$ form, we see that the quantifier-free formulas obtained by this process are among the primary formulas defined as follows.

Definition 2

The primary formulas of a vocabulary L form the smallest class such that

• atomic formulas whose predicate symbol is negatable are primary,

• negations of arbitrary atomic formulas are primary,

• conjunctions of primary formulas are primary,

• disjunctions of primary formulas are primary, and

• if $\alpha$ and $\delta _1,\dots ,\delta _k$ are primary formulas for the vocabulary $L\cup \{P_1,\dots ,P_k\}$, where the $P_i$ are new positive predicate symbols, then

  $$\begin{aligned} \alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i) \end{aligned}$$

  is primary.

We refer to the last item in this list of constructors as the mix constructor, because it mixes conjunction and disjunction. Each $P_i$ occurring there will be called a key predicate, and $\mathbf {x}_i$ and $\delta _i$ will be called its associated variables and formula, respectively.

Note that the primary formulas include all negated atomic formulas, but they include the unnegated ones only when the predicate symbol is negatable. This strange-sounding situation — the predicate must be negatable in order to appear unnegated — arises from the fact that we are working with the translations not of $\exists$FPL formulas themselves but of their negations. Note further that a positive predicate can have at most one positive occurrence in a primary formula, namely an occurrence as the key predicate of a mix construction. Here the “at most one” claim follows from our no clashes assumption.

In this new context, argument joining becomes the fact that, if $\alpha$ is a primary formula and if a variable occurs in two or more subformulas of $\alpha$ obtained by the mix construction, then that variable is among the arguments of the key predicates of those mix subformulas.

The next definition describes a subclass of the primary formulas for which the conjunction problem does not arise. In fact, formulas in this subclass have an especially useful structure, which we describe, in terms of their parse trees, after the definition.

Definition 3

The basic secondary formulas of a vocabulary L form the smallest class such that

• atomic formulas whose predicate symbol is negatable are basic secondary,

• negations of arbitrary atomic formulas are basic secondary,

• conjunctions of basic secondary formulas are basic secondary, and

• disjunctions of basic secondary formulas are basic secondary.

The secondary formulas of a vocabulary L form the smallest class such that

• all basic secondary formulas are secondary, and

• if $\alpha$ and $\delta _1,\dots ,\delta _k$ are secondary formulas for the vocabulary $L\cup \{P_1,\dots ,P_k\}$, where the $P_i$ are new positive predicate symbols, then the result of the mix construction,

  $$\begin{aligned} \alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i), \end{aligned}$$

  is secondary.

Thus, secondary formulas are built by the same constructors as primary formulas but, in a secondary formula, the mix constructors must be applied after all the others, not intermingled with the others.

It is useful to consider parse trees showing how secondary formulas are built from basic secondary ones. The internal nodes of such a tree correspond to the mix construction $\alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)$; such a node has $2k+1$ children, one for $\alpha$, k for the key predicate subformulas $P_i(\mathbf {x}_i)$, and k corresponding to the associated $\delta _i$’s. Of these, the k corresponding to $P_i(\mathbf {x}_i)$ are leaves of the parse tree; the other $k+1$ might be leaves or internal nodes. All the leaves of the parse tree are either of the $P_i(\mathbf {x}_i)$ form just mentioned or basic secondary formulas. Notice that the leaves of the $P_i(\mathbf {x}_i)$ sort are the only place where positive predicate symbols have positive occurrences.

The main result in this section will say that every primary formula can be transformed into a secondary one while preserving the essential property relevant for $\exists$FPL. That essential property is, in view of the results of Sect. 3, instance-equisatifiability, defined as follows.

Definition 4

Two sets of quantifier-free formulas $\varSigma _1$ and $\varSigma _2$ (in a first-order language that extends L) are equisatisfiable if, whenever there exists a truth assignment satisfying one of them, there also exists a (possibly different) truth assignment satisfying the other. They are instance-equisatisfiable if, for every L-structure $\mathfrak {A}$, $\varSigma _1(\mathfrak {A})$ and $\varSigma _2(\mathfrak {A})$ are equisatisfiable, where $\varSigma _i(\mathfrak {A})$ is obtained from $\varSigma _i$ by replacing the variables by elements of $\mathfrak {A}$ in all possible ways and then replacing all atomic subformulas whose predicate is in L by their truth values in $\mathfrak {A}$.

Notice that the construction of $\varSigma _i(\mathfrak {A})$ from $\varSigma _i$ described in this definition is exactly the last two steps, 4 and 5, in the construction of $\varSigma '$ in Sect. 3. Thus, for the purpose of model-checking $\exists$FPL formulas, the $\varSigma '$ there, which consists of primary formulas, can safely be replaced by any instance-equisatisfiable set of formulas. That is how we shall use the following proposition and its corollary.

Proposition 5

The conjunction and disjunction of two secondary formulas are each instance-equisatisfiable with a secondary formula.

Proof

We proceed by induction on the two given secondary formulas, and we treat the most difficult case, namely where both of them arise from the mix construction. (If both of the given formulas are basic, then the result is trivial. If one arises from mix and the other is basic, then the proof is easier, or one can regard the basic formula as resulting from a mix in which the number of key predicates happens to be zero.) Suppose, therefore, that the given formulas are

$$\begin{aligned} \gamma \ =\ \alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i) \quad \text{ and } \quad \gamma '\ =\ \alpha '\wedge \bigwedge _{i=1}^{k'}(P'_i(\mathbf {x}'_i)\vee \delta '_i). \end{aligned}$$

Their conjunction $\gamma \wedge \gamma '$ is not merely instance-equisatisfiable but tautologically equivalent with

$$\begin{aligned} (\alpha \wedge \alpha ')\wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)\wedge \bigwedge _{i=1}^{k'}(P'_i(\mathbf {x}'_i)\vee \delta '_i), \end{aligned}$$

which is a secondary formula with $k+k'$ key predicates, because, by the induction hypothesis, $\alpha \wedge \alpha '$ is a secondary formula.

For the disjunction, we use

$$\begin{aligned} \theta \ =\ (\alpha \vee \alpha ')\wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)\wedge \bigwedge _{i=1}^{k'}(P'_i(\mathbf {x}'_i)\vee \delta '_i), \end{aligned}$$

which is a secondary formula, as above, because $\alpha \vee \alpha '$ is secondary by induction hypothesis. It is easy to see that $\theta$ tautologically implies $\gamma \vee \gamma '$. The converse, however, is not generally correct; we do not get equivalence but only instance-equisatisfiability.

To prove the non-trivial direction of instance-equisatisfiability, suppose we have an L-structure $\mathfrak {A}$ and truth assignment v satisfying all the instances of $\gamma \vee \gamma '$, where by “instance” we understand, as in the definition of instance-equisatisfiability, the result of substituting elements of $\mathfrak {A}$ for variables and then replacing all atomic formulas involving L-symbols by their truth values in $\mathfrak {A}$. Notice that the predicate symbols in $\gamma$ and $\gamma '$ are all either L-symbols or key predicates of mix constructions.

To emphasize the essential idea of the proof, we first consider the special case where $\gamma$ and $\gamma '$ have no (first-order) variables in common. In this case, we claim that v either satisfies all instances of $\gamma$ or satisfies all instances of $\gamma '$ (not merely some instances of the one and the remaining instances of the other). Suppose the claim were false, so some instance of $\gamma$, and some other instance of $\gamma '$ were falsified by v. Then we could form a third instance, giving the variables in $\gamma$ the same values as in the first instance (thus making $\gamma$ false under v) and giving the variables in $\gamma '$ the same values as in the second instance (thus making $\gamma '$ false under v). But then this third instance would make $\gamma \vee \gamma '$ false under v, contrary to our choice of v.

Thus, we may suppose without loss of generality, that v satisfies all instances of $\gamma$. Now we can produce a truth assignment $v^*$ satisfying $\theta$ as follows. Let $v^*$ assign the value “true” to all those atomic formulas whose predicate symbol is one of the key predicates $P'_i$ of $\gamma '$, and let $v^*$ agree with v on all other atomic formulas. The difference between v and $v^*$, affecting only the $P'_i$, will not affect $\gamma$, because the $P'_i$ don’t occur in $\gamma$ (thanks to the no clashes assumption). Thus $v^*$ satisfies $\gamma$ and therefore satisfies the part $(\alpha \vee \alpha ')\wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)$ of $\theta$. But it also satisfies the remaining conjunct, $\bigwedge _{i=1}^{k'}(P'_i(\mathbf {x}'_i)\vee \delta '_i)$ of $\theta$. So $v^*$ satisfies $\theta$ as required.

The preceding argument used the assumption that $\gamma$ and $\gamma '$ have no common variables. We now indicate how to modify it to accommodate common variables, say the list $\mathbf {y}$ of variables. We no longer claim that v satisfies all instantiations of $\gamma$ or all instantiations of $\gamma '$; instead, we claim that, for any fixed instantiation of $\mathbf {y}$, v satisfies all its extensions to instantiations of $\gamma$ or all its extensions to instantiations of $\gamma '$. In other words, whether $\gamma$ or $\gamma '$ is satisfied (by v) may depend on the instantiation but only via the values assigned to the common variables $\mathbf {y}$. The proof of this modified claim is exactly as in the easier argument given above; once we fix the values of $\mathbf {y}$, the remaining variables, occurring in only one of $\gamma$ and $\gamma '$, can be treated as before.

In the easier argument, we obtained $v^*$ by modifying the truth values assigned by v to the key predicates of $\gamma '$, under the assumption that v satisfied all instances of $\gamma$. Of course, if v had satisfied all instances of $\gamma '$, then we would have modified the truth values assigned to the key predicates of $\gamma$. Now in the present, more complicated situation, the decision as to which predicates should get new truth values may depend on the values assigned to $\mathbf {y}$. Thanks to argument joining, this is no problem. The variables $\mathbf {y}$ occur as arguments of all the key predicates in $\gamma$ and in $\gamma '$. So we can modify the values assigned to instances of $P_i$ with certain values for the $\mathbf {y}$ arguments and modify the values assigned to instances of $P_i'$ with other values for the $\mathbf {y}$ arguments. What we do with one instantiation of $\mathbf {y}$ has no effect on what happens with other instantiations. (Another way to view this argument is that we treat the variables $\mathbf {y}$ as new constant symbols and consider separately all the expansions of $\mathfrak {A}$ giving values to these new constants. That reduces the problem to the easier case already treated.)

This completes the proof of the proposition.

Corollary 6

Every primary formula is instance-equisatisfiable with a secondary formula.

Proof

Induction on primary formulas, using Proposition 5 for the only nontrivial cases.

The proofs of the proposition and corollary provide an explicit algorithm for converting a primary formula to an instance-equisatisfiable secondary one.

5 Satisfiability and Trimming

This section is entirely about propositional logic, specifically about satisfiability of sets of clauses. Here “clause” means, as usual, a disjunction of literals, i.e., of propositional variables and negations of propositional variables. So a set of clauses is semantically equivalent to a conjunctive normal form, namely the conjunction of its clauses.

Theorem 7

Let $\varGamma$ be a set of clauses, let p be a propositional variable, and let Q be a set of propositional variables other than p. Suppose that, whenever a clause in $\varGamma$ contains a negative occurrence of a variable from Q, it also contains a positive occurrence of p or of some variable from Q. Obtain $\varGamma '$ from $\varGamma$ by deleting positive occurrences of p from those clauses that also contain positive occurrences of at least one variable from Q. Then $\varGamma$ is satisfiable if and only if $\varGamma '$ is.

Proof

One direction is trivial, because any truth assignment that satisfies all the clauses in $\varGamma '$ will certainly satisfy the corresponding clauses in $\varGamma$, since the latter differ from the former at most by having additional disjuncts.

Suppose, therefore, that we have a truth assignment v that satisfies all the clauses in $\varGamma$. If it makes p false, then it also satisfies all the clauses in $\varGamma '$, because the positive occurrences of p that were removed when we produced $\varGamma '$ were not satisfied by v and so some other disjuncts in those clauses must have been satisfied.

So we may assume that v makes p true. In this situation, v need not satisfy $\varGamma '$, but we can find another truth assignment $v'$ that will satisfy $\varGamma '$. Let $v'$ make all the variables in Q true, and let it agree with v on all the other variables. To show that $v'$ satisfies every clause $\gamma$ in $\varGamma '$, we consider three cases.

First, suppose $\gamma$ is one of the clauses that was altered, by removing the positive disjunct p, when we transformed $\varGamma$ to $\varGamma '$. Recall that we undertook such a removal only when the clause in $\varGamma$ contained, along with p, a positive occurrence of some variable from Q. Such variables are true under $v'$, and therefore our clause $\gamma$ is also true under $v'$.

It remains to consider those clauses $\gamma$ that were not changed in the transition from $\varGamma$ to $\varGamma '$. These were true under v, but we need that they are true under $v'$. That is very easy to check for those clauses $\gamma$ in which variables from Q occur only positively. Since, in going from v to $v'$, the only changes were that variables in Q, which might have been false under v, became true under $v'$, any clause containing them only positively cannot change from true under v to false under $v'$.

There remain those clauses $\gamma$ that are the same in $\varGamma$ and in $\varGamma '$ but have negative occurrences of some variable(s) from Q. By the hypothesis of the theorem, every such $\gamma$ also has positive occurrences of p or of some variable from Q. Since p and all variables from Q are true under $v'$, it follows that $v'$ satisfies all such clauses $\gamma$.

Definition 8

The transformation from $\varGamma$ to $\varGamma '$ described in the theorem is called trimming $\varGamma$ or, in more detail, trimming p using Q.

6 Trimming to Horn Form

In this section, we complete the reduction of the model-checking problem for any $\exists$FPL sentence to a decidable case of the propositional satisfiability problem, namely the satisfiability of sets of Horn clauses.

Given an $\exists$FPL sentence $\varphi$, we saw in Sect. 3 how to reduce the problem “Given $\mathfrak {A}$, decide whether $\varphi$ is true in $\mathfrak {A}$” to the problem of satisfiability of the set of all $\mathfrak {A}$-instances of a certain formula constructed from $\varphi$. That formula is primary, in the sense defined in Sect. 4 and, as proved there, instance-equisatisfiable with a certain secondary formula. So the model-checking problem for $\varphi$ is reduced to determining the satisfiability of the instances of this secondary formula.

The next step is to convert this secondary formula, say $\psi$, into conjunctive normal form. (As mentioned earlier, the possible exponential increase in the formula’s size caused by this conversion is not a problem, because we are considering the model-checking problem for a fixed formula, with only the structure $\mathfrak {A}$ as input. The set of all $\mathfrak {A}$-instances still has size polynomial in the size of $\mathfrak {A}$.) We now look into the structure of this conjunctive normal form and its $\mathfrak {A}$-instances (for arbitrary $\mathfrak {A}$).

Recall that, when forming $\mathfrak {A}$-instances of $\psi$, we replace any atomic subformulas that use predicates from L by their truth values in $\mathfrak {A}$. The atomic subformulas of an instance therefore use only the predicates not in L, which are the recursion variables of $\varphi$ and the key predicates of the primary and secondary formulas derived from $\varphi$. We shall use the letters P and Q to stand for such predicates in the following discussion.

Let us consider the conjunctive normal form of a secondary formula $\psi$, paying particular attention to the positive occurrences of atomic subformulas using the P, Q predicates. Basic secondary formulas are built using $\wedge$ and $\vee$ from atomic subformulas, subject to the condition that positive predicates — which include the P, Q predicates — occur only negatively. So there are not yet any positive occurrences of P’s and Q’s at this basic stage. That situation changes when we apply the mix construction to produce secondary formulas of the form

$$\begin{aligned} \alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i). \end{aligned}$$

Now each $P_i$ has a positive occurrence, and, in addition, other P’s and Q’s may have positive occurrences in $\alpha$ and in the $\delta _i$’s. To convert $\alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)$ to conjunctive normal form, we would first convert $\alpha$ and the $\delta _i$’s to conjunctive normal form and then, for each i, distribute $P_i(\mathbf {x}_i)\vee -$ across the conjunctive normal form of $\delta _i$. Thus, each conjunct of that conjunctive form acquires $P_i(\mathbf {x}_i)$ as a new literal. Note that such a conjunct may already have other positive occurrences of other P’s and Q’s, but only when these are the key predicates of subformulas of $\delta _i$. Thus, those other P’s and Q’s come from mix subformulas that are descendants of the current mix formula $\alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)$ in the parse tree of $\psi$. We emphasize that, in this conjunct, the new positive P and previously present Q are key predicates of comparable mix nodes of the parse tree.

Repeating this process for every application of the mix constructor in $\psi$, we arrive at a conjunctive normal form $\theta$ in which every individual conjunct has, because of the comparability noted at the end of the preceding paragraph, the following crucial property: All the positive occurrences of P’s and Q’s in it originated from mix nodes in a single branch of the parse tree of $\psi$.

From now on, to make contact with the terminology of Sect. 5, we shall identify the conjunction $\theta$ with the set of its conjuncts, which may thus be called clauses.

Consider a P and a Q such that the mix node with key P is an ancestor of the mix node with key Q in the parse tree of $\psi$. So P is some $P_i$ in a mix formula $\alpha \wedge \bigwedge _{i=1}^k(P_i(\mathbf {x}_i)\vee \delta _i)$, while Q is the key of a mix subformula of $\delta _i$. That mix subformula contains all the occurrences of Q in $\psi$, because of our no clash assumption. As a result, in the conjunctive normal form $\theta$, every clause with an occurrence of Q also has a positive occurrence of $P(\mathbf {x}_i)$. (We need this information only for the negative occurrences of Q, but it is true for all occurrences of Q.)

Recall that, in this situation, when we formed the strict $\forall ^1_1$ form of $\varphi$ (as the first step toward $\psi$ and $\theta$), the variables $\mathbf {x}_i$ associated to $P_i$ became additional arguments of Q. Because of that, when we now form instances of $\theta$, all clauses containing negative occurrences of any particular instance of Q will also contain a positive occurrence of the corresponding instance of $P_i(\mathbf {x}_i)$. This means, by Theorem 7, that we can delete positive occurrences of any instance of P from any clause that also contains a positive occurrence of a corresponding instance Q.

These deletions can be uniformly summarized as follows, in terms of $\theta$ itself rather than its instances: In any clause containing positive occurrences of P and Q, where Q originated in a descendant of the mix formula of P, one can delete the occurrence of P. But, in every conjunct of $\theta$, the positively occurring P’s and Q’s originated along a branch, and so one can delete all the positive P’s and Q’s except the one farthest from the root of the parse tree of $\psi$.

That leaves at most one positive P in any clause; all instances then have at most one positive literal. That is, we have only Horn clauses in the trimmed conjunctive normal form.

7 Summary

The strict $\forall ^1_1$ translation of any $\exists$FPL sentence has a special syntactic form. Its quantifier-free matrix is the negation of what we called a primary formula in Sect. 4, and the occurrences of variables are constrained by the no clash assumption and the argument joining property. This special form ensures polynomial-time model-checking, because this special syntactic form allows, first, reduction to a secondary formula (still subject to no clashes and argument joining) and, second, trimming to Horn form. Then the original $\exists$FPL sentence holds in $\mathfrak {A}$ if and only if the set of all $\mathfrak {A}$-instances of this Horn form is not satisfiable.