RANK HIERARCHIES FOR GENERALIZED QUANTIFIERS

H. JEROME KEISLER AND WAFIK BOULOS LOTFALLAH

Abstract. We show that for each n and m, there is an existential first order sentence which is NOT logically equivalent to a sentence of quantifier rank at most m in infinitary logic augmented with all generalized quantifiers of arity at most n. We use this to show the strictness of the quantifier rank hierarchies for various logics ranging from existential (or universal) fragments of first order logic to infinitary logics augmented with arbitrary classes of generalized quantifiers of bounded arity.

The sentence above is also shown to be equivalent to a first order sentence with at most n + 2 variables (free and bound). This gives the strictness of the quantifier rank hierarchies for various logics with only n + 2 variables. The proofs use the bijective Ehrenfeucht-Fraisse game and a modification of the building blocks of Hella.

1. Introduction

In the context of finite model theory and descriptive complexity, first order logic F O is known to have severe limitations. On one hand it cannot count, because very simple linear time queries such as parity are not first order definable. On the other hand, it lacks recursion, because it cannot express some simple nondeterministic logarithmic space queries such as reachability.

To overcome the first limitation, we can augment first order logic with the ability to count. If S is a set of natural numbers, the quantifier Q_{S} can be added to first order logic, with the following semantics:

A ⊧ (Q_{S} x)φ(x) iff |{a ∈ A : A ⊧ φ[a]}| ∈ S.

The property of odd parity is simply expressed by (Q_{S} x)(x = x), where S is the set of odd natural numbers.

To express a recursive query like reachability, we can augment first order logic with the transitive closure operator T C with the following semantics^{1}:

A ⊧ (T C x_{1}, x_{2}, y, z)(φ(x_{1}, x_{2}), α(y), β(z)) iff for each pair (a, b) in A, if (A, a) ⊧ α[a] and (A, b) ⊧ β[b], then (a, b) belongs to the transitive closure of the relation on A defined by φ(x_{1}, x_{2}).

Reachability over the signature {E, s, t} is expressed by the sentence

(T C x_{1}, x_{2}, y, z)(E(x_{1}, x_{2}), y = s, z = t).

Date: May 22, 2010.

1Usually Transitive Closure is defined by [(T C x_{1}, x_{2})φ(x_{1}, x_{2})](y′, z′), which is the special case of the definition here, with α(y, y′) being y = y′ and β(z, z′) being z = z′.

These different ways of extending first order logic are two instances of the generalized quantifiers introduced by Lindström in [Lin66]. A generalized quantifier Q is simply a class of (finite) models with a fixed finite signature ν_{Q} that is closed under isomorphism, and acts like an oracle in the interpretation of a formula. Q is n-ary, or has arity n, if n is the maximum number of arguments in the relations in ν_{Q}. In general, we can add a class Q of generalized quantifiers to first order logic to produce the logic F O(Q) (defined in Section 2 below).

It should be noted here that if Q is the class of all generalized quantifiers, then any class of Boolean queries on finite models can be defined by a formula in F O(Q). (Non-Boolean queries can also be expressed by turning them into Boolean queries over wider signatures, similar to the definition of T C above.) One would like to capture interesting classes of queries by augmenting F O with finitely many generalized quantifiers. However, this is not always possible. Hella proved in [Hel96] that if the class Q has bounded arity, then F O(Q) cannot capture the language P T IME, or even the weaker language DAT ALOG. This suggests that the class of all generalized quantifiers is too large, but one should consider infinite class of generalized quantifiers, and that the class Q_{n} of all generalized quantifiers of arity at most n is interesting.

In this paper, Q will always denote a class of generalized quantifiers of bounded arity, so that Q ⊆ Q_{n} for some n.

To capture different kinds of recursion, Moschovakis proposed in [Mos74] the addition of inductive operators to first order logic. This has been described as the most successful logic in computer science. Indeed, in the presence of order, Vardi [Var82] and Immerman [Imm86] showed that F O(LF P) and F O(P F P) (first order logic augmented with the least- and partial- fixed point operator) capture P T IME and P SP ACE, respectively.

The study of logics with inductive operators was greatly simplified when Kolaitis and Vardi noted in [KV92] that these logics are mere fragments of the logic L_{∞ ω}^{ω}, whose formulas have infinite conjunctions and disjunctions but finitely many free and bound variables. L_{∞ ω}^{ω} was introduced by Barwise [Bar77] in the context of infinite models (see [EF99], [Imm99]).

The infinitary logic L_{∞ ω} contains F O and allows infinite conjunction and disjunction, which enables inductive constructions as many times as needed. L_{∞ ω}, however, is too powerful for finite model theory, as it can express all possible queries over finite models. Thus, going backwards, we should restrict L_{∞ ω} (or its extension L_{∞ ω}(Q)) by limiting either the quantifier rank m of the formulas, or the total number k of variables (free and bound) occurring in the formulas. Note that, in descriptive complexity theory, the quantifier rank may be considered as a kind of time resource, while the number of variables may be considered as a kind of time resource. This leads to the logics L_{∞ ω}(Q, m) and L_{∞ ω}^{k}(Q), and their respective unions L_{∞ ω}(Q, ω) and L_{∞ ω}^{ω}(Q). The following natural questions arise:

Do the quantifier rank hierarchies of L_{∞ ω}(Q, m) and F O(Q, m)

collapse at some finite level?

In this paper we will give a negative answer to these questions when the set of quantifiers Q has bounded arity and contains at least the existential quantifier ∃. In particular, we show that for each m, L_{∞ ω}(Q, m) is strictly contained in L_{∞ ω}(Q, m + 1), and F O(Q, m) is strictly contained in F O(Q, m + 1). We also show the strictness of the quantifier rank hierarchies with one or both of the following restrictions:

(1) The set of all variables occurring in formulas has cardinality at most k, where k ≥ n + 2 is fixed. This leads to the k-variable logics L_{∞ ω}^{k}(Q, m).

(2) Negation is allowed only on quantifier-free formulas. This leads to the quantifier-positive logics L_{∞ ω}^{+}(Q, m).

These results complement different hierarchy strictness results in the literature. In [Hel89] Hella showed the strictness of the hierarchy based on the maximum arity n of the quantifiers in Q. Hella used an Ehrenfeucht-Fraïssé like game (called the bijective game) that characterizes the power of the logic L_{∞ ω}(Q_{n}, m). Later on, he together with Luosto and Väänänen gave a cardinality argument in [HLV96] showing the strictness of the hierarchy based on the similarity type of the quantifier, which contains both the quantifier arity and width (= the maximum number of formulas bound by the quantifier). However, their result was not explicit, that is, it did not lead to specific queries in the levels of the hierarchies. In the unary case, Luosto gave in [Luo00] an explicit strict hierarchy result based on the width of unary quantifiers.

Our results here are “almost explicit”. Fix a maximum arity n. We say that a sentence φ is expressible in a class of sentences L if φ is logically equivalent to some sentence ψ ∈ L. For each m we give an existential first order sentence σ_{m} that is not expressible in L_{∞ ω}(Q_{n}, m). We then use the sentences σ_{m} to show that the hierarchies are strict. To prove that σ_{m} is not expressible in L_{∞ ω}(Q_{n}, m), we give a recursive construction of particular models A_{m} and B_{m} that disagree on σ_{m} but agree on each sentence of L_{∞ ω}(Q_{n}, m). The construction of these models uses building blocks that are similar to those of Hella in [Hel96].

After giving the basic definitions, including Hella’s bijective game in Section 2, we introduce our recursive building strategy of the models A_{m} and B_{m} in Section 3. In Section 4, we introduce the operation Array_{n}(θ) defined on sentences θ. This leads to Section 5, where the main hierarchy results are obtained. We define a recursive sequence ρ_{m} of first order sentences such that ρ_{m} is not expressible in L_{∞ ω}(Q_{n}, m), and use these sentences to show that the quantifier rank hierarchies of F O(Q) and L_{∞ ω}(Q) are strict at all finite levels. In Section 6 we strengthen the results by getting a version σ_{m} of ρ_{m} which has just n + 2 variables. The sentence σ_{m} is an existential first order sentence, and is equivalent to a purely existential first order sentence σ′_{m} = (∃y_{1}) ⋯ (∃y_{ℓ})φ(y_{1}, …, y_{ℓ}) where φ is quantifier-free and the number of variables is ℓ = (n + 1)m + 1. We then show that the quantifier rank hierarchies of F O^{k}(Q) and L_{∞ ω}^{k}(Q) are strict at all finite levels. In Section 7 we get analogous results for the logics F O^{+}(Q) and L_{∞ ω}^{+}(Q). Finally, In Section 8 we show that the logics L_{∞ ω}^{k}(Q) and L_{∞ ω}^{+}(Q) have sentences that are not equivalent to any sentences of finite quantifier rank.

2. Basic Definitions

We always consider classes of finite models with a fixed underlying signature ν, which is a set of relation symbols. Given two formulas φ and ψ, φ ⊧ ψ will mean that every finite model of φ is a model of ψ. Two formulas φ, ψ will be called equivalent if ⊧ φ ↔ ψ. Two sets of formulas will be called equivalent if every formula in one set is equivalent to some formula in the other set, and vice versa.

A generalized quantifier Q is simply a class of finite models over a finite signature ν_{Q} = {R_{1}, …, R_{k}} that is closed under isomorphisms. The arity of Q is the maximum number of arguments of the relation symbols in ν_{Q}, and the width of Q is the length k of the signature ν_{Q}. The symbol Q can be used to build a formula of the form φ(x) = (Q y_{1}, …, y_{k})(ψ_{1}(x, y_{1}), …, ψ_{k}(x, y_{k})), where all the variables in the variable strings x, y_{1}, …, y_{k} are distinct, and each ψ_{i}(x, y_{i}) has its free variables included in x, y_{i}. φ(x) has its free variables included in x, and is given the following semantics in a finite structure A with a tuple a interpreting the free variable tuple x:

(A, a) ⊧ φ(x) iff the ν_{Q}-model over the universe of A with each R_{i} interpreted by the relation {b : (A, a) ⊧ ψ_{i}(a, b)} is in the class Q.

We let Q_{n} denote the class of all quantifiers of arity at most n. Thus, the universal and existential quantifiers ∀, ∃, as well as the counting quantifiers ∃^{≥k} all belong to Q_{1}. Note that different quantifiers Q ∈ Q can have different signatures ν_{Q}.

For any class of quantifiers Q ⊆ Q_{n} and underlying signature ν, we let L_{∞ ω}(Q) be the class of all formulas with finitely many (possibly zero) free variables built from atomic formulas over ν using negations, infinite conjunctions and disjunctions, as well as generalized quantifiers in Q. We take the classical infinitary logic to be the logic L_{∞ ω} = L_{∞ ω}({∃}) with just the existential quantifier. (The logics L_{∞ ω}({∃}), L_{∞ ω}({∀}), and L_{∞ ω}({∃, ∀}) are equivalent, but have different quantifier-positive fragments). We will only consider classes Q of bounded arity, that is, Q ⊆ Q_{n} for some n.

It is well known that the logic L_{∞ ω} is too powerful for finite model theory, as it can express any class of finite models closed under isomorphism. One way to weaken this logic, and the logic L_{∞ ω}(Q) in general, is to restrict the quantifier rank of its formulas. The quantifier rank of a formula φ in L_{∞ ω}(Q_{n}) is defined by induction on the complexity of φ as in [Hel89]:

• A quantifier-free formula has quantifier rank 0;

• The quantifier rank of ¬φ is equal to the quantifier rank of φ; • The quantifier rank of ⋀_{i∈I} φ_{i}, and also of ⋁_{i∈I} φ_{i}, is the supremum

of the quantifier ranks of φ_{i}, i ∈ I;

• the quantifier rank of (Q y_{1}, …, y_{k})(ψ_{1}(x, y_{1}), …, ψ_{k}(x, y_{k})) is 1

plus the maximum of the quantifier ranks of ψ_{1}, …, ψ_{k}. For a class Q ⊆ Q_{n}, we let L_{∞ ω}(Q, m) be the set of all formulas of L_{∞ ω}(Q) of quantifier rank at most m. Also, let L_{∞ ω}(Q, ω) = ⋃_{m} L_{∞ ω}(Q, m). Note that for any Q, L_{∞ ω}(Q, 0) is the set of quantifier-free formulas of L_{∞ ω}.

We define F O(Q) to be the first order part of L_{∞ ω}(Q), i.e. the set of all formulas of L_{∞ ω}(Q) of finite length. Also, F O(Q, m) is the set of all formulas of F O(Q) of quantifier rank at most m. Since all formulas in F O(Q) have finite quantifier rank, we have F O(Q) = ⋃_{m} F O(Q, m). We take the classical first order logic to be F O = F O({∃}). Note that for any Q, F O(Q, 0) is the set of quantifier-free first order formulas. And if the underlying signature is finite, L_{∞ ω}(Q, 0) = F O(Q, 0).

The following proposition shows that, unless Q is infinite, every formula in the restricted logic L_{∞ ω}(Q, m) is equivalent to a formula in F O(Q, m).

Proposition 2.1. If both the underlying signature and the class Q are finite, then for each m:

(i) For each finite set of variables x, the set of formulas in L_{∞ ω}(Q, m) with at most x free is equivalent to a finite set of formulas of F O(Q, m).

(ii) L_{∞ ω}(Q, m) is equivalent to F O(Q, m).

Proof: Part (i) is proved by induction on m. Part (ii) then follows. 2.1

The logics L_{∞ ω}(Q_{n}, m) are characterized by the n-bijective Ehrenfeucht-Fraïssé game introduced in [Hel89]. This game is played on two models by two players, Spoiler and Duplicator. Roughly speaking, Spoiler tries to prove that the two models look different, while Duplicator tries to prove that they look alike. By a game position we will mean a triple ((A, a), (B, b), m) where |a| = |b|, and m is a natural number that represents the number of moves yet to be played. The game is defined by recursion on m as follows.

When m > 0, the game proceeds from the position ((A, a), (B, b), m) according to the rules:

(1) Duplicator chooses a bijection f : A ⟶ B. (If |A| ≠ |B|, then Spoiler wins.)

(2) Spoiler chooses an n-tuple c in A.

(3) The game continues from the new position

((A, ac), (B, bf(c)), m − 1),

where f(c) = f(c_{1}, …, c_{n}) = (f(c_{1}), …, f(c_{n})). When m = 0 the game ends. ((A, a), (B, b), 0) is a winning position for Duplicator iff (A, a) and (B, b) satisfy the same atomic formulas. (In other words, a, b are either empty or generate submodels of A, B that are isomorphic with an isomorphism mapping a to b.)

We write (A, a) ≡_{n}^{m} (B, b) if Duplicator has a winning strategy in the n-bijective game starting from the position ((A, a), (B, b), m), and we write A ≡_{n}^{m} B if Duplicator has a winning strategy starting from the position (A, B, m). By the game A ≡_{n}^{m} B we will mean the n-bijective game starting from the position (A, B, m).

The importance of this game stems from the following result, which is proved in [Hel89, Hel96].

Proposition 2.2. (A, a) ≡_{n}^{m} (B, b) iff (A, a) and (B, b) agree on all formulas in L_{∞ ω}(Q_{n}, m). 2.2

3. The Building Strategy

The following definitions will use a modification of the building block introduced in [Hel96]. We first introduce some notation.

Definition 3.1. A signature ν is called n-adequate if ν contains at least a binary relation symbol E and an (n + 1)-ary relation symbol R.

We assume throughout this section that n > 0 and the underlying signature ν is n-adequate. Let A and B be finite models with signature ν. Also let X = C ∪ D, with C = {c_{1}, …, c_{n+1}} and D = {d_{1}, …, d_{n+1}}, where all the c_{i}’s and d_{i}’s are distinct, i.e. |X| = 2n + 2. Let G be the set

G = X ∪ (A × C) ∪ (B × D).

For each i ∈ {1, …, n + 1}, let

A_{i} = A × {c_{i}}, B_{i} = B × {d_{i}}, G_{i} = {c_{i}, d_{i}} ∪ A_{i} ∪ B_{i}.

Note that G_{i} is the set of elements of G that involve i, and the sets G_{i} form a partition of G. Let A_{i} be the copy of A with universe A_{i} such that a ↦ (a, c_{i}) is an isomorphism, and B_{i} be the copy of B with universe B_{i} such that b ↦ (b, d_{i}) is an isomorphism.

Definition 3.2. Let G(A, B) be the model with universe G and signature ν such that:

(i) For each i ∈ {1, …, n + 1}, A_{i} and B_{i} are submodels of G(A, B). (ii) For each i ∈ {1, …, n+1}, a ∈ A_{i}, and b ∈ B_{i}, E(c_{i}, a) and E(d_{i}, b)

hold in G(A, B). (iii) No atomic formulas hold in G(A, B) except for equalities and those

given in (1) and (2).

[figure: A; B; A_{i}; B_{i}; C; c_{i}; D; d_{i}; G(A, B)]

Intuitively, G(A, B) is the union of n+1 copies of A and n+1 copies of B, which is also equipped with an “edge” relation E(x, y), that connects each c_{i} ∈ C to each element of the corresponding copy of A, and similarly for D and B. In the terminology of [JM01] and [KL04], c_{i} is the root of a cone over A_{i}, and d_{i} is the root of a cone over B_{i}, in the model G(A, B).

With some extra work, it may be possible to dispense with the extra relation symbol E by coding with the (n + 1)-ary relation R. However, this would make the proofs harder to follow, so we chose instead to include E in our notion of an adequate vocabulary.

Definition 3.3. We now define two new models G^{+}(A, B) and G^{−}(A, B), which have the same universe and signature as G(A, B). G^{+}(A, B) is built from G(A, B) by replacing R by R ∪R^{+} where R^{+} is the relation on X given by:

R^{+}(a_{1}, …, a_{n+1}) iff |U ∩ {c_{i}, d_{i}}| = 1 for each i, and |U ∩ D| is even,

where U = {a_{1}, …, a_{n+1}}. G^{−}(A, B) is defined similarly but replacing R by R ∪ R^{−} where:

R^{−}(a_{1}, …, a_{n+1}) iff |U ∩ {c_{i}, d_{i}}| = 1 for each i, and |U ∩ D| is odd.

We define χ(x) to be the special formula (∃y)E(x, y)∧¬(∃y)E(y, x), which says that x is a source for the graph E. The next lemma is easily verified.

Lemma 3.4. For every pair of models A, B, the set X is defined by χ(x) in both of the models G^{+}(A, B) and G^{−}(A, B). 3.4

The set X can also be defined by the simpler formula ¬(∃y)E(y, x), but later on it will be useful to know that X is defined by the particular formula χ(x).

For each k ∈ {1, …, n + 1}, define the bijection f_{k} on X by:

f_{k}(x) = \{ \begin{matrix}d_{k} & if x = c_{k} \\ c_{k} & if x = d_{k} \\ x & otherwise \end{matrix} ,

i.e. f_{k} just swaps c_{k} with d_{k}.

The following lemma is easily proved.

Lemma 3.5. The bijection f_{k} is an isomorphism from (X, R^{+}) to (X, R^{−}). 3.5

We now prove our key lemma.

Lemma 3.6. Suppose A ≡_{n}^{m} B. Then

G^{+}(A, B) ≡_{n}^{m+1} G^{−}(A, B).

Proof: We write G^{+} = G^{+}(A, B) and G^{−} = G^{−}(A, B). Duplicator uses the identity bijection ι : G ⟶ G for her first move. Spoiler selects n elements e_{1}, …, e_{n} ∈ G. Since these elements belong to at most n of the sets G_{i}, there must exist k ∈ {1, …, n + 1} such that G_{k} is disjoint from {e_{1}, …, e_{n}}. Hold k fixed for the rest of the proof.

Suppose first that m = 0. In this case one can check directly that (G^{+}, e_{1}, …, e_{n}) and (G^{−}, e_{1}, …, e_{n}) satisfy the same atomic formulas, so Duplicator wins the game.

Now suppose m > 0. By hypothesis, A_{k} ≡_{n}^{m} B_{k}. In the last m moves Duplicator plays the auxiliary game A_{k} ≡_{n}^{m} B_{k} and uses her winning bijections for that game to give her moves for the main game. Each of these moves will be a bijection of G that agrees with f_{k} on X, matches the auxiliary game on A_{k} ∪ B_{k}, and is the identity function on the rest of G. Below is the detailed description of Duplicator’s strategy.

Suppose that at some stage 0 < j ≤ m, the two games have the positions

((G^{+}, s), (G^{−}, t), j), ((A_{k}, u), (B_{k}, v), j).

In the auxiliary game, let Duplicator’s next winning move be h_{j}, which is a bijection from A_{k} to B_{k}. We note that since Duplicator is using a winning strategy in the auxiliary game, and equalities are atomic formulas, we must have h_{j}(u) = v.

Then in the main game, we define Duplicator’s next move to be the bijection g_{j} on G such that:

g_{j}(x) = \{ \begin{matrix}f_{k}(x) & if x ∈ X \\ h_{j}(x) & if x ∈ A_{k} \\ h_{j}^{−1}(x) & if x ∈ B_{k} \\ x & otherwise. \end{matrix}

Let Spoiler’s next move in the main game be r = (r_{1}, …, r_{n}), an n-tuple in G. Let a be an arbitrary element of A_{k}. In the auxiliary game, take Spoiler’s next move to be w = (w_{1}, …, w_{n}), an n-tuple in A_{k}, where

w_{i} = \{ \begin{matrix}r_{i} & if r_{i} ∈ A_{k} \\ g_{j}(r_{i}) & if r_{i} ∈ B_{k} \\ a & otherwise. \end{matrix}

To show that Duplicator wins the main game, we must show that at the final position

((G^{+}, s), (G^{−}, t), 0),

(G^{+}, s) and (G^{−}, t) satisfy the same atomic formulas. We know that Duplicator wins the auxiliary game at the final position

((A_{k}, u), (B_{k}, v), 0).

That is, (A_{k}, u) and (B_{k}, v) satisfy the same atomic formulas. Moreover, Duplicator’s last move h_{1} is a bijection from A_{k} to B_{k}, and h_{1}(u) = v. It follows from the definition of g_{1} that g_{1}(s) = t.

Consider an atomic formula α(s′) with parameters from s such that s′ is the list of all parameters occurring in α(s′). Let t′ = g_{1}(s′). We show that α(s′) holds in G^{+} iff α(t′) holds in G^{−}. We suppose first that α(s′) holds in G^{+} and prove that α(t′) holds in G^{−}. We must consider several cases.

Case 1: s′ does not meet G_{k} (= {c_{k}, d_{k}} ∪ A_{k} ∪ B_{k}). In this case,

t′ = s′ and G^{−} also satisfies α(s′). Case 2: s′ ⊆ A_{k}. Then A_{k} satisfies α(s′) and t′ = h_{1}(s′), so B_{k}

satisfies α(t′) and hence G^{−} satisfies α(t′). Case 3: s′ ⊆ B_{k}. Similar to Case 2. Case 4: s′ ⊆ X and α(s′) is R(s′). Then R^{+}(s′) holds and t′ = f_{k}(s′),

so by Lemma 3.5, R^{−}(t′) holds and G^{−} satisfies R(t′). Case 5: s′ = (c_{k}, a) where a ∈ A_{k}. Then t′ = (d_{k}, b) where b = h_{1}(a),

so E(s′) holds in G^{+} and E(t′) holds in G^{−}. Case 6: s′ = (d_{k}, b) where b ∈ B_{k}. Similar to Case 5.

The other direction is proved by a similar argument. Therefore Duplicator wins the main game G^{+} ≡_{n}^{m+1} G^{−}. 3.6

4. The Array_{n} Operation

In this section we will introduce the operation Array_{n} on L_{∞ ω}, which can climb up one step in the generalized quantifier rank ladder. For a first order sentence θ that distinguishes between two models A and B, Array_{n}(θ) will distinguish between the models G^{+}(A, B) and G^{−}(A, B).

We assume throughout this section that n > 0 and the underlying signature ν is n-adequate.

Definition 4.1. Let θ be a formula in L_{∞ ω}. Define (θ ↾ z) to be the formula obtained from θ by first replacing each bound occurrence of z by a variable z′ that does not occur in θ, and then relativizing all of its quantifiers to the set {y : E(z, y)}, i.e. everywhere replacing (∃y)φ(x, y) by (∃y)(E(z, y) ∧ φ(x, y)).

Note that in the above definition, the variable z may have already been free in θ.

Recall that χ(x) is the formula (∃y)E(x, y) ∧ ¬(∃y)E(y, x), which says that x is a source for E.

Definition 4.2. Let θ be a sentence in L_{∞ ω}. Define Array_{n}(θ) to be the sentence

(∃x_{1}) ⋯ (∃x_{n+1})[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1} [χ(x_{i}) ∧ (θ ↾ x_{i})]].

Informally, (θ ↾ z) says that z points to a (nonempty) submodel that satisfies θ, and Array_{n}(θ) says:

“There are n + 1 elements related by R, which are sources for E and point to θ-submodels.”

Array_{n}(θ) is a sentence in L_{∞ ω} with the same underlying signature ν. If θ is first order, then Array_{n}(θ) is also first order. We also have a bound on the quantifier rank of Array_{n}(θ).

Lemma 4.3. If m > 0 and θ ∈ L_{∞ ω}({∃}, m), then

Array_{n}(θ) ∈ L_{∞ ω}({∃}, m + n + 1).

Proof: This follows easily from the definition of Array_{n}(θ). 4.3

Lemma 4.4. Let θ and φ be sentences in L_{∞ ω}. If θ is equivalent to φ, then Array_{n}(θ) is equivalent to Array_{n}(φ).

Proof: Suppose θ is equivalent to φ. Since χ(x) implies that the set {y : E(x, y)} is nonempty, the sentence

(∀x)[χ(x) → [(θ ↾ x) ↔ (φ ↾ x)]]

holds in all models. The lemma follows from this. 4.4

The above lemma would fail if we replaced χ(x) by the simpler formula ¬(∃y)E(y, x). If we defined Array_{n} with the formula ¬(∃y)E(y, x) in place of χ(x), and took θ to be (∃y)y = y and φ to be ¬(∃y)¬y = y, then θ would be equivalent to φ but Array_{n}(θ) would not be equivalent to Array_{n}(φ).

The power of the Array_{n} operation stems from the following:

Lemma 4.5. Let A and B be two finite models, and let θ be a first order sentence.

(i) If A ⊧ θ then G^{+}(A, B) ⊧ Array_{n}(θ).

(ii) If B |̸= θ then G^{−}(A, B) |̸= Array_{n}(θ).

Proof: (i) In G^{+}(A, B) the (n + 1)-tuple (c_{1}, …, c_{n+1}) belongs to R^{+} because |{c_{1}, …, c_{n+1}} ∩ D| = 0 which is even, and each c_{i} points to a copy of A.

(ii) In G^{−}(A, B), every (n + 1)-tuple in R^{−} has at least one term that points to a copy of B, which is not a model of θ. 4.5

Lemma 4.6. Let m > 0 and let θ be a sentence in L_{∞ ω}. If θ is not expressible in L_{∞ ω}(Q_{n}, m), then Array_{n}(θ) is not expressible in L_{∞ ω}(Q_{n}, m + 1).

Proof: By Proposition 2.2, there must be two models A, B such that A ⊧ θ, B |̸= θ, and A ≡_{n}^{m} B. By Lemma 4.5,

G^{+}(A, B) ⊧ Array_{n}(θ) and G^{−}(A, B) |̸= Array_{n}(θ).

Also, using Lemma 3.6, we get

G^{+}(A, B) ≡_{n}^{m+1} G^{−}(A, B).

By Proposition 2.2 again, Array_{n}(θ) is not expressible in L_{∞ ω}(Q_{n}, m + 1). 4.6

We remark that there is a natural way to extend the Array_{n} operation to all sentences of L_{∞ ω}(Q_{n}). However, this would require a discussion of relativized generalized quantifiers, and will not be needed here.

5. The Quantifier Rank Hierarchies

It will be convenient to have a short way to say that a sentence is not expressible in a logic L. Given a logic L, we let [L] denote the set of all sentences (of some L_{∞ ω}(Q)) that are expressible in L. Then φ ∉ [L] says that φ is not expressible in L, i.e., no sentence of L is equivalent to φ.

From Lemmas 4.3 and 4.6, we get:

Theorem 5.1. Suppose n > 0 and the underlying signature ν is n-adequate. For each m there is a first order sentence of quantifier rank m(n + 1) + 1 that is not expressible in L_{∞ ω}(Q_{n}, m), that is, there is a sentence

ρ_{m} ∈ F O({∃}, m(n + 1) + 1) \ [L_{∞ ω}(Q_{n}, m)].

Proof: Let ρ_{0} be any first order sentence of quantifier rank 1 that is not equivalent to a quantifier-free formula, that is, ρ_{0} ∈ F O({∃}, 1) \ [L_{∞ ω}(Q_{n}, 0)]. For definiteness, we’ll take ρ_{0} = (∃x_{1})E(x_{1}, x_{1}). For each m, let

ρ_{m+1} = Array_{n}(ρ_{m}).

Proceeding by induction on m, we use Lemma 4.3 to show that ρ_{m} ∈ F O({∃}, m(n + 1) + 1), and use Lemma 4.6 to show that ρ_{m} ∉ [L_{∞ ω}(Q_{n}, m)]. 5.1

For each j, let (∃ x_{1}, …, x_{j}) be the j-ary existential quantifier

{(A, S) : (A, S) ⊧ (∃x_{1}) ⋯ (∃x_{j})S(x_{1}, …, x_{j})},

and let (∀ x_{1}, …, x_{j}) be the corresponding j-ary universal quantifier.

Note that if the n-ary existential quantifier belongs to Q, then the preceding proof shows that ρ_{m} is expressible in F O(Q, 2m + 1).

We can now prove the first of our main results.

Theorem 5.2. Suppose n > 0 and the underlying signature ν is n-adequate. Let Q be a class of generalized quantifiers of arity at most n (i.e. Q ⊆ Q_{n}). Assume that for some j > 0, Q contains at least one of the quantifiers (∃ x_{1}, …, x_{j}) or (∀ x_{1}, …, x_{j}). Then:

(i) The finite quantifier rank hierarchy of the logic L_{∞ ω}(Q) is strict, i.e. for each m,

[L_{∞ ω}(Q, m)] ⊊ [L_{∞ ω}(Q, m + 1)].

(ii) The quantifier rank hierarchy of the logic F O(Q) is strict, i.e. for

each m,

[F O(Q, m)] ⊊ [F O(Q, m + 1)].

Proof: Suppose that (i) fails, so for some m,

[L_{∞ ω}(Q, m)] = [L_{∞ ω}(Q, m + 1)].

It follows by induction that the quantifier rank hierarchy in L_{∞ ω}(Q) collapses. Thus,

[L_{∞ ω}(Q, m(n + 1) + 1)] = [L_{∞ ω}(Q, m)].

By Lemma 5.1 there is a sentence

ρ_{m} ∈ F O({∃}, m(n + 1) + 1) \ [L_{∞ ω}(Q_{n}, m)].

Q is a subset of Q_{n}, so ρ_{m} ∉ [L_{∞ ω}(Q, m)]. If the variables x_{2}, …, x_{j} do not occur in a formula φ, then the formula (∃x_{1})φ is equivalent to each of the formulas (∃x_{1}, …, x_{j})φ and ¬(∀x_{1}, …, x_{j})¬φ. Since Q contains either the quantifier (∃ x_{1}, …, x_{j}) or the quantifier (∀ x_{1}, …, x_{j}), it follows that ρ_{m} is expressible in F O(Q, m(n + 1) + 1). But

[F O(Q, m(n + 1) + 1)] ⊆ [L_{∞ ω}(Q, m(n + 1) + 1)] = [L_{∞ ω}(Q, m)],

so ρ_{m} ∈ [L_{∞ ω}(Q, m)] and we have a contradiction.

The proof of (ii) is similar. 5.2

In Theorem 5.2, Q could in particular be just {∃} or the whole Q_{n}. This theorem concerns finite quantifier ranks. Sentences of quantifier rank ω will be considered in Section 8. Note that the quantifier rank hierarchies collapse beyond ω, because every class of finite models can be defined by a sentence of L_{∞ ω} of quantifier rank ω. When the underlying signature is finite, every class can even be defined by a countable disjunction of first order sentences. On the other hand, every formula in F O(Q) has finite quantifier rank.

6. Bounding the Number of Variables

We now obtain hierarchy results similar to those of Theorem 5.2 but within the fragments of L_{∞ ω}(Q_{n}) and F O(Q_{n}) whose formulas have at most a fixed finite number of variables (free and bound).

Definition 6.1. For a formula φ in L_{∞ ω}(Q_{n}), let Var(φ) be the set of distinct variables (free and bound) occurring in φ. The number of variables of φ is simply |Var(φ)|.

Given a natural number k and a logic L ⊆ L_{∞ ω}(Q_{n}), the k-variable fragment of L is the set L^{k} of all formulas φ ∈ L with |Var(φ)| ≤ k. We also define L^{ω} = ⋃_{k} L^{k}.

In particular, for each set of quantifiers Q ⊆ Q_{n} we will consider the k-variable fragments

L_{∞ ω}^{k}(Q), L_{∞ ω}^{k}(Q, m), F O^{k}(Q), F O^{k}(Q, m).

It is obvious that F O(Q) = F O^{ω}(Q), and for each m, F O(Q, m) = F O^{ω}(Q, m). From Proposition 2.1, we know that if both Q and the underlying signature ν are finite, then for each m, there exists a k (that depends on m, ν, and Q), such that

[L_{∞ ω}(Q, m)] = [L_{∞ ω}^{ω}(Q, m)] = [F O(Q, m)] = [F O^{k}(Q, m)].

The k-variable fragment of first order logic is F O^{k}. We note that there is no fixed k such that for all m, the sentences ρ_{m} of Lemma 4.6 is expressible in F O^{k}. The reason is that when passing from ρ_{m} to ρ_{m+1} = Array_{n}(ρ_{m}), the number of variables in (ρ_{m} ↾ x_{i}) is one more than the number of variables in ρ_{m}.

The next result is an analogue of Theorem 5.1 which gives sentences σ_{m} ∈ F O^{n+2} that do the same thing as the sentences ρ_{m}.

Theorem 6.2. Suppose n > 0 and the underlying signature ν is n-adequate. Let k = n + 2. For each m there is a first order sentence of quantifier rank mk + 1 that has at most k variables and is not expressible in L_{∞ ω}(Q_{n}, m), that is, there is a sentence

σ_{m} ∈ F O^{k}({∃}, mk + 1) \ [L_{∞ ω}(Q_{n}, m)].

Proof: Let ρ_{m} be the sentences defined in the proof of Theorem 5.1,

ρ_{0} = (∃x_{1})E(x_{1}, x_{1}), ρ_{m+1} = Array_{n}(ρ_{m}).

We first define σ_{0} = ρ_{0} = (∃x_{1})E(x_{1}, x_{1}), which belongs to F O^{k}({∃}, 1) but not to [L_{∞ ω}(Q_{n}, 0)]. Next, we define auxiliary formulas η_{m}(z) in F O^{k}({∃}, mk + 1), which will play the role of the relativized formula (ρ_{m} ↾ x_{i}) in the sentence ρ_{m+1} = Array_{n}(ρ_{m}).

We define

η_{0}(z) : (∃x_{1})[E(z, x_{1}) ∧ ¬E(x_{1}, z) ∧ E(x_{1}, x_{1})],

and define η_{m+1}(z) inductively by

(∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1} (E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z)(z = x_{i} ∧ η_{m}(z)))] .

Note how the variable z was reused. The idea is that once we know that E(z, x_{i}) holds for all i, we can just forget about z, and concentrate on each x_{i}. We now define σ_{m+1} as follows:

σ_{m+1} : (∃x_{1}) ⋯ (∃x_{n+1})[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}(∃z)(z = x_{i} ∧ η_{m}(z))].

This formula can be compared with the defining formula for ρ_{m+1}, which is

(∃x_{1}) ⋯ (∃x_{n+1})[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1} [χ(x_{i}) ∧ (ρ_{m} ↾ x_{i})]]

where χ(z) is the formula (∃y)E(z, y) ∧ ¬(∃y)E(y, z).

By induction on m, we can easily see that both η_{m}(z) and σ_{m} belong to F O^{k}({∃}, mk + 1).

We note that for each m, z is the only free variable in the formula η_{m}(z). If x is any other variable, we define η_{m}(x) to be the formula obtained from η_{m}(z) by replacing each occurrence of x by a new variable x′, and then replacing each free occurrence of z by x. Thus the formula

x = z → [η_{m}(x) ↔ η_{m}(z)]

is logically valid.

Claim 6.3. Let A be a finite model with signature ν. Suppose that the interpretation of E in A is transitive, that is,

A ⊧ (∀x)(∀y)(∀z)[[E(x, y) ∧ E(y, z)] → E(x, z)].

Then for each m, (i) A ⊧ (∀z)(∀y)[E(z, y) → [η_{m}(y) ↔ (η_{m}(y) ↾ z)]], (ii) A ⊧ (∀z)[η_{m}(z) ↔ (η_{m}(z) ↾ z)].

Proof of Claim 6.3: (i) We argue by induction on m. The result is clear for m = 0. Let A be a finite model with signature ν. Work in A and assume the result for m. By renaming bound occurrences of y in η_{m}(z), we see that η_{m+1}(y) is equivalent to

(∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ (∃z)[z = x_{i} ∧ η_{m}(z)]}] .

(η_{m+1}(y) ↾ z) is equivalent to each of the following formulas:

(∃x_{1}) ⋯ (∃x_{n+1}) [ ⋀_{i=1}^{n+1} E(z, x_{i}) ∧ R(x_{1}, …, x_{n+1})∧] ,

⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ (∃z′)[E(z, z′) ∧ z′ = x_{i} ∧ (η_{m}(z′) ↾ z)]}] ,

(∃x_{1}) ⋯ (∃x_{n+1}) [ ⋀_{i=1}^{n+1} E(z, x_{i}) ∧ R(x_{1}, …, x_{n+1})∧

⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ E(z, x_{i}) ∧ (η_{m}(x_{i}) ↾ z)}] ,

(∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ E(z, x_{i}) ∧ (η_{m}(x_{i}) ↾ z)}] .

Now assume E(z, y). Then since E is transitive, we have

(∀x)[E(y, x) ↔ [E(y, x) ∧ E(z, x)]].

Therefore (η_{m+1}(y) ↾ z) holds if and only if (∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ (η_{m}(x_{i}) ↾ z)}] .

By inductive hypothesis, this holds if and only if (∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}{E(y, x_{i}) ∧ ¬E(x_{i}, y) ∧ η_{m}(x_{i})}] ,

which is clearly equivalent to η_{m+1}(y). This completes the induction.

(ii) The formula (η_{m+1}(z) ↾ z) is built by replacing the bound occurrences of z by a new variable z′ and then relativizing all quantifiers to {u : E(z, u)}. Thus (η_{m+1}(z) ↾ z) is

(∃x_{1}) ⋯ (∃x_{n+1}) [ ⋀_{i=1}^{n+1} E(z, x_{i}) ∧ R(x_{1}, …, x_{n+1})∧

⋀_{i=1}^{n+1}{E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z′)[E(z, z′) ∧ z′ = x_{i} ∧ (η_{m}(z′) ↾ z)]}] .

By part (i), the subformula

E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z′)[E(z, z′) ∧ z′ = x_{i} ∧ (η_{m}(z′) ↾ z)] is equivalent to each of the following:

E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z′)[E(z, z′) ∧ z′ = x_{i} ∧ η_{m}(z′)],

E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z′)[E(z, x_{i}) ∧ z′ = x_{i} ∧ η_{m}(z′)],
E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z′)[z′ = x_{i} ∧ η_{m}(z′)],
E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z)[z = x_{i} ∧ η_{m}(z)].

Therefore (η_{m+1}(z) ↾ z) is equivalent to

(∃x_{1}) ⋯ (∃x_{n+1}) [ ⋀_{i=1}^{n+1} E(z, x_{i}) ∧ R(x_{1}, …, x_{n+1})∧

⋀_{i=1}^{n+1}{E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z)[z = x_{i} ∧ η_{m}(z)]}] .

This is clearly equivalent to

(∃x_{1}) ⋯ (∃x_{n+1})

[R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}{E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ (∃z)[z = x_{i} ∧ η_{m}(z)]}] ,

which by definition is η_{m+1}(z). 6.3

The proof of the theorem will be complete once we show that σ_{m} ∉ [L_{∞ ω}(Q_{n}, m)]. We will do this by producing a sequence of pairs of models A_{m}, B_{m} such that A_{m} ≡_{n}^{m} B_{m}, but A_{m} ⊧ σ_{m} and B_{m} |̸= σ_{m}.

We start by choosing two models A_{0} and B_{0} in which the interpretation of E is transitive, such that A_{0} ⊧ σ_{0} and B_{0} |̸= σ_{0}, but A_{0} ≡_{n}^{0} B_{0}. This is easy, since the relation ≡_{n}^{0} holds between any two relational models, but for definiteness, we take A_{0} and B_{0} to have a universe {c} of size 1. Also, in A_{0} the only atomic formula that holds is E(c, c), while in B_{0} no atomic formula holds. Next, we recursively define

A_{m+1} = G^{+}(A_{m}, B_{m}) and B_{m+1} = G^{−}(A_{m}, B_{m}).

The following claim is proved by an easy induction on m:

Claim 6.4. For each m, both A_{m} and B_{m} have a transitive interpretation of E, and moreover satisfy the following formula for each i ≤ n + 1:

[R(x_{1}, …, x_{n+1}) ∧ E(z, x_{i})] → ¬E(x_{i}, z).

6.4

It follows from Lemma 3.6 that A_{m} ≡_{n}^{m} B_{m}, so by Proposition 2.2, A_{m} and B_{m} agree on L_{∞ ω}(Q_{n}, m). From Lemma 4.5 and the recursive definition of ρ_{m}, we know that A_{m} ⊧ ρ_{m} and B_{m} |̸= ρ_{m}. So it will be enough to show that for each m, σ_{m} ↔ ρ_{m} holds in both A_{m} and B_{m}. We first get a connection between η_{m}(z) and χ(z).

Claim 6.5. For each m, both A_{m+1} and B_{m+1} satisfy (∀z)[η_{m}(z) → χ(z)].

Proof of Claim 6.5: One can show by induction that in both A_{m+1} and B_{m+1}, an element a satisfies χ(z) if and only if there is a directed path of length m + 1 starting at a. Also, if a satisfies η_{m}(z) then there is such a directed path. 6.5

We now get a connection between η_{m}(z) and the relativized formula (ρ_{m} ↾ z).

Claim 6.6. For each m, both A_{m+1} and B_{m+1} satisfy the sentence

(∀z)[η_{m}(z) ↔ [χ(z) ∧ (ρ_{m} ↾ z)]].

Proof of Claim 6.6: We argue by induction on m. The result is clear for m = 0. Suppose m > 0 and assume the result for m − 1. To prove the result for m, we work in either A_{m+1} or B_{m+1}.

Suppose that χ(z) ∧ (ρ_{m} ↾ z). Since (ρ_{m} ↾ z), z points to a model C of ρ_{m}. Then there are elements x_{1}, …, x_{n+1} of C such that

C ⊧ R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}[χ(x_{i}) ∧ (ρ_{m−1} ↾ x_{i})].

Since χ(z), C is a copy of either A_{m} or B_{m}. By inductive hypothesis,

C ⊧ R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1} η_{m−1}(x_{i}).

Therefore

R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}[E(z, x_{i}) ∧ (η_{m−1}(x_{i}) ↾ z)].

By Claim 6.3,

R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}[E(z, x_{i}) ∧ η_{m−1}(x_{i})].

By Claim 6.4,

R(x_{1}, …, x_{n+1}) ∧ ⋀_{i=1}^{n+1}[E(z, x_{i}) ∧ ¬E(x_{i}, z) ∧ η_{m−1}(x_{i})],

and η_{m}(z) follows.

Now suppose η_{m}(z). By Claim 6.5, χ(z) holds, so again z points to a model C which is a copy of A_{m} or B_{m}. By reversing the steps in the preceding paragraph, we can show that (ρ_{m} ↾ z). 6.6

To complete the proof of Theorem 6.2, we show that for each m, σ_{m} ↔ ρ_{m} holds in both A_{m} and B_{m}. The case m = 0 is trivial, since σ_{0} = ρ_{0}. For m + 1, this follows easily from Claim 6.6 and the defining formulas for ρ_{m+1} and σ_{m+1}. 6.2

We now get the following theorem, which parallels Theorem 5.2 with a similar proof:

Theorem 6.7. Suppose n > 0 and the underlying signature ν is n-adequate. Let n > 0 and let Q ⊆ Q_{n} be a class of generalized quantifiers of arity at most n. Also, assume that for some j > 0, Q contains at least one of the quantifiers (∃ x_{1}, …, x_{j}) or (∀ x_{1}, …, x_{j}). Then:

(i) For each k ≥ n + 2, the finite quantifier rank hierarchy of the logic L_{∞ ω}^{k}(Q) is strict, i.e. for each m,

[L_{∞ ω}^{k}(Q, m)] ⊊ [L_{∞ ω}^{k}(Q, m + 1)].

(ii) The finite quantifier rank hierarchy of the logic L_{∞ ω}^{ω}(Q) is strict, i.e. for each m,

[L_{∞ ω}^{ω}(Q, m)] ⊊ [L_{∞ ω}^{ω}(Q, m + 1)].

(iii) For each k ≥ n+2, the quantifier rank hierarchy of the logic F O^{k}(Q) is strict, i.e. for each m,

[F O^{k}(Q, m)] ⊊ [F O^{k}(Q, m + 1)].

6.7

7. The Quantifier-positive Rank Hierarchies

In this section we consider the quantifier rank hierarchies inside the quantifierpositive fragments of L_{∞ ω}(Q, n) defined below. The term “quantifier-positive” stems from the fact that negation must only have a quantifier-free scope, so every occurrence of a quantifier is positive.

Definition 7.1. Given a logic L ⊆ L_{∞ ω}(Q, n), the quantifier-positive fragment L^{+} of L is the set of all formulas φ ∈ L in which no occurrence of a quantifier is in the scope of a negation.

In particular, we will consider the quantifier-positive fragments

L_{∞ ω}^{+}(Q), L_{∞ ω}^{+}(Q, m), F O^{+}(Q), F O^{+}(Q, m)

and the k-variable quantifier-positive fragments

L_{∞ ω}^{k+}(Q), L_{∞ ω}^{k+}(Q, m), F O^{k+}(Q), F O^{k+}(Q, m).

It is important in this section that the underlying logic L_{∞ ω}(Q) has both the conjunction and the disjunction connectives. Thus each of the above fragments is closed under conjunction and disjunction.

Each sentence ρ ∈ F O^{+} = F O^{+}({∃}) is equivalent to a purely existential sentence, that is, a sentence of the form

(∃x_{1}) ⋯ (∃x_{ℓ})φ(x_{1}, …, x_{ℓ})

where φ is quantifier-free. The logics L_{∞ ω}^{k+} and L_{∞ ω}^{ω+} = ⋃_{k} L_{∞ ω}^{k+} have been studied in the literature under the names ∃L_{∞ ω}^{k} and ∃L_{∞ ω}^{ω}, respectively, and are characterized by the so-called existential pebble game. The importance of these logics stems from the fact that the latter contains the language DAT ALOG (see [KV95]).

We are going to show that each of the above fragments has a strict finite quantifier rank hierarchy. We can do this using the same sentences σ_{m} as we used in Section 6.

Proposition 7.2. Suppose n > 0 and the underlying signature ν is nadequate. Let k = n + 2. The sentences σ_{m} from Theorem 6.2 belong to F O^{k+}({∃}, mk + 1). Moreover, σ_{m} is equivalent to a purely existential first order sentence

σ′_{m} = (∃y_{1}) … (∃y_{ℓ})φ(y_{1}, …, y_{ℓ})

where φ is quantifier-free and ℓ = m(n + 1) + 1.

Proof: It is clear from the definition that for each m the formula η_{m}(z) belongs to F O^{+}, and hence that σ_{m} belongs to F O^{+}. The equivalent sentence σ′_{m+1} is obtained by first replacing (∃z)[x = x_{i} ∧ η_{m}(z)] by η_{m}(x_{i}), then replacing x_{1}, …, x_{n+1} by new variables in the formula σ_{m+1}, and moving all the quantifiers to the front. 7.2

Note that the number m(n+1)+1 in Proposition 7.2 is close to optimal— the sentence σ_{m} is not expressible in L_{∞ ω}(Q_{n}, m), but any purely existential sentence

(∃y_{1}) … (∃y_{mn})φ(y_{1}, …, y_{mn})

is expressible in L_{∞ ω}(Q_{n}, m).

If Q contains the n-ary existential quantifier, then by merging the existential quantifiers we see that σ_{m} is expressible in F O^{+}(Q, m + [m/n] + 1).

We now get the following theorem, which again parallels Theorem 5.2 with a similar proof:

Theorem 7.3. Suppose n > 0 and the underlying signature ν is n-adequate. Let Q ⊆ Q_{n} be a class of generalized quantifiers of arity at most n. Also, assume that for some j > 0, Q contains at least one of the quantifiers (∃ x_{1}, …, x_{j}) or (∀ x_{1}, …, x_{j}). Then:

(i) The finite quantifier rank hierarchies of the logics L_{∞ ω}^{+}(Q), L_{∞ ω}^{k+}(Q), and L_{∞ ω}^{ω+}(Q) are strict

(ii) The quantifier rank hierarchies of the logics F O^{+}(Q) and F O^{k+}(Q) are strict. 7.3

8. Beyond Finite Quantifier Ranks

In this section we show that each of the hierarchies in Theorems 5.2 (i), 6.7 (i), (ii), and 7.3 (i) has sentences at level ω. To do this, it is enough to show that there are sentences τ ∈ L_{∞ ω}^{k} and τ^{+} ∈ L_{∞ ω}^{k+}, both of quantifier rank ω, that are not expressible in the logic L_{∞ ω}(Q_{n}, ω) of sentences of L_{∞ ω}(Q_{n}) with finite quantifier rank. We will build τ and τ^{+} out of the sentences σ_{m} that were constructed in Section 6.

We first take up the finite variable case.

Theorem 8.1. Suppose n > 0 and the underlying signature ν is n-adequate. Let k = n+2. Then there is a sentence τ ∈ L_{∞ ω}^{k}\[L_{∞ ω}(Q_{n}, ω)] of quantifier rank ω.

Proof: For each m, let σ_{m} be the sentence constructed in Section 6. There is a first order sentence π_{m} ∈ F O^{2} with two variables that says that the graph E has a directed path of length m, that is, there is a sequence of elements y_{0}, …, y_{m} such that E(y_{k}, y_{k+1}) ∧ ¬E(y_{k+1}, y_{k}) for each k < m. Let τ be the sentence

τ : ⋁_{m}[σ_{m} ∧ ¬π_{m+1}].

It is clear that τ ∈ L_{∞ ω}^{k} with quantifier rank ω. Let A_{m} and B_{m} be the models constructed in Section 6. It was shown in the proof of Theorem 6.2 that A_{m} and B_{m} satisfy the same sentences of L_{∞ ω}(Q_{n}, m), and that A_{m} ⊧ σ_{m} and B_{m} |̸= σ_{m}. It is clear from the construction that both A_{m} and B_{m} satisfy π_{j} for all j ≤ m and also satisfy ¬π_{m+1}. Moreover, σ_{m} implies π_{j} for all j ≤ m. It follows that for all m, A_{m} ⊧ τ and B_{m} |̸= τ. Therefore τ is not expressible in L_{∞ ω}(Q_{n}, ω). 8.1

We will give two examples of sentences which do the job in the quantifierpositive fragment L_{∞ ω}^{k+}. In first example the underlying signature has countably many proposition symbols in addition to the relation symbols E and R. In the second example the underlying signature has just two symbols in addition to E and R, a binary predicate F and a unary predicate U.

Theorem 8.2. Suppose n > 0 and the underlying signature ν is n-adequate and contains countably many proposition symbols P_{0}, P_{1}, . . .. Let k = n + 2. Then there is a sentence τ^{+} ∈ L_{∞ ω}^{k+} \ [L_{∞ ω}(Q_{n}, ω)] of quantifier rank ω.

Proof: Let ν_{0} = ν \ {P_{0}, P_{1}, …} be the signature obtained by removing each proposition symbol P_{i} from ν. The sentences σ_{m} constructed in Section 6 use only the smaller signature ν_{0}. Let τ^{+} be the sentence

τ^{+} : ⋁_{m}[σ_{m} ∧ P_{m}].

Then τ^{+} ∈ L_{∞ ω}^{k+} with quantifier rank ω. For each model A with signature ν_{0} and each m, let A(P_{m}) be the model with signature ν which is built from A by making P_{m} true and making P_{j} false for all j ≠ m. Let A_{m} and B_{m} be the models constructed in Section 6 in the smaller signature ν. Then A_{m}(P_{m}) and B_{m}(P_{m}) satisfy the same sentences of L_{∞ ω}(Q_{n}, m) in the larger signature ν, and A_{m}(P_{m}) ⊧ σ_{m} ∧ P_{m} and B_{m}(P_{m}) |̸= σ_{m}. Moreover, for all j ≠ m, B_{m}(P_{m}) |̸= P_{j}. Therefore for all m, A_{m}(P_{m}) ⊧ τ^{+} and B_{m}(P_{m}) |̸= τ^{+}. This shows that τ^{+} is not expressible in L_{∞ ω}(Q_{n}, ω). 8.2

Theorem 8.3. Suppose n > 0 and the underlying signature ν is n-adequate and contains at least another binary predicate symbol F and unary predicate symbol U. Let k = n+2. Then there is a sentence τ′^{+} ∈ L_{∞ ω}^{k+}\[L_{∞ ω}(Q_{n}, ω)] of quantifier rank ω.

Proof: Let ν_{1} = ν \ {F, U} be the signature obtained by removing the symbols F, U from ν. As in the preceding proof, the sentences σ_{m} constructed in Section 6 use only the smaller signature ν_{1}. We first define a first order positive existential sentence π′_{n} with two variables that says that the relation F has a directed path with n edges that begins at an element of U and ends at an element x such that E(x, x). Formally, we inductively define formulas φ′_{n}(x) and φ′_{n}(y) by:

φ′_{0}(x) : E(x, x), φ′_{0}(y) : E(y, y),

φ′_{n+1}(x) : (∃y)[F (x, y) ∧ φ′_{n}(y)], φ′_{n+1}(y) : (∃x)[F (y, x) ∧ φ′_{n}(x)].

We then define

π′_{n} : (∃x)[U(x) ∧ φ′_{n}(x)].

Let τ′^{+} be the sentence

τ′^{+} : ⋁_{m=1}^{∞}[σ_{m} ∧ π′_{m}].

Then τ′^{+} ∈ L_{∞ ω}^{k+} with quantifier rank ω. Let A_{m} and B_{m} be the models constructed in Section 6 in the smaller signature ν_{1}. Recall that for each m, A_{m} ⊧ σ_{m} and B_{m} |̸= σ_{m}. Moreover, G(A_{m}, B_{m}) has universe

G = X ∪ (A_{m} × C) ∪ (B_{m} × D)

where

C = {c_{1}, …, c_{n+1}}, D = {d_{1}, …, d_{n+1}}, X = C ∪ D.

For each c ∈ C, the c-th copy of A_{m} in G(A_{m}, B_{m}) has universe A_{m} × {c}, and for each d ∈ D the d-th copy of B_{m} in G(A_{m}, B_{m}) has universe B_{m}×{d}. We expand A_{m} and B_{m} to models A′_{m} and B′_{m} in the signature ν as follows. A′_{0} and B′_{0} are the expansions of A_{0} and B_{0} in which F is empty and U = {c}. A′_{m+1} and B′_{m+1} are the expansions of A_{m+1} and B_{m+1} where U is the set X in the construction G(A_{m}, B_{m}), and F is the set of all pairs (x, y) such that one of the following holds:

• x = (x′, c) and y = (y′, c) belong to the same copy of A_{m}, and

A′_{m} ⊧ F (x′, y′),

• x = (x′, d) and y = (y′, d) belong to the same copy of B_{m}, and

B′_{m} ⊧ F (x′, y′),
• x ∈ C, y = (y′, c) belongs to a copy of A_{m}, and A′_{m} ⊧ U(y′), or
• x ∈ D, y = (y′, d) belongs to a copy of B_{m}, and B′_{m} ⊧ U(y′).

It is easily shown by induction on m that F is included in E, that is, the sentence

∀x∀y(F (x, y) → E(x, y))

holds in both A′_{m} and B′_{m}. The proof of Lemma 3.6 can be slightly modified to show that A′_{m} and B′_{m} satisfy the same sentences of L_{∞ ω}(Q_{n}, m) in the whole signature ν.

One can show by an easy induction that for each m, the sentence π′_{m} holds in A′_{m} (and holds in B′_{m} if m > 0), but for all j ≠ m the sentence π′_{j} fails in both A′_{m} and B′_{m}. Therefore A′_{m} ⊧ σ_{m} ∧ π′_{m}, and for all j, B′_{m} |̸= σ_{j} ∧ π′_{j}. Therefore for all m, A′_{m} ⊧ τ′^{+} and B′_{m} |̸= τ′^{+}, so τ′^{+} is not expressible in L_{∞ ω}(Q_{n}, ω). 8.3

References:

[Bar77] J. Barwise, On Moschovakis closure ordinals, Journal of Symbolic Logic, vol. 42 (1977), pp. 292-296.

[EF99] H-D. Ebbinghaus and J. Flum, Finite Model Theory, Second Edition, Springer Verlag (1999).

[Hel89] L. Hella, Definability hierarchies of generalized quantifiers, Annals of Pure and Applied Logic, vol. 43 (1989), pp. 235-271.

[Hel96] L. Hella, Logical hierarchies in PTIME, Information and Computation, vol. 129 (1996), pp. 1-19.

[HLV96] L. Hella, K. Luosto, and J. Väänänen, The Hierarchy Theorem for Generalized Quantifiers. Journal of Symbolic Logic, vol. 61 (1996), pp. 802-817.

[Imm86] N. Immerman, Relational queries computable in polynomial time, Information & Control, vol. 68 (1986), pp. 86-104.

[Imm99] N. Immerman, Descriptive Complexity, Springer Verlag, New York (1999).

[JM01] D. Janin and J. Marcinkowski, Toolkit for first order extensions of monadic games, Proceedings of STACS, Springer, LNCS (2001).

[KL04] H. J. Keisler and W. B. Lotfallah, First order quantifiers in monadic second order logic, J. Symbolic Logic, vol. 69 (2004), pp. 118-136.

[KV92] P. G. Kolaitis and M. Y. Vardi, Fixpoint logic vs. infinitary logic in finite-model theory, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, (1992), pp. 46-57.

[KV95] P. G. Kolaitis and M. Y. Vardi, On the expressive power of Datalog: tools and a case study, Journal of Computer and System Sciences vol. 51, iss. 1 (1995), pp. 110-134.

[Lin66] P. Lindström, First order predicate logic with generalized quantifiers, Theoria, vol. 32 (1966), pp. 186195.

[Luo00] K. Luosto, Hierarchies of monadic generalized quantifiers, The Journal of Symbolic Logic, vol. 65 (3) (2000), pp. 1241-1263.

[Mos74] Y. Moschovakis, Elementary induction on abstract structures, North Holland (1974).

[Var82] M. Vardi, Complexity of relational query languages, Proceedings of 14th ACM Symposium on Theory of Computing, (1982), pp. 137-146.

Department of Mathematics, University of Wisconsin, 480 Lincoln Drive, Madison WI 53706

E-mail address: keisler@math.wisc.edu

Department of Mathematics and Actuarial Science, The American University in Cairo, AUC Avenue, P.O. Box 74, New Cairo 11835, Egypt

E-mail address: lotfallah@aucegypt.edu, lotfalla@uwalumni.com