Semántica del juego

Semántica
LingüísticoLógico
Análisis Computacional Léxico ( léxico lexicología ) Estadístico Estructural Teoría de prototipos Dinámica de fuerza Problemas lingüísticos no resueltos Teoría de descripciones
Informática
Tipos Acción Algebraico Axiomático Categórico Concurrencia Denotacional Juego Operacional Predicado transformacional Teoría Interpretación abstracta Gráfico semántico abstracto Coincidencia semántica Análisis Latente Aprendizaje automático Aplicaciones Sistema de archivos semántico Web semántica Wiki semántico
Idioma Lingüística
v t mi

La semántica del juego ( alemán : dialogische Logik , traducido como lógica dialógica ) es un enfoque de la semántica formal que basa los conceptos de verdad o validez en conceptos de la teoría del juego , como la existencia de una estrategia ganadora para un jugador, algo parecido a los diálogos socráticos o Teoría medieval de Obligationes .

Historia

A finales de la década de 1950, Paul Lorenzen fue el primero en introducir la semántica de un juego para la lógica , y fue desarrollado 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) y sus colaboradores desarrollaron la lógica dialógica en 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 colaboradores en Amsterdam.que examinó detenidamente la interfaz entre la lógica y los juegos, y Hanno Nickau, que abordó el problema de la abstracción total en los lenguajes de programación por medio de los 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 otro lado dieron como resultado el 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 los 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 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 reglas de introducción) deben 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 conectivo principal en el cálculo del lenguaje ( de Queiroz (1988) , de Queiroz (1991) , de Queiroz (1994), de Queiroz (2001) , de Queiroz (2008) )

Lógica clásica

La aplicación más simple de la semántica de los juegos es la lógica proposicional . Cada fórmula de este lenguaje se interpreta como un juego entre dos jugadores, conocido como el "Verificador" y el "Falsificador". Al Verificador se le da la "propiedad" de todas las disyunciones en la fórmula, y al Falsificador también se le da la propiedad de todas las conjunciones.. Cada movimiento del juego consiste en permitir que el propietario del conectivo dominante elija una de sus ramas; el juego continuará entonces en esa subfórmula, con el jugador que controle su conectivo dominante haciendo 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 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 siempre que el Falsificador 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 que se niega 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 los juegos se puede aplicar a la lógica de predicados ; las nuevas reglas permiten que un cuantificador dominante sea ​​eliminado por su "propietario" (el Verificador para los cuantificadores existenciales y el Falsificador para los cuantificadores universales ) y su variable ligada reemplazada en todos los casos por un objeto elegido por el propietario, extraído del dominio de cuantificación . Tenga en cuenta que un solo contraejemplo falsifica un enunciado cuantificado universalmente, y un solo ejemplo es suficiente para verificar uno cuantificado 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 habitualsemántica basada en modelos (tarskiana) . Para la lógica clásica de primer orden, la estrategia ganadora para el Verificador consiste esencialmente en encontrar funciones y testigos adecuados de Skolem . Por ejemplo, si S denota, entonces un enunciado equitativo 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 de la subfórmula existencial para cada elección de x que pueda hacer el Falsificador. ^[1]${\displaystyle \forall x\exists y\,\phi (x,y)}$${\displaystyle \exists f\forall x\,\phi (x,f(x))}$

La definición anterior fue formulada por primera vez por Jaakko Hintikka como parte de su interpretación de GTS. La versión original de la semántica del juego 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 los 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 GTS para la lógica clásica en las estrategias ganadoras dialógicas y viceversa.

Para las lógicas más 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 precedentes en el juego. Sin embargo, con el advenimiento de la semántica de juegos, se han propuesto lógicas, como la lógica independentista de Hintikka y Sandu, con una semántica natural en términos de juegos de información imperfecta.

Lógica intuicionista, semántica denotacional, lógica lineal, pluralismo lógico

La motivación principal de Lorenzen y Kuno Lorenz fue encontrar una semántica teórica de juegos (su término era dialógico , en alemán Dialogische Logik  [ de ] ) para la lógica intuicionista . Andreas Blass ^[2] fue el primero en señalar las conexiones entre la semántica del juego y la lógica lineal . Esta línea fue desarrollada por Samson Abramsky , Radhakrishnan Jagadeesan , Pasquale Malacaria e independientemente Martin Hyland y Luke Ong., quien puso especial énfasis en la composicionalidad, es decir, la definición de estrategias inductivamente sobre la sintaxis. Utilizando la semántica del juego, 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 del juego ha llevado 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 verificación del modelo de software .

Shahid Rahman  [ fr ] y Helge Rückert ampliaron 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 colaboradores desarrollaron el enfoque dialógico en un marco general dirigido a la discusión del pluralismo lógico.

Cuantificadores

Las consideraciones fundamentales de la semántica del juego han sido más enfatizadas por Jaakko Hintikka y Gabriel Sandu, 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 pensó que el principio de composicionalidad falla para estas lógicas, por lo que una definición de verdad tarskiana no podría proporcionar una semántica adecuada. Para solucionar 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 anteriores del otro jugador.Wilfrid Hodges ha propuesto una semántica compositiva y ha demostrado que es equivalente a la semántica de juegos para lógicas IF.

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

Lógica de computabilidad

Japaridze ‘s lógica computabilidades un enfoque semántico de juego a la lógica en un sentido extremo, que trata a los juegos como objetivos a los que debe servir 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 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 como puente entre mundo real y sistemas formales sin sentido (sintaxis). Por tanto, la sintaxis es secundaria, interesante sólo en la medida en que sirve 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, con LorenzenEl enfoque de la lógica intuicionista es un ejemplo. Esta línea de pensamiento luego procede a argumentar que la semántica, a su vez, debería ser una semántica de juego, 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 ”. ^[4]En consecuencia, el paradigma de construcción de lógica adoptado por la lógica de 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 del juego. En este camino han surgido una 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 juegan entre dos agentes: una máquina y su entorno, donde se requiere que la máquina siga solo estrategias efectivas. 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 diversas áreas de la informática. Lógica clásica , lógica favorable a la independencia y ciertas extensiones de linealy las lógicas intuicionistas resultan ser fragmentos especiales de la lógica de la computabilidad, obtenidas simplemente al rechazar ciertos grupos de operadores o átomos.

Ver también

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

Referencias

Este artículo incluye una lista de referencias generales , pero permanece en gran parte sin verificar porque carece de suficientes citas en línea correspondientes . Ayude a mejorar este artículo introduciendo citas más precisas. ( Mayo de 2010 ) ( Obtenga información sobre cómo y cuándo eliminar este mensaje de plantilla )

1. J. Hintikka y G. Sandu, 2009, "Semántica teórica de juegos" en Keith Allan (ed.) Concise Encyclopedia of Semantics , Elsevier, ISBN  0-08095-968-7 , págs. 341–343
2. Andreas R. Blass
3. S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: Razonamiento inmanente o igualdad en acción. Un jugador de juego para el nivel de juego . Springer (2018). https://www.springer.com/gp/book/9783319911489 .
   Para una aplicación del enfoque dialógico de la teoría de tipos intuicionista al axioma de elección, véase S. Rahman y N. Clerbout: Linking Games and Constructive Type Theory: Dialogical Strategies, CTT-Demonstrations and the Axiom of Choice. Springer-Briefs (2015). https://www.springer.com/gp/book/9783319190624 .
4. G. Japaridze , " Al principio fue la semántica de juegos ". En: Juegos: Unificando Lógica, Lenguaje y Filosofía . O. Majer, A.-V. Pietarinen y T. Tulenheimo, eds. Springer 2009, páginas 249-350. [1]

Bibliografía

Libros

• T. Aho y AV. Pietarinen (eds.) Verdad y juegos. Ensayos en honor a Gabriel Sandu . Societas Philosophica Fennica (2006). ISBN 951-9264-57-4 . 
• J. van Benthem, G. Heinzmann, M. Rebuschi y H. Visser (eds.) La era de las lógicas alternativas . Springer (2006). ISBN 978-1-4020-5011-4 . 
• R. Inhetveen: Logik. Eine dialog-orientierte Einführung. , Leipzig 2003 ISBN 3-937219-02-1 
• L. Keiff Le Pluralisme Dialogique . Tesis Université de Lille 3 (2007).
• K. Lorenz, P. Lorenzen: Dialogische Logik , Darmstadt 1978
• P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie , Stuttgart 2000 ISBN 3-476-01784-2 
• O. Majer, A.-V. Pietarinen y T. Tulenheimo (editores). Juegos: Unificando Lógica, Lenguaje y Filosofía . Springer (2009).
• S. Rahman, Über Dialogue protologische Kategorien und andere Seltenheiten . Fráncfort 1993 ISBN 3-631-46583-1 
• S. Rahman y H. Rückert (editores), Nuevas perspectivas en lógica dialógica . Synthese 127 (2001) ISSN 0039-7857 . 
• S. Rahman y N. Clerbout: Juegos de vinculación y teoría de tipos constructivos: estrategias dialógicas, demostraciones CTT y el axioma de la elección. Springer-Briefs (2015). https://www.springer.com/gp/book/9783319190624 .
• S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: Razonamiento inmanente o igualdad en acción. Un jugador de juego para el nivel de juego . Springer (2018). https://www.springer.com/gp/book/9783319911489 .
• J. Redmond y M. Fontaine, Cómo jugar diálogos. Introducción a la lógica dialógica. London, College Publications (Col. Diálogos y juegos de lógica. Una perspectiva filosófica N ° 1). ( ISBN 978-1-84890-046-2 ) 

Artículos

• S. Abramsky y R. Jagadeesan, Juegos y completitud total para la lógica lineal multiplicativa . Revista de lógica simbólica 59 (1994): 543-574.
• A. Blass, Semántica de un juego para lógica lineal . Annals of Pure and Applied Logic 56 (1992): 151-166.
• DR Ghica, Aplicaciones de la semántica de juegos: del análisis de programas a la síntesis de hardware . 2009 24th Annual IEEE Symposium on Logic In Computer Science: 17-26. ISBN 978-0-7695-3746-7 . 
• G. Japaridze, Introducción a la lógica de computabilidad . Anales de lógica pura y aplicada 123 (2003): 1-99.
• G. Japaridze, Al principio era la semántica de los juegos . En Ondrej Majer, Ahti-Veikko Pietarinen y Tero Tulenheimo (editores), Juegos: lógica unificadora, lenguaje y filosofía . Springer (2009).
• Krabbe, ECW, 2001. " Dialogue Foundations: Dialogue Logic Restituted [el título ha sido mal impreso como" ... Revisited "]," Suplemento de las Actas de la Sociedad Aristotélica 75 : 33-49.
• H. Nickau (1994). "Funcionales secuenciales hereditariamente". En A. Nerode; Yu.V. Matiyasevich (eds.). Proc. Symp. Fundamentos lógicos de la informática: lógica en San Petersburgo . Apuntes de conferencias en informática. 813 . Springer-Verlag . págs. 253-264. doi : 10.1007 / 3-540-58140-5_25 .
• de Queiroz, R. (1988). "Una explicación teórica de la prueba de la programación y el papel de las reglas de reducción" . Dialectica . 42 (4): 265-282.
• de Queiroz, R. (1991). "Significado como gramática más consecuencias" . Dialectica . 45 (1): 83–86.
• de Queiroz, R. (1994). "Normalización y Juegos de Lenguaje" . Dialectica . 48 (2): 83-123.
• de Queiroz, R. (2001). "Significado, función, propósito, utilidad, consecuencias - conceptos interconectados" . Revista Lógica de la IGPL . 9 (5): 693–734.
• de Queiroz, R. (2008). "Sobre las reglas de reducción, el significado como uso y la semántica de la teoría de la prueba" . Studia Logica . 90 : 211–247.
• S. Rahman y L. Keiff, Sobre cómo ser un dialogista . En Daniel Vanderken (ed.), Logic Thought and Action , Springer (2005), 359-408. ISBN 1-4020-2616-1 . 
• S. Rahman y T. Tulenheimo, From Games to Dialogues and Back: Towards a General Frame for Validity . En Ondrej Majer, Ahti-Veikko Pietarinen y Tero Tulenheimo (editores), Juegos: lógica unificadora, lenguaje y filosofía . Springer (2009).
• Johan van Benthem (2003). "Lógica y teoría de juegos: encuentros cercanos de tercer tipo". En GE Mints; Reinhard Muskens (eds.). Juegos, lógica y decorados constructivos . Publicaciones CSLI. ISBN 978-1-57586-449-5.

Enlaces externos

• Página de inicio de la lógica de computabilidad
• GALOP: Taller de juegos para lógica y lenguajes de programación
• ¿Semántica del juego o lógica lineal?
• Thomas Piecha. "Lógica dialógica" . Enciclopedia de Filosofía de Internet .
• Entrada de "Lógica y juegos" de Wilfrid Hodges en la Enciclopedia de Filosofía de Stanford
• Entrada de "lógica dialógica" de Laurent Keiff en la Enciclopedia de Filosofía de Stanford