It is a classical result that the monadic fragment of secondorder logic admits elimination of second-order quantifiers. Recently, the separated fragment (SF) of first-order logic has been introduced. SF generalizes the monadic first-order fragment without equality, while preserving decidability of the satisfiability problem. Therefore, it is a natural question to ask whether SF also admits elimination of second-order quantifiers. Interestingly, already Ackermann answered this question in the negative as far as full SF with unrestricted occurrences of second-order quantifiers is concerned. However, with appropriate restrictions on the syntax of a second-order version of SF, one could hope to define a substantial extension of the monadic fragment that admits second-order quantifier elimination. The present note is about preliminary results of ongoing research in this direction. As a first positive result a restricted second-order version of SF is defined that admits the elimination of at least one existential second-order quantifier. The elimination of existential second-order quantifiers from a monadic sentence without equality constitutes a special case of the methods presented here.
It is a classical result that the monadic fragment of second-order logic admits
elimination of second-order quantifiers. This was discovered by L¨owenheim [
Recently, the separated fragment (SF) of first-order logic has been
introduced [
As SF generalizes the monadic first-order fragment without equality while
retaining a decidable satisfiability problem, it is natural to ask whether a
secondorder version of SF admits elimination of second-order quantifiers. Interestingly,
already Ackermann gave a negative answer to this question. In an article from
1935 [
Although Ackermann’s observation seems to be discouraging, it only means that there is, apparently, no straight-forward way of extending the quantifierelimination techniques that work for second-order monadic logic to the separated fragment. The purpose of this note is to present certain syntactic restrictions that allow the elimination of existentially quantified unary predicate symbols in separated formulas. The presented results are of a preliminary character and are not yet fully developed. They provide only a first hint at some directions that might be worth following in future work.
In Section 2 we present the used notation and some basic results. A definition of the separated fragment is given in Section 3. The main result is developed in Section 4 and concisely formulated in Theorem 8. Finally, Section 5 concludes with a discussion of the results and future directions. 2
We consider second-order logic formulas with equality. We call a formula relational if it contains neither function nor constant symbols. In all formulas, if not explicitly stated otherwise, we tacitly assume that no variable occurs freely and bound at the same time and that no variable is bound by two different occurrences of quantifiers. For convenience, we sometimes identify tuples x¯ of variables with the set containing all the variables that occur in x¯. By vars(ϕ) we denote the set of all variables occurring in ϕ.
The symbol |= denotes the is-a-model-of relation as well as semantic entailment of formulas, i.e. ϕ |= ψ holds whenever for every structure A and every variable assignment β, A, β |= ϕ entails A, β |= ψ. The symbol |=| denotes semantic equivalence of formulas, i.e. ϕ |=| ψ holds whenever ϕ |= ψ and ψ |= ϕ.
The following are standard lemmas that we simply add for completeness. Lemma 1 (Miniscoping). Let ϕ, ψ, χ be formulas, and assume that x and y do not occur freely in χ. We have the following equivalences, where ◦ ∈ {∧, ∨}: (i) ∃y.(ϕ ∨ ψ) |=| (∃y.ϕ) ∨ (∃y.ψ) (ii) ∀x.(ϕ ∧ ψ) |=| (∀x.ϕ) ∧ (∀x.ψ) (iii) ∃y.(ϕ ◦ χ) |=| (∃y.ϕ) ◦ χ (iv) ∀x.(ϕ ◦ χ) |=| (∀x.ϕ) ◦ χ Lemma 2. Let ψ[t] be some second-order formula in which the term t occurs. Let x be some first-order variable that does not occur in ψ[t]. Then, ψ[t] is semantically equivalent to ∀x. x = t → ψ[x], where ψ[x] is derived from ψ[t] by replacing every occurrence of t with the variable x. 3
Consider a second-order formula ϕ. We say that two disjoint sets of first-order variables X and Y are separated in ϕ if and only if for every atom A in ϕ we have vars(A) ∩ X = ∅ or vars(A) ∩ Y = ∅.
The following definition of the separated fragment is a slightly simplified
version of the fragment investigated in [
Definition 3 (Separated fragment (SF)). The separated fragment (SF) of first-order logic consists of all relational first-order sentences with equality that are of the form ∃z¯ ∀x¯1∃y¯1 . . . ∀x¯n∃y¯n. ψ, in which ψ is quantifier free, and in which the two sets x¯1 ∪ . . . ∪ x¯n and y¯1 ∪ . . . ∪ y¯n are separated. The tuples z¯ and y¯n may be empty, i.e. the quantifier prefix does not have to start with an existential quantifier and it does not have to end with an existential quantifier either.
Notice that the variables in z¯ are not subject to any restriction concerning their occurrences.
It is not hard to see that SF generalizes the Bernays–Sch¨onfinkel–Ramsey fragment (relational ∃ ∀
∗ ∗ prenex formulas with equality) and the monadic
firstorder fragment without equality (see [
As already mentioned in the introduction, it is known that the satisfiability
problem for SF sentences (SF-Sat ) is decidable and non-elementary [
Lemma 4. Let ϕ := ∀x¯1∃y¯1 . . . ∀x¯n∃y¯n. ψ(x¯, y¯, z¯) be a relational first-order formula in which ψ is quantifier free and the sets x¯ := x¯1 ∪ . . . ∪ x¯n and y¯ := y¯1 ∪ . . . ∪ y¯n are separated. Moreover, we assume that every variable occurring in the quantifier prefix and in z¯ also occurs in the matrix ψ.
Let xe1, . . . , xem1 ⊆ x¯ and ye1, . . . , yem2 ⊆ y¯ be partitions of the sets x¯ and y¯, respectively, such that the xe1, . . . , xem1 , y1, . . . , yem2 are nonempty, pairwise e disjoint, and pairwise separated in ϕ. Then, ϕ is equivalent to a finite disjunction of formulas of the form where the Kk` and the Lij are literals whose atoms are renamed variants of atoms that occur in ϕ. Moreover, any two sets xe0k01 , x00 ei2 ek2 with k1 6= k2, yei001 , y00 with i1 6= i2, and xe0k0, yei00 are separated in the resulting formula.
Proof. The proof is an adaptation of the proof of Lemma 12 in [
Claim I (Lemma 11 in [
Let I and Ji, i ∈ I, be sets that are finite, nonempty, and pairwise disjoint. The elements of these sets serve as indices. Let ∃v¯. ^ i∈I χi(u¯) ∨ _ ηk(v¯, u¯) k∈Ji We transform ϕ into an equivalent CNF formula of the form where I and the Ji are finite, pairwise disjoint sets of indices, the subformulas χi are disjunctions of literals, and the Lk are literals. By Claim I, we can construct an equivalent formula of the form
S ⊆ I i∈S
S 6= ∅ ϕ0 := ∀x¯1∃y¯1 . . . ∀x¯n. ^ _ χi(x¯) ∨ _ f∈F ∃y¯n. ^ ηf(i)(y¯) i∈S where F is the set of all selectors over the index sets Ji, i ∈ I. Applying miniscoping (Lemma 1), we move inward the universal quantifier block ∀x¯n and thus obtain ϕ00 := ∀x¯1∃y¯1 . . . ∃y¯n−1. ^
S ⊆ I S 6= ∅ ∀x¯n. _ χi(x¯) ∨ _ ∃y¯n. ^ ηf(i)(y¯) .
i∈S f∈F i∈S be some first-order formula where the χi and the ηk denote arbitrary subformulas that we treat as indivisible units in what follows. We say that f : I → Si∈I Ji is a selector if for every i ∈ I we have f (i) ∈ Ji. We denote the set of all selectors of this form by F .
Then, the above formula is equivalent to
^ S ⊆ I i∈S S 6= ∅ _ χi(u¯) ∨ _ ∃v¯. ^ ηf(i)(v¯, u¯) .
f∈F i∈S We now iterate these two steps in an alternating fashion until all quantifier blocks have been moved inwards in the described way. The constituents of the result ϕ(3) := Vq χ(q3) ∨ Wp ηq(3p) of this process have the form χ(q3) = ∀x¯1. _ ∀x¯2. _ . . . _ ∀x¯n.
`1 `2 `n−1
_ i∈S`1,...,`n−1 χi(x¯) . . . where the S`1,...,`n−1 are certain subsets of I and the χi are still disjunctions of literals, and ηq(3p) = ∃y¯1. ^ ∃y¯2. ^ . . . ^ ∃y¯n.
`1 `2 `n−1
^ k∈J`1,...,`n−1
Lk(y¯) . . . where the J`1,...,`n−1 are certain subsets of Si∈I Ji.
By definition of the sets xe1, . . . , xem1 , which are pairwise separated in the χ(q3), we can rewrite every χ(q3) into the following form by regrouping the inner disjuncts: χ(q4) = ∀x¯1. _ ∀x¯2. _ . . . _ ∀x¯n.
_ i0=1,...,m1
χ0`¯i0 (xei0 ) . . . `1 `1 `2 `2 `n−1 `n−1 where the χ0`¯i0 are (possibly empty) disjunctions of literals. Analogously, we rewrite every ηq(3p) into the form ηq(4p) = ∃y¯1. ^ ∃y¯2. ^ . . . ^ ∃y¯n.
^ j0=1,...,m2 η`0¯j0 (yej) . . . = | | = | | `1 `1 . . . _ _ where the η`0¯j0 are (possibly empty) conjunctions of literals.
We then observe the following equivalences, starting from χ(q4): ∀x¯1. _ ∀x¯2. _ . . . _ ∀x¯n.
`1 `2
`n−1 |=| ∀x¯1. _ ∀x¯2. _ . . . _
_ i0=1,...,m1
_ |=| ∀x¯1. _ ∀x¯2. _ . . .
`2 `2 `n−1 i0=1,...,m1
_ _ i0=1,...,m1 `0n−1
χ0`¯i0 (xei0 ) . . . ∀(x¯n ∩ xei0 ). χ0`¯i0 (xei0 ) . . .
∀(x¯n ∩ xei0 ). χ0`¯0i0 (xei0 ) . . . ∀(x¯1 ∩ xei0 ). _ ∀(x¯2 ∩ xei0 ). _ . . . _ `01 `02
`0n−1 ∀xe0i0 . χ0i00 (xe0i0 ) , ∀(x¯n ∩ xei0 ). χ0`¯0i0 (xei0 ) . . . where the ηj000 are conjunctions of literals. formula ϕ(4) of the form ϕ(4) = ^
_ q
i0=1,...,m1 where the χ0i00 are disjunctions of literals. Before moving universal quantifiers outwards in the last step of the above transformation, bound variables are renamed such that all quantifiers bind pairwise distinct variables. Analogously, we have ηq(4p) |=|
^ Consequently, we have rewritten ϕ(3) = Vq χ(q3) ∨ Wp ηq(3p) into an equivalent ∀xe0i0 . χ0q0i0 (xe0i0 ) ∨ _
^ p j0=1,...,m2 ∃yej00 . ηq00pj0 (yei00 ) .
After renaming bound variables again such that all quantifiers bind pairwise distinct variables, we transform ϕ(4) into an equivalent formula that is a disjunction of formulas of the form ^ ∀xe0k0. _ Kk`(xe0k0) k ` ∧ ^ ∃yei00. ^ Lij(yei00) .
i j
The just proven lemma will provide the syntactic transformations necessary to eliminate second-order quantifiers that occur in a separated formula under certain conditions.
Example 5. We have already mentioned the following SF sentence in the introduction: ϕ := ∀x1∃y1∀x2∃y2. R(x1, x2) ↔ Q(y1, y2). As indicated by Lemma 4, nested alternating quantifiers can be transformed away. An intermediate result of this process is ∀x1∃y1.
∀x2. R(x1, x2) ∨ ∃y2. ¬Q(y1, y2) ∧ ∀x2. ¬R(x1, x2) ∨ ∃y2. Q(y1, y2) .
Continuing the transformation process, we eventually obtain ∃y1y2y3. Q(y1, y2) ∧ ¬Q(y1, y3) ∀x1x2. R(x1, x2) ∧ ∃y1y2. Q(y1, y2) ∀x1x2. ¬R(x1, x2) ∧ ∃y1y2. ¬Q(y1, y2) ∀x1x2x3. R(x1, x2) ∨ ¬R(x1, x3) ∧ ∃y1y2. Q(y1, y2) ∧ ∃y3y4. ¬Q(y3, y4) which is equivalent to ϕ but does not contain any quantifier alternation.
In this section we formulate syntactic restrictions that enable the elimination of second-order quantifiers over unary predicates from sentences that belong to the separated fragment. The notion of separation of sets of variables in a formula plays a central role in our criterion. However, this time it is not only of interest that universal variables are separated from existential variables. It is rather of importance that within each set of non-separated variables there is at most one that occurs as the argument of the predicate symbol that is bound by the quantifier we intend to eliminate.
Lemma 6. Let ϕ := ∀x¯1∃y¯1 . . . ∀x¯n∃y¯n. ψ(x¯, y¯, z¯) be a relational first-order formula in which ψ is quantifier free and the sets x¯ := x¯1 ∪ . . . ∪ x¯n and y¯ := y¯1 ∪ . . . ∪ y¯n are separated. We assume that every variable occurring in the quantifier prefix and in z¯ also occurs in the matrix ψ.
Let xe1, . . . , xem1 ⊆ x¯ and ye1, . . . , yem2 ⊆ y¯ be partitions of the sets x¯ and y¯, respectively, such that the xe1, . . . , xem1 , ye1, . . . , yem2 are nonempty, pairwise disjoint, and pairwise separated in ϕ. Let P be a unary predicate symbol satisfying the following conditions: (1) For every set xi, 1 ≤ i ≤ m1, there is at most one variable xi∗ ∈ xei for which e ϕ contains atoms P (xi∗). (2) For every set yi, 1 ≤ i ≤ m2, there is at most one variable yi∗ ∈ yei for which e ϕ contains atoms P (yi∗).
Then ∃P. ϕ is equivalent to a finite disjunction of formulas of the form where (a) the χk1 and the χ0k2 are disjunctions of literals and the ηi1 and the ηi02 are conjunctions of literals, (b) all the atoms in θ and in the χk1 , χ0k2 , ηi1 , and ηi2 are renamed variants of atoms that occur in ϕ and do not contain the predicate symbol P , and (c) the variables z`∗1 , z`∗2 are pairwise distinct and stem from z¯.
Proof. By Lemma 4, we know that ϕ can be rewritten to an equivalent formula that is a finite disjunction of formulas in which no universal quantifier lies within the scope of an existential quantifier and vice versa. We apply this transformation to ϕ and obtain a formula as described in Lemma 4. In the next step, we isolate atoms that exclusively contain variables from z¯, narrow the scopes of first-order quantifiers so that these atoms are not within their scopes anymore, and transform the resulting formulas into a formula ϕ0 that is a disjunction of formulas of the form ^ ∀xe0k. _ Kk`(xe0k, z¯) k ` ∧ ^ ∃yei0. ^ Lij (yei0, z¯) i j ∧ ^ Mr(z¯) , r where the Kk` and the Lij are literals whose atoms are renamed variants of atoms that occur in ϕ and contain at least one variable from some xe0k or yei0. The Mr are literals whose atoms occur in ϕ and contain exclusively variables from z¯. Moreover, any two sets xe0k1 , xe0k2 with k1 6= k2, yei01 , y0 ei ei2 with i1 6= i2, and xe0k, y0 are separated in ϕ0. By inspection of the transformations performed in the proof of Lemma 4, we observe that Conditions (1) and (2) are preserved such that they also apply to the sets xe0k and yei0 with respect to variables x∗k and yi∗, respectively.
This enables us to regroup the disjunctions and conjunctions in the constituents of ϕ0 such that each of these disjuncts has the form ^ ∀xe0k0 . _ Kk0`0 (xe0k0 , z¯) ∨ [¬]P (x∗k0 ) k0 `0 ∧ ∧ ^ ∃yei00 . ^ Li0j0 (yei00 , z¯) ∧ [¬]P (yi∗0 ) i0 j0 ^ Mr0 (z¯) ∧ ^[¬]P (zq∗) , r0 q where the literals Kk0`0 , Li0j0 , and Mr0 do not contain the predicate symbol P . The variables zq∗ stem from z¯. Moreover, we replace disjuncts (conjuncts) which contain two literals P (v) and ¬P (v) with the logical constant true (false). Having this, it only remains to regroup conjuncts and distribute the existential quantifier ∃P over the topmost disjunction, in order to obtain the formula advertised in the lemma. tu
The formula resulting from the lemma gives us the right starting point for the
elimination of the second-order quantifier ∃P from a formula. Before we elaborate
on this, we present the lemma that we shall employ for elimination.
Lemma 7 (Basic elimination lemma, see [
Consider a formula ϕ := ∀x¯1∃y¯1 . . . ∀x¯n∃y¯n.ψ(x¯, y¯, z¯) as described in Lemma 6.
Moreover, let there be sets x1, . . . , xem1 and ye1, . . . , yem2 and a unary predicate
e
symbol P as described in the lemma. Then, Lemma 6 stipulates the existence of
a formula equivalent to ϕ that is a disjunction of formulas of the form
θ(z¯) ∧ ∃P. ^
k1
∧
i1
in which we can eliminate the quantifier ∃P as follows. The shape of the above
formula is very similar to what Behmann called “Eliminationshauptform” in [
=:{χz∗k1 ∧ ∧ ∧ ^ ∀x∗k2 . ∀(xe0k2 \{x∗k2 }). χk2 (xe0k2 , z¯) ∨ ¬P (x∗k2 ) k2 | }
=:{χz∗k2 ^ ∃yi∗1 . ∃(yei01 \{yi∗1 }). ηi01 (yei01 , z¯) ∧ P (yi∗1 ) i1 | } ^ ∃yi∗2 . ∃(yei02 \{yi∗2 }). ηi02 (yei02 , z¯) ∧ ¬P (yi∗2 ) i2 | } =:{ηzi∗1 =:{ηzi∗2 ∧ ^ P (z`∗1 ) ∧ ^ ¬P (z`∗2 ) `1
`2 Next, we treat the subformulas χ∗k and ηi∗ as indivisible units, move universal quantifiers outwards that occur in different conjuncts (and merge them while doing so), pull first-order existential quantifiers outwards (without merging them), and rename the variables that are bound by the moved quantifiers. Moreover, we reorder the conjunctions in the scope of the quantifier blocks ∃u¯ and ∃v¯. θ(z¯) ∧ ∃P. ∀x.
∧ ∧ ∧ ∧ | ∀x. ∃u¯. ∃v¯. ∧
^ ¬P (vi2 ) ^ P (z`∗1 ) ∧ ^ ¬P (z`∗2 ) In what follows we treat the χ1∗, χ2∗ and η1∗, η2∗ as indivisible units. One more step remains to establish a kind of “Eliminationshauptform”. We move the quantifier blocks ∃u¯ and ∃v¯ outwards over the ∃P , reorder the conjuncts within the scope of ∃P , and narrow the scope of ∃P such that it does not contain the η1∗, η2∗ anymore. Moreover, we make use of Lemma 2 and turn the literals P (ui1 ) into subformulas ∀x. x = ui1 → P (x). We proceed analogously with the literals ¬P (vi2 ), P (z`∗1 ), and ¬P (z`∗2 ). ∧ ∃P. ∀x. χ1∗(x, z¯) ∨ P (x) ∧
∀x. χ2∗(x, z¯) ∨ ¬P (x) ∧ ∧ ∀x. ^ x = ui1 → P (x)
i1 ∀x. ^ x = z`∗1 → P (x) `1 ∧ ∧ ∀x. ^ x = vi2 → ¬P (x)
i2 ∀x. ^ x = z`∗2 → ¬P (x) `2 At this point, the subformula staring with ∃P is in “Eliminationshauptform”. After converting the implications into disjunctions and factoring out the [¬]P (x), we arrive at a formula from which the second-order quantifier ∃P can be eliminated immediately via the basic elimination lemma.
θ(z¯) ∧ ∃u¯v¯. η1∗(u¯, z¯) ∧ η2∗(v¯, z¯) Using Lemma 7, we eliminate the quantifier ∃P and obtain the following result. θ(z¯) ∧ ∃u¯v¯. η1∗(u¯, z¯) ∧ η2∗(v¯, z¯) ∧ ∀x.
χ1∗(x, z¯) ∧ ^ x 6= ui1 ∧ ^ x 6= z`∗1
i1 `1
In order to convert this result into a somewhat nicer form, we proceed as described
in the proof of Lemma 19 in [
Consequently, we get the following result.
Theorem 8. Let ϕ := ∀x¯1∃y¯1 . . . ∀x¯n∃y¯n. ψ(x¯, y¯, z¯) be a relational first-order formula in which ψ is quantifier free and the sets x¯ := x¯1 ∪ . . . ∪ x¯n and y¯ := y¯1 ∪ . . . ∪ y¯n are separated. We assume that every variable occurring in the quantifier prefix and in z¯ also occurs in the matrix ψ.
Let xe1, . . . , xem1 ⊆ x¯ and ye1, . . . , yem2 ⊆ y¯ be partitions of the sets x¯ and y¯, respectively, such that the xe1, . . . , xem1 , ye1, . . . , yem2 are nonempty, pairwise disjoint, and pairwise separated in ϕ. Let P be a unary predicate symbol satisfying the following conditions: (1) For every set xi, 1 ≤ i ≤ m1, there is at most one variable xi∗ ∈ xei for which e ϕ contains atoms P (xi∗). (2) For every set yi, 1 ≤ i ≤ m2, there is at most one variable yi∗ ∈ yei for which e ϕ contains atoms P (yi∗).
Then ∃P. ϕ is equivalent to some first-order formula ϕ0 that is a finite disjunction of formulas of the form θ(z¯) ∧ ∀x. χ1∗(x, z¯) ∨ χ2∗(x, z¯) ∧ ∃u¯v¯. η1∗(u¯, z¯) ∧ η2∗(v¯, z¯) where all free predicate symbols and all free first-order variables also occur freely in ∃P. ϕ. Moreover, all the ui1 are variables from u¯, the vi2 are from v¯, and the z`∗1 and z`∗2 are certain free variables from z¯.
Example 9. Consider the sentence ϕ := ∃P. ∀x1∃y∀x2. R(x1, x2) ↔ P (y). We transform it into the equivalent sentence ∃P. ∀x1x2x3. R(x1, x2) ∨ ¬R(x1, x3) ∧ ∧ ∀x1x2. R(x1, x2) ∨ ∃y. ¬P (y) ∀x1x2. ¬R(x1, x2) ∨ ∃y. P (y) .
For the sake of simplicity, we narrow the scope of ∃P so that it only stretches over the last two conjuncts, which we thereafter transform into a disjunction of conjunctions. This yields ∀x1x2x3. R(x1, x2) ∨ ¬R(x1, x3) ∧ ∃P.
∀x1x2. R(x1, x2) ∧ ∃y. P (y) ∨ ∨ ∀x1x2. ¬R(x1, x2) ∧ ∃y. ¬P (y) ∃y. P (y) ∧ ∃y. ¬P (y) .
Since we can distribute the quantifier ∃P over disjunction, it is enough to eliminate ∃P in the following three formulas: (1) ∃P. ∃y. P (y) |=| ∃y. ∃P. ∀x. x 6= y ∨ P (x) ∧ true ∨ ¬P (x) |=| ∃y∀x. x 6= y ∨ true |=| true (2) ∃P. ∃y. ¬P (y) |=| ∃y. ∃P. ∀x. x 6= y ∨ ¬P (x) ∧ true ∨ P (x) |=| ∃y∀x. x 6= y ∨ true |=| true Hence, ϕ is semantically equivalent to .
Several remarks regrading the shape of the resulting formulas in Theorem 8 are in order. (a) Although the elimination of ∃P potentially introduces new (dis)equations, these only involve existentially quantified and free variables. This means, the separation conditions are not violated by these newly introduced equations. Hence, the introduction of these atoms in one elimination step does not pose an obstacle to the iterated elimination of multiple existential second-order quantifiers. (b) As the subformulas χ1∗(vi2 , z¯) may contain universal quantifiers ∀w and atoms R(. . . w . . . vi2 . . .), the separateness condition regarding universally and existentially quantified variables might be violated when introducing the subformulas χ1∗(vi2 , z¯) and, similarly, the subformulas χ2∗(ui1 , z¯). (c) Perhaps more severely, the introduction of atoms R(. . . w . . . vi2 . . .) may create a connection between sets xk and yi, if w ∈ xek and vi2 ∈ yei. Then, the sets xk and yi are not e e e e separated anymore in formulas that contain the new atom. Similar effects might affect pairs xek, xek0 and yi, yei0 . Hence, if we were to predict whether elimination of e both second-order quantifiers in a formula ∃Q∃P. ϕ is possible using the methods outlined above, we would need to predict which sets of variables will be separated in the formula that results from eliminating ∃P .
The above observations seem to make it hard to formulate a version of
Theorem 8 that clearly facilitates iterative elimination of multiple quantifiers. On
the other hand, it might be worthwhile to base the theorem on a generalization
of the separated fragment that still has a decidable satisfiability problem. The
generalized Bernays–Sch¨onfinkel–Ramsey fragment (GBSR) is described in [
Another interesting aspect is that the symmetry regarding the two Conditions (1) and (2) in Theorem 8 is perhaps more restrictive than necessary. It seems that Condition (2) is obsolete, as the resulting formula in Lemma 6 could be generalized in such a way that the restriction imposed by (2) is not satisfied but second-order quantifiers can still be eliminated.
Altogether, it is subject to future investigations whether Theorem 8 can be enhanced to facilitate iterative elimination of multiple quantifiers.
We have developed a preliminary result regarding the elimination of second-order quantifiers in a logic fragment that extends the monadic first-order fragment without equality and the Bernays–Sch¨onfinkel–Ramsey fragment.
Notice that the elimination of ∃P from a formula ∃P. ϕ, where ϕ is a monadic first-order formula without equality, constitutes a special case of the method shown in the present note. The reason is that, if every atom contains at most one variable, then variables cannot occur jointly in atoms. Hence, given a monadic first-order formula ϕ without equality, any two singleton sets {x}, {y} of variables are separated in ϕ. Consequently, any formula ∃P. ϕ with monadic ϕ satisfies the prerequisites of Theorem 8, if we choose the sets xk and yei to be singleton sets e covering all the variables that occur bound in ϕ.
The presented result can only be a first step towards the formulation of a novel fragment of second-order logic that (a) extends the monadic second-order fragment, (b) is based on the concept of separateness of certain variables at the atomic level, (c) admits elimination of second-order quantifiers, also in an iterated fashion. The discussion following Theorem 8 already makes clear that a lot remains to be done, in order to achieve this goal. Furthermore, there seems to be no good reason to confine ourselves to the elimination of quantifiers over unary predicates, but aim for higher arities as well. Moreover, (b) can be weakened by taking boolean structure into account instead of only concentrating on the atoms in a given formula. For example, the formula ∃P.∀xy. P (x)∧ P (y)∨R(x, y) does not satisfy the prerequisites of Theorem 8, as {x} and {y} are not separated and the set {x, y} contains two variables that occur as arguments of P . However, the theorem can be applied to the equivalent formula ∃P.∀x1x2y. P (x1) ∧ P (y) ∨ R(x2, y) , as the sets {x1} and {x2, y} are separated and x2 does not occur as argument of P . As a third possible improvement, equations between universal and existential variables should be allowed in a less restrictive way than they are in the present note. To this end, some of the methods that are used to handle equations during quantifier elimination in the monadic second-order fragment might be applicable in the more general setting as well.
In the present note we concentrate on transforming the input formulas
syntactically until the basic elimination lemma (Lemma 7) is applicable. In future work,
it is of course advisable to also try other known approaches, such as the ones
described in [