NORMAL FORMS FOR 2ND-ORDER LOGIC OVER FINITE STRUCTURES, AND CLASSIFICATION OF NP OPTIMIZATION PROBLEMS

We start with a simple proof of Leivant's normal form theorem for Sigm a(1)(1) formulas over finite successor structures. Then we use that no rmal form to prove the following: (i) over all finite structures, ever y Sigma(2)(1) formula is equivalent to a Sigma(2)(1) formula whose fir st-order part is a Boolean combination of existential formulas, and (i i) over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hie rarchy of maximization problems collapses partially. The normal form t heorem for Sigma(2)(1) fails if Sigma(2)(1) is replaced with Sigma(1)( 1) or if infinite structures are allowed.