Correspondence between complexity classes and logic 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?
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/