On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Resumen Técnico: Sobre Expansiones No Lineales Acotadas por Variables de la Aritmética de Presburger

Enunciado del Problema
La aritmética de Presburger, la teoría de primer orden de los enteros con adición y orden, es decidible. Sin embargo, su expansión mediante predicados no lineales, como el conjunto de cuadrados perfectos ($Z^2$) o imágenes polinómicas generales, es conocida por ser indecidible en el caso general. Esta indecidibilidad se deriva de la capacidad de codificar la multiplicación dentro de estas teorías. Aunque la decidibilidad del fragmento existencial de tales expansiones sigue siendo un problema abierto importante (por ejemplo, la conjetura de Büchi respecto a los cuadrados perfectos), este artículo investiga una vía diferente para recuperar la decidibilidad: restringir el número de variables.

Los autores se centran en expansiones de la aritmética de Presburger acotadas por variables con familias de predicados polinómicos monádicos. Específicamente, examinan fragmentos donde el número de variables distintas está acotado por una constante $k$ (denotado como $FO_k$, $\exists FO_k$ y $SMT_k$). El desafío central es que, incluso para una sola variable ($k=1$), la decidibilidad de si dos predicados polinómicos se intersecan (por ejemplo, $f(u) = g(v)$) es una instancia severamente restringida del décimo problema de Hilbert, que generalmente permanece abierto.

Metodología
El artículo emplea una combinación de técnicas de teoría de números, geometría algebraica y teoría de la medida para analizar los conjuntos de soluciones de restricciones dentro de estos fragmentos de variables acotadas.

1. Preprocesamiento y Reducción: El procedimiento de decisión comienza reduciendo oraciones arbitrarias a un problema de satisfacibilidad que involucra una conjunción de restricciones. Estas restricciones incluyen desigualdades lineales ($x > c$), aritmética modular ($x \equiv_m c$) y predicados polinómicos de la forma $R(ax+b)$ o sus negaciones $\neg R(ax+b)$. Los autores utilizan el Teorema Chino del Resto para consolidar las restricciones modulares y realizan un análisis de casos para eliminar intervalos acotados, reduciendo el problema a determinar la satisfacibilidad de restricciones sobre un dominio no acotado.
2. Manejo de Restricciones Positivas: El núcleo de la metodología consiste en caracterizar los conjuntos de soluciones de sistemas de restricciones polinómicas positivas.
   • Para potencias fijas (por ejemplo, $Z_k = \{n^k\}$), los autores aprovechan resultados sobre ecuaciones diofánticas hiperelípticas. Demuestran que la intersección de dos tales restricciones produce un conjunto finito (si los grados son lo suficientemente altos) o un conjunto parametrizado por sucesiones de recurrencia lineal (LRS) si los grados son 2.
   • Para polinomios generales de grado a lo sumo 3, el análisis se basa en el género de las curvas algebraicas resultantes. Los sistemas que involucran polinomios cúbicos a menudo conducen a curvas de género 1 (curvas elípticas) o superiores, las cuales tienen un número finito de puntos enteros según el teorema de Siegel o las cotas de Baker. Los sistemas que involucran polinomios cuadráticos se relacionan con ecuaciones de Pell, cuyas soluciones forman LRS reversibles.
3. Manejo de Restricciones Negativas (Argumentos de Densidad): Una idea crucial es que, cuando el conjunto de soluciones de las restricciones positivas es infinito, el conjunto de soluciones que violan una restricción negativa (es decir, que satisfacen la versión positiva del predicado negado) tiene densidad relativa cero dentro del conjunto de soluciones original.
   • Para imágenes polinómicas, la tasa de crecimiento de la imagen es polinómica, mientras que el conjunto "prohibido" (si surge de un polinomio diferente) a menudo crece a una tasa diferente o es escaso.
   • En casos donde el conjunto de soluciones es una LRS, los autores demuestran que los índices de las soluciones "prohibidas" forman progresiones aritméticas. Esto permite una verificación efectiva para determinar si quedan soluciones después de excluir el subconjunto de densidad nula.
4. Redundancia y Coalescencia: Los autores definen nociones de restricciones "redundantes" y "similares". Las restricciones redundantes pueden descartarse, mientras que las restricciones similares pueden coalescerse en una sola restricción utilizando valuaciones $p$-ádicas y el Teorema Chino del Resto, simplificando el sistema antes de aplicar los argumentos de densidad.

Contribuciones y Resultados Clave

El artículo establece dos resultados principales de decidibilidad para teorías de una sola variable ($k=1$):

1. Decidibilidad con Potencias Fijas: La teoría $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$ es decidible. Este resultado se basa en la resolubilidad de ecuaciones diofánticas hiperelípticas ($w^k - nz^j = N$) y en el hecho de que los sistemas de tales ecuaciones tienen un número finito de soluciones o soluciones parametrizadas por LRS.
2. Decidibilidad con Polinomios de Bajo Grado: La teoría $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$ es decidible, donde cada $R_i$ corresponde a la imagen de un polinomio de valor entero de grado a lo sumo 3. Este resultado utiliza el bajo género de las curvas algebraicas asociadas (género 0 o 1) y la estructura de las soluciones a ecuaciones de Pell simultáneas.

Resultados de Indecidibilidad
Para delinear los límites de estos resultados positivos, el artículo proporciona pruebas de indecidibilidad cuando se elimina el límite de variables o se combinan predicados específicos:

• El fragmento existencial $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$ es indecidible. Esto se demuestra codificando la negación de la conjetura de Büchi, lo que permite definir la multiplicación utilizando un número limitado de variables.
• Utilizando las ecuaciones diofánticas universales de Jones y la prueba reciente de Xiao de la conjetura de Büchi, los autores establecen que las teorías con conteos de variables significativamente más altos (por ejemplo, $SMT_{600}$ o $SMT_{2200}$ con $Z^2$) son indecidibles.

Significado
El significado del artículo radica en identificar límites precisos donde se puede recuperar la decidibilidad en expansiones no lineales de la aritmética de Presburger. Al restringir el número de variables a uno, los autores demuestran que resultados profundos de la geometría diofántica (como la finitud de puntos enteros en curvas de género $\ge 2$) y la teoría de las sucesiones de recurrencia lineal son suficientes para construir procedimientos de decisión.

El trabajo destaca una dicotomía: mientras que las expansiones no lineales generales son indecidibles, e incluso el fragmento existencial con dos variables y cuadrados perfectos es indecidible, el caso de una sola variable sigue siendo tratable para amplias familias de predicados. Los autores señalan que extender estos resultados a dos o tres variables se ve obstaculizado por famosos problemas abiertos, como la existencia de ladrillos de Euler perfectos (que requieren 3 variables y $Z^2$) y el problema de la suma de tres cubos (que requiere 2 variables y $Z^3$). Por lo tanto, el artículo proporciona un marco riguroso para comprender la complejidad computacional de las teorías aritméticas restringidas por límites de variables.