Correspondencia entre clases de complejidad y lógica.

Una vez tomé una clase sobre computabilidad y lógica. El material incluía una correlación entre las clases de complejidad / computabilidad (R, RE, co-RE, P, NP, Logspace, ...) y la lógica (cálculo de predicados, lógica de primer orden, ...).

La correlación incluyó varios resultados en un campo, que se obtuvieron utilizando técnicas del otro campo. Se conjeturó que P! = NP podría ser atacado como un problema en la lógica (proyectando el problema desde el dominio de las clases de complejidad a la lógica).

¿Hay un buen resumen de estas técnicas y resultados?

Es posible que esté preguntando acerca de los resultados en la teoría de modelos finitos (como la caracterización de P y NP en términos de varios fragmentos de lógica). El reciente intento de prueba de P! = NP inicialmente hizo un uso intensivo de tales conceptos, y algunas buenas referencias (tomadas de la wiki ) son

• Revisión de Erich Gradel sobre FMT y complejidad descriptiva
• Artículo de Ron Fagin sobre complejidad descriptiva

Neil Immerman produjo un hermoso diagrama que proporciona correspondencias de un vistazo entre clases de complejidad y lógicas interpretadas por modelos finitos. Está en la portada de su libro, y también en la parte inferior de su página web aquí: http://www.cs.umass.edu/~immerman/

Conozco dos formas de asociar la lógica con las clases de complejidad. El primero es la complejidad descriptiva, que es el modelo teórico mencionado en otras respuestas. (Volviendo a la caracterización de de Ronald Fagin ).$NP$

El segundo enfoque (que también es un poco más antiguo, volviendo a las obras de personas como Steve Cook y Sam Buss) es una prueba teórica. Aquí una clase de complejidad está asociada con teorías en aritmética. Las funciones demostrablemente totales de estas teorías son exactamente las funciones en la clase de complejidad. Por ejemplo, las funciones probables totales de la teoría 1_2 de Sam Buss son funciones computables de tiempo polinomial exactamente. También hay enlaces con sistemas de prueba proposicionales. Para obtener más información sobre este enfoque, consulte el libro de Jan Krajicek "Aritmética limitada, lógica proposicional y teoría de la complejidad", 1995, o Stephen A. Cook y Phuong El libro más reciente de Nguyen "FUNDAMENTOS LÓGICOS DE LA COMPLEJIDAD DE LA PRUEBA", 2010 (se puede encontrar un borrador aquí )$S^1_2$

Antonina Kolokolova ha trabajado en las relaciones entre estos dos enfoques.

Para aquellos que no están familiarizados con la multitud de siglas que se encuentran en el gran diagrama de Immerman, hay un artículo de Wikipedia sobre la complejidad descriptiva . Debe haber un diagrama con enlaces, para que pueda buscar directamente la definición en Complexity Zoo y otras fuentes. También me gustaría ver mejor las relaciones con los lenguajes / gramáticas formales correspondientes y dónde puede encontrar la prueba.

Esta no es una respuesta, sino un comentario a la respuesta de Aarons, que no puedo comentar por alguna razón.