-

Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas

TU Dresden

Germany

82 98

We investigate second-order quantifier elimination for a class of formulas characterized by a restriction on the quantifier prefix: existential predicate quantifiers followed by universal individual quantifiers and a relational matrix. For a given second-order formula of this class a possibly infinite sequence of universal first-order formulas that have increasing strength and are all entailed by the second-order formula can be constructed. Any first-order consequence of the second-order formula is a consequence of some member of the sequence. The sequence provides a recursive base for the first-order theory of the second-order formula, in the sense investigated by Craig. The restricted formula class allows to derive further properties, for example that the set of those members of the sequence that are equivalent to the second-order formula, or, more generally, have the same first-order consequences, is co-recursively enumerable. Also the set of first-order formulas that entails the secondorder formula is co-recursively enumerable. These properties are proven with formula-based tools used in automated deduction, such as domain closure axioms, eliminating individual quantifiers by ground expansion, predicate quantifier elimination with Ackermann's Lemma, Craig interpolation and decidability of the Bernays-Schönfinkel-Ramsey class.

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 relational1 monadic2 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 elim1 No function symbols with exception of individual constants. 2 No predicate symbols with arity larger than one.

Copyright c 2017 by the paper's authors ination succeeds seems still scarce [ 12 ]. Ackermann [ 1 ] was the first to publish 3 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 ∀x1 . . . ∀xm∃y1 . . . ∃yn.4 As 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 3 [15, p. 336] and a letter by Ackermann dated 1 November 1928 [ 22 ] suggest that

Löwenheim earlier obtained similar results. 4 That these classes are restricted to relational formulas can be guessed from the symbolic notation in [ 21 ] (actually only the case with a single unquantifed predicate seems considered there) and the observation that if function symbols would be permitted, then the second class would be as expressive as the third one. 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 {G0, G1, G2, . . .} 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 Gi. Formula F has a resultant if and only if it is equivalent to some Gi. The set of the formulas Gi 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 {G0, G1, G2, . . .} 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. 2

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 VP (F ), and the set of individual symbols that occur free in F (commonly termed the set of constants occurring in F ) by VC (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 = t1, . . . , tn is an n-ary sequence of terms, and s is an n-ary predicate or function symbol, we write st for s(t1, . . . , tn), or, in case n = 0, for s, respectively. If t = t1, . . . , tn and u = u1, . . . , un are both n-ary sequences of terms, we write t = u for t1 = u1 ∧ . . . ∧ tn = un and t 6= u for ¬(t = u). If x = x1, . . . , xn is a sequence of individual symbols or of predicates, we write ∃s (∀s, resp.) for ∃s1 . . . ∃sn (∀s1 . . . ∀sn, 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 ∀r-formulas ∃∀r-formulas ∃∀r-formulas empty empty ∃p1 . . . ∃pm

∀x1 . . . ∀xn ∃x1 . . . ∃xm∀y1 . . . ∀yn ∀x1 . . . ∀xn The class ∀r-formulas is the class of universal relational first-order formulas. The class ∃∀r-formulas is also known as Bernays-Schönfinkel-Ramsey class.

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. 3.1

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).

mula F 0 such that 1. F 0 is first-order, 2. F 0 ≡ F , 3. V(F 0) ⊆ V(F ).

A resultant of a second-order formula F is a for

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 0. They are, so-to-speak, “forgotten” in F 0.

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 = x1, . . . , xn be a sequence of distinct individual symbols that do not occur bound in G and do not occur in H. Let H[p 7→ G] stand for H with each occurrence of atoms p(t1, . . . , tn) whose predicate is p replaced by G{x1 7→ t1, . . . , xn 7→ tn}, that is, G under the substitution that maps xi to ti, for i ∈ {1, . . . , n}. If p does not occur with positive polarity in H, then

∃p (∀x(px ∨ G) ∧ H) ≡ H[p 7→ 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 7→ 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 K1 ∨ . . . ∨ Kn, where each disjunct is a conjunction of literals. Propagate the second-order quantifier inwards to obtain the formula ∃p K1 ∨ . . . ∨ ∃p Kn, which is equivalent to ∃p F . Eliminate ∃p in each disjunct individually: Arrange the disjunct in the form

∃p (pt1 ∧ . . . ∧ ptk ∧ ¬pu1 ∧ . . . ∧ ¬pul) ∧ K0, where p does not occur in K0 and k, l ≥ 0. Rewrite this formula to the equivalent formula ∃p (∀x (px ∨ x 6= t1 ∧ . . . ∧ x 6= tk) ∧ ¬pu1 ∧ . . . ∧ ¬pul) ∧ K0, (i) form

∃p1 . . . ∃pm∃x1 . . . ∃xn F, 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 (u1 6= t1 ∧ . . . ∧ u1 6= tk) ∧ . . . ∧ (ul 6= t1 ∧ . . . ∧ ul 6= tk) ∧ K0.

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 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 ∃x1 . . . ∃xn∃p1 . . . ∃pn F , obtained by switching the firstand second-order quantifier prefix. If F 0 is a resultant of ∃p1 . . . ∃pn F , obtained for example with Algorithm 3, then ∃x1 . . . ∃xnF 0 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 Ki a different formula (x 6= t1 ∧ . . . ∧ x 6= tk) 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 ]. 3.2

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 = {c1, . . . , cn} be a nonempty set of individual symbols, let k ∈ N0, and assume that x, y1, . . . , yk are individual symbols that are not in C. Define

DCAkC d=ef ∃y1 . . . ∃yk∀x (x = y1 ∨ . . . ∨ x = yk ∨ x = c1 ∨ . . . ∨ x = cn). 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 VC (F ) 6= ∅ is equivalent to DCA0C ∧ F , where C = VC (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 ⊇ VC (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 I0 such that 1. I0 |= DCAkC ∧ F. 2. For all ground atoms A constructed from predicates in F and individual symbols in C it holds that I |= A iff I0 |= 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 VC (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 ⊇ VC (F ) ∪ VC (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 if DCAkC ∧ F |= G, then F |= G.

Proof. Assume the left side of the proposition, that is, DCAkC ∧ F |= G. Assume further that the right side does not hold. Then there exists an interpretation I such that I |= F ∧ ¬G. Observe that F ∧ ¬G is equivalent to an ∃∀r-formula with k existential quantifiers. Thus, by Prop. 5 there exists an interpretation I0 such that I0 |= DCAkC ∧ F ∧ ¬G. With the assumption DCAkC ∧ F |= G it then follows that I0 |= G ∧ ¬G, which contradicts with I0 being an interpretation. tu 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 ⊇ VC (F ) ∪ VC (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 DCAkC ∧ F

≡ DCAkC ∧ G, then F ≡ G.

Proof. Follows from Prop. 6.

tu 3.3

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. VP (H) ⊆ VP (F ) ∩ VP (G). 4. VC (H) ⊆ VC (F ).

Proof. Let G0 be G conjoined with tautologies such that VC (G0) ⊇ VC (F ), whereas VP (G0) = VP (G) and G0 ≡ G. Let F 0 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 0 and G0 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 0 |= H |= G0 implies F |= H |= G; from V(H) ⊆ V(F 0) ∩ V(G0) it follows, since VP (F 0) = VP (F ) and VP (G0) = VP (G), that VP (H) ⊆ VP (F ) ∩ VP (G), and, since VC (F 0) = VC (F ) ⊆ VC (G0), that VC (H) ⊆ VC (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. tu 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 . tu

Approximating Resultants of ∃∀r-formulas The main results of the paper are now shown: For a given ∃∀r-formula F a sequence {G0, G1, G2, . . .} 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 Gi. Formula F has a resultant if and only if it is equivalent to some Gi. However, only methods are provided to detect that the consequences of a given Gi do not include all first-order consequences of F , or, respectively, Gi 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 Gi, 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.

Definition 10 (Entailment and Equivalence Modulo First-Order Con

sequences). For second-order formulas F, G define

These notions are helpful to express properties of second-order formulas that possibly have no resultant. Their meaning is identical to the standard notions of entailment and equivalence, respectively, if no such second-order formulas are involved: If G is a first-order formula or a second-order formula that has a resultant, then, also in the case where F is a second-order formula, it holds that F |=FO G if and only if F |= G. If each of F and G is first-order or has a resultant, then F ≡FO G if and only if F ≡ G.

Theorem 11 (Approximating Resultants of ∃∀r-formulas). Let F be an ∃∀r-formula and let C ⊇ VC (F ) be a nonempty set of individual constants. Then there exist ∀r-formulas G0, G1, G2, . . . such that (a) The set {G0, G1, G2, . . .} is recursive. (b) G0 =| G1 =| G2 =| . . . =| F. (c) For all i ∈ N0 it holds that DCAiC ∧ Gi ≡ DCAi (d) For all i, j ∈ N0 such that i ≤ j it holds that DCCA∧iC F∧. Gi |= DCAjC ∧ Gj . (e) For all i ∈ N0 it holds that F has a resultant that is an ∀r-formula with quantifier prefix length i if and only if Gi ≡ F. (f ) F has a resultant if and only if there exists a k ∈ N0 such that Gk ≡ F. (g) For all i ∈ N0 and ∀r-formulas H with quantifier prefix length i it holds that

F |= H if and only if Gi |= H. (h) There is an effective method to compute from F and a given first-order formula H such that F |= H a number k ∈ N0 such that Gk |= H. (i) The set {i | i ∈ N0 and Gi ≡FO F } is co-recursively enumerable. (j) The set {i | i ∈ N and Hi |=FO F }, where {H1, H2, H3, . . .} is the set of all ∃∀r-formulas, is co-recursively enumerable (under assumption of a countable vocabulary).

Proof. Let

F = ∃p1 . . . ∃pn ∀x1 . . . ∀xm F 0, where F 0 is quantifier-free. Let F 0[a1, . . . , am] denote F 0 with xi replaced by some individual symbol ai, for all i ∈ {1, . . . , m}. Let U be a set {u1, u2, u3, . . .} of individual symbols that are not in C and let Ui denote {u1, . . . , ui}. For i ∈ N0 construct Gi as

Gi d=ef ∀u1 . . . ∀ui G0i, where G0i is the resultant, computed by Algorithm 3, of the following formula:

The following semantic property of Gi, for all i ∈ N0, then immediately follows from the construction of Gi: (∗)

Gi ≡ ∀u1 . . . ∀ui ∃p1 . . . ∃pn Va1,...,am∈C∪Ui F 0[a1, . . . , am].

(a) Follows from the construction of the formulas Gi: 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 {G0, G1, G1, . . .} by comparing it syntactically with Gi.

(b) Let i, j ∈ N0 that i ≤ j. Since then Uj ⊇ Ui it follows that

^ a1,...,am∈C∪Uj

F 0[a1, . . . , am] |=

^ a1,...,am∈C∪Ui

F 0[a1, . . . , am].

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

F ≡ ∃p1 . . . ∃pn ∀x1 . . . ∀xm F 0 |= ∃p1 . . . ∃pn ∀u1 . . . ∀ui V F 0[a1, . . . , am] |= ∀u1 . . . ∀ui ∃p1 . . . ∃pn Vaa11,,......,,aamm∈∈CC∪∪UUii F 0[a1, . . . , am] (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 Gi at the first step is justified by (∗):

DCAiC ∧ Gi ≡ DCAiC ∧ ∀u1 . . . ∀ui ∃p1 . . . ∃pn Va1,...,am∈C∪Ui F 0[a1, . . . , am] ≡ ∃u1 . . . ∃ui DCA0C∪Ui ∧

∀u1 . . . ∀ui ∃p1 . . . ∃pn Va1,...,am∈C∪Ui F 0[a1, . . . , am] |= ∃u1 . . . ∃ui (DCA0 a1,...,am∈C∪Ui F 0[a1, . . . , am]) ≡ ∃u1 . . . ∃ui DCA0CC∪∪UUii∧∧∃∃pp11. .. .. .∃∃ppnn∀xV1 . . . ∀xm F 0 DCA(diC)∧FGroim≡ iDC≤AiCj ∧itFfo|=lloDwCsAtjCha∧tFD≡CADiCCA|=jC ∧DCGAj jC.. By (c) we can conclude (e) The right-to-left direction follows immediately from the construction of Gi: If Gi ≡ F , then Gi 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

DCAiC ∧ Gi ≡ DCAiC ∧ H.

This equivalence matches the precondition of Prop. 7 that lets us deduce Gi ≡ H, implying Gi ≡ 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 ∈ N0 if and only if Gi 6≡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 Gi 6|= Gj , that is, whether Gi ∧ ¬Gj is satisfiable. Since Gi and Gj are ∀r-formulas, Gi ∧ ¬Gj 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 Gi 6≡FO F can be shown as follows: By (b) it holds that F |= Gi. Hence Gi 6≡FO F if and only Gi 6|=FO F . Consider the case Gi 6|=FO F and first the subcase where there exists a natural number j > i such that Gi 6|= Gj . 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 ∈ N0 it holds that Gi |= Gl. With (h) we can conclude that it holds for all first-order formula H that if F |= H, then Gi |= H. Hence Gi |=FO F , contradicting the assumption Gi 6|=FO F made for that case, and thus yielding the alternate subcase impossible. Now consider the case Gi |=FO F . From the definition of |=FO it follows that for all j ≥ 0 it holds that if F |= Gj , then Gi |= Gj . With (b) it follows that for all j ≥ 0 it holds that Gi |= Gj , 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 6|=FO F : Let j be an integer variable that is initialized to 0. Proceed in a loop: Test whether H 6|= Gj , that is, whether H ∧ ¬Gj is satisfiable. Since H is an ∃∀rformula and Gi is an ∀r-formula, H ∧ ¬Gj 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 6|=FO F follows since H 6|=FO F holds if and only if there exists a j ∈ N0 such that H 6|= Gj , or, equivalently, H |=FO F if and only if for all j ∈ N0 it holds that H |= Gj . 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 ∈ N0 it holds that if F |= Gj , then H |= Gj . With (b) it follows that for all j ∈ N0 it holds that H |= Gj , 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 ∈ N0 such that Gk |= K. Hence, if for all i ∈ N0 it holds that H |= Gj , 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 ∈ N0 it holds that H |= Gj , then for H |=FO F , that is, the right-to-left direction of the equivalence to show. tu

The formulas Gi 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 u1, . . . , ui. 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 Gi is then obtained by prefixing that resultant, which is quantifier-free, with existential first-order quantifiers upon u1, . . . , ui.

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

Property (c) holds invariantly for all i ∈ N0: Formula Gi “under domain closure with i existential individuals” (that is, conjoined with DCAiC ) 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 Gi under domain closure with i existential objects get (not necessarily strictly) weaker, conversely to the formulas Gi 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 Gi 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 Gk for some k ∈ N0. The right-to-left directions of the respective equivalences Gi ≡ F and Gk ≡ F are immediate from (b), such that the existence of a resultant can be also characterized with just the entailments Gi |= F and Gk |= 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 Gi 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 Gk, 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 Gi 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 Gi is not a formula with the same first-order consequences as F . If F has a resultant, this is equivalent to the statement that Gi 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 Gi 6≡FO F can also be expressed as the negated entailment Gi 6|=FO F , which in the case where F has a resultant is equivalent to Gi 6|= 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 Gi.

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 6|=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. 5

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 Gi for which monotonicity (i.e., G0 =| G1 =| G2 =| . . .) 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 Gi for a second-order formula F = ∃p F 0 where F 0 is first-order involves the construction of a first-order prefix Qi and of an intermediate quantifier-free formula Fi0 such that F = ∃p F 0 |= ∃pQFi0 |= Q∃pFi0 ≡ Gi. The setting in [ 6 ] is the same, except that the first entailment is replaced by an equivalence, that is, it holds that ∃p F 0 ≡ ∃pQFi0. Actually, the techniques in [ 6 ] seem even to preserve F 0 ≡ QFi0. 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 p1 . . . , pn, which can be expressed as ∃p1 . . . ∃pn A |= A. The first form F |= H is straightforwardly accessible to verification : The set {i | i ∈ N and F |= Hi}, where {H1, H2, H3, . . .} 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 |= Hi is equivalent to the first-order entailment F 0 |= Hi, where F 0 is obtained from F by dropping the second-order prefix and renaming the quantified predicates with fresh symbols. The entailment F 0 |= Hi can then be expressed as validity of F 0 → Hi. Moreover, if F and Hi are restricted such that F 0 ∧ ¬Hi belong to a decidable formula class, then {i | i ∈ N and F |= Hi} 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 |= ∃p1 . . . ∃pn(A ∧ B), where p1, . . . , pn 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 Gi constructed from it have the same ∀r-formulas with quantiefir prefix length i as consequences. In a sense, the formulas Gi can be considered as capturing the first-order semantics of F “up to quantifier prefix length i”. This suggests to consider Gi 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 Gk of the sequence G0, G1, G2, . . . subsumes all Gi with i ≥ k, that is, for all i ≥ k it holds that Gi ≡ Gk. This would follow, for example, if for all i, j ∈ N0 it holds that if Gi ≡ Gj , then Gi+1 ≡ Gj+1. A third direction would be trying to express for all i ≥ k it holds that Gi ≡ Gk 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 Gi 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 potential approach might be the use of quantifier relativizations to compactly express formulas equivalent to expansions. Possibly the resultant required in the construction of Gi 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. 6

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.

Acknowledgments. This work was supported by DFG grant WE 5641/1-1.

1. Ackermann , W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik . Math. Ann. 110 , 390 - 413 ( 1935 )

2. Baumgartner , P. , Thorstensen , E.: Instance based methods - A brief overview . KI 24 ( 1 ), 35 - 42 ( Apr 2010 )

3. Behmann , H.: Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem . Math. Ann. 86 ( 3-4 ), 163 - 229 ( 1922 )

4. Börger , E. , E. , Grädel , Gurevich, Y. : The Classical Decision Problem . Springer ( 1997 )

5. Conradie , W.: On the strength and scope of DLS . J. Applied Non-Classical Logic 16 ( 3-4 ), 279 - 296 ( 2006 )

6. Craig , W.: Bases for first-order theories and subtheories . J. Symb. Log . 25 ( 2 ), 97 - 142 ( 1960 )

7. Doherty , P. , Łukaszewicz , W. , Szałas , A. : Computing circumscription revisited: A reduction algorithm . J. Autom. Reasoning 18 ( 3 ), 297 - 338 ( 1997 )

8. Doherty , P. , Łukaszewicz , W. , Szałas , A.: General domain circumscription and its effective reductions . Fundamenta Informaticae 36 , 23 - 55 ( 1998 )

9. Eberhard , S. , Hetzl , S. , Weller , D. : Boolean unification with predicates . J. Logic and Computation 27 ( 1 ), 109 - 128 ( 2017 )

10. Fermüller , C. , Leitsch , A. , Hustadt , U. , Tammet , T. : Resolution decision procedures . In: Robinson, A. , Voronkov , A . (eds.) Handb. of Autom. Reasoning , vol. 2 , pp. 1793 - 1849 . Elsevier ( 2001 )

11. Fitting , M. : First-Order Logic and Automated Theorem Proving . Springer, 2nd edn. ( 1995 )

12. Gabbay , D.M. , Schmidt , R.A. , Szałas , A. : Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications . College Publications ( 2008 )

13. Lin , F. , Reiter , R.: Forget It! In: Working Notes, AAAI Fall Symposium on Relevance. pp. 154 - 159 ( 1994 )

14. Löwenheim , L. : Über Möglichkeiten im Relativkalkül . Math. Ann. 76 , 447 - 470 ( 1915 )

15. Löwenheim , L. : Funktionalgleichungen im Gebietekalkül und Umformungsmöglichkeiten im Relativkalkül . History of Philosophy and Logic 28 , 305 - 336 ( 2007 ), assumed to be written in 1935 [20]

16. Reiter , R.: Deductive quastion-answering on relational databases . In: Gallaire, H. , Minker , J . (eds.) Logic and Databases, pp. 149 - 178 . Plenum Press, New York ( 1978 )

17. Schröder , E.: Vorlesungen über die Algebra der Logik , vol. 1 . Teubner ( 1890 )

18. Skolem , T. : Untersuchungen über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme welche gewisse Klassen von Aussagen betreffen . Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(3) ( 1919 )

19. Smullyan , R.M. : First-Order Logic . Springer, New York ( 1968 ), also republished with corrections by Dover publications , New York, 1995

20. Thiel , C. : A short introduction to Löwenheim's life and work and to a hitherto unknown paper . History of Philosophy and Logic 28 , 289 - 302 ( 2007 )

21. Van Benthem , J. , Doets , K. : Higher-order logic . In: Handbook of Philosophical Logic , vol. 1 , pp. 189 - 243 . Springer, second edn. ( 2001 )

22. Wernhard , C. : Heinrich Behmann's contributions to second-order quantifier elimination . Tech. Rep. KRR 15-05 ,

Dresden ( 2015 )

23. Wernhard , C. : Second-order quantifier elimination on relational monadic formulas - A basic method and some less expected applications . In: TABLEAUX 2015. LNCS (LNAI) , vol. 9323 , pp. 249 - 265 . Springer ( 2015 )

24. Wernhard , C. : The Boolean solution problem from the perspective of predicate logic . In: FroCoS 2017 . LNCS (LNAI) , vol. 10483 , pp. 333 - 350 ( 2017 )