Introduction

The objective of second-order quantifier elimination is to compute from a given second-order formula a so-called resultant (from German Resultante, used by Schröder [17]), that is, an equivalent first-order formula. Finding such a resultant is not in general possible for arbitrary second-order formulas. The early technical investigations of second-order quantifier elimination on the basis of first-order logic were done jointly with the early investigations of the decision problem: Löwenheim [14], Skolem [18] and Behmann [3] gave decision methods for relational 1 monadic 2 formulas with equality. Their methods are based on existentially quantifying upon all predicates in the formula to decide and computing a resultant by elimination. The obtained resultant of a relational monadic formula is then a truth value constant or a formula that just constrains domain cardinality (see, e.g., [23]).

Whereas much is known today about decidable fragments of first-order logic, see, e.g., [4], knowledge about fragments on which second-order quantifier elim-ination succeeds seems still scarce [12]. Ackermann [1] was the first to publish3 a proof that second-order quantifier elimination on the basis of first-order logic does not succeed in general, by means of a second-order formalization of the induction axiom. Conradie [5] formulated quite specific syntactic conditions under which the modern DLS algorithm [7] for second-order quantifier elimination succeeds. However, it appears that for the case of simultaneous elimination of multiple existential predicate quantifiers only a sufficient condition has been found. In addition, DLS as considered there does not cover the relational monadic case. Van Benthem and Doets [21] consider three classes of relational formulas with existential second-order quantifier prefix, distinguished by the subsequent first-order quantifier prefix: existential first-order quantifiers, universal first-order quantifiers, and first-order quantifier prefixes of the form ∀x 1 . . . ∀x m ∃y 1 . . . ∃y n . 4As shown in [21], formulas with arbitrary further first-order prefixes can be converted to the latter class by Skolemization. For the second class, it is sketched in [21] with model theoretic arguments that a resultant exists which is an (infinite) disjunction of an (infinite) conjunction of first-order formulas.

Here we will take a closer look on that second class, applying formula-based tools that are used in automated deduction. In particular, our toolkit comprises domain closure axioms as familiar from logical modeling of database semantics, formula normalization and elimination of first-order quantifiers by ground expansion, second-order quantifier elimination by rewriting with an equivalence of a second-order formula of a certain form to a first-order formula (Ackermann's Lemma [1]), a strengthening of Craig interpolation that can be proven with a tableau technique, and decidability of the Bernays-Schönfinkel-Ramsey class.

The main original motivation was to explore possible foundations for applying instance-based [2] techniques as known for theorem proving also to solve elimination tasks. Their underlying principle is Herbrand's theorem, which justifies reducing unsatisfiability of a first-order formula to unsatisfiability of a propositional formula obtained by eliminating first-order quantifiers through ground expansion with terms constructed from the input vocabulary. The general idea of instance-based methods for theorem proving is to successively generate conjunctions of instances of the universally quantified input formulas and test these for propositional unsatisfiability. In presence of various techniques to avoid naive explicit expansion and the ability of recent SAT solvers to handle quite large propositional formulas this a practically feasible approach to first-order theorem proving. Thus, the question came up, whether there are quantifier-free formula expansions that are large enough to ensure that elimination can be performed on these instead of the original formula, in analogy to detecting unsatisfiability.

With the expectation of considering an important but somehow easier special case we focus on relational formulas, which underlie most formalizations of databases. Of course, functions can be represented by predicates, such that without restriction on quantification, the relational property is not a limitation of expressive power. We focus on the restriction to universal relational formulas. In Skolemized form, formulas of the Bernays-Schönfinkel-Ramsey class are such formulas. Typically, in contrast to many resolution-based methods [10], instance-based methods decide universal relational formulas. An intuitive argument is that these formulas trivially have a largest expansion that needs to be considered to determine satisfiability. Do they also have in some sense a largest expansion that needs to be considered for elimination?

The obtained results are not as positive as desired, but at least shed some light on the properties of elimination problems with certain quantification restrictions. The considered formulas have an existential second-order quantifier prefix, followed by a universal first-order prefix and a quantifier-free formula. It is shown that for such a second-order formula F a sequence {G 0 , G 1 , G 2 , . . .} of universal relational first-order formulas that have (not necessarily strictly) increasing strength and are all entailed by F can be constructed. Any first-order consequence of F is a consequence of some G i . Formula F has a resultant if and only if it is equivalent to some G i . The set of the formulas G i that constitute a resultant of F or, more generally, have the same first-order consequences as F is co-recursively enumerable. Also the set of first-order formulas that entail F is co-recursively enumerable.

Craig [6] considered the question of constructing a so-called base for a given formula with existential second-order prefix, that is, a recursive set of firstorder formulas whose set of consequences is identical to the set of first-order consequences of the given second-order formula. He notes that this corresponds to a weakened version of Ackermann's [1] generalized notion of resultant. Our construction of {G 0 , G 1 , G 2 , . . .} can be viewed as construction of a monotonic base, actually with similar techniques as in [6], but where the restriction to universal relational formulas allows to derive additional properties.

The rest of the paper is structured as follows: Notation and definitions of the considered formula classes are introduced in Sect. 2 and the toolkit of the used techniques is specified in Sect. 3. In Sect. 4 then the main results are stated, proven and informally described, followed by a discussion of related work, potential applications and open issues in Sect. 5. Section 6 concludes the paper.

Notation and Preliminaries

We consider second-order formulas where second-order quantification is just upon predicates (in contrast to functions), or, in other words, first-order formulas extended by second-order quantification upon predicates. They are constructed from atoms (including equality atoms), constant operators , ⊥, the unary operator ¬, binary operators ∧, ∨ and quantifiers ∀, ∃ with their usual meaning. Further binary operators →, ←, ↔, as well as n-ary versions of ∧ and ∨ can be understood as meta-level notation. The operators ∧ and ∨ bind stronger than →, ← and ↔. The scope of ¬, the quantifiers, and the n-ary connectives is the immediate subformula to the right.

A subformula occurrence has in a given formula positive (negative) polarity if it is in the scope of an even (odd) number of negations. A vocabulary is a set of symbols, that is, predicate symbols (briefly predicates), function symbols (briefly functions) and individual symbols. (Function symbols are assumed to have an arity ≥ 1. Individual symbols are not partitioned into variables and constants. Thus, an individual symbol is -like a predicate in second-order logic -considered as variable if and only if it is bound by a quantifier.) The set of symbols that occur free in a formula F is denoted by V(F ), the set of predicate symbols that occur free in F by V P (F ), and the set of individual symbols that occur free in F (commonly termed the set of constants occurring in F ) by V C (F ). The arity of a predicate or function symbol s is denoted by arity(s).

We use straightforward shorthands based on sequences of terms for expressing application of predicates and functions to arguments, simultaneous comparison of multiple terms and quantifying upon multiple variables: If t = t 1 , . . . , t n is an n-ary sequence of terms, and s is an n-ary predicate or function symbol, we write st for s(t 1 , . . . , t n ), or, in case n = 0, for s, respectively. If t = t 1 , . . . , t n and u = u 1 , . . . , u n are both n-ary sequences of terms, we write t = u for t 1 = u 1 ∧ . . . ∧ t n = u n and t = u for ¬(t = u). If x = x 1 , . . . , x n is a sequence of individual symbols or of predicates, we write ∃s (∀s, resp.) for ∃s 1 . . . ∃s n (∀s 1 . . . ∀s n , resp.).

We consider three specific formula classes whose members are constructed as a second-order quantifier prefix followed by a first-order quantifier prefix and a quantifier-free relational formula of first-order logic with equality. These classes are characterized by restrictions on the second-order and first-order prefix as shown in the following table, where the r in the class names points out the restriction to relational formulas: Formula class Second-order prefix First-order prefix

Underlying Toolkit

We now specify the technical background underlying the proofs of the main results. It is essentially a small toolkit of formula-based concepts and construction techniques used in automated deduction.

Second-Order Quantifier Elimination

The objective of second-order quantifier elimination is to compute for a given second-order formula a first-order resultant, which is characterized as follows:

Definition 1 (Resultant). A resultant of a second-order formula F is a formula F such that

1. F is first-order, 2. F ≡ F , 3. V(F ) ⊆ V(F ).

It follows immediately from condition 2. of Def. 1 that all resultants of a given formula are equivalent. Hence, we also speak of the resultant of a second-order formula. From conditions 1. and 3. it follows that none of the quantified predicates possibly occurring in F do occur in F . They are, so-to-speak, "forgotten" in F .

The following proposition shows an equivalence of a second-order formula with a certain shape and a first-order formula, due to Ackermann [1]. It can be applied to compute the resultant of a second-order formula that matches its left side by rewriting with the right side. The DLS algorithm [7,5] for second-order quantifier elimination surrounds such rewriting steps with pre-and postprocessing operations.

Proposition 2 (Ackermann's Lemma [1]). Let p be an n-ary predicate, let G and H be first-order formulas such that p does not occur in G, let x = x 1 , . . . , x n be a sequence of distinct individual symbols that do not occur bound in G and do not occur in H. Let H[p → G] stand for H with each occurrence of atoms p(t 1 , . . . , t n ) whose predicate is p replaced by G{x 1 → t 1 , . . . , x n → t n }, that is, G under the substitution that maps x i to t i , for i ∈ {1, . . . , n}. If p does not occur with positive polarity in H, then

∃p (∀x(px ∨ G) ∧ H) ≡ H[p → G].

Ackermann's lemma also holds in a dual variant: If p does not occur with negative polarity in H, then ∃p (∀x

(¬px ∨ G) ∧ H) ≡ H[p → G].

For quantifier-free formulas (also with function symbols) with an existential second-order prefix, it is always possible to compute a resultant on the basis of Ackermann's lemma, as demonstrated with the following algorithm: Algorithm 3 (Second-Order Quantifier Elimination upon Quantifier-Free Formulas). Input: An formula that consists of a prefix of existential predicate quantifiers followed by a quantifier-free formula of first-order logic with equality. Method: Starting with the input formula, repeatedly eliminate the innermost existential second-order quantifier with the following method: Given is a formula ∃p F , where F is quantifier-free. Convert F to disjunctive normal form K 1 ∨ . . . ∨ K n , where each disjunct is a conjunction of literals. Propagate the second-order quantifier inwards to obtain the formula ∃p

K 1 ∨ . . . ∨ ∃p K n , which is equivalent to ∃p F . Eliminate ∃p in each disjunct individually: Arrange the disjunct in the form ∃p (pt 1 ∧ . . . ∧ pt k ∧ ¬pu 1 ∧ . . . ∧ ¬pu l ) ∧ K

, where p does not occur in K and k, l ≥ 0. Rewrite this formula to the equivalent formula

∃p (∀x (px ∨ x = t 1 ∧ . . . ∧ x = t k ) ∧ ¬pu 1 ∧ . . . ∧ ¬pu l ) ∧ K ,

where x is a sequence of fresh individual symbols whose length is the arity of p. Apply Ackermann's Lemma (Prop. 2) to rewrite this formula to its resultant

(u 1 = t 1 ∧ . . . ∧ u 1 = t k ) ∧ . . . ∧ (u l = t 1 ∧ . . . ∧ u l = t k ) ∧ K .

Combine these individual resultants disjunctively to obtain a resultant of ∃p F . Output: A resultant of the input formula. Algorithm 3 also justifies the computation of resultants of formulas of the form

∃p 1 . . . ∃p m ∃x 1 . . . ∃x n F,(i)

where F is quantifier-free. These are the formulas of the first of the three classes with existential second-order quantification explicitly considered in [21] as mentioned in the introduction, now generalized by allowing function symbols. Formula (i) is equivalent to ∃x 1 . . . ∃x n ∃p 1 . . . ∃p n F , obtained by switching the firstand second-order quantifier prefix. If F is a resultant of ∃p 1 . . . ∃p n F , obtained for example with Algorithm 3, then ∃x 1 . . . ∃x n F is a resultant of (i). Algorithm 3 can be considered as a specialized variant of DLS [7], with a simpler pre-and postprocessing that just suffices to handle predicate quantification applied to quantifier-free first-order formulas. In [6] a similar technique is used and some refinements are shown. In [9] a further variant of DLS is introduced that computes resultants of quantifier-free formulas under existential second-order quantification, however constrained such that all occurrences of a quantified predicate are replaced by the same "witness" formula, whereas in Algorithm 3 it is allowed that in the processing of each disjunct K i a different formula (x = t 1 ∧ . . . ∧ x = t k ) is used to replace p. In fact, the algorithm from [9] can be considered as based on Algorithm 3, but followed by a second step in which the different replacement formulas in each disjunct are combined to a single witness that is suitable as replacement in all disjuncts. The necessity of only a single replacement formula is imposed by the restricted form of secondorder quantifier elimination through finding a witnesses that is considered in [9], which can be also viewed as finding a Boolean unifier and as finding a particular solution of the Boolean solution problem [24].

Domain Closure Axioms and Restricted Prefixes

The domain closure axiom, which restricts the universe of discourse to just those individuals denoted by constants in the given formula, emerged as a tool for the logical modeling of relational databases [16]. Following [8], we consider a generalized variant that in addition permits a fixed number of further objects. Definition 4 (Domain Closure Axiom). Let C = {c 1 , . . . , c n } be a nonempty set of individual symbols, let k ∈ N 0 , and assume that x, y 1 , . . . , y k are individual symbols that are not in C. Define

DCA k C def = ∃y 1 . . . ∃y k ∀x (x = y 1 ∨ . . . ∨ x = y k ∨ x = c 1 ∨ . . . ∨ x = c n ).

It is possible, to specify domain closure axiom with a formula as parameter whose free individual symbols are taken as considered set C. However, considered as a function of formulas, domain closure axiom is then not "semantic", that is, it might have semantically different values for semantically equivalent argument formulas, which, despite being equivalent, might have different sets of free individual symbols. To avoid "non-semantic" functions of formulas, we use here a version of domain closure axiom that is explicitly parameterized with a set C of individual symbols.

Domain closure axioms play a role in general domain circumscription [8]. As shown with [8, Thm. 6.1], the domain circumscription of an ∀r-formula

F such that V C (F ) = ∅ is equivalent to DCA 0 C ∧ F , where C = V C (F ).

The remaining propositions in this section show properties of first-order formulas with restricted quantifier prefixes conjoined with domain closure axioms. Roughly, the intuition there is that for these formulas the addition of domain closure axioms does not essentially alter the semantics, but allows to eliminate first-order quantification by ground expansion with respect to the finite set of symbols presupposed in the domain closure axioms. The underlying core property is that from a model of an ∃∀r-formula a further model can be derived that in addition also satisfies the domain closure axiom with respect to length of the existential quantifier prefix and the free individual symbols: Proposition 5 (Domain Closure Extension for ∃∀r-Formulas). Let F be an ∃∀r-formula and let I be an interpretation such that I |= F . Then for all non-empty sets C ⊇ V C (F ) of individual symbols and for all natural numbers k larger than or equal to the length of the existential quantifier prefix of F there exists an interpretation I such that

1. I |= DCA k C ∧ F. 2.

For all ground atoms A constructed from predicates in F and individual symbols in C it holds that

I |= A iff I |= A.

This proposition is not hard to prove by considering the submodel of I obtained by restricting the domain to the union of the ≤ k individuals whose existence is presupposed by the existential quantifier prefix of F and the set of the values of the members of V C (F ) in I. From this proposition it follows that if an ∃∀rformula conjoined with a suitable domain closure axiom entails an ∀∃r-formula, then also the ∃∀r-formula alone entails that formula:

Proposition 6 (Redundancy of Domain Closure for ∃∀r-∀∃r Entailments).

Let F be an ∃∀r-formula and let G be an ∀∃r-formula, let C ⊇ V C (F ) ∪ V C (G) be a non-empty set of individual symbols, and let k be a natural number that is larger than or equal to the sum of the length of the existential quantifier prefix of F and the length of universal quantifier prefix of G. It then holds that From this proposition it follows that the semantics of ∀r-formulas F is preserved under conjunction with a suitable domain closure axiom: Proposition 7 (Semanticity of Domain Closure for ∀r-formulas). Let F, G be ∀r-formulas, let C ⊇ V C (F ) ∪ V C (G) C be a non-empty set of individual symbols, and let k be a natural number that is larger than or equal to the maximum of the quantifier prefix lengths of F and G. It then holds that

if DCA k C ∧ F |= G, then F |= G. Proof. Assume the left side of the proposition, that is, DCA k C ∧ F |= G.if DCA k C ∧ F ≡ DCA k C ∧ G, then F ≡ G.

Proof. Follows from Prop. 6.

Resultants of ∃∀r-formulas are Universal

Based on a strengthening of Craig's interpolation theorem it can be shown that whenever an ∃∀r-formula has a resultant, then the resultant is equivalent to an ∀r-formula, and, moreover, that there is an effective method to compute for any given resultant of an ∃∀r-formula such an equivalent ∀r-formula. Before we state this as a proposition, we show the underlying interpolation property: Proposition 8 (Interpolants with ∃∀r-Formula on the Left). Let F be an ∃∀r-formula and let G be a first-order formula such that F |= G. Then there is an effective method to compute from given F and G a formula H such that

1. H is an ∀r-formula. 2. F |= H |= G. 3. V P (H) ⊆ V P (F ) ∩ V P (G). 4. V C (H) ⊆ V C (F ).

Proof. Let G be G conjoined with tautologies such that V C (G ) ⊇ V C (F ), whereas V P (G ) = V P (G) and G ≡ G. Let F be the ∀r-formula obtained from F by renaming the quantified predicates with fresh symbols and dropping the second-order prefix. Compute H as Craig interpolant of F and G with the tableau-based interpolant construction method described in [19] and [11]. Conditions 2.-4. of the proposition follow from the properties of Craig interpolants:

F |= H |= G implies F |= H |= G; from V(H) ⊆ V(F ) ∩ V(G ) it follows, since V P (F ) = V P (F ) and V P (G ) = V P (G), that V P (H) ⊆ V P (F ) ∩ V P (G), and, since V C (F ) = V C (F ) ⊆ V C (G ), that V C (H) ⊆ V C (F ). Condition 1.

follows from particular features of the interpolant construction method of [19,11], where an existential quantifier in the interpolant would not be introduced if the left formula of the interpolation is universal and all individual symbols that occur free in the left formula also occur free in the right formula.

Proposition 9 (Resultants of ∃∀r-Formulas are Universal). A resultant of an ∃∀r formula F is equivalent to an ∀r-formula. Moreover, there is an effective method to compute from F and any given resultant a resultant that is an ∀rformula.

Proof. Assume that G is an arbitrary resultant of F . Thus F ≡ G. Let H be computed from F and G according to Prop. 8. It is easy to verify that H an ∀r-formula and is a resultant of F .

Approximating Resultants of ∃∀r-formulas

The main results of the paper are now shown: For a given ∃∀r-formula F a sequence {G 0 , G 1 , G 2 , . . .} of universal first-order formulas that have (not necessarily strictly) increasing strength and are all entailed by F can be constructed. Any first-order consequence of F is a consequence of some G i . Formula F has a resultant if and only if it is equivalent to some G i . However, only methods are provided to detect that the consequences of a given G i do not include all first-order consequences of F , or, respectively, G i is not equivalent to F . This leads to co-recursive enumerability of the first-order formulas that are equivalent to F or entail F , directly in case F has a resultant, or with respect the firstorder consequences of F in case it has no resultant. Theorem 11 below makes this precise and shows further properties of the formulas G i , some of which are underlying the proofs of the mentioned results. First the theorem is stated and proven formally, then the individual claimed properties are described informally.

The following definition is used in the statement of Theorem 11. It specifies notions of entailment and equivalence of second-order formulas modulo the sets of entailed first-order formulas.

G 0 , G 1 , G 2 , . . . such that (a) The set {G 0 , G 1 , G 2 , . . .} is recursive. (b) G 0 =| G 1 =| G 2 =| . . . =| F. (c) For all i ∈ N 0 it holds that DCA i C ∧ G i ≡ DCA i C ∧ F. (d) For all i, j ∈ N 0 such that i ≤ j it holds that DCA i C ∧ G i |= DCA j C ∧ G j . (e)}. For i ∈ N 0 construct G i as G i def = ∀u 1 . . . ∀u i G i ,

where G i is the resultant, computed by Algorithm 3, of the following formula:

∃p 1 . . . ∃p n a1,...,am∈C∪Ui F [a 1 , . . . , a m ].

The following semantic property of G i , for all i ∈ N 0 , then immediately follows from the construction of G i :

( * ) G i ≡ ∀u 1 . . . ∀u i ∃p 1 . . . ∃p n a1,...,am∈C∪Ui F [a 1 , . . . , a m ].

(a) Follows from the construction of the formulas G i : For any given first-order formula whose universal first-order quantifier prefix has length i ≥ 0 it can be decided whether it is a member of {G 0 , G 1 , G 1 , . . .} by comparing it syntactically with G i .

(b) Let i, j ∈ N 0 that i ≤ j. Since then U j ⊇ U i it follows that a1,...,am∈C∪Uj

F [a 1 , . . . , a m ] |= a1,...,am∈C∪Ui F [a 1 , . . . , a m ].

With ( * ) this implies G j |= G i . To conclude the proof of (b) we show that for an arbitrary number i ∈ N 0 it holds that F |= G i . This can be proven in the following steps, where the last step, the contraction into G i , is justified by ( * ):

F ≡ ∃p 1 . . . ∃p n ∀x 1 . . . ∀x m F |= ∃p 1 . . . ∃p n ∀u 1 . . . ∀u i a1,...,am∈C∪Ui F [a 1 , . . . , a m ] |= ∀u 1 . . . ∀u i ∃p 1 . . . ∃p n a1,...,am∈C∪Ui F [a 1 , . . . , a m ] ≡ G i .

(c) The right-to-left direction follows immediately from (b). The left-to-right direction can be shown in the following steps, where the expansion of G i at the first step is justified by ( * ):

DCA i C ∧ G i ≡ DCA i C ∧. . . ∀x m F ≡ DCA i C ∧ ∃p 1 . . . ∃p n ∀x 1 . . . ∀x m F ≡ DCA i C ∧ F. (d) From i ≤ j it follows that DCA i C |= DCA j C . By (c) we can conclude DCA i C ∧ G i ≡ DCA i C ∧ F |= DCA j C ∧ F ≡ DCA j C ∧ G j . (e)

The right-to-left direction follows immediately from the construction of G i : If G i ≡ F , then G i clearly is a resultant of F that is an ∀r-formula with quantifier prefix length i. The left-to-right direction can be show as follows: Assume that there exists an ∀r-formula H with quantifier prefix length i that is a resultant of F . Since H ≡ F it follows from (c) that

DCA i C ∧ G i ≡ DCA i C ∧ H.

This equivalence matches the precondition of Prop. 7 that lets us deduceG i ≡ H, implying G i ≡ F .

(f ) Follows from (e) and Prop. 9.

(g) The right-to-left direction follows immediately from (b). The left-to-right direction can be shown in the following steps, where the last two equivalences follow from (c) and Prop. 6, respectively: (i) The following algorithm halts for a given i ∈ N 0 if and only if G i ≡ FO F : Let j be an integer variable that satisfies the invariant j > i and is initialized to i + 1. Proceed in a loop: Test whether G i |= G j , that is, whether G i ∧ ¬G j is satisfiable. Since G i and G j are ∀r-formulas, G i ∧ ¬G j is an ∃∀r-formula, and thus decidable. If the test succeeds, then halt, else increment j by 1 and re-enter the loop.

F |= H implies DCA i C ∧ F |= H iff DCA i C ∧ G i |= H iff G i |= H.(

That the algorithm indeed halts if and only if G i ≡ FO F can be shown as follows:

By (b) it holds that F |= G i . Hence G i ≡ FO F if and only G i |= FO F .

Consider the case G i |= FO F and first the subcase where there exists a natural number j > i such that G i |= G j . Then the satisfiability test in the algorithm eventually succeeds and the algorithm halts. Now consider the alternate subcase where no such number j exists. From (b) it then follows that for all l ∈ N 0 it holds that G i |= G l . With (h) we can conclude that it holds for all first-order formula H that if F |= H, then G i |= H. Hence G i |= FO F , contradicting the assumption G i |= FO F made for that case, and thus yielding the alternate subcase impossible. Now consider the case G i |= FO F . From the definition of |= FO it follows that for all j ≥ 0 it holds that if F |= G j , then G i |= G j . With (b) it follows that for all j ≥ 0 it holds that G i |= G j , which implies that the satisfiability test in the algorithm never succeeds and the algorithm thus loops forever.

(j) The following algorithm halts for a given ∃∀r-formula H if and only if H |= FO F : Let j be an integer variable that is initialized to 0. Proceed in a loop: Test whether H |= G j , that is, whether H ∧ ¬G j is satisfiable. Since H is an ∃∀rformula and G i is an ∀r-formula, H ∧ ¬G j is an ∃∀r-formula, and thus decidable. If the test succeeds, then halt, else increment j by 1 and re-enter the loop.

That the algorithm indeed halts if and only if H |= FO F follows since H |= FO F holds if and only if there exists a j ∈ N 0 such that H |= G j , or, equivalently, H |= FO F if and only if for all j ∈ N 0 it holds that H |= G j . The left-to-right direction of this equivalence can be proven as follow: Assume the left side H |= FO F . By expanding |= FO this can be expressed as: For all first-order formulas K it holds that if F |= K, then H |= K. Hence, for all j ∈ N 0 it holds that if F |= G j , then H |= G j . With (b) it follows that for all j ∈ N 0 it holds that H |= G j , that is, the right side. The right-to-left direction of the equivalence to show can be proven as follows: From (h) it follows that for all first-order formulas K it holds that if F |= K, then there exists a k ∈ N 0 such that G k |= K. Hence, if for all i ∈ N 0 it holds that H |= G j , then for all first-order formulas K such that F |= K it holds that H |= K. By contracting into |= FO , the latter statement can be expressed as: If for all j ∈ N 0 it holds that H |= G j , then for H |= FO F , that is, the right-to-left direction of the equivalence to show.

The formulas G i whose existence is claimed by Theorem 11 are constructed from F and i as follows: The first-order quantifiers in F , which are universal, are eliminated by expansion with respect to the members of C and i additional individual symbols u 1 , . . . , u i . Then a resultant of the obtained formula, that is, of the second-order quantifier prefix of F applied to the quantifier-free expansion, is computed. The formula G i is then obtained by prefixing that resultant, which is quantifier-free, with existential first-order quantifiers upon u 1 , . . . , u i .

By property (b), with increasing i the formulas G i get (not necessarily strictly) stronger, and all the formulas G i are entailed by F .

Property (c) holds invariantly for all i ∈ N 0 : Formula G i "under domain closure with i existential individuals" (that is, conjoined with DCA i C ) is equivalent to F under domain closure with the same number of existential individuals. This property is used in the proofs of (d), (e), and (g).

Property (d), which follows from (c), shows that with increasing i the formulas G i under domain closure with i existential objects get (not necessarily strictly) weaker, conversely to the formulas G i themselves, as shown with (b).

Properties (e) and (f ) show necessary and sufficient conditions for the existence of a resultant of F , and in case of existence give a resultant. The first of these, (e), states that F has a resultant that is a universal relational formula with quantifier prefix length i if and only if G i is equivalent to F . This property follows from (c) and Prop. 7. With Prop. 9 it leads to (f ), which states that F has a resultant if and only if it is equivalent to G k for some k ∈ N 0 . The right-to-left directions of the respective equivalences G i ≡ F and G k ≡ F are immediate from (b), such that the existence of a resultant can be also characterized with just the entailments G i |= F and G k |= F , respectively, instead. These entailments have F on their right side, a second-order formula, such that, differently from first-order logic, there is in general no algorithm that halts if and only if such an entailment holds.

Property (g) shows that F and G i have the same ∀r-formulas with quantifier prefix length i as consequences. This follows from (c) and Prop. 6. It is used together with the strengthened Craig interpolation property Prop. 8 to prove (h), by which any first-order consequence of F is a consequence of some G k , and, moreover, such an index k can be effectively computed from F and the given consequence. Property (h) is applied to prove (i) and (j).

Properties (i) and (j) show certain settings where co-recursive enumerability with respect to equivalence and entailment, respectively, of the second-order formula F can be established. Property (i) states that the set of (the index numbers i of) the formulas G i that are different from F with respect to their first-order consequences is recursively enumerable. This means that there is an algorithm that halts for given i if and only if G i is not a formula with the same first-order consequences as F . If F has a resultant, this is equivalent to the statement that G i is not a resultant of F . Property (i) is proven by giving such an algorithm and showing its correctness with referring to (b) and (h). By (b) the negated equivalence G i ≡ FO F can also be expressed as the negated entailment G i |= FO F , which in the case where F has a resultant is equivalent to G i |= F . From the perspective of trying to find a resultant of F or, more generally, a formula with the same first-order consequences as F , the property (i) only justifies a method to exclude failing candidate formulas G i . Property (j) states that the set of (the code numbers in some arithmetization of syntax of) the first-order formulas that do not entail F with respect to its first-order consequences is recursively enumerable. This means that there is an algorithm that halts for a given first-order formula H and only if H |= FO F . Like (i), this property is proven by giving such an algorithm and showing its correctness with referring to (b) and (h). The property justifies a method that detects for a given first-order formula H in the case where F has a resultant that F is not a consequence of H, and in the case where F has no resultant that not all first-order consequences of F are included in the consequences of H.

Discussion and Open Issues

In this section, Craig's work [6] on recursive bases is briefly compared, attempts are made to place the results of Theorem 11 in the context of applications of second-order quantifier elimination, open issues are shown, and potential directions for further research are indicated.

Comparison to Craig's Construction of Recursive Bases. The setting in [6] is more general and comprehensive: First-order formulas under existential second-order quantification are considered without assuming syntactic restrictions and also the case without equality is considered. Our syntactic restriction allows an apparently simpler construction of the approximation formulas G i for which monotonicity (i.e., G 0 =| G 1 =| G 2 =| . . .) directly follows. The restriction also allows to derive further properties of the approximation formulas: They are universal and the length of their quantifier prefix is related to that of entailed universal first-order consequences of the second-order formula. Decidability of specific entailment problems, which is implied by the syntactic restrictions, leads to co-recursive enumerability of certain sets.

Our construction of an approximation formula G i for a second-order formula F = ∃p F where F is first-order involves the construction of a first-order prefix Q i and of an intermediate quantifier-free formula F i such that F = ∃p F |= ∃pQF i |= Q∃pF i ≡ G i . The setting in [6] is the same, except that the first entailment is replaced by an equivalence, that is, it holds that ∃p F ≡ ∃pQF i . Actually, the techniques in [6] seem even to preserve F ≡ QF i . Of course, more weakly constrained transformations, in our case mainly justified through the use of domain closure axioms, are favorable. However, it remains to be investigated in how far the weaker constraints are made possible through the restricted formula class and whether there are associated complexity properties. Entailments Involving Existential Second-Order Formulas. Property (j) of Theorem 11 can be considered in the context of mechanical verification and falsification (that is, existence of an algorithm that terminates in case a statement does hold or does not hold, respectively) of entailments of the forms F |= H and H |= F , where F is a second-order formula with an existential second-order quantifier prefix applied to a first-order formula and H is a first-order formula.

An application of the first form F |= H is to verify that a first-order formula A is semantically independent from predicates p 1 . . . , p n , which can be expressed as ∃p 1 . . . ∃p n A |= A. The first form F |= H is straightforwardly accessible to verification: The set {i | i ∈ N and F |= H i }, where {H 1 , H 2 , H 3 , . . .} is the set of all first-order formulas, is recursively enumerable, which follows from recursive enumerability of the set of (the code numbers of) the valid first-order formulas. The entailment F |= H i is equivalent to the first-order entailment F |= H i , where F is obtained from F by dropping the second-order prefix and renaming the quantified predicates with fresh symbols. The entailment F |= H i can then be expressed as validity of F → H i . Moreover, if F and H i are restricted such that F ∧ ¬H i belong to a decidable formula class, then {i | i ∈ N and F |= H i } is recursive, allowing then also to falsify entailments of the form F |= H.

An application of the second form H |= F is expressing for first-order formulas A and B that A ∧ B is a conservative extension of A as the entailment A |= ∃p 1 . . . ∃p n (A ∧ B), where p 1 , . . . , p n are the predicates that occur in B but not in A. Justified by property (j) of Theorem 11, the second form H |= F (if restricted to ∃∀r-formulas H and ∃∀-formulas F ) can be mechanically falsified.

To sum up, entailments of the form F |= H can always be verified and for formula classes that lead to decidable formulas F ∧ ¬H also be falsified. Property (j) of Theorem 11 extends this, by establishing that also entailments of the form H |= F can be falsified, for certain formula classes. Approximate Resultants with Respect to Quantifier Prefix Length. By property (g) of Theorem 11, the ∃∀r-formula F and the formulas G i constructed from it have the same ∀r-formulas with quantifier prefix length i as consequences. In a sense, the formulas G i can be considered as capturing the first-order semantics of F "up to quantifier prefix length i". This suggests to consider G i as resultant of a generalized form of elimination where not just the existentially quantified predicates are "forgotten", but also the part of the formula's meaning that would be only expressible with quantifier prefix length > i. Exploring this idea is an open issue.

Showing Non-Recursiveness. Properties (i) and (j) of Theorem 11 show co-recursive enumerability of certain sets related to second-order quantifier elimination. It remains to consider the question whether this is the strongest recursiveness property that can be asserted about these sets, that is, to show whether they are actually not recursive. It is expected that this holds because the formula ∃f (x ∧ ¬f y ∧ ∀u∀v (¬f u ∨ f v ∨ ¬nuv) used in [1] to show non-existence of a resultant is actually an ∃∀r-formula.

Potential Approaches for Strengthening the Co-Recursive Enumerability. Of course, it would be of interest, not just for practical application, to strengthen the co-recursive enumerability of finding resultants and verifying entailments shown with properties (i) and (j) of Theorem 11 to recursiveness, at least for special cases. So far, this is an open issue. A direction for further investigation might be trying to determine for certain ∃∀r-formulas the maximally required quantifier prefix length of the resultant. A further direction could be ensuring that a semantic fixed point G k of the sequence G 0 , G 1 , G 2 , . . . subsumes all G i with i ≥ k, that is, for all i ≥ k it holds that G i ≡ G k . This would follow, for example, if for all i, j ∈ N 0 it holds that if G i ≡ G j , then G i+1 ≡ G j+1 . A third direction would be trying to express for all i ≥ k it holds that G i ≡ G k in some algorithmically verifiable way.

Possibly Generalization to Further Formula Classes. Theorem 11 takes decidability of the Bernays-Schönfinkel-Ramsey class (∃∀r-formulas) as basis to derive co-recursive enumerability of problems related to computing elimination resultants of existential second-order quantifiers upon universal relational formulas (∃∀-formulas). This raises the question, whether the techniques applied there can be generalized to further formula classes.

A straightforward transfer appears to be the computation of resultants of formulas of the Bernays-Schönfinkel-Ramsey class under existential second-order quantification, by switching the existential second-and first-order quantifier prefixes and then considering elimination of the inner ∃∀r-formula. However, with this approach a further source of failure to find resultants sneaks in: There are ∃∃∀r-formulas that have a resultant, but where after the suggested quantifier switching the obtained inner ∃∀r-formula does not have a resultant. As an example, consider a formula ∃p (x = a∨F ) that does not have a resultant. However, ∃p ∃x (x = a ∨ F ) clearly has for arbitrary formulas F the resultant . Avoiding Explicit Ground Expansion. The construction of the approximation formulas G i described in the proof of Theorem 11 involves ground expansion of the input formula F . As in instance-based theorem proving, such expansions are useful as a conceptual construct, but their construction should in practice usually be avoided as much as possible. With respect to elimination, a poten-tial approach might be the use of quantifier relativizations to compactly express formulas equivalent to expansions. Possibly the resultant required in the construction of G i can then be computed by applying the elimination method for single ground atoms described in [13] to the finite number of atoms upon which the quantifiers are relativized. Also techniques of [6], where quantified formulas are duplicated by conjoining copies of them, but without performing instantiation, might be relevant here.

Conclusion

We have considered second-order quantifier elimination for a class of relational formulas characterized by a restriction of the quantifier prefix: existential predicate quantifiers followed by universal individual quantifiers. The main original motivation was to transfer instance-based techniques from automated theorem proving to second-order quantifier elimination. The technical result, however, does not indicate an immediate possibility for such a transfer, but gives some insight into the elimination problem for this class: The set of elimination resultants of a given formula and the set of formulas entailing the given second-order formula of that class is co-recursively enumerable. Candidate resultants can be generated, and there is an algorithm that halts on exactly those candidates that are not a resultant. Similarly, there is a method to detect that a given first-order formula does not entail the given second-order formula. By comparing formulas with respect to their first-order consequences, it is possible to express the respective theorem statements in a generalized way that applies to given second-order formulas independently of whether they have a resultant. These results were proven on the basis of small number of formula-based tools used in automated deduction. Actually, the results and involved constructions might be seen as a specialization to a formula class of Craig's setting of determining recursive bases for subtheories of first-order formulas. The hope is that some inspiration and material for further investigation of "eliminability", that is, existence of a resultant, or, more generally, of a formula that is equivalent with respect to first-order consequences, is provided.