semántica de juegos

La semántica de juegos es un enfoque de la semántica formal que fundamenta los conceptos de verdad o validez en conceptos de la teoría de juegos , como la existencia de una estrategia ganadora para un jugador. En este marco, las fórmulas lógicas se interpretan como definitorias de juegos entre dos jugadores. El término abarca varias tradiciones relacionadas pero distintas, incluyendo la lógica dialógica (desarrollada por Paul Lorenzen y Kuno Lorenz en Alemania a partir de la década de 1950) y la semántica de la teoría de juegos (desarrollada por Jaakko Hintikka en Finlandia).

La semántica de juegos representa una ruptura significativa con los enfoques tradicionales de la teoría de modelos, al enfatizar la naturaleza dinámica e interactiva del razonamiento lógico en lugar de las asignaciones de verdad estáticas. Proporciona interpretaciones intuitivas para diversos sistemas lógicos, incluyendo la lógica clásica , la lógica intuicionista , la lógica lineal y la lógica modal . Este enfoque guarda similitudes conceptuales con los antiguos diálogos socráticos , la teoría medieval de las Obligaciones y las matemáticas constructivas . Desde la década de 1990, la semántica de juegos ha encontrado importantes aplicaciones en la informática teórica , particularmente en la semántica de los lenguajes de programación , la teoría de la concurrencia y el estudio de la complejidad computacional .

A finales de la década de 1950, Paul Lorenzen fue el primero en introducir una semántica de juegos para la lógica , que posteriormente fue desarrollada por Kuno Lorenz . Casi al mismo tiempo que Lorenzen, Jaakko Hintikka desarrolló un enfoque basado en la teoría de modelos, conocido en la literatura como GTS (semántica de juegos). Desde entonces, se han estudiado diversas semánticas de juegos en lógica.

Shahid Rahman ( Lille III ) y sus colaboradores desarrollaron la lógica dialógica como un marco general para el estudio de cuestiones lógicas y filosóficas relacionadas con el pluralismo lógico . A partir 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 exhaustivamente la interfaz entre la lógica y los juegos, y el de Hanno Nickau, quien abordó el problema de la abstracción total en los lenguajes de programación mediante juegos. Los nuevos resultados en lógica lineal de Jean-Yves Girard en las interfaces entre la teoría matemática de juegos y la lógica , por un lado, y la teoría de la argumentación y la lógica, por 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 demostración y la teoría del significado, que aboga por que el paradigma de Wittgenstein del "significado como uso", entendido en el contexto de la teoría de la demostración, donde las llamadas reglas de reducción (que muestran el efecto de las reglas de eliminación en el resultado de las reglas de introducción) deberían considerarse apropiadas para formalizar la explicación de las consecuencias (inmediatas) que se pueden extraer de una proposición, mostrando así la función/propósito/utilidad de su conector 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) , de Queiroz (2025a) , de Queiroz (2025b) ).

La aplicación más sencilla de la semántica de juegos se encuentra en 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 otorga la "propiedad" de todas las disyunciones de la fórmula, y al Falsificador, la propiedad de todas las conjunciones . Cada movimiento del juego consiste en permitir que el propietario del conector principal elija una de sus ramas; el juego continúa entonces en esa subfórmula, y el jugador que controla su conector principal realiza el siguiente movimiento. El juego termina cuando ambos jugadores han elegido una proposición primitiva; en ese momento, el Verificador se considera ganador si la proposición resultante es verdadera, y el Falsificador 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 cuando el Falsificador tenga la estrategia ganadora.

Si la fórmula contiene negaciones o implicaciones, se pueden utilizar otras técnicas más complejas. Por ejemplo, una negación debe ser verdadera si lo negado es falso, por lo que debe tener el efecto de intercambiar los roles de los dos jugadores.

De manera más general, 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 "propietario" (el Verificador para cuantificadores existenciales y el Falsificador para cuantificadores universales ) y su variable ligada sea reemplazada en todas las ocurrencias por un objeto elegido por el propietario, extraído del dominio de cuantificación. Nótese que un solo contraejemplo falsifica una proposición cuantificada universalmente, y un solo ejemplo basta para verificar una cuantificada existencialmente. Suponiendo el axioma de elección , la semántica de la 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${\displaystyle \forall x\exists y\,\phi (x,y)}$entonces una afirmación equisatisfacible para S es${\displaystyle \exists f\forall x\,\phi (x,f(x))}$La función f de Skolem (si existe) codifica en realidad 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 pueda hacer. ^{[ 1 ]}

La definición anterior fue formulada por primera vez por Jaakko Hintikka como parte de su interpretación de la Teoría de Juegos de Semántica (TGS). La versión original de la semántica de juegos para la lógica clásica (e intuicionista), propuesta por Paul Lorenzen y Kuno Lorenz, no se definió en términos de modelos, sino de estrategias ganadoras en 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 TGS 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 usar reglas de fin de juego en lugar de dejar que los jugadores decidan cuándo terminar 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 la parada y excede las capacidades 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 un juego sin IEDS.

En la mayoría de las lógicas comunes, incluidas las mencionadas anteriormente, los juegos que de ellas se derivan poseen 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 previos en el juego. Sin embargo, con el advenimiento de la semántica de juegos, se han propuesto lógicas, como la lógica de Hintikka y Sandu, que favorece la independencia , con una semántica natural en términos de juegos de información imperfecta.

La principal motivación de Lorenzen y Kuno Lorenz fue encontrar una semántica de teoría de juegos (su término era dialógica , 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 por Martin Hyland y Luke Ong , quienes hicieron especial hincapié en la composicionalidad, es decir, la definición de estrategias inductivamente sobre la sintaxis. Utilizando la semántica de juegos, los autores mencionados anteriormente han resuelto el antiguo problema de definir un modelo completamente abstracto para el lenguaje de programación PCF . En consecuencia, la semántica de juegos ha dado lugar a modelos semánticos completamente abstractos para diversos 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 conexiva . Recientemente, Rahman y sus colaboradores desarrollaron el enfoque dialógico en un marco general orientado al análisis del pluralismo lógico.

Jaakko Hintikka y Gabriel Sandu han hecho mayor hincapié en las consideraciones fundamentales de la semántica de juegos , especialmente para la lógica amigable con la independencia (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 fallaba para estas lógicas, por lo que una definición de verdad tarskiana no podía proporcionar una semántica adecuada. Para sortear este problema, se les dio a los cuantificadores 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 propuso una semántica composicional y demostró su equivalencia con la semántica de juegos para las lógicas IF.

Más recientemente, Shahid Rahman y el equipo de lógica dialógica en Lille implementaron dependencias e independencias dentro de un marco dialógico mediante un enfoque dialógico de la teoría de tipos intuicionista llamado razonamiento inmanente . ^{[ 4 ]}

La lógica de la computabilidad de Japaridze es un enfoque semántico-lúdico de la lógica en un sentido extremo, que trata los juegos como objetivos a los que la lógica debe servir, en lugar de como medios técnicos o fundamentales para estudiar o justificar la lógica. Su punto de partida filosófico es que la lógica está concebida como 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, ya que 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 significado. La sintaxis es, por lo tanto, secundaria, interesante solo en la medida en que sirve a la semántica subyacente. Desde esta perspectiva, Japaridze ha criticado repetidamente la práctica frecuente de ajustar la semántica a construcciones sintácticas objetivo ya existentes, siendo el enfoque de Lorenzen sobre la lógica intuicionista un ejemplo de ello. Esta línea de pensamiento continúa argumentando 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 consiste en 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 válidas desde el punto de vista semántico de los juegos. En este camino, han surgido multitud 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 desarrollan entre dos agentes: una máquina y su entorno, donde la máquina debe seguir únicamente estrategias computables . De esta forma, los juegos se conciben como problemas computacionales interactivos, y las estrategias ganadoras de la máquina como soluciones a dichos problemas. Se ha demostrado que la lógica de computabilidad es robusta ante variaciones razonables en la complejidad de las estrategias permitidas, las cuales pueden reducirse hasta alcanzar un espacio logarítmico y un tiempo polinomial (en los cálculos interactivos, una no implica la otra) sin afectar la lógica. Todo esto explica el nombre de «lógica de computabilidad» y determina su aplicabilidad en diversas áreas de la informática. La lógica clásica , la lógica independiente y ciertas extensiones de las lógicas lineal e intuicionista resultan ser fragmentos especiales de la lógica de computabilidad, obtenidos simplemente al excluir ciertos grupos de operadores o átomos.

• lógica de computabilidad
• Lógica de dependencia
• Juego de Ehrenfeucht-Fraïssé
• Lógica favorable a la independencia
• Computación interactiva
• Lógica intuicionista
• Lúdicos

• Página principal de Computability Logic
• GALOP: Taller sobre juegos para lenguajes de lógica y programación
• ¿Semántica de juegos o lógica lineal?
• Thomas Piecha. "Lógica dialógica" . En Fieser, James; Dowden, Bradley (eds.). Internet Encyclopedia of Philosophy . ISSN 2161-0002 . OCLC 37741658 .  
• Entrada de "Lógica y juegos"Por Wilfrid Hodges en la Enciclopedia de Filosofía de Stanford
• Entrada de "Lógica Dialógica"Por Laurent Keiff en la Enciclopedia de Filosofía de Stanford