Normal forms for second-order logic over finite structures, and classification of NP optimization problems Original Research Article

We start with a simple proof of Leivantʹs normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following: 1. (i) over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and 2. (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 ∑21 fails if ∑21 is replaced with ∑11 or if infinite structures are allowed.