Arytmetyka Presburgera

Ten artykuł należy dopracować:

od 2024-04 → zweryfikować treść i dodać przypisy,
od 2024-04 → sformatować tekst (pomoc: podział na sekcje, tabele, wzory).
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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 ${\displaystyle 2^{2^{cn}}}$ kroków dla pewnej stałej c > 0.