<p>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$.)</p>

<p>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 <a href="http://www.cs.toronto.edu/~sacook/homepage/book">here</a>).</p>

<p>Antonina Kolokolova has worked on relations between these two approaches.</p>

CC BY-SA 2.5
2010-08-17T01:55:39.530Z
2010-08-17T07:21:19.750Z
2010-08-17T07:21:19.750Z
Kaveh
<p>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: <a href="http://www.cs.umass.edu/~immerman/">http://www.cs.umass.edu/~immerman/</a></p>

CC BY-SA 2.5
2010-08-16T23:40:23.640Z
This picture is worth many thousands of words.
András Salamon
CC BY-SA 2.5
2010-08-17T01:12:13.813Z
Immerman's book is probably the best single reference for the direct links between logic and computational complexity.  This topic is usually called "Descriptive Complexity", as is the book.
András Salamon
CC BY-SA 2.5
2010-08-16T21:58:36.573Z
2010-08-16T21:58:36.573Z
Aaron Sterling
<p>For those not familiar with the multitude of acronyms found in <a href="http://www.cs.umass.edu/~immerman/book/descriptiveComplexity.html">Immerman's great diagram</a> there is a Wikipedia article on <a href="http://en.wikipedia.org/wiki/Descriptive_complexity">descriptive complexity</a>. 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.</p>

<p><i>This is not an answer but a comment to Aarons answer, which I cannot comment on for some reason.</i></p>

CC BY-SA 2.5
2010-09-07T08:23:18.823Z
you need a little more rep to post a comment (it's a spam blocking mechanism).
Suresh Venkat
CC BY-SA 2.5
2010-09-07T08:10:18.160Z
2010-09-07T08:10:18.160Z
Jakob
<p>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 <a href="http://michaelnielsen.org/polymath1/index.php?title=Deolalikar_P_vs_NP_paper">wiki</a>) are </p>

<ul>
<li><a href="http://www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf">Erich Gradel's review of FMT and descriptive complexity</a></li>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=38D2317557C5EF25F3ED6D0D3CBE6E69?doi=10.1.1.28.6917&amp;rep=rep1&amp;type=pdf">Ron Fagin's article on descriptive complexity</a></li>
</ul>

CC BY-SA 2.5
2010-08-17T01:13:45.260Z
I think the scope of FMT is slightly broader than just linking logic and computational complexity.  Descriptive complexity seems a more precise term.
András Salamon
CC BY-SA 2.5
2010-08-16T20:31:32.583Z
2010-08-16T20:31:32.583Z
Suresh Venkat
<p>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, ...).</p>

<p>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).</p>

<p>Is there a good summary of these techniques and results?</p>

<cc.complexity-theory><lo.logic><computability>
Correspondence between complexity classes and logic
ripper234
# Correspondence between complexity classes and logic

(Asked by: username_0 on 2010-08-16)

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?

**Tags:** cc.complexity-theory, lo.logic, computability

---

## 4 answers

### Answer by username_5 on 2010-08-16. Score: 23 | Accepted answer

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](http://michaelnielsen.org/polymath1/index.php?title=Deolalikar_P_vs_NP_paper)) are

* [Erich Gradel's review of FMT and descriptive complexity](http://www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf)
* [Ron Fagin's article on descriptive complexity](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=38D2317557C5EF25F3ED6D0D3CBE6E69?doi=10.1.1.28.6917&rep=rep1&type=pdf)

> **Comments:**
> **username_3**: I think the scope of FMT is slightly broader than just linking logic and computational complexity.  Descriptive complexity seems a more precise term.  

---

### Answer by username_2 on 2010-08-16. Score: 25

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/>

> **Comments:**
> **username_3**: This picture is worth many thousands of words.  
> **username_3**: Immerman's book is probably the best single reference for the direct links between logic and computational complexity.  This topic is usually called "Descriptive Complexity", as is the book.  

---

### Answer by username_1 on 2010-08-17. Score: 16

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](http://www.cs.toronto.edu/~sacook/homepage/book)).

Antonina Kolokolova has worked on relations between these two approaches.


---

### Answer by username_4 on 2010-09-07. Score: 11

For those not familiar with the multitude of acronyms found in [Immerman's great diagram](http://www.cs.umass.edu/~immerman/book/descriptiveComplexity.html) there is a Wikipedia article on [descriptive complexity](http://en.wikipedia.org/wiki/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.*

> **Comments:**
> **username_5**: you need a little more rep to post a comment (it's a spam blocking mechanism).  

---

