## Monday, November 07, 2005

### Favorite Logic of November 2005: Second-Order Logic

Last month we talked about monadic second-order logic (MSO). We now shall proceed to a more expressive logic: second-order logic (SO) and some of its fragments, such as existential second-order logic (ESO) and universal second-order logic (ASO). In fact, some of the most tantalizing open questions in complexity theory can be reduced to questions about the expressive power of the afore-mentioned logics. More precisely, ESO equals NP, whereas ASO equals coNP. Hence, to separate P from NP, it is sufficient to prove that ASO and ESO have different expressive power. Since we have numerous tools for proving inexpressibility results in finite model theory, it is natural to ask whether it is possible to separate NP from coNP using finite model theory. This, as you would have expected, is still open. However, we have managed to prove a weaker version: that Monadic NP is different from Monadic coNP.

So, what exactly is SO? MSO permits quantifications over sets (i.e. unary relations). SO is just a generalization of this idea: you are allowed to quantify over k-ary relations. So, formulas in SO will look like

ψ := Q1X1...QmXm φ

where Q ∈ {∃,∀}, Xi is a ki-ary "second-order variable" to be interpreted as a ki-ary relation, and φ is just a first-order (FO) formula that talks about these second-order variables as well as some relations in the given vocabulary. An example of a sentence in this logic has been given in here, in which case all second-order variables are unary. Another example that uses non-unary relations is hamiltonianicity:

∃ L ∃ S ( (L is a strict linear ordering over the vertices) and (S is L's successor relation) and ∀ x ∀ y( S(x,y) -> E(x,y) ) )

A graph is hamiltonian iff there exists a path that visits every vertex in the graph. You can think of L as the transitive closure of the path P that witnesses the hamiltonianicity of the graph, and of S as the path P. [Example: a strict linear ordering on {1,2,3} is the binary relation ≤ = {(1,2),(1,3),(2,3)}, while its successor relation is the binary relation {(1,2),(2,3)}. Perhaps, it is more descriptive to say "immediate successor" than just "successor".] Notice that in these two examples we only used ∃ quantifiers for the second-order variables. We use ESO (read: existential second-order logic) to denote all formulas in SO of this kind, i.e., where all the Qi is ∃. We use ASO (read: universal second-order logic) to denote formulas in SO where Qi equals ∀.

Theorem (Fagin 1974): ESO captures NP. ASO captures coNP.

The notion of "capture" here has been defined in a previous post. The examples above give two concrete NP properties (hamiltonianicity, and 3-colorability) that you can express in ESO. How do you express non-hamiltonianicity in ASO? It's simple: just negate the formula above and use the fact that "not ∃ Xi ψ" is equivalent to "∃ Xi not &psi". This can easily be generalized to other coNP properties. Let's summarize the results.

Theorem: NP = coNP iff ESO = ASO iff 3-colorability is expressible in ASO.

What complexity class does SO correspond to?

Theorem (Stockmeyer 1977) SO captures PH.

Actually, Stockmeyer proved a much stronger result relating the kth level in the hierarchy to an SO fragment that contains formulas with k second-order quantifier alternation.

Of course, we have not been successful in proving that ESO != ASO. However, a weaker version has been proven in the literature.