Resumen Técnico: Satisfactibilidad en la Lógica de Łukasiewicz y su Versión Relativa No Acotada

Enunciado del Problema

El artículo aborda la complejidad computacional de la teoría existencial (problema de satisfactibilidad) para la Lógica de Łukasiewicz No Acotada ($L_u$). $L_u$ es una lógica subestructural que combina características de la lógica de Łukasiewicz de infinitos valores ($L$) con la lógica abeliana. Su semántica pretendida es el grupo aditivo totalmente ordenado abeliano punteado sobre los números reales, denotado como $\mathbb{R}_{-1}$, donde el dominio es $\mathbb{R}$ y una constante distinguida $-1$ representa la falsedad.

Mientras que la complejidad de la lógica de Łukasiewicz estándar ($L$) está bien establecida —específicamente, la satisfactibilidad de términos en el álgebra MV estándar $[0, 1]_L$ es NP-completa (Mundici [35])—, la complejidad de la teoría existencial para $L_u$ (y su álgebra subyacente $\mathbb{R}_{-1}$) no había sido determinada explícitamente en el contexto de una reducción a la lógica de Łukasiewicz estándar. Los autores tienen como objetivo proporcionar una estimación de complejidad para $L_u$ estableciendo una reducción de tiempo polinomial entre la teoría existencial de $\mathbb{R}_{-1}$ y la teoría existencial de $[0, 1]_L$.

Metodología

El artículo emplea un enfoque metodológico de dos frentes que involucra reducciones algebraicas y análisis de modelos acotados:

1. Acotación de las Asignaciones Satisfactorias

Los autores establecen primero que si una sentencia existencial se cumple en $\mathbb{R}_{-1}$, posee una asignación satisfactoria dentro de un intervalo específico, acotado polinomialmente.

• Lema 3.2 (Asignación Acotada): Para cualquier fórmula abierta $\Phi$ en el lenguaje de grupos $\ell$ punteados ($L_{pAb}$), si $\mathbb{R}_{-1} \models \exists \bar{x} \Phi$, existe una asignación racional $\bar{a}$ tal que $\Phi(\bar{a})$ se cumple, donde el tamaño de la representación binaria de los valores en $\bar{a}$ es polinomial en el tamaño de $\Phi$.
• Este resultado se basa en reducir el problema de satisfactibilidad a un sistema de desigualdades lineales y aplicar cotas derivadas de la regla de Cramer (Lema 3.1), asegurando que las soluciones se encuentren dentro de un intervalo $[-2^M, 2^M]$ donde $M$ está relacionado polinomialmente con el tamaño de la fórmula.

2. Reducción de Tiempo Polinomial mediante Mapeo Lineal

El núcleo de la metodología es una reducción de tiempo polinomial desde la teoría existencial de $\mathbb{R}_{-1}$ hacia la teoría existencial del álgebra MV estándar $[0, 1]_L$.

• Construcción del Mapeo: Los autores definen un mapeo $\tau$ desde términos en $L_{Ab}$ (grupos $\ell$ abelianos) hacia términos en $L_{MV}[1/2]$ (álgebras MV con una constante $1/2$). Este mapeo utiliza una transformación lineal $r_{M,k}(a) = \frac{a}{2^{M+k+1}} + \frac{1}{2}$, que mapea un intervalo acotado $[-2^M, 2^M]$ en $\mathbb{R}$ a un subintervalo de $[0, 1]$.
• Traducción de Términos: La traducción $\tau$ preserva la estructura semántica de los términos (suma, negación, operaciones de retícula) bajo este mapeo lineal, siempre que la profundidad de los términos esté acotada.
• Manejo de la Complejidad: Para evitar una explosión exponencial en el tamaño de los términos (que ocurre con una traducción ingenua de sumas anidadas), los autores emplean transformaciones de Tseitin. Esto introduce nuevas variables para subtérminos, convirtiendo fórmulas complejas en fórmulas equisatisfactorias de tamaño polinomial donde los términos tienen una profundidad de a lo más 1.
• Codificación de Constantes: La constante $-1$ en $\mathbb{R}_{-1}$ se codifica dentro del álgebra MV utilizando variables auxiliares ($z_i, q, r$) restringidas por ecuaciones específicas (por ejemplo, $z_1 = \neg z_1$, $z_{i+1} \oplus z_{i+1} = z_i$) que fuerzan valores racionales específicos (potencias de $1/2$) en la semántica estándar.

3. Autoredacción de la Lógica de Łukasiewicz

El artículo también investiga la composición de la reducción desde $[0, 1]_L$ hacia $\mathbb{R}_{-1}$ (establecida en trabajos anteriores [12]) y la nueva reducción desde $\mathbb{R}_{-1}$ hacia $[0, 1]_L$.

• Los autores definen una traducción compuesta $\sigma_q$ que mapea términos de $L_{MV}$ directamente a términos de $L_{MV}[1/2]$.
• Demuestran que esta composición resulta en una traducción de tamaño polinomial, proporcionando efectivamente una reducción no trivial de la teoría existencial de $[0, 1]_L$ hacia sí misma.

Resultados Clave

1. NP-Completitud de la Teoría Existencial de $L_u$: La teoría existencial de $\mathbb{R}_{-1}$ (y por tanto el conjunto de teoremas y la relación de consecuencia finita de la Lógica de Łukasiewicz No Acotada) es NP-completa.

   • Cota Superior: El problema está en NP porque las asignaciones satisfactorias pueden encontrarse dentro de un intervalo acotado polinomialmente (Lema 3.2), y la reducción a $[0, 1]_L$ (que se sabe es NP-completa) es de tiempo polinomial (Teorema 4.6).
   • Cota Inferior: La dureza se deriva de la conocida NP-completitud de la satisfactibilidad de términos en $[0, 1]_L$ (Mundici [35]) y de la existencia de una reducción de tiempo polinomial desde $[0, 1]_L$ hacia $\mathbb{R}_{-1}$ (de [12]).

2. CoNP-Completitud de los Fragmentos Universales: En consecuencia, la teoría universal, la teoría ecuacional y la teoría cuasiecuacional de $\mathbb{R}_{-1}$ son CoNP-completas.

3. Autotraducción de $[0, 1]_L$: El artículo demuestra una reducción de tiempo polinomial de la teoría existencial del álgebra MV estándar $[0, 1]_L$ hacia sí misma (Teorema 5.6). Esto se logra componiendo la reducción hacia $\mathbb{R}_{-1}$ y la reducción de vuelta hacia $[0, 1]_L$.

Significado y Afirmaciones

Los autores afirman que la contribución principal de este trabajo es el método de reducción más que el resultado de complejidad en sí mismo, el cual podría haberse anticipado dada la complejidad conocida de estructuras relacionadas.

• Nueva Conexión: La reducción establece una nueva conexión explícita entre la Lógica de Łukasiewicz No Acotada ($L_u$) y la Lógica de Łukasiewicz estándar ($L$). Muestra que el problema de satisfactibilidad para la lógica no acotada puede traducirse efectivamente a la lógica estándar mediante un mapeo lineal de un vecindario suficientemente grande de 0 al intervalo $[0, 1]$.
• Reducción Explícita: A diferencia de enfoques anteriores que podrían basarse en la existencia abstracta o en marcos lógicos diferentes (como la reducción de campos reales cerrados a $L_{\Pi 1/2}$ por Marchioni y Montagna [31]), este artículo proporciona una reducción explícita de tiempo polinomial que escala bien a fragmentos del lenguaje.
• Perspectiva Teórica: El resultado implica una traducción de la teoría existencial del álgebra MV estándar hacia sí misma. Los autores notan que esto invita a una comparación con otras reducciones lógicas, pero enfatizan que su método se basa en estructuras aditivas y mapeos lineales, evitando los símbolos de función multiplicativa requeridos en otros marcos.

El artículo concluye que la cuestión de satisfactibilidad para $L_u$ es decidible y reside en la misma clase de complejidad que su contraparte proposicional clásica (NP-completa), a pesar de la naturaleza de infinitos valores de la lógica.