Correspondence between complexity classes and logic

Question

I took a class once on Computability and Logic. The material included a correlation between complexity / computability classes (R, RE, co-RE, P, NP, Logspace, ...) and Logics (Predicate calculus, first order logic, ...).

The correlation included several results in one fields, that were obtained using techniques from the other field. It was conjectured that P != NP could be attacked as a problem in Logic (by projecting the problem from the domain of complexity classes to logics).

Is there a good summary of these techniques and results?

Answer 1

It's possible that you're asking about results in finite model theory (such as the characterization of P and NP in terms of various fragments of logic). The recent attempted proof of P != NP initially made heavy use of such concepts, and some good references (taken from the wiki) are

• Erich Gradel's review of FMT and descriptive complexity
• Ron Fagin's article on descriptive complexity

Answer 2

Neil Immerman produced a beautiful diagram that provides at-a-glance correspondences between complexity classes and logics interpreted by finite models. It's on the cover of his book, and also at the bottom of his web page here: http://www.cs.umass.edu/~immerman/

Answer 3

I know two ways of associating logic with complexity classes. The first one is descriptive complexity which is model theoretic mentioned in other answers. (Going back to Ronald Fagin's characterization of $NP$.)

The second approach (which is also a little bit older going back to works of people like Steve Cook ans Sam Buss) is proof theoretic. Here a complexity class is associated with theories in arithmetic. The provably total functions of these theories are exactly the functions in the complexity class. For example, provably total functions of Sam Buss's theory $S^1_2$ are exactly polynomial time computable functions. There are also links with propositional proof systems. For more on this approach check Jan Krajicek's book "Bounded arithmetic, propositional logic, and complexity theory", 1995, or Stephen A. Cook and Phuong The Nguyen's more recent book "LOGICAL FOUNDATIONS OF PROOF COMPLEXITY" , 2010 (a draft can be found here).

Antonina Kolokolova has worked on relations between these two approaches.

Answer 4

For those not familiar with the multitude of acronyms found in Immerman's great diagram there is a Wikipedia article on descriptive complexity. There should be a diagram with links, so you could directly look up the definition in Complexity Zoo and other sources. I'd also like to better see the relations to the corresponding formal languages/grammars and where you can find the proof.

This is not an answer but a comment to Aarons answer, which I cannot comment on for some reason.