Nella logica matematica , l' aritmetica Presburger è la teoria del primo ordine dei numeri naturali forniti con l' aggiunta . È stato introdotto nel 1929 da Mojżesz Presburger . Questa è l'aritmetica di Peano senza moltiplicazione , cioè con solo addizioni , oltre allo zero e all'operazione successiva. A differenza dell'aritmetica di Peano, l'aritmetica di Presburger è decidibile . Ciò significa che esiste un algoritmo che determina se un'affermazione del linguaggio dell'aritmetica di Presburger è dimostrabile dagli assiomi dell'aritmetica di Presburger.
La firma del linguaggio dell'aritmetica di Presburger contiene i simboli delle costanti 0 e 1, il simbolo della funzione binaria +. L'aritmetica è definita dai seguenti assiomi:
(5) è lo schema di induzione ed è un insieme infinito di assiomi. Possiamo dimostrare che l'aritmetica di Presburger non può essere finemente assiomatizzata nella logica del primo ordine.
Mojżesz Presburger ha dimostrato nel 1929 che la sua aritmetica, che è coerente, è completa . Come un modo ricorsivo assiomatizzabile e completa assiomatica teoria è decidibile , si deduce l'esistenza di un algoritmo che decide, data una proposizione della lingua del Presburger di aritmetica, se è dimostrabile o meno.
A differenza dell'aritmetica di Presburger, l'aritmetica di Peano non è completa sotto il teorema di incompletezza di Gödel . L'aritmetica di Peano non è decidibile (vedi problema decisionale ).
Considera qui il seguente problema decisionale : decidere se una formula dell'aritmetica di Presburger è vera. Michael J. Fisher e Michael O. Rabin hanno dimostrato che questo problema decisionale ha una complessità intrinseca doppiamente esponenziale. In altre parole, il problema decisionale è 2EXPTIME-hard: è uno dei problemi più difficili della classe di complessità 2EXPTIME , che è la classe dei problemi decidibili a tempo doppiamente esponenziali.
Esiste una procedura decisionale non elementare basata sulla teoria degli automi finiti.
Oppen nel 1978 ha fornito un algoritmo triplo esponenziale, cioè il problema se una formula dell'aritmetica di Presburger è vera è in 3EXPTIME, la classe dei problemi decidibili triplicamente esponenziali nel tempo.
Berman nel 1980 ha fornito un risultato più preciso della teoria della complessità usando macchine alternate : l'aritmetica di Presburger è completa per la classe di problemi decisa nel tempo 2 2 n O (1) en alternazioni, dove il numero n è la dimensione della formula da controllare . Questa classe contiene 2EXPTIME ed è contenuta in 3EXPTIME.
Il solutore SMT Z3 implementa l'aritmetica Presburger. L' assistente di prova Coq fornisce la strategia omega .
L' aritmetica di Peano è impostata sul linguaggio dell'aritmetica Presburger più un simbolo × funzione binaria la cui interpretazione intuitiva è la moltiplicazione. L'aritmetica di Peano contiene assiomi addizionali. L' aritmetica Robinson , non contiene il regime di induzione.