La semántica de juegos ( en alemán : dialogische Logik , traducido como lógica dialógica ) es un enfoque de la semántica formal que fundamenta los conceptos de verdad o validez en conceptos de teoría de juegos , como la existencia de una estrategia ganadora para un jugador, algo similar a los diálogos socráticos o a la teoría medieval de las Obligationes .
A finales de los años 50, Paul Lorenzen fue el primero en introducir una semántica de juegos para la lógica , que fue desarrollada posteriormente por Kuno Lorenz . Casi al mismo tiempo que Lorenzen, Jaakko Hintikka desarrolló un enfoque teórico de modelos conocido en la literatura como GTS (semántica teórica de juegos). Desde entonces, se han estudiado varias semánticas de juegos diferentes en lógica.
Shahid Rahman ( Lille III ) y sus colaboradores desarrollaron la lógica dialógica como marco general para el estudio de cuestiones lógicas y filosóficas relacionadas con el pluralismo lógico . A principios de 1994, esto desencadenó una especie de renacimiento con consecuencias duraderas. Este nuevo impulso filosófico experimentó una renovación paralela en los campos de la informática teórica , la lingüística computacional , la inteligencia artificial y la semántica formal de los lenguajes de programación , por ejemplo, el trabajo de Johan van Benthem y sus colaboradores en Ámsterdam, quienes analizaron en profundidad la interfaz entre la lógica y los juegos, y Hanno Nickau, quien abordó el problema de la abstracción total en los lenguajes de programación por medio de juegos. Los nuevos resultados en lógica lineal de Jean-Yves Girard en las interfaces entre la teoría de juegos matemáticos y la lógica por un lado y la teoría de la argumentación y la lógica por el otro dieron lugar al trabajo de muchos otros, incluidos S. Abramsky , J. van Benthem, A. Blass , D. Gabbay , M. Hyland , W. Hodges , R. Jagadeesan, G. Japaridze , E. Krabbe, L. Ong, H. Prakken, G. Sandu, D. Walton y J. Woods, quienes colocaron la semántica de juegos en el centro de un nuevo concepto en lógica en el que la lógica se entiende como un instrumento dinámico de inferencia. También ha habido una perspectiva alternativa sobre la teoría de la prueba y la teoría del significado, defendiendo que el paradigma del "significado como uso" de Wittgenstein tal como se entiende en el contexto de la teoría de la prueba, donde las llamadas reglas de reducción (que muestran el efecto de las reglas de eliminación sobre el resultado de las reglas de introducción) deberían considerarse apropiadas para formalizar la explicación de las consecuencias (inmediatas) que uno puede extraer de una proposición, mostrando así la función/propósito/utilidad de su conectivo principal en el cálculo del lenguaje (de Queiroz (1988), de Queiroz (1991), de Queiroz (1994), de Queiroz (2001), de Queiroz (2008), de Queiroz (2023)).
La aplicación más simple de la semántica de juegos es la lógica proposicional . Cada fórmula de este lenguaje se interpreta como un juego entre dos jugadores, conocidos como el "Verificador" y el "Falsificador". Al Verificador se le da la "propiedad" de todas las disyunciones en la fórmula, y al Falsador se le da asimismo la propiedad de todas las conjunciones . Cada movimiento del juego consiste en permitir que el propietario del conectivo principal elija una de sus ramas; el juego continuará entonces en esa subfórmula, y el jugador que controle su conectivo principal hará el siguiente movimiento. El juego termina cuando los dos jugadores han elegido una proposición primitiva; en este punto, el Verificador se considera ganador si la proposición resultante es verdadera, y el Falsador se considera ganador si es falsa. La fórmula original se considerará verdadera precisamente cuando el Verificador tenga una estrategia ganadora , mientras que será falsa siempre que el Falsador tenga la estrategia ganadora.
Si la fórmula contiene negaciones o implicaciones, se pueden utilizar otras técnicas más complicadas. Por ejemplo, una negación debe ser verdadera si lo negado es falso, por lo que debe tener el efecto de intercambiar los papeles de los dos jugadores.
En términos más generales, la semántica de juegos puede aplicarse a la lógica de predicados ; las nuevas reglas permiten que un cuantificador principal sea eliminado por su "dueño" (el Verificador para cuantificadores existenciales y el Falsificador para cuantificadores universales ) y que su variable ligada sea reemplazada en todas las ocurrencias por un objeto elegido por el dueño, extraído del dominio de cuantificación. Nótese que un único contraejemplo falsifica una afirmación cuantificada universalmente, y un único ejemplo es suficiente para verificar una afirmación cuantificada existencialmente. Suponiendo el axioma de elección , la semántica de teoría de juegos para la lógica clásica de primer orden concuerda con la semántica usual basada en modelos (tarskiana) . Para la lógica clásica de primer orden, la estrategia ganadora para el Verificador consiste esencialmente en encontrar funciones de Skolem y testigos adecuados . Por ejemplo, si S denota entonces una afirmación equisatisfacible para S es . La función de Skolem f (si existe) en realidad codifica una estrategia ganadora para el Verificador de S al devolver un testigo para la subfórmula existencial para cada elección de x que el Falsificador pudiera hacer. [1]
La definición anterior fue formulada por primera vez por Jaakko Hintikka como parte de su interpretación de la GTS. La versión original de la semántica de juegos para la lógica clásica (e intuicionista) debida a Paul Lorenzen y Kuno Lorenz no se definió en términos de modelos sino de estrategias ganadoras sobre diálogos formales (P. Lorenzen, K. Lorenz 1978, S. Rahman y L. Keiff 2005). Shahid Rahman y Tero Tulenheimo desarrollaron un algoritmo para convertir las estrategias ganadoras de la GTS para la lógica clásica en estrategias ganadoras dialógicas y viceversa.
Los diálogos formales y los juegos GTS pueden ser infinitos y utilizar reglas de fin de juego en lugar de dejar que los jugadores decidan cuándo dejar de jugar. Llegar a esta decisión por medios estándar para inferencias estratégicas ( eliminación iterada de estrategias dominadas o IEDS) sería, en GTS y diálogos formales, equivalente a resolver el problema de detención y excede las habilidades de razonamiento de los agentes humanos. GTS evita esto con una regla para probar fórmulas contra un modelo subyacente; diálogos lógicos, con una regla de no repetición (similar a la repetición triple en ajedrez). Genot y Jacot (2017) [2] demostraron que los jugadores con racionalidad severamente limitada pueden razonar para terminar una partida sin IEDS.
En la mayoría de las lógicas comunes, incluidas las anteriores, los juegos que surgen de ellas tienen información perfecta , es decir, los dos jugadores siempre conocen los valores de verdad de cada primitiva y están al tanto de todos los movimientos anteriores en el juego. Sin embargo, con la llegada de la semántica de juegos, se han propuesto lógicas, como la lógica favorable a la independencia de Hintikka y Sandu, con una semántica natural en términos de juegos de información imperfecta.
La motivación principal de Lorenzen y Kuno Lorenz fue encontrar una semántica de teoría de juegos (su término era dialógico , en alemán Dialogische Logik ) para la lógica intuicionista . Andreas Blass [3] fue el primero en señalar conexiones entre la semántica de juegos y la lógica lineal . Esta línea fue desarrollada posteriormente por Samson Abramsky , Radhakrishnan Jagadeesan, Pasquale Malacaria e independientemente Martin Hyland y Luke Ong, quienes pusieron especial énfasis en la composicionalidad, es decir, la definición de estrategias de forma inductiva sobre la sintaxis. Utilizando la semántica de juegos, los autores mencionados anteriormente han resuelto el problema de larga data de definir un modelo completamente abstracto para el lenguaje de programación PCF . En consecuencia, la semántica de juegos ha conducido a modelos semánticos completamente abstractos para una variedad de lenguajes de programación y a nuevos métodos de verificación de software dirigidos por la semántica mediante la comprobación de modelos de software .
Shahid Rahman y Helge Rückert extendieron el enfoque dialógico al estudio de varias lógicas no clásicas, como la lógica modal , la lógica de relevancia , la lógica libre y la lógica conectiva . Recientemente, Rahman y sus colaboradores desarrollaron el enfoque dialógico en un marco general destinado a la discusión del pluralismo lógico.
Jaakko Hintikka y Gabriel Sandu han enfatizado más las consideraciones fundamentales de la semántica de juegos , especialmente para la lógica independiente (lógica IF, más recientemente lógica amigable con la información ), una lógica con cuantificadores ramificados . Se pensaba que el principio de composicionalidad falla para estas lógicas, de modo que una definición de verdad tarskiana no podría proporcionar una semántica adecuada. Para evitar este problema, a los cuantificadores se les dio un significado de teoría de juegos. Específicamente, el enfoque es el mismo que en la lógica proposicional clásica, excepto que los jugadores no siempre tienen información perfecta sobre los movimientos previos del otro jugador. Wilfrid Hodges ha propuesto una semántica compositiva y ha demostrado que es equivalente a la semántica de juegos para las lógicas IF.
Más recientemente, Shahid Rahman y el equipo de lógica dialógica de Lille implementaron dependencias e independencias dentro de un marco dialógico por medio de un enfoque dialógico de la teoría de tipo intuicionista llamada razonamiento inmanente . [4]
La lógica computacional de Japaridze es un enfoque semántico de juegos para la lógica en un sentido extremo, que trata los juegos como objetivos a los que debe prestar servicio la lógica en lugar de como medios técnicos o fundamentales para estudiar o justificar la lógica. Su punto filosófico de partida es que la lógica está destinada a ser una herramienta intelectual universal y de utilidad general para "navegar por el mundo real" y, como tal, debe interpretarse semánticamente en lugar de sintácticamente, porque es la semántica la que sirve de puente entre el mundo real y los sistemas formales (sintaxis) que de otro modo carecerían de sentido. La sintaxis es, por tanto, secundaria, interesante sólo en la medida en que sirva a la semántica subyacente. Desde este punto de vista, Japaridze ha criticado repetidamente la práctica a menudo seguida de ajustar la semántica a algunas construcciones sintácticas objetivo ya existentes, siendo un ejemplo el enfoque de Lorenzen a la lógica intuicionista. Esta línea de pensamiento procede entonces a argumentar que la semántica, a su vez, debería ser una semántica de juegos, porque los juegos “ofrecen los modelos matemáticos más completos, coherentes, naturales, adecuados y convenientes para la esencia misma de todas las actividades de ‘navegación’ de los agentes: sus interacciones con el mundo circundante”. [5] En consecuencia, el paradigma de construcción lógica adoptado por la lógica de la computabilidad es identificar las operaciones más naturales y básicas en los juegos, tratar esos operadores como operaciones lógicas y luego buscar axiomatizaciones sólidas y completas de los conjuntos de fórmulas semánticamente válidas para los juegos. En este camino, ha surgido una gran cantidad de operadores lógicos familiares o desconocidos en el lenguaje abierto de la lógica de la computabilidad, con varios tipos de negaciones, conjunciones, disyunciones, implicaciones, cuantificadores y modalidades.
Los juegos se juegan entre dos agentes: una máquina y su entorno, donde se requiere que la máquina siga solo estrategias computables . De esta manera, los juegos se ven como problemas computacionales interactivos y las estrategias ganadoras de la máquina para ellos como soluciones a esos problemas. Se ha establecido que la lógica de computabilidad es robusta con respecto a variaciones razonables en la complejidad de las estrategias permitidas, que pueden reducirse hasta el espacio logarítmico y el tiempo polinomial (uno no implica al otro en los cálculos interactivos) sin afectar la lógica. Todo esto explica el nombre de "lógica de computabilidad" y determina la aplicabilidad en varias áreas de la ciencia informática. La lógica clásica , la lógica favorable a la independencia y ciertas extensiones de las lógicas lineal e intuicionista resultan ser fragmentos especiales de la lógica de computabilidad, obtenidos simplemente al no permitir ciertos grupos de operadores o átomos.
