Lógicas para la computabilidad

Las lógicas de computabilidad son formulaciones lógicas que capturan algún aspecto de la computabilidad como noción básica. Esto suele implicar una combinación de conectores lógicos especiales , así como una semántica que explica cómo interpretar la lógica desde una perspectiva computacional.

Probablemente, el primer tratamiento formal de la lógica para la computabilidad sea la interpretación de realizabilidad propuesta por Stephen Kleene en 1945, quien ofreció una interpretación de la teoría de números intuicionista en términos de cálculos de máquinas de Turing . Su motivación era precisar la interpretación de Heyting-Brouwer-Kolmogorov (BHK) del intuicionismo, según la cual las demostraciones de enunciados matemáticos deben considerarse procedimientos constructivos.

Con el auge de muchos otros tipos de lógica, como la lógica modal y la lógica lineal , y nuevos modelos semánticos, como la semántica de juegos , se han formulado lógicas para la computabilidad en diversos contextos. Aquí mencionamos dos.

La interpretación original de Kleene sobre la realizabilidad ha recibido mucha atención entre quienes estudian las conexiones entre la computabilidad y la lógica. En 1982, Martin Hyland la extendió a la lógica intuicionista de orden superior completa , construyendo el topos efectivo . En 2002, Steve Awodey , Lars Birkedal y Dana Scott formularon una lógica modal para la computabilidad , que extendió la interpretación habitual de la realizabilidad con dos operadores modales que expresan la noción de ser "computablemente verdadero".

La lógica de la computabilidad se refiere a un programa de investigación iniciado por Giorgi Japaridze en 2003. Su objetivo es reformular la lógica a partir de una semántica de la teoría de juegos. Dicha semántica considera los juegos como equivalentes formales de problemas computacionales interactivos, y su "verdad" como la existencia de estrategias algorítmicas ganadoras.

• semántica de juegos
• Computación interactiva

• SC Kleene. Sobre la interpretación de la teoría intuicionista de números . Journal of Symbolic Logic , 10:109-124, 1945.
• JME Hyland. El topos efectivo . En AS Troelstra y D. van Dalen , editores, Simposio del Centenario de LEJ Brouwer, páginas 165-216. North Holland Publishing Company, 1982.
• S. Awodey, L. Birkedal y DS Scott. Topos de realizabilidad local y una lógica modal para la computabilidad . Mathematical Structures in Computer Science, 12(3):319-334, 2002.
• G. Japaridze, Introducción a la lógica de la computabilidad . Anales de lógica pura y aplicada 123 (2003), páginas 1–99.

• Lógica de tipos y computación en CMU
• Página principal de Computability Logic
• Giorgi Japaridze
• ¿Semántica de juegos o lógica lineal?