Aritmética de Presburger

La aritmética de Presburger es la teoría de primer orden de los números naturales con adición , llamada así en honor a Mojżesz Presburger , quien la introdujo en 1929. La signatura de la aritmética de Presburger contiene únicamente la operación de adición y la igualdad , omitiendo por completo la operación de multiplicación . La teoría es computablemente axiomatizable; los axiomas incluyen un esquema de inducción .

La aritmética de Presburger es mucho más débil que la aritmética de Peano , que incluye operaciones tanto de suma como de multiplicación. A diferencia de la aritmética de Peano, la aritmética de Presburger es una teoría decidible . Esto significa que es posible determinar algorítmicamente, para cualquier oración en el lenguaje de la aritmética de Presburger, si esa oración es demostrable a partir de los axiomas de la aritmética de Presburger. Sin embargo, la complejidad computacional asintótica en tiempo de ejecución de este algoritmo es al menos doblemente exponencial , como lo demostraron Fischer y Rabin (1974).

El lenguaje de la aritmética de Presburger contiene las constantes 0 y 1 y una función binaria +, interpretada como suma.

En este lenguaje, los axiomas de la aritmética de Presburger son los cierres universales de los siguientes:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + ( y + 1) = ( x + y ) + 1
5. Sea P ( x ) una fórmula de primer orden en el lenguaje de la aritmética de Presburger con una variable libre x (y posiblemente otras variables libres). Entonces la siguiente fórmula es un axioma:
   ( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y ).

(5) es un esquema axiomático de inducción que representa una cantidad infinita de axiomas. Estos no pueden ser reemplazados por ningún número finito de axiomas, es decir, la aritmética de Presburger no es finitamente axiomatizable en la lógica de primer orden. ^[1]

La aritmética de Presburger puede considerarse como una teoría de primer orden con igualdad que contiene precisamente todas las consecuencias de los axiomas anteriores. Alternativamente, puede definirse como el conjunto de aquellas oraciones que son verdaderas en la interpretación pretendida : la estructura de números enteros no negativos con constantes 0, 1 y la adición de números enteros no negativos.

La aritmética de Presburger está diseñada para ser completa y decidible. Por lo tanto, no puede formalizar conceptos como divisibilidad o primalidad o, de manera más general, ningún concepto numérico que conduzca a la multiplicación de variables. Sin embargo, puede formular casos individuales de divisibilidad; por ejemplo, demuestra "para todo x , existe y  : ( y + y = x ) ∨ ( y + y + 1 = x )". Esto establece que todo número es par o impar.

Presburger (1929) demostró que la aritmética de Presburger era:

• consistente : No hay ningún enunciado en la aritmética de Presburger que pueda deducirse de los axiomas de manera que también pueda deducirse su negación.
• completo : Para cada enunciado en el lenguaje de la aritmética de Presburger, es posible deducirlo de los axiomas o es posible deducir su negación.
• decidible : Existe un algoritmo que decide si cualquier enunciado dado en la aritmética de Presburger es un teorema o un no teorema - nótese que un "no teorema" es una fórmula que no se puede demostrar, no necesariamente en general una cuya negación se pueda demostrar, pero en el caso de una teoría completa como aquí ambas definiciones son equivalentes.

La decidibilidad de la aritmética de Presburger se puede demostrar utilizando la eliminación de cuantificadores , complementada con un razonamiento sobre la congruencia aritmética . ^{[2] [3] [4] [5] [6]} Los pasos utilizados para justificar un algoritmo de eliminación de cuantificadores se pueden utilizar para definir axiomatizaciones computables que no necesariamente contienen el esquema axiomático de inducción. ^{[2] [7]}

Por el contrario, la aritmética de Peano , que es la aritmética de Presburger aumentada con la multiplicación, no es decidible, como lo demostró Church junto con la respuesta negativa al Entscheidungsproblem . Por el teorema de incompletitud de Gödel , la aritmética de Peano es incompleta y su consistencia no es demostrable internamente (pero véase la prueba de consistencia de Gentzen ).

El problema de decisión para la aritmética de Presburger es un ejemplo interesante en la teoría de la complejidad computacional y la computación . Sea n la longitud de un enunciado en la aritmética de Presburger. Luego, Fischer y Rabin (1974) demostraron que, en el peor de los casos, la prueba del enunciado en lógica de primer orden tiene una longitud de al menos , para alguna constante c > 0. Por lo tanto, su algoritmo de decisión para la aritmética de Presburger tiene un tiempo de ejecución al menos exponencial. Fischer y Rabin también demostraron que para cualquier axiomatización razonable (definida con precisión en su artículo), existen teoremas de longitud n que tienen pruebas de longitud doblemente exponencial . Intuitivamente, esto sugiere que hay límites computacionales sobre lo que se puede demostrar mediante programas de computadora. El trabajo de Fischer y Rabin también implica que la aritmética de Presburger se puede utilizar para definir fórmulas que calculen correctamente cualquier algoritmo siempre que las entradas sean menores que límites relativamente grandes. Los límites se pueden aumentar, pero solo mediante el uso de nuevas fórmulas. Por otra parte, Oppen (1978) demostró un límite superior triplemente exponencial en un procedimiento de decisión para la aritmética de Presburger. ${\displaystyle 2^{2^{cn}}}$

Berman (1980) demostró un límite de complejidad más estricto utilizando clases de complejidad alternadas. El conjunto de enunciados verdaderos en la aritmética de Presburger (PA) se muestra completo para TimeAlternations (2 ^{2 n O(1)} , n). Por lo tanto, su complejidad está entre el tiempo no determinista exponencial doble (2-NEXP) y el espacio exponencial doble (2-EXPSPACE). La completitud está bajo reducciones de muchos a uno en tiempo polinomial . (Además, tenga en cuenta que, si bien la aritmética de Presburger se abrevia comúnmente PA, en matemáticas en general PA generalmente significa aritmética de Peano ).

Para obtener un resultado más detallado, sea PA(i) el conjunto de declaraciones PA Σ _{i verdaderas, y PA(i, j) el conjunto de declaraciones PA Σ i} verdaderas con cada bloque cuantificador limitado a j variables. '<' se considera libre de cuantificadores; aquí, los cuantificadores acotados se cuentan como cuantificadores.
PA(1, j) está en P, mientras que PA(1) es NP-completo. ^[8]
Para i > 0 y j > 2, PA(i + 1, j) es Σ _i ^P -completo . El resultado de dureza solo necesita j>2 (en lugar de j=1) en el último bloque cuantificador.
Para i>0, PA(i+1) es Σ _i ^EXP -completo . ^[9]

La aritmética de Presburger corta ( ) es completa (y por lo tanto NP-completa para ). Aquí, 'corta' requiere un tamaño de oración acotado (es decir, ) excepto que las constantes enteras no son acotadas (pero su número de bits en binario cuenta contra el tamaño de entrada). Además, la PA de dos variables (sin la restricción de ser 'corta') es NP-completa. ^[10] La PA corta (y por lo tanto ) está en P, y esto se extiende a la programación lineal entera paramétrica de dimensión fija. ^[11]${\displaystyle \Sigma__{n}}$${\displaystyle n>2}$$Estilo de visualización: Sigma _{n-2}^{P}}$${\estilo de visualización n=3}$${\estilo de visualización O(1)}$${\displaystyle \Sigma _{2}}$$Estilo de visualización: Pi _{2}$${\displaystyle \Sigma _{2}}$

Debido a que la aritmética de Presburger es decidible, existen demostradores automáticos de teoremas para la aritmética de Presburger. Por ejemplo, el sistema de asistente de prueba Coq presenta la táctica omega para la aritmética de Presburger y el asistente de prueba Isabelle contiene un procedimiento de eliminación de cuantificadores verificado por Nipkow (2010). La complejidad exponencial doble de la teoría hace que sea inviable utilizar los demostradores de teoremas en fórmulas complicadas, pero este comportamiento ocurre solo en presencia de cuantificadores anidados: Nelson y Oppen (1978) describen un demostrador automático de teoremas que utiliza el algoritmo simplex en una aritmética de Presburger extendida sin cuantificadores anidados para demostrar algunas de las instancias de fórmulas aritméticas de Presburger sin cuantificadores. Los solucionadores de teorías de satisfacibilidad módulo más recientes utilizan técnicas de programación entera completa para manejar fragmentos sin cuantificadores de la teoría aritmética de Presburger. ^[12]

La aritmética de Presburger se puede ampliar para incluir la multiplicación por constantes, ya que la multiplicación es una suma repetida. La mayoría de los cálculos con subíndices de matrices caen entonces dentro de la región de los problemas decidibles. ^[13] Este enfoque es la base de al menos cinco sistemas de prueba de corrección para programas informáticos , comenzando con el Stanford Pascal Verifier a finales de los años 1970 y continuando hasta el sistema Spec# de Microsoft de 2005.

Se dan ahora algunas propiedades sobre relaciones de números enteros definibles en la aritmética de Presburger. Para simplificar, todas las relaciones consideradas en esta sección se refieren a números enteros no negativos.

Una relación es definible según Presburger si y sólo si es un conjunto semilineal . ^[14]

Una relación entera unaria , es decir, un conjunto de números enteros no negativos, es definible según Presburger si y solo si es en última instancia periódica. Es decir, si existe un umbral y un período positivo tales que, para todo número entero tal que , si y solo si . ${\estilo de visualización R}$${\displaystyle t\in \mathbb {N}}$${\displaystyle p\in \mathbb {N} ^{>0}}$${\estilo de visualización n}$${\displaystyle |n|\geq t}$${\displaystyle n\en R}$${\displaystyle n+p\en R}$

Por el teorema de Cobham-Semenov , una relación es definible según Presburger si y solo si es definible en aritmética de Büchi de base para todos los . ^{[15] [16]} Una relación definible en aritmética de Büchi de base y para y que sean enteros multiplicativamente independientes es definible según Presburger. ${\estilo de visualización k}$${\displaystyle k\geq 2}$${\estilo de visualización k}$${\estilo de visualización k'}$${\estilo de visualización k}$${\estilo de visualización k'}$

Una relación entera es definible según Presburger si y solo si todos los conjuntos de números enteros que son definibles en lógica de primer orden con adición y (es decir, aritmética de Presburger más un predicado para ) son definibles según Presburger. ^[17] De manera equivalente, para cada relación que no es definible según Presburger, existe una fórmula de primer orden con adición y que define un conjunto de números enteros que no es definible utilizando solo adición. ${\estilo de visualización R}$${\estilo de visualización R}$${\estilo de visualización R}$${\estilo de visualización R}$${\estilo de visualización R}$

Las relaciones definibles por Presburger admiten otra caracterización: mediante el teorema de Muchnik. ^[18] Es más complicado de enunciar, pero condujo a la demostración de las dos caracterizaciones anteriores. Antes de poder enunciar el teorema de Muchnik, deben introducirse algunas definiciones adicionales.

Sea un conjunto, la sección de , para y se define como ${\displaystyle R\subseteq \mathbb {N} ^{d}}$$Estilo de visualización x_{i}=j$${\estilo de visualización R}$${\displaystyle i<d}$${\displaystyle j\in \mathbb {N}}$

${\displaystyle \left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,x_{d-1})\in R\right\}.}$

Dados dos conjuntos y una -tupla de enteros , el conjunto se llama -periódico en si, para todos tales que entonces si y solo si . Para , se dice que el conjunto es -periódico en si es -periódico para algunos tales que ${\displaystyle R,S\subseteq \mathbb {N} ^{d}}$${\estilo de visualización d}$${\displaystyle (p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}}$${\estilo de visualización R}$${\displaystyle (p_{0},\puntos ,p_{d-1})}$${\estilo de visualización S}$${\displaystyle (x_{0},\puntos ,x_{d-1})\en S}$${\displaystyle (x_{0}+p_{0},\puntos ,x_{d-1}+p_{d-1})\en S,}$${\displaystyle (x_{0},\ldots ,x_{d-1})\en R}$${\displaystyle (x_{0}+p_{0},\puntos ,x_{d-1}+p_{d-1})\en R}$${\displaystyle s\in \mathbb {N}}$${\estilo de visualización R}$${\estilo de visualización s}$${\estilo de visualización S}$${\displaystyle (p_{0},\ldots ,p_{d-1})}$${\displaystyle (p_{0},\puntos ,p_{d-1})\in \mathbb {Z} ^{d}}$

${\displaystyle \suma _{i=0}^{d-1}|p_{i}|<s.}$

Finalmente, para dejar ${\displaystyle k,x_{0},\puntos ,x_{d-1}\en \mathbb {N} }$

${\displaystyle C(k,(x_{0},\ldots ,x_{d-1}))=\left\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1})\mid 0\leq c_{i}<k\right\}}$

denota el cubo de tamaño cuyo ángulo menor es . ${\estilo de visualización k}$${\displaystyle (x_{0},\puntos ,x_{d-1})}$

Intuitivamente, el entero representa la longitud de un desplazamiento, el entero es el tamaño de los cubos y es el umbral antes de la periodicidad. Este resultado sigue siendo cierto cuando se cumple la condición ${\estilo de visualización s}$${\estilo de visualización k}$${\estilo de visualización t}$

${\displaystyle \suma _{i=0}^{d-1}x_{i}>t}$

se reemplaza por o por . ${\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}$${\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}$

Esta caracterización dio lugar al denominado "criterio definible para la definibilidad en la aritmética de Presburger", es decir: existe una fórmula de primer orden con adición y un predicado -ario que se cumple si y sólo si se interpreta mediante una relación definible según Presburger. El teorema de Muchnik también permite demostrar que es decidible si una secuencia automática acepta un conjunto definible según Presburger. ${\estilo de visualización d}$${\estilo de visualización R}$${\estilo de visualización R}$

• Aritmética de Robinson
• Aritmética de Skolem

• Un demostrador de teoremas completo para la aritmética de Presburger por Philipp Rümmer