En teoría de la demostración , la lúdica es un análisis de los principios que rigen las reglas de inferencia de la lógica matemática . Las características clave de la lúdica incluyen la noción de conectivos compuestos, utilizando una técnica conocida como enfoque o focalización (inventada por el científico informático Jean-Marc Andreoli), y su uso de ubicaciones o loci sobre una base en lugar de proposiciones .
Más precisamente, la lúdica intenta recuperar los conectores lógicos conocidos y los comportamientos de prueba siguiendo el paradigma de la computación interactiva, de manera similar a lo que se hace en la semántica de juegos con la que está estrechamente relacionada. Al abstraer la noción de fórmulas y centrarse en sus usos concretos (es decir, ocurrencias distintas), proporciona una sintaxis abstracta para la ciencia informática , ya que los loci pueden verse como indicadores de la memoria.
El logro principal de la lúdica es el descubrimiento de una relación entre dos nociones naturales, pero distintas, de tipo o proposición.
La primera perspectiva, que podría denominarse interpretación de las proposiciones basada en la prueba o en el estilo Gentzen , sostiene que el significado de una proposición surge de sus reglas de introducción y eliminación. La focalización refina este punto de vista al distinguir entre proposiciones positivas, cuyo significado surge de sus reglas de introducción, y proposiciones negativas, cuyo significado surge de sus reglas de eliminación. En los cálculos focalizados, es posible definir conectivos positivos dando solo sus reglas de introducción, y la forma de las reglas de eliminación está forzada por esta elección. (Simétricamente, los conectivos negativos pueden definirse en los cálculos focalizados dando solo las reglas de eliminación, y las reglas de introducción están forzadas por esta elección.)
La segunda perspectiva, que podría denominarse interpretación computacional o interpretación de Brouwer-Heyting-Kolmogorov de las proposiciones, considera que fijamos un sistema computacional de antemano y luego damos una interpretación de realizabilidad de las proposiciones para darles un contenido constructivo. Por ejemplo, un realizador para la proposición "A implica B" es una función computable que toma un realizador para A y lo usa para calcular un realizador para B. Los modelos de realizabilidad caracterizan a los realizadores de las proposiciones en términos de su comportamiento visible y no en términos de su estructura interna.
Girard muestra que para la lógica lineal afín de segundo orden , dado un sistema computacional con no terminación y topes de error como efectos, la realizabilidad y la focalización dan el mismo significado a los tipos.
La lúdica fue propuesta por el lógico Jean-Yves Girard . Su artículo de introducción a la lúdica, Locus solum: de las reglas de la lógica a la lógica de las reglas , tiene algunas características que pueden considerarse excéntricas para una publicación sobre lógica matemática (como las ilustraciones de zorrillos). La intención de estas características es reforzar el punto de vista de Jean-Yves Girard en el momento de su redacción y, por lo tanto, ofrece a los lectores la posibilidad de comprender la lúdica independientemente de sus antecedentes. [ dudoso – discutir ] [ cita requerida ]