Arytmetyka Presburgera

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

Arytmetyka Presburgera jest układem aksjomatycznym liczb naturalnych z dodawaniem. Nazywana jest także arytmetyką Peano 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.