Arytmetyka Presburgera

Arytmetyka Presburgera jest układem aksjomatycznym liczb naturalnych z dodawaniem. Nazywana jest także arytmetyką Peana bez mnożenia. Język arytmetyki Presburgera zawiera 0 i 1, binarną funkcję + określaną jako dodawanie oraz relację równości. Główne aksjomaty arytmetyki:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. (x + y) + 1 = x + (y + 1)
5. Niech P(x) będzie formułą w języku Presburgera i niech dana będzie określona zmienna x. Wtedy następująca formuła jest aksjomatem:

(P(0) ∧ ∀x(P(x) → P(x + 1))) → P(y).

Ostatni aksjomat określany jest schematem indukcji reprezentującym nieskończoną liczbę aksjomatów. W roku 1929 Mojżesz Presburger udowodnił, że arytmetyka ta jest rozstrzygalna. Rozstrzygalność (decydowalność) problemu matematycznego to następująca jego właściwość: zawsze można określić czy dana odpowiedź na pytanie stawiane przez problem jest poprawna. Presburger udowodnił także, że taka arytmetyka jest niesprzeczna i zupełna (istnieje dowód T lub negacji T). Arytmetyka Presburgera przydaje się do rozstrzygalności problemów, choć czas działania zgrubnego algorytmu jest niejasny. Czas najlepszych algorytmów jest potrójnie wykładniczy. Niech n będzie długością twierdzenia w arytmetyce Presburgera; Fischer i Rabin (1974) udowodnili, że każdy algorytm sprawdzający prawdziwość twierdzenia musi wykonać w pesymistycznym przypadku co najmniej $2^{2^{cn}}$ kroków dla pewnej stałej c > 0.