On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Sintesi Tecnica: Sulle Espansioni Non Lineari Limitate in Variabili dell'Aritmetica di Presburger

Enunciato del Problema
L'aritmetica di Presburger, la teoria del primo ordine degli interi con addizione e ordine, è decidibile. Tuttavia, la sua espansione mediante predicati non lineari, come l'insieme dei quadrati perfetti ($Z^2$) o le immagini di polinomi generali, è nota per essere indecidibile nel caso generale. Tale indecidibilità deriva dalla capacità di codificare la moltiplicazione all'interno di queste teorie. Sebbene la decidibilità del frammento esistenziale di tali espansioni rimanga un importante problema aperto (ad esempio, la congettura di Büchi riguardante i quadrati perfetti), questo articolo indaga una diversa via per recuperare la decidibilità: limitare il numero di variabili.

Gli autori si concentrano su espansioni dell'aritmetica di Presburger limitate in variabili con famiglie di predicati polinomiali monadici. Nello specifico, esaminano frammenti in cui il numero di variabili distinte è limitato da una costante $k$ (denotati come $FO_k$, $\exists FO_k$ e $SMT_k$). La sfida centrale è che, anche per una singola variabile ($k=1$), la decidibilità della questione se due predicati polinomiali si intersechino (ad esempio, $f(u) = g(v)$) costituisce un caso severamente ristretto del decimo problema di Hilbert, che è generalmente aperto.

Metodologia
L'articolo impiega una combinazione di tecniche di teoria dei numeri, geometria algebrica e teoria della misura per analizzare gli insiemi di soluzioni dei vincoli all'interno di questi frammenti limitati in variabili.

1. Pre-elaborazione e Riduzione: La procedura decisionale inizia riducendo frasi arbitrarie a un problema di soddisfacibilità che coinvolge una congiunzione di vincoli. Tali vincoli includono disuguaglianze lineari ($x > c$), aritmetica modulare ($x \equiv_m c$) e predicati polinomiali della forma $R(ax+b)$ o le loro negazioni $\neg R(ax+b)$. Gli autori utilizzano il Teorema Cinese del Resto per consolidare i vincoli modulari ed eseguono un'analisi dei casi per eliminare intervalli limitati, riducendo il problema alla determinazione della soddisfacibilità dei vincoli su un dominio illimitato.
2. Gestione dei Vincoli Positivi: Il cuore della metodologia consiste nel caratterizzare gli insiemi di soluzioni di sistemi di vincoli polinomiali positivi.
   • Per potenze fisse (ad esempio, $Z_k = \{n^k\}$), gli autori sfruttano risultati sulle equazioni diofantee iperellittiche. Dimostrano che l'intersezione di due vincoli del genere produce un insieme finito (se i gradi sono sufficientemente alti) o un insieme parametrizzato da sequenze di ricorrenza lineare (LRS) se i gradi sono 2.
   • Per polinomi generali di grado al massimo 3, l'analisi si basa sul genere delle curve algebriche risultanti. Sistemi che coinvolgono polinomi cubici spesso conducono a curve di genere 1 (curve ellittiche) o superiori, che hanno un numero finito di punti interi per il teorema di Siegel o i limiti di Baker. Sistemi che coinvolgono polinomi quadratici sono correlati alle equazioni di Pell, le cui soluzioni formano LRS reversibili.
3. Gestione dei Vincoli Negativi (Argomenti di Densità): Un'insight cruciale è che, quando l'insieme delle soluzioni ai vincoli positivi è infinito, l'insieme delle soluzioni che violano un vincolo negativo (cioè, soddisfano la versione positiva del predicato negato) ha densità relativa zero all'interno dell'insieme di soluzioni originale.
   • Per le immagini polinomiali, il tasso di crescita dell'immagine è polinomiale, mentre l'insieme "vietato" (se deriva da un polinomio diverso) spesso cresce a un ritmo diverso o è sparso.
   • Nei casi in cui l'insieme delle soluzioni è un LRS, gli autori dimostrano che gli indici delle soluzioni "vietate" formano progressioni aritmetiche. Ciò consente un controllo efficace per determinare se rimangono soluzioni dopo l'esclusione del sottoinsieme a densità nulla.
4. Ridondanza e Fusione: Gli autori definiscono nozioni di vincoli "ridondanti" e "simili". I vincoli ridondanti possono essere scartati, mentre i vincoli simili possono essere fusi in un singolo vincolo utilizzando le valutazioni $p$-adiche e il Teorema Cinese del Resto, semplificando il sistema prima di applicare gli argomenti di densità.

Contributi e Risultati Chiave

L'articolo stabilisce due principali risultati di decidibilità per le teorie monovariabili ($k=1$):

1. Decidibilità con Potenze Fisse: La teoria $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$ è decidibile. Questo risultato si basa sulla risolubilità delle equazioni diofantee iperellittiche ($w^k - nz^j = N$) e sul fatto che sistemi di tali equazioni hanno un numero finito di soluzioni o soluzioni parametrizzate da LRS.
2. Decidibilità con Polinomi di Basso Grado: La teoria $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$ è decidibile, dove ogni $R_i$ corrisponde all'immagine di un polinomio a valori interi di grado al massimo 3. Questo risultato utilizza il basso genere delle curve algebriche associate (genere 0 o 1) e la struttura delle soluzioni alle equazioni di Pell simultanee.

Risultati di Indecidibilità
Per delimitare i confini di questi risultati positivi, l'articolo fornisce dimostrazioni di indecidibilità quando il limite delle variabili viene rimosso o predicati specifici vengono combinati:

• Il frammento esistenziale $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$ è indecidibile. Ciò è dimostrato codificando la negazione della congettura di Büchi, che permette di definire la moltiplicazione utilizzando un numero limitato di variabili.
• Utilizzando le equazioni diofantee universali di Jones e la recente dimostrazione della congettura di Büchi da parte di Xiao, gli autori stabiliscono che le teorie con numeri di variabili significativamente più elevati (ad esempio, $SMT_{600}$ o $SMT_{2200}$ con $Z^2$) sono indecidibili.

Significato
Il significato dell'articolo risiede nell'identificare confini precisi in cui la decidibilità può essere recuperata nelle espansioni non lineari dell'aritmetica di Presburger. Limitando il numero di variabili a uno, gli autori dimostrano che risultati profondi della geometria diofantea (come la finitezza dei punti interi su curve di genere $\ge 2$) e la teoria delle sequenze di ricorrenza lineare sono sufficienti per costruire procedure decisionali.

Il lavoro evidenzia una dicotomia: mentre le espansioni non lineari generali sono indecidibili, e persino il frammento esistenziale con due variabili e quadrati perfetti è indecidibile, il caso monovariabile rimane trattabile per ampie famiglie di predicati. Gli autori notano che l'estensione di questi risultati a due o tre variabili è ostacolata da famosi problemi aperti, come l'esistenza di mattoni di Euler perfetti (che richiedono 3 variabili e $Z^2$) e il problema della somma di tre cubi (che richiede 2 variabili e $Z^3$). Pertanto, l'articolo fornisce un quadro rigoroso per comprendere la complessità computazionale delle teorie aritmetiche vincolate da limiti sulle variabili.