Las lógicas para la computabilidad son formulaciones de lógica que capturan algún aspecto de la computabilidad como noción básica. Esto generalmente implica una mezcla de conectivos lógicos especiales , así como semántica, lo que explica cómo se debe interpretar la lógica de una manera computacional.
Probablemente el primer tratamiento formal de la lógica para la computabilidad sea la interpretación de realizabilidad de Stephen Kleene en 1945, quien dio una interpretación de la teoría intuicionista de números en términos de cálculos de máquina de Turing . Su motivación era precisar la interpretación de Heyting-Brouwer-Kolmogorov (BHK) del intuicionismo, según la cual las pruebas de enunciados matemáticos deben considerarse como procedimientos constructivos.
Con el surgimiento de muchos otros tipos de lógica, como la lógica modal y la lógica lineal , y los modelos semánticos novedosos, como la semántica de juegos , se han formulado lógicas para la computabilidad en varios contextos. Aquí mencionamos dos.
Lógica modal para computabilidad
La interpretación de realizabilidad original de Kleene ha recibido mucha atención entre aquellos que estudian las conexiones entre computabilidad y lógica. Fue ampliado a la lógica intuicionista de orden superior completo por Martin Hyland en 1982, quien construyó 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 de realizabilidad habitual con dos operadores modales que expresan la noción de ser "computablemente verdadero".
Lógica de computabilidad de Japaridze
"Computability Logic" es un nombre propio que se refiere 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. Tal semántica ve los juegos como equivalentes formales de problemas computacionales interactivos, y su "verdad" como existencia de estrategias algorítmicas ganadoras. Ver lógica de computabilidad .
Referencias
- SC Kleene. Sobre la interpretación de la teoría intuicionista de números . Revista de lógica simbólica, 10: 109-124, 1945.
- JME Hyland. Los topos efectivos . En AS Troelstra y D. Van Dalen, editores, The LEJ Brouwer Centenary Symposium, páginas 165-216. Compañía Editorial de Holanda Septentrional, 1982.
- S. Awodey, L. Birkedal y DS Scott. Topos de realizabilidad local y una lógica modal para la computabilidad . Estructuras matemáticas en informática, 12 (3): 319-334, 2002.
- G. Japaridze, Introducción a la lógica de computabilidad . Annals of Pure and Applied Logic 123 (2003), páginas 1–99.