🔢 mathematics

Inferentialist Game Semantics (Extended Abstract)

Este artículo establece una correlación plenamente abstracta entre la semántica de base-extensión (B-eS) y la semántica de juegos de Hyland-Ong para proporcionar una teoría intensional del significado para sistemas lógicos, ilustrada a través del ejemplo de un Sudoku de 4x4.

Autores originales: Joaquim T. Waddington, Alexander V. Gheorghiu, David J. Pym

Publicado 2026-07-16

📖 4 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Joaquim T. Waddington, Alexander V. Gheorghiu, David J. Pym

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás tratando de entender cómo piensa una computadora o cómo un matemático demuestra un teorema. Durante mucho tiempo, hemos observado estos procesos como un mapa: comprobamos si el destino final (la respuesta) es "verdadero" basándonos en una imagen estática del mundo. Pero hay otra forma de verlo, una que trata la lógica como una conversación o un juego. En esta visión, una "demostración" no es solo un hecho estático; es una estrategia ganadora en un diálogo entre dos jugadores. Un jugador, el "Proponente", intenta defender una afirmación, mientras que el otro, el "Oponente", actúa como un entorno escéptico, lanzando desafíos y pidiendo justificaciones. Si el Proponente puede responder a cada desafío que el Oponente le lanza, tiene una estrategia ganadora, y esa estrategia es la demostración. Este enfoque, conocido como semántica de juegos, hace que la lógica se sienta dinámica e interactiva, como un deporte en lugar de una estatua.

Ahora, imagina una forma diferente de definir la lógica, que no depende de mapas ni de juegos, sino de reglas de inferencia puras. Esto es la "semántica de la teoría de la prueba". El significado de una afirmación proviene enteramente de cómo puedes construirla a partir de reglas básicas, como un chef que define un plato no por su sabor, sino por los pasos específicos de la receta utilizados para prepararlo. Durante mucho tiempo, estos dos mundos —el juego dinámico de "Proponente contra Oponente" y el enfoque de "receta" basado en reglas— parecieron estar hablando lenguajes diferentes. La gran pregunta era: ¿Están en realidad describiendo lo mismo, solo que de diferentes maneras? ¿Podrían las reglas del juego construirse directamente a partir de los pasos básicos de la receta, haciendo que el juego sea una consecuencia natural de las reglas?

Este artículo dice que "sí". Los autores, Joaquim T. Waddington, Alexander V. Gheorghiu y David J. Pym, han traducido con éxito el lenguaje del "juego" al lenguaje de la "receta". Muestran que las complejas interacciones de un juego lógico pueden reconstruirse enteramente a partir de los bloques de construcción básicos de la semántica de la teoría de la prueba. No solo lo supusieron; lo demostraron matemáticamente. Crearon un diccionario perfecto donde una "base" de reglas (la receta) se convierte en una "arena" (el tablero de juego), una "derivación" (los pasos de la receta) se convierte en un "juego" (los movimientos en el juego) y una "demostración" se convierte en una "estrategia ganadora".

Para hacer esto concreto, incluso utilizaron un rompecabezas Sudoku de 4x4 como caso de prueba. En su modelo, el tablero de Sudoku es la "arena". Las reglas del Sudoku son las "reglas atómicas". El "Proponente" es el jugador que intenta resolver el rompecabezas, y el "Oponente" es el entorno que otorga o deniega movimientos basándose en las reglas. Demostraron que si puedes resolver el Sudoku (ganar el juego), tienes una "estrategia ganadora" que corresponde exactamente a una demostración lógica válida.

El artículo va más allá para manejar las partes complicadas de la lógica, como las afirmaciones de "O". En un juego normal, si tienes que elegir entre dos caminos (A o B), podrías tener que adivinar cuál es el correcto. Pero en este nuevo marco, una estrategia ganadora para una afirmación "O" no significa que tengas que elegir un camino inmediatamente. En cambio, significa que tienes un plan que funciona sin importar cuál de los dos caminos resulte ser el correcto. Es como tener un plan de respaldo para cada resultado posible, asegurando que ganarás independientemente de cómo se desarrolle el juego. Este enfoque evita la necesidad de "retroceder" (cambiar de opinión más tarde), que es un truco común en otros modelos de juego.

Los autores están muy seguros de sus resultados. No solo lo simularon en una computadora; proporcionaron pruebas matemáticas rigurosas que muestran que su "semántica de extensión de juego" está perfectamente alineada con la lógica intuicionista estándar. Demostraron que si una afirmación es demostrable en su sistema de juego, es demostrable en la lógica estándar, y viceversa. También descartaron explícitamente una forma más simple y naive de manejar las afirmaciones "O" (donde simplemente eliges un ganador), mostrando que tal enfoque simple falla en capturar todo el poder del razonamiento lógico.

En resumen, este artículo tiende un puente entre dos formas principales de pensar la lógica. Muestra que el mundo dinámico e interactivo de la semántica de juegos no es una capa externa añadida sobre la lógica; puede construirse desde la base utilizando las reglas fundamentales de la demostración. Al hacer esto, nos brinda una comprensión más profunda y unificada de lo que significa "saber" que algo es cierto: significa que tienes una estrategia que gana el juego, sin importar cómo juegue el oponente.

Resumen Técnico: Semántica de Juegos Inferencialista

Planteamiento del Problema
El artículo aborda la relación entre dos teorías distintas de la intensionalidad del significado para la lógica: la Semántica de Juegos y la Semántica Teórica de la Prueba (P-tS).

La Semántica de Juegos (específicamente los juegos de Hyland-Ong) interpreta la validez lógica a través de interacciones dinámicas entre un Proponente y un Oponente, donde las pruebas corresponden a estrategias ganadoras.
La Semántica Teórica de la Prueba (específicamente la Semántica de Extensión de Bases o B-eS, desarrollada por Sandqvist) interpreta el significado mediante la demostrabilidad en "bases" de reglas atómicas, fundamentando la validez en una noción pre-lógica de derivabilidad en lugar de la verdad modelo-teórica.

Aunque ambos marcos ofrecen cuentas intensionales del significado, era una pregunta abierta si los conceptos de la semántica de juegos podían reconstruirse a partir de los primitivos de la P-tS. Específicamente, ¿pueden los juegos ser vistos como entidades inherentemente teóricas de la prueba en lugar de modelos impuestos externamente? Los autores pretenden establecer una correlación totalmente abstracta entre la B-eS y la semántica de juegos de Hyland-Ong para la Lógica Proposicional Intuicionista (LPI).

Metodología
Los autores emplean una estrategia de traducción constructiva para cerrar la brecha entre ambos marcos.

Construcción del Diccionario: Definen una correspondencia precisa entre los primitivos de la B-eS de Sandqvist y los componentes de los juegos de Hyland-Ong:
- Una base de reglas atómicas corresponde a una arena (un bosque de árboles enraizados).
- Un argumento desde supuestos corresponde a una partida (una secuencia de movimientos).
- Una prueba corresponde a una estrategia ganadora.
Definiciones Formales:
- Arenas Atómicas: Definidas como bosques de árboles donde los nodos representan átomos. Los nodos raíz son reclamos del Proponente (P); los hijos son desafíos del Oponente (O).
- Movimientos y Partidas: Los movimientos se categorizan como preguntas (demandas de justificación) o respuestas (concesiones). Una partida es una secuencia finita que satisface restricciones estructurales específicas respecto a la justificación, la alternancia y el manejo de los supuestos iniciales.
- Estrategias: Una estrategia es una función que mapea partidas que terminan en un movimiento del Oponente hacia una secuencia de movimientos del Proponente. Una estrategia es "ganadora" si garantiza una respuesta del Proponente a la pregunta inicial en cada partida máxima.
Manejo de la Disyunción: Un paso metodológico crítico involucra el tratamiento de la disyunción ( $\lor$ ). Los autores rechazan un enfoque ingenuo de "ganar un disjunto". En su lugar, adoptan la segunda cláusula de Sandqvist: una disyunción es soportada si, para cualquier meta atómica $p$ y cualquier extensión de la arena, si $p$ es derivable de ambos disjuntos, es derivable de la disyunción. Esto se interpreta en términos de juegos como una estrategia que proporciona continuaciones para ambos disjuntos, evitando el compromiso prematuro (una lectura de estilo de paso de continuación o continuation-passing style).
Ejemplo: El marco se ilustra utilizando un rompecabezas Sudoku de 4x4, formalizado como una arena donde las "reglas" del juego definen los árboles, demostrando la dinámica jugador-contra-entorno sin referencia inmediata a la consecuencia lógica.

Resultados Clave
El artículo establece los siguientes teoremas y corolarios:

Isomorfismo de Estructuras de Datos (Lema 13): Existe una traducción inversa mutua entre bases (conjuntos de reglas) y arenas (bosques de árboles), probando que son isomorfos como estructuras de datos.
Adecuación (Corolario 16): Para cualquier conjunto finito de átomos $S$ y átomo $p$ , $S$ es derivable en una base $B$ ( $S \vdash_B p$ ) si y solo si el Proponente tiene una estrategia ganadora para $p$ desde $S$ en la arena correspondiente a $B$ ( $S \triangleright_{Arena(B)} p$ ). Esto establece que la interpretación de la teoría de juegos es sólida y completa para la derivabilidad en una base.
Semántica de Extensión de Juegos (G-eS): Al reemplazar el caso base de "derivabilidad en una base" por la "existencia de una estrategia ganadora en una arena" en las cláusulas de Sandqvist, los autores definen una nueva semántica para la LPI.
Resultado Lógico Principal (Corolario 20): Los autores demuestran que la Lógica Proposicional Intuicionista (específicamente el sistema de deducción natural NJ) es sólida y completa con respecto a esta nueva Semántica de Extensión de Juegos. Es decir, $\Gamma \vdash_{NJ} \phi$ si y solo si $\Gamma \Vdash' \phi$ (validez en la semántica de juegos).

Significancia y Reivindicaciones
El artículo afirma lograr una correlación totalmente abstracta entre la B-eS y la semántica de juegos de Hyland-Ong para la LPI. Su significancia primaria reside en los siguientes puntos:

Reconstrucción de los Juegos desde la P-tS: Los autores demuestran que los conceptos de la semántica de juegos pueden reconstruirse a partir de los primitivos de la semántica teórica de la prueba. Esto sugiere que los juegos no son meramente modelos externos, sino que pueden verse como intrínsecos al carácter teórico de la prueba.
Lectura Operacional de la Validez: Al vincular la validez con las estrategias ganadoras, la semántica adquiere una lectura operacional. La validez en una arena no es solo una propiedad estática, sino que es "ejecutable", con estrategias computables mediante búsqueda dirigida a objetivos.
Contenido Computacional de la Disyunción: El artículo argumenta que la cláusula técnicamente motivada de Sandqvist para la disyunción en la B-eS adquiere un contenido computacional directo en el entorno de los juegos. Representa una estrategia que sabe cómo continuar la búsqueda independientemente de cuál disjunto se resuelva finalmente, efectivamente internalizando el mecanismo de retroceso (backtracking) encontrado en la búsqueda clásica dentro de un marco intuicionista.
Fundamento para Investigaciones Futuras: El trabajo proporciona una base para extender esta semántica a la lógica de primer orden y de orden superior, explorar lógicas subestructurales mediante restricciones en la partida (por ejemplo, limitando la contracción) e investigar el razonamiento clásico mediante modificaciones a las reglas de justificación o juegos concurrentes.

Los autores mantienen un tono modesto, señalando que, si bien establecen la adecuación (equivalencia extensional), una correspondencia completa y fiel (mapeando derivaciones distintas a estrategias distintas) requiere un trabajo adicional sobre la definición de la identidad para derivaciones y estrategias, lo cual se deja para investigaciones futuras.

Más como este