Normal Forms for Second-Order Logic over Finite Structures, and Classification of NP

Optimization Problems

Thomas Eiter, Georg Gottlob, Yuri Gurevich Christian Doppler Labor für Expertensyteme

Technische Universität Wien Paniglgasse 16, 1040 Wien

April 7, 1995

CD-TR 95/77

To appear in Annals of Pure and Applied Logic.

To appear in Annals of Pure and Applied Logic.

Normal Forms for Second-Order Logic over Finite Structures, and Classification of NP

Optimization Problems

Thomas Eiter^{∗} Georg Gottlob^{∗} Yuri Gurevich^{†}

April 7, 1995

Abstract

We start with a simple proof of Leivant’s normal form theorem for Σ_{1}^{1} formulas over finite successor structures. Then we use that normal form to prove the following:

(i) over all finite structures, every Σ_{2}^{1} formula is equivalent to a Σ_{2}^{1} formula whose first-order part is a boolean combination of existential formulas, and (ii) over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially. The normal form theorem for Σ_{2}^{1} fails if Σ_{2}^{1} is replaced with Σ_{1}^{1} or if infinite structures are allowed.

1 Introduction

We consider second-order logic with equality (unless otherwise stated explicitly) and without function symbols of positive arity. Predicates are denoted by capitals and individual variables by lower case letters; a bold face version of a letter denotes a tuple of corresponding symbols. For brevity, we say that a formula Φ reduces to a formula Ψ over a class K of structures if the two formulas have the same vocabulary σ and the same free variables and if the two formulas are equivalent at each σ-structure in K. We recall the definition of Σ_{k}^{1} and Π_{k}^{1} formulas, k ≥ 1, on the example when k = 3. A Σ_{3}^{1} (respectively, Π_{3}^{1}) formula is a second-order formula of the form

(∃S_{1})(∀S_{2})(∃S_{3})ψ (respectively (∀S_{1})(∃S_{2})(∀S_{3})ψ)

∗Christian Doppler Laboratory for Expert Systems, Information Systems Department, TU Vienna, Paniglgasse 16, A-1040 Wien, Austria. Email: (eiter|gottlob)@dbai.tuwien.ac.at

†Electrical Engineering and CS Department, University of Michigan, Ann Arbor, MI 48109–2122, USA.

Email: gurevich@umich.edu. The work of this author is partially supported by NSF and ONR.

where ψ is first-order. Classes Σ_{k}^{0} and Π_{k}^{0}, k ≥ 1, of first-order formulas are defined similarly. In particular, a Σ_{2}^{0} formula is a first-order formula of the form (∃x)(∀y)ψ where ψ is quantifier free. It is well-known that every Σ_{1}^{1} formula reduces to a Σ_{1}^{1} formula with first-order part of the form (∀x)(∃y)φ(x, y) where φ is quantifier-free. The reduction is a simple skolemization [13, Sec. 2.5.2]. It follows that every Σ_{k}^{1} (respectively Π_{k}^{1}) formula reduces to a Σ_{k}^{1} (respectively Π_{k}^{1}) formula with only one quantifier alternation in the first-order part. Leivant found a simpler normal form for Σ_{1}^{1} formulas over finite successor structures: every such formula reduces to a Σ_{1}^{1} formula with universal first-order part [8]. In Section 2, we give a shorter, simpler and more direct proof of this normal form theorem. Leivant’s theorem fails in the case of all finite structures. Moreover, let Σ_{k}^{1}(bool) (respectively Π_{k}^{1}(bool)) be the collection of Σ_{k}^{1} (respectively Π_{k}^{1}) formulas whose first-order parts are Boolean combinations of existential formulas. We exhibit a Σ_{1}^{1} formula without individual or predicate variables that does not reduce to any Σ_{1}^{1}(bool) formula. In Section 3, we use Leivant’s to prove our main result, announced in [3]: Over arbitrary finite structures, every Σ_{2}^{1} formula reduces to a Σ_{2}^{1}(bool) formula. It follows that every Σ_{k}^{1} formula (respectively Π_{k}^{1} formula), k ≥ 2, reduces to a Σ_{k}^{1}(bool) formula (respectively Π_{k}^{1}(bool) formula). In Section 4, we exhibit a Σ_{2}^{1} formula which does not reduce over infinite structures to any Σ_{2}^{1}(bool). The final Section 5 is devoted to the classification of NP optimization problems. We recall the definition of NP optimization problems and the Kolaitis-Thakur hierarchies of polynomially bounded minimization and maximization problems [6]. In the context of optimization problems, first-order structures serve as inputs to algorithms. In fact, genuine inputs are representations of structures, e.g, as strings. Such representations order the given structure on one way or another. Thus it is most natural to ask what happens to the Kolaitis-Thakur hierarchies in the case of successor (with or without order) structures. We show that in the case of successor structures the minimization hierarchy collapses completely and the maximization hierarchy collapses partially. The case of ordered successor structures does not differ from the case of successor structures for these purposes.

2 Leivant’s Normal Form

Fix a binary predicate Succ and unary predicates F and L. A successor structure is a structure A such that

• the vocabulary of A includes the three fixed predicates,

• A is finite, and

• there exists a linear order < on the universe of A such that on the expanded structure (A, <)

– Succ is the successor relation of <, – F (x) is satisfied by and only by the first element, and

– L(x) is satisfied by and only by the last element.

The expanded structure (A, <) is an ordered successor structure.

Theorem 2.1 (Leivant) Over successor structures, every Σ_{1}^{1} formula (possibly with free predicate or individual variables) reduces to a Σ_{1}^{1} formula of the form (∃T)(∀x)ψ where ψ is quantifier-free.

Proof. Without loss of generality, the given formula Φ has the form

(∃S)(∀x)(∃y)φ(x, y), (1)

where x = (x_{1}, …, x_{m}), y = (y_{1}, …, y_{n}) and φ is quantifier free. We prove that the formula

α = (∀x)(∃y)φ(x, y)

is equivalent to a formula

β = (∃G)(∀x, y, y′)ψ

where G is a 2n-ary predicate and ψ is quantifier free. The idea is this: β asserts that (i) G(x, y) holds if and only if φ(x, z) holds for some z ≤ y, and (ii) G(x, y) holds for the last y. The order corresponding to Succ, F, and L gives rise to the lexicographical order on ntuples of elements. Obvious quantifier free formulas Succ^{n}(y, y′), F^{n}(y) and L^{n}(y) describe the successor relation on n-tuples, the first n-tuple and the last n-tuple respectively. The desired ψ is the conjunction of the following formulas:

F (y) → [G(x, y) ↔ φ(x, y)],
Succ(y, y′) → [G(x, y′) ↔ (G(x, y) ∨ φ(x, y′)],
L(y) → G(x, y).

We check that α and β are equivalent. Treat free variables of Φ (individual as well as predicate variables) as constants. Suppose that α holds in some successor structure A. For each x, let M(x) be the least y such that φ(x, y) holds in A. Choose G(x, y) ↔ y ≥ M(x). Clearly (A, G) ⊧ (∀x, y, y′)ψ. Hence, A ⊧ β. Conversely, suppose that β holds in some structure A, and G is a witness to that fact, and x is an m-tuple of elements of A. Let end be the last y; by the third conjunct of ψ, G(x, end) holds for all x. Let M(x) be the least y such that G(x, y) holds. If M(x) is the very first n-tuple then, by the first conjunct of ψ, φ(x, M(x)) holds in A. Otherwise, use the second conjunct of ψ, to establish that φ(x, M(x)) holds in A. Thus, α holds in A.

Remark. Theorem 2.1 can also be derived from Stewart’s result that graph 3-colorability is complete for NP via quantifier-free translations with successor [12] and the fact that graph 3-colorability is expressible by a Σ_{1}^{1} formula with universal first-order part.

Theorem 2.2 There is a Σ_{1}^{1} sentence Φ which does not reduce over finite structures to any Σ_{1}^{1}(bool) sentence or even to any Σ_{1}^{1} sentence with the first-order part in Σ_{2}^{0}.

Proof. The desired Φ expresses that the universe has an even number of elements. For example, Φ may assert the existence of an equivalence relation such that every equivalence class contains precisely two elements. By contradiction, suppose that Φ reduces over finite structures to a sentence Ψ = (∃X)(∃x)(∀y)ψ where ψ is quantifier free. Let k be the number of existential individual quantifiers in φ and U be a set of even cardinality with ∥U∥ > k. Clearly, U ⊧ Ψ. Therefore, for some tuple X_{0} of appropriate relations, ⟨U, X_{0}⟩ ⊧ (∃x)(∀y)φ. Choose k appropriate witnesses and let V ⊆ U contain all k witnesses and be of odd cardinality. It is easy to see that V ⊧ Ψ which is impossible.

Remark. It is shown in [7] that the fragment of Σ_{1}^{1} with first-order parts in Σ_{2}^{0} has a 0-1 law on finite structures. This gives another proof of Theorem 2.2.

3 A Σ_{2}^{1} Normal Form

Now we consider arbitrary finite structures. Let Σ_{1}^{0}(bool) be the collection of Boolean combinations of first-order existential formulas.

Lemma 3.1 Let < and Succ be binary predicates, and let F, L, Z be unary predicates. There exists a Σ_{1}^{0}(bool) formula SUCCORD(<, Succ, F, L, Z) such that the formula (∀Z)SUCCORD(<, Succ, F, L, Z) asserts that <, Succ, F, and L give an ordered successor structure.

Proof. Define the following formulas:

• LINORD(<) = (∀x, y, z)((x < y ∧ y < z) → x < z) ∧
(∀x)¬(x < x) ∧
(∀x, y)(x = y ∨ x < y ∨ y < x),

asserting that < is a linear order;

• FIRST(<, F) = (∀x, y)(F (x) → ¬(y < x)) ∧ (∃x)(F (x)),

asserting that F describes the smallest element according to <;

• LAST(<, L) = (∀x, y)(L(x) → ¬(x < y)) ∧ (∃x)(L(x)),

asserting that L describes the greatest element according to <;

• SUCCESSOR_{1}(<, Succ) =
(∀x, y, z)[Succ(x, y) → (x < y ∧ ¬(x < z ∧ z < y))];

and

• SUCCESSOR_{2}(Succ, L, Z) =
[(∃u)(Z(u) ∧ ¬L(u)) → (∃u, v)(Z(u) ∧ Succ(u, v))] .

Note that the formula (∀Z)SUCCESSOR_{2} implies that every element, except the greatest, has a successor. To see that, consider the case when Z is of cardinality one. The second-order quantification allows us to avoid alternating quantifiers in the first-order formula. The desired

SUCCORD(<, Succ, F, L, Z) = LINORD(<) ∧ FIRST(<, F) ∧ LAST(<, L)∧
SUCCESSOR_{1}(<, Succ) ∧ SUCCESSOR_{2}(Succ, L, Z)

Corollary 3.2 Over finite structures, every Σ_{1}^{1} formula (possibly with free predicate or individual variables) reduces to a Π_{2}^{1}(bool) formula.

Proof. Let SUCCORD(<, Succ, F, L, Z) be as above and Ψ be any Σ_{1}^{1} formula. Since every nonempty finite set supports an ordered successor structure, Ψ is equivalent (we consider only finite structures here) to

(∀ <, Succ, F, L)( [(∀Z)(SUCCORD(<, Succ, F, L, Z)] → Ψ ) (2)

By Theorem 2.1, over successor structures, Ψ reduces to a formula (∃S)(∀x)φ where φ is quantifier-free. Clearly, formula (2) is equivalent to

(∀ <, Succ, F, L)( [(∀Z)(SUCCORD(<, Succ, F, L, Z)] → (∃S)(∀x)φ) (3)

which is equivalent to

(∀ <, Succ, F, L)(∃Z, S)[SUCCORD(<, Succ, F, L, Z) → (∀x)φ] (4)

Theorem 3.3 For k ≥ 2, every Σ_{k}^{1} formula (respectively Π_{k}^{1} formula) reduces over finite structures to a Σ_{k}^{1}(bool) formula (respectively Π_{k}^{1}(bool) formula).

Proof. It is sufficient to prove the theorem for Π_{2}^{1} formulas. All other cases follow trivially. Let Ψ = (∀P)(∃Q)φ, where φ is first-order. By Corollary 3.2, the Σ_{1}^{1} formula Φ = (∃Q)φ reduces over finite structures to some Π_{2}^{1}(bool) formula Φ^{∗}. Thus, Ψ reduces over finite structures to (∀P)Φ^{∗}, which is a Π_{2}^{1}(bool) formula.

Notice that the theorem remains valid for logic without equality because the fact that a free binary predicate is equality can be expressed by a Π_{1}^{1} formula without alternating first-order quantifiers.

Remark. A Σ_{k}^{1} formula does not necessarily reduce over finite structures to a Σ_{k}^{1} formula whose first-order part is purely universal or existential. In fact, even a Σ_{1}^{0}(bool) formula does not necessarily reduce over finite structures to any Σ_{k}^{1} formula whose first-order part is purely universal or existential. The reason is that every Σ_{k}^{1} sentence whose first-order part is purely universal or existential is preserved under submodels or extensions, respectively. Indeed, each universal first-order sentence is preserved under submodels (see [2]). An easy induction on k shows that each Σ_{k}^{1} formula with universal first-order part is preserved under submodels. On the other hand, it is easy to construct a Σ_{1}^{0}(bool) sentence that is not preserved under submodels or extensions.

4 Limited expressiveness of the Σ_{2}^{1}(bool) fragment

In the previous section, we considered normal forms for second-order logic over finite structures. Now, let us consider second-order logic over arbitrary structures. Even if the syntactical form of the formulas in Σ_{2}^{1}(bool) is rather simple, many interesting properties can be expressed within this fragment. For example, the following properties of sets can be expressed.

Infinity:

(∃ <)(∀X) [LINORD(<) ∧ [(∃x)(X(x)) → (∃x, y)(X(x) ∧ y < x)] ] , (5)

where LINORD(<) is the universal first-order formula, defined above, that asserts that < is a linear order.

Countability (that is, finite or infinite countability):

(∃ <, Succ, F)(∀X) [ Γ(<, Succ, F) ∧ INDUCTION(F, Succ, X) ] , (6)

where Γ(<, Succ, F) is the conjunction of the formulas LINORD(<), FIRST(<, F), and SUCCESSOR_{1}(<, Succ), defined above and the formula

INDUCTION(F, Succ, X) =

[(∀x)(F (x) → X(x)) ∧ (∀x, y)(Succ(x, y) ∧ X(x) → X(y))] → (∀x)X(x)

Finiteness:

(∃ <, Succ, F, L)(∀X) [ Γ(<, Succ, F) ∧ LAST(<, L) ∧ INDUCTION(F, Succ, X) ] (7)

where LAST(<, L), Γ(<, Succ, F) and INDUCTION(F, Succ, X) are as above. Infinite countability (ℵ_{0}) is the conjunction of (5) and (6) and thus can be expressed in Σ_{2}^{1}(bool). The question arises whether all Σ_{2}^{1} properties over arbitrary structures can be expressed by Σ_{2}^{1}(bool) formulas. This is not the case.

Theorem 4.1 There exists a Σ_{2}^{1} formula that is not equivalent to any Σ_{2}^{1}(bool) formula or even to any Σ_{2}^{1} formula with first-order part in Π_{2}^{0}.

Proof. It suffices to prove the claim when we allow formulas to use the standard arithmetical operations and restrict attention to structures on the set of natural numbers where the arithmetical operations have their usual interpretations. Indeed, suppose that Φ is a Σ_{2}^{1} formula that is not equivalent to any Σ_{2}^{1} formula with first-order part in Π_{2}^{0} over the standard arithmetical structure A (that is over the class of structures described above). Let A′ be the relational structure obtained from A by replacing the arithmetical operations with their graphs, e.g. the successor operation Succ is replaced with the binary relation {(x, y) : y = Succ(x)}. In the obvious way, define the notion that a formula about A is equivalent to a formula about A′. Transform Φ into an equivalent relational Σ_{2}^{1} formula Φ′. By contradiction suppose that Φ′ is logically equivalent to a Σ_{2}^{1} formula Ψ′ with first-order part in Π_{2}^{0}. Then Φ′ and Ψ′ are equivalent over A′. Transform Ψ′ to an equivalent Σ_{2}^{1} formula Ψ with first-order part in Π_{2}^{0} about A. Then Φ and Ψ are equivalent, which gives the desired contradiction. It is well known (see e.g. [13, Sec. 3.2]) that there exists a Σ_{2}^{1} formula Ψ without free individual variables that is not equivalent to any Σ_{1}^{1} formula over A. Thus it suffices to prove that every arithmetical Σ_{2}^{1} formula with first-order part in Π_{2}^{0} is equivalent to an arithmetical Σ_{1}^{1} formula. This follows from the following lemma.

Lemma 4.2 Over A, every formula

Φ = (∀T)(∃y)α(T, y),

where α is quantifier free, is equivalent to a first-order formula ψ.

We note that α may have free predicate and individual variables. Lemma 4.2 is not new to experts. In fact, it remains true if bounded universal quantification is allowed in the first-order part of Φ and if it is required that all universal quantors in ψ are bounded. Barwise attributes the stronger result to Kreisel and proves a generalization of it to countable admissible sets in [1]. For reader’s convenience, we give a direct proof of our lemma.

Proof of Lemma 4.2. Since every recursively enumerable relation can be expressed with a first-order existential formula [9] over A, there are first-order existential formulas G_{k}(x, y_{1}, …, y_{k}) such that, for every x, there exists a unique sequence (y_{1}, …, y_{k}) with A ⊧ G_{k}(x, y_{1}, …, y_{k}), and, for every sequence (y_{1}, …, y_{k}), there is a unique x with A ⊧ G_{k}(x, y_{1}, …, y_{k}) [5]. Fix appropriate formulas G_{k}. To make our intentions clearer we write x = Code(y_{1}, …, y_{k}) instead of G_{k}(x, y_{1}, …, y_{k}). Without loss of generality T is a single unary predicate T. The reason is that the sequence T of predicates (T_{1}, …, T_{m}) can be appropriately encoded by a single unary predicate T. We assume without loss of generality that all predicates T_{i} have the same arity and illustrate the coding procedure on an example. Suppose that α contains only two atomic formulas involving T, namely β = T_{1}(u_{1}, u_{2}) and γ = T_{2}(v_{1}, v_{2}). Let z_{β} and z_{γ} be fresh variables and α^{∗} be the result of replacing β with T (z_{β}) and γ with T (z_{γ}) in α(T, y). Given any T, let the desired T contain a number x if and only if either there are u_{1}, u_{2} such that x = Code(1, u_{1}, u_{2}) and T_{1}(u_{1}, u_{2}) holds or else there are v_{1}, v_{2} such that x = Code(2, v_{1}, v_{2}) and T_{2}(v_{1}, v_{2}) holds. It is easy to see that (∃y)α(T, y) is equivalent to

(∃y)(∃z_{β}, z_{γ})[ z_{β} = Code(1, u_{1}, u_{2}) ∧ z_{γ} = Code(2, v_{1}, v_{2}) ∧ α^{∗}]

and therefore Φ is equivalent to

(∀T)(∃y)(∃z_{β}, z_{γ})[ z_{β} = Code(1, u_{1}, u_{2}) ∧ z_{γ} = Code(2, v_{1}, v_{2}) ∧ α^{∗}].

Now consider the tree B of binary strings where the empty string is the root and each node ℓ has two children ℓ0 and ℓ1. For each T, let Branch(T) be the infinite branch of nodes l_{0}l_{1} ⋯ l_{d−1} such that the restriction T |d = T ∩ {0, …, d − 1} is equal to {i : l_{i} = 1}. For brevity we write x > y (or y < x) to mean that x > y_{i} for every component y_{i} of y. Fix all free variables of Φ. We construct a subset P of B such that, for every unary relation T, (∃y)α(T, y) holds if and only if Branch(T) intersects P. For each y, let c(y) be the maximum among the arguments of predicate T that occur in the quantifier-free formula α(T, y). Clearly,

(*) for every d > c(y), α(T, y) is equivalent to α(T |d, y).

Put a string l_{0} ⋯ l_{d−1} into P if and only if there exists y such that c(y) < d and the set T′ = {i : l_{i} = 1} satisfies α(T′, y). We fix a unary relation T and check that (∃y)α(T, y) holds if and only if Branch(T) intersects P. First suppose that α(T, y) holds for some y and set d = c(y) + 1, T′ = T |d. By (*), α(T′, y) holds. By the definition of P, the unique string ℓ of length d in Branch(T′) belongs to P. Of course ℓ ∈ Branch(T) as well. Thus, Branch(T) intersects P. Second suppose that a string ℓ = l_{0} ⋯ l_{d−1} belongs to Branch(T) and P, and let T′ = T |d = {i : l_{i} = 1}. Since ℓ ∈ P, we have that, for some y with c(y) < d, α(T′, y) holds and therefore α(T |d, y) holds. By (*), (∃y)α(T, y) holds. Let B′ be the subtree of B obtained by removing all strings ℓ such that a proper prefix of ℓ belongs to P. Notice that every maximal string ℓ in B′ (the maximality of ℓ means that neither ℓ0 nor ℓ1 belongs to B′) belongs to P. We show that B′ has no infinite branches if and only if

(**) (∃k)(∀T ⊆ {0, …, k − 1})(∃y)[ c(y) < k ∧ α(T, y) ].

First assume that B′ has no infinite branch. By König’s lemma, B′ is finite. Let k be one plus the maximal length of a string in B′. Every string ℓ of length k has a proper prefix in P; otherwise ℓ would belong to B′ which is impossible. Now let T be an arbitrary subset of {0, …, k − 1} and ℓ be the string l_{0} ⋯ l_{k−1} such that T = {i : l_{i} = 1}. Since |ℓ| = k, there is d < k such that the string l_{0} … l_{d−1} belongs to P. By the definition of P, there exists y such that c(y) < d and the set T′ = {i : i < d and l_{i} = 1} satisfies α(T′, y). Clearly, T′ = T |d. Now use (*) to establish (**).

Second assume (**) and fix an appropriate k. We prove that B′ has no infinite branch. By contradiction suppose that B′ has an infinite branch

l_{0}, l_{0}l_{1}, l_{0}l_{1}l_{2}, …

and define T = {i : i < k and l_{i} = 1}. By (**), there exists y such that c(y) < k and α(T, y). By the definition of P, the string l_{0} ⋯ l_{k−1} belongs to P. This contradicts the fact that l_{0} ⋯ l_{k} belongs to B′. We have that Φ holds if and only if every Branch(T) intersects P if and only if B′ has no infinite branches if and only (**) holds. It remains to notice that (**) is equivalent to a first-order formula of the form.

(∃k)(∀t)(∃y)α^{∗}(k, t, y).

α^{∗} can be obtained from [c(y) < k ∧ α(T, y)] by replacing each T (z) with a formula saying that z < k and there exist p and m such that p is prime, m is not divisible by p and t = p^{z}m. Lemma 4.2 is proved and thus Theorem 4.1 is proved.

5 On Classification of NP Optimization Problems

For brevity, we write Σ_{k} for Σ_{k}^{0} and the same for Π. An NP minimization problem [10, 6] is given by a tuple M = (I_{M}, F_{M}, f_{M}) such that

• I_{M} is a set of input instances, which is assumed to be recognizable in polynomial time.

• F_{M}(I) is a set of so-called feasible solutions for the input I.

• f_{M} is a polynomial time computable function, called the objective function, which takes positive integer values and is defined on pairs I, T, where I is an input instance and T is a feasible solution of I.

• The following decision problem is in NP: Given I ∈ I_{M} and an integer k, does there exist a feasible solution T ∈ F_{M}(I) such that f_{M}(I, T) ≤ k?

Define opt_{M}(I) = min_{T} f_{M}(I, T).

NP maximization problems are defined similarly. In particular, we have:

• The following decision problem is in NP: Given I ∈ I_{M} and an integer k, does there exist a feasible solution T ∈ F_{M}(I) such that f_{M}(I, T) ≥ k?

• opt_{M}(I) = max_{T} f_{M}(I, T).

A well-known minimization problem is MIN CHROMATIC NUMBER, where the instances I_{M} are finite graphs, feasible solutions for graph G are colorings of the vertices of G such that no two adjacent vertices have the same color, and the function f_{M}(G, T) is the number of colors used in T. An example of a maximization problem is MAX CONNECTED COM-PONENT: find the size of a largest connected component of an undirected finite graph. In the spirit of Fagin’s logical characterization of NP [4], characterizations of NP optimization problems in terms of logical definability have been given e.g. in [11, 10, 6]. An NP optimization problem is said to be polynomially bounded if there is a polynomial p such that

opt_{M}(I) ≤ p(|I|), for all I ∈ I_{M},

where |I| is the length of the input I. MIN PB (respectively MAX PB) denotes the class of all polynomially bounded NP minimization (respectively maximization) problems. We restrict attention to optimization problems whose inputs are finite structures of a fixed vocabulary. As shown in [6], an NP optimization problem M with finite structures A over a vocabulary σ is polynomially bounded if and only if there is a first-order formula φ(w, S) with predicates among those of σ and S such that for every instance A of M,

opt_{M}(A) = |{ w : (A, S) ⊧ φ(w, S) }|.

(Here and thereafter it is assumed that the universe of A contains at least two elements.) Moreover, in [6] hierarchies of classes of NP optimization problems have been analyzed. We start with minimization problems. Denote by MIN Σ_{k} (respectively MIN Π_{k}) the class of NP minimization problems definable by a Σ_{k} (respectively Π_{k}) formulas, k ≥ 0. According to [6],

MIN Σ_{0} = MIN Σ_{1} ⊂ MIN Π_{1} = MIN Σ_{2} = MIN PB. (8)

We show that for minimization problems over successor structures, MIN PB is contained in MIN Σ_{1}, so that all polynomially bounded minimization problems can be defined with a quantifier-free first-order formula. This fits Kolaitis and Thakur’s observation that “… the pattern of the quantifier prefix does not impact on the approximability of minimization problems” [6, p.348]. Theorem 2.1 allows one to strengthen Fagin’s theorem [4], that a class of finite structures closed under isomorphisms is recognizable in NP if and only if it is definable in existential second-order logic, as follows.

Lemma 5.1 Let K be a class of successor structures of vocabulary σ closed under isomorphisms. Then, K is NP if and only if K is definable by a Σ_{1}^{1} σ-formula of the form (∃S)(∀x)ψ, where ψ is quantifier-free.

Proof. Use Theorem 2.1.

Theorem 5.2 Let M be an NP minimization problem over successor structures of vocabulary σ. Then, M is in MIN PB if and only if there is an existential first-order formula φ(w, S) with predicates among those in σ and S such that for every instance A of M,

opt_{M}(A) = min_{S} |{w : (A, S) ⊧ φ(w, S)}|.

Thus,

MIN PB = MIN Σ_{1} = MIN Σ_{k} = MIN Π_{k}, for all k ≥ 1.

Proof. The proof is analogous to the proof of Theorem 3 in [6], but uses Lemma 5.1 instead of Fagin’s theorem. The if direction is obvious. For the only if direction, let m be a positive integer such that for any instance A, we have that opt_{M}(A) ≤ ∥A∥^{m}, where ∥A∥ is the size of the structure A (i.e., the size of the universe of A). Consider the following NP problem Q: Given a finite σ-structure A and an m-ary relation W on the universe A of A, is there a feasible solution T for A such that f_{M}(A, T) ≤ |W |? Here, f_{M} is the objective function of M and |W | is the cardinality of W. By Lemma 5.1, there is an existential second-order formula (∃T)(∀x)ψ(T, W, x), where ψ is quantifier-free, such that the expanded structure (A, W) is a YES instance of Q if and only if (A, W) ⊧ (∃T)(∀x)ψ. Since the minimization problem M is bounded by ∥A∥^{m}, we have that

opt_{M}(A) = min_{T,W}{ |W | : (A, T, W) ⊧ (∀x)ψ(T, W, x) }.

It follows that

opt_{M}(A) = min_{T,W} |{ w : (A, T, W) ⊧ (∀x)(ψ(T, W, x)) → W (w) }|
= min_{T,W} |{ w : (A, T, W) ⊧ (∃x)(¬ψ(T, W, x)) ∨ W (w) }|

Let S denote the sequence (T, W) and let φ(w, S) be a Σ_{1} formula logically equivalent to (∃x)(¬ψ(T, W, x)) ∨ W (w). It follows that

opt_{M}(A) = min_{S} |{ w : (A, S) ⊧ φ(w, S) }|.

This proves the theorem.

Combining Theorem 5.2 with Kolaitis and Thakur’s result that MIN Σ_{0} = MIN Σ_{1}, we get:

Corollary 5.3 In the case of successor structures, a minimization problem is polynomially bounded if and only if it is definable with a quantifier-free first order formula, that is,

MIN PB = MIN Σ_{0} = MIN Σ_{k}, for all k.

Remark. The classes MIN Σ_{1} and MIN Σ_{2} are separated in [6] by showing that the problem MIN CHROMATIC NUMBER is in MIN Σ_{2} but not in MIN Σ_{1} (Theorem 4, Part B). The proof in [6] uses the fact that a graph G obtained by taking the direct sum of graphs H_{1} and H_{2} without common vertices is an extension of both H_{1} and H_{2}. In our case, each graph has to have, in addition to the edge relation, a successor relation and the corresponding First and Last relations. In fact, G can extend neither H_{1} nor H_{2}. Indeed, assume G extends, say, H_{1}. Check by induction on k, that kth element of H_{1} is the kth element of G. Further, the last element of H_{1} is the last element of G. Thus G contains no elements of H_{2} which is impossible. Thus, the proof in [6] fails for successor structures.

We turn our attention to maximization problems. Denote by MAX Σ_{k} (respectively MAX Π_{k}) the class of NP maximization problems definable by Σ_{k} (respectively Π_{k}) formulas, k ≥ 0. According to [6],

MAX Σ_{0} ⊂ MAX Σ_{1} ⊂ MAX Σ_{2} = MAX Π_{1} ⊂ MAX Π_{2} = MAX PB. (9)

Over successor structures, MAX Π_{2} collapses to MAX Π_{1}.

Theorem 5.4 Let M be a maximization problem over successor structures of vocabulary σ. Then, M is in MAX PB if and only if there is a universal first-order formula φ(w, S) with predicate symbols among those in σ and S such that for every instance A of M,

opt_{M}(A) = max_{S} |{w : (A, S) ⊧ φ(w, S)}|.

Thus

MAX PB = MAX Π_{1} = MAX Σ_{k} = MAX Π_{k}, for all k ≥ 2.

Proof. The proof is similar to the proof of Theorem 1 in [6]. Follow the same arguments as in Theorem 5.2 to show that if M is a polynomially bounded NP maximization problem over finite successor structures, then there is a Π_{1} formula ψ(T, W) such that

opt_{M}(A) = max_{T,W}{ |W | : (A, T, W) ⊧ ψ(T, W) },

or equivalently,

opt_{M}(A) = max_{T,W} |{ w : (A, T, W) ⊧ ψ(T, W, x) ∧ W (w) }|.

Let S denote the sequence (T, W) and let φ(w, S) be a Π_{1} formula logically equivalent to ψ(T, W) ∧ W (w). It follows that

opt_{M}(A) = max_{S} |{ w : (A, S) ⊧ φ(w, S) }|.

Remark. The classes MAX Π_{1} and MAX Π_{2} are separated in [6] by showing that the problem MAX CONNECTED COMPONENT is in MAX Π_{2} but not in MAX Π_{1} (Theorem 2, part B). The proof in [6] fails for successor structures, since it uses the fact that certain graphs H_{i}, obtained by removing vertices a_{i} from the input graph G, are substructures of G.

Contrary to the case of minimization problems, not every polynomially bounded NP maximization problem can be defined over successor structures with a quantifier-free first-order formula. In fact, the two leftmost containments of the hierarchy (9) are also strict for successor structures and even for ordered successor structures. We show this by exhibiting two NP maximization problems, EVEN and EMPTY, which separate the classes MAX Σ_{0}, MAX Σ_{1}, and MAX Σ_{2} in the case of ordered successor structures.

• EVEN: The instances are ordered successor structures without any additional predicates (that is of vocabulary {<, Succ, F, L}), the only feasible solution for a structure A is the empty set, and the function f_{EVEN}(A, ∅) equals 1 if ∥A∥ is even and equals 2 otherwise.

• EMPTY: The instances are ordered successor structures of vocabulary {<, Succ, F, L, P } where P is a unary predicate. The only feasible solution T for a structure A is the relation P, and f_{EMPTY}(A, P) equals 1 if P is empty and equals 2 otherwise.^{1}

Note that both problems are easily solvable in polynomial time.

Theorem 5.5 (i) EVEN is in MAX Σ_{2} but not in MAX Σ_{1}, and (ii) EMPTY is in MAX Σ_{1} but not in MAX Σ_{0}.

Proof. Part (i). Clearly, EVEN is polynomially bounded, and hence, by Theorem 5.4, it is in MAX Σ_{2}. By contradiction assume that EVEN is in MAX Σ_{1}. There exists a formula (∃x)φ(w, x, S) where φ is quantifier-free such that, for all A,

opt_{EVEN}(A) = |{ w : (A, S) ⊧ (∃x)φ(w, x, S) }|.

Let k be the number of variables in φ and let A be such that ∥A∥ > 2k and ∥A∥ is odd. Let S^{∗} be such that |{w : (A, S^{∗}) ⊧ (∃x)φ }| is maximal. Let v denote the sequence wx. Since opt_{EVEN}(A) = 2, there exist on A two tuples v_{1}, v_{2} different on their w-parts such that (A, S^{∗}) ⊧ φ(v_{i}, S^{∗}) for i = 1, 2. Since ∥A∥ > 2k, there exists an element a of A such that a does not occur in v_{1} or v_{2}. Let b be an element adjacent to a and let A′ be the structure obtained from A by inserting a new element between a and b. Each φ(v_{i}, S^{∗}) is satisfied in A′. This implies opt_{EVEN}(A′) ≥ 2. However, since the size of the universe of A′ is even, opt_{EVEN}(A′) = 1. Thus we arrived at the desired contradiction.

Part (ii). Clearly, EMPTY is in MAX Σ_{1}; it can be defined e.g. by formula

1It may seem more natural to use 0 rather than 2 as a value for f_{EMP T Y} and f_{EV EN}, but the objective functions take only positive values.

(∃x)[ (F (w) ∧ P (x)) ∨ L(w) ]

which is equivalent to [F (w) ∧ (∃x)P (x)] ∨ L(w). (Recall that structures A are supposed to have at least two elements.) By contradiction suppose that EMPTY is in MAX Σ_{0}, so that some quantifier-free formula φ(w, S) defines EMPTY:

opt_{EMPTY}(A) = max_{S} |{w : (A, S) ⊧ φ(w, S)}|.

Let k be the number of distinct variables in φ, and let A be an instance of EMPTY such that ∥A∥ = n > 20k and P = {a_{10k}}, where a_{1}, a_{2}, …, a_{n} are the elements of A in the order of A. Then, opt_{EMPTY}(A) = 2. The idea is to modify A and to find some S on the new structure A′ such that there are more than two tuples w satisfying φ(w, S) in (A′, S). Let S_{0} be such that |{ w : (A, S_{0}) ⊧ φ(w, S_{0}) }| is maximal. Then there exist distinct tuples w_{1}, w_{2} such that (A, S_{0}) ⊧ φ(w_{i}, S_{0}) for i = 1, 2. Elements that occur in w_{1} or w_{2} will be called red. It is easy too see that a_{10k} is red. Otherwise let A_{0} be the structure obtained from A by removing a_{10k} from P. We have (A_{0}, S_{0}) ⊧ φ(w_{i}, S_{0}) for i = 1, 2 and thus opt_{EMPTY}(A_{0}) ≥ 2. It is clear, however, that opt_{EMPTY}(A_{0}) = 1. Obviously there is i < 10k such that neither a_{i} nor a_{i+1} is red. Let [a_{ℓ}, a_{u}] be the first contiguous red segment after a_{i+1}. In other words, a_{ℓ} is the least red element > a_{i+1} and a_{u+1} is the least non-red element > a_{ℓ}. Clearly u < 10k + 2k < n. Let A′ be a structure obtained from A as follows: Add a segment a′_{ℓ}, a′_{ℓ+1}, …, a′_{u} of new elements between a_{i} and a_{i+1} and put a′_{10k} into P if l ≤ 10k ≤ u. Let S_{1} be obtained from S_{0} by replacing elements a_{j} with the corresponding elements a′_{j}, ℓ ≤ j ≤ u. Let S_{2} be the union of S_{0} and S_{1}. It is clear that (A′, S_{2}) ⊧ φ(w_{i}, S_{2}). Let w′_{i} be the tuple obtained from w_{i} by replacing elements a_{j} with the corresponding elements a′_{j}, ℓ ≤ j ≤ u. We have (A′, S_{2}) ⊧ φ(w′_{1}, S_{2}) for i = 1, 2. Obviously, w′_{1} ≠ w_{1} or w′_{2} ≠ w_{2}. It follows that

opt_{EMPTY}(A′) = max_{S} |{ w : (A′, S) ⊧ φ(w, S) }| ≥ |{ w : (A′, S_{2}) ⊧ φ(w, S_{2}) }| ≥ 3.

However, opt_{EMPTY}(A′) = 2. This gives the desired contradiction.

From Theorems 5.4 and 5.5 we obtain the following.

Corollary 5.6 In the case of successor or ordered successor structures, the polynomially bounded maximization problems form the following hierarchy:

MAX Σ_{0} ⊂ MAX Σ_{1} ⊂ MAX Σ_{2} = MAX Π_{1} = MAX PB.

Acknowledgment The authors would like to thank Andreas Blass and Daniel Leivant for helpful discussions related to Lemma 4.2.

References

[1] J. Barwise. Admissible Sets and Structures: An Approach to Definability Theory. Springer Verlag, 1975.

[2] C. C. Chang and H. J. Keisler. Model Theory. North-Holland, 2nd edition, 1973.

[3] T. Eiter, G. Gottlob, and H. Mannila. Adding Disjunction to Datalog. In Proceedings of the Thirteenth ACM SIGACT SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-94), pages 267–278, May 1994.

[4] R. Fagin. Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. In R. M. Karp, editor, Complexity of Computation, pages 43–74. AMS, 1974.

[5] S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.

[6] P. Kolaitis and M. N. Thakur. Logical Definability of NP Optimization Problems. Information and Computation, 115:321–353, 1994.

[7] P. Kolaitis and M. Y. Vardi. 0-1 Laws and Decision Problems for Fragments of Second-Order Logic. Information and Computation, 87:302–338, 1990.

[8] D. Leivant. Descriptive Characterizations of Computational Complexity. Journal of Computer and System Sciences, 39:51–83, 1989.

[9] Y. Matijasevich. Hilbert’s Tenth Problem. MIT Press, 1993.

[10] A. Panconesi and D. Ranjan. Quantifiers and Approximation. Theoretical Computer Science, 107:145–163, 1993.

[11] C. H. Papadimitriou and M. Yannakakis. Optimization, Approximation, and Complexity Classes. Journal of Computer and System Sciences, 43:425–440, 1991.

[12] I. Stewart. Comparing the Expressibility of Languages Formed Using NP-complete Operators. Journal of Logic and Computation, 1:305–330, 1991.

[13] J. van Benthem and K. Doets. Higher Order Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol.I, chapter I.4, pages 275–329. D. Reidel Publishing Company, 1983.