Арифметика Пресбургера

Арифметика Прессбургера — це теорія першого порядку яка описує натуральні числа з додаванням, але на відміну від арифметики Пеано, виключає висловлювання щодо множення. Названа в честь польського математика Мозеса Прессбургера, котрий в 1929 році запропонував відповідну систему аксіом в логіці першого порядку, а також показав її вирішуваність.

У цьому розділі ми описуємо вирази безлічі [1] [Архівовано 24 вересня 2015 у Wayback Machine.] в . Відзначимо відразу ж, що з такою сигнатурою елімінація кванторів неможлива. Справді, формула [2] [Архівовано 24 вересня 2015 у Wayback Machine.], справжня для парних Х , не є еквівалентною ніякої бескванторной формули. Тому нам потрібно, перш ніж проводити елімінацію кванторів, розширити сигнатуру. Наведений приклад формули підказує, яке розширення нам необхідно. Розглянемо рахункове сімейство двомісних предикатних символів 2″′, 3″′, 4″′,.... Символ С″′ буде інтерпретуватися як рівність по модулю С. Іншими словами, формула Х буде істинною в нашій інтерпретації, якщо порівняти з по модулю (залишки по модулю рівні; кратно).

Важливо мати на увазі, що індекс в не є змінною: у нас не триміснийпредикат, а рахункове сімейство двомісних предикатів.

Таке розширення не міняє класу виразність предикатів, оскільки, наприклад, можна виразити як [3] [Архівовано 24 вересня 2015 у Wayback Machine.]. Зате після цього всяка формула еквівалентна бескванторной, як показує наступна теорема (звана теоремою про елімінації кванторів в Арифметика Прессбургера).

Аксіоми

Мова арифметики Прессбургера включає константи 0, 1, одну операцію + і предикат рівності =. Аксіоми мають вигляд:

¬(0 = x + 1)
x + 1 = y + 1 → x = y
x + 0 = x
(x + y) + 1 = x + (y + 1)
(P(0) ∧ (P(x)→P(x + 1))) → P(y), де P — формула першого порядку включаючи 0, 1, +, = і одну вільну змінну x.

Слід зауважити, що (5) насправді не одна аксіома, а схема аксіом, що представляє нескінченну безліч аксіом, по одній, для кожної формули P. (5) є формалізацією принципу математичної індукції. Вона не може бути еквівалентно замінена ніякою скінченною системою аксіом. Таким чином арифметика Прессбургера не є скінченно аксіоматизовною.

Властивості

Мозес Прессбургер довів що арифметика Прессбургера є:

несуперечливою: Не існує такого твердження в арифметиці Прессбургера яке може бути виведене з аксіом, разом з своїм запереченням.

повною: Для кожного твердження в алфавіті арифметики Прессбургера, незалежно від того чи можливо довести його з аксіом чи можна довести його заперечення.

розвязною: Існує алгоритм який дозволяє сказати чи дане твердження буде істинним або хибним.

Розв'язність арифметики Прессбургера може бути показана за допомогою елімінації кванторів, доповненим аргументацією про арифметичні рівняння.

Арифметика Пеано, яка являє собою арифметику Прессбургера доповнену операцією множення, не є розв'язною, внаслідок негативної відповіді Задачі розв'язності. За теоремою Геделя про неповноту, арифметика Пеано є неповною і її несуперечливість не є внутрішньо доведеною.

Див. також

Література

Верещагин Н.К., Шень А. — Языки и исчисления стор. 114, 121, 224

Барвайс Д. — Справочная книга по математической логике. Часть 3: теория рекурсии

Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91–100.
Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
Fischer, M. J., and Michael O. Rabin, 1974, ""Super-Exponential Complexity of Presburger Arithmetic." Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27–41.
G. Nelson and D. C. Oppen (Apr. 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141—150.
Mojżesz Presburger, 1929, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt" in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
Pugh, William, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis, [Архівовано 22 листопада 2008 у Wayback Machine.]".
Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320–325.