Las lógicas para la computabilidad son formulaciones de lógica que capturan algún aspecto de la computabilidad como una noción básica. Esto generalmente implica una combinación de conectores lógicos especiales , así como una semántica que explica cómo se debe interpretar la lógica de manera computacional.
Probablemente el primer tratamiento formal de la lógica para la computabilidad es la interpretación de la realizabilidad de Stephen Kleene en 1945, quien dio una interpretación de la teoría de números intuicionista en términos de cálculos de la máquina de Turing . Su motivación era hacer precisa 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 surgimiento de muchos otros tipos de lógica, como la lógica modal y la lógica lineal , y de nuevos modelos semánticos, como la semántica de juegos , se han formulado lógicas para la computabilidad en varios 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. Martin Hyland la amplió a la lógica intuicionista de orden superior en 1982, cuando construyó el topos efectivo . En 2002, Steve Awodey , Lars Birkedal y Dana Scott formularon una lógica modal para la computabilidad , que amplió la interpretación habitual de la realizabilidad con dos operadores modales que expresaban la noción de ser "computablemente verdadero".
"Lógica de computabilidad" es un nombre propio que hace referencia a un programa de investigación iniciado por Giorgi Japaridze en 2003. Su ambición es volver a desarrollar la lógica a partir de una semántica de teoría de juegos. Esta semántica considera los juegos como equivalentes formales de problemas computacionales interactivos y su "verdad" como la existencia de estrategias algorítmicas ganadoras. Véase Lógica de computabilidad