Арифметика Пресбургера
Арифметика Пресcбургера — це теорія першого порядку яка описує натуральні числа з додаванням, але на відміну від арифметики Пеано, виключає висловлювання щодо множення. Названа в честь польського математика Мозеса Пресcбургера, котрий в 1929 році запропонував відповідну систему аксіом в логіці першого порядку, а також показав її вирішуваність.
У цьому розділі ми описуємо вирази безлічі в . Відзначимо відразу ж, що з такою сигнатурою елімінація кванторів неможлива. Справді, формула , справжня для парних Х , не є еквівалентною ніякої бескванторной формули. Тому нам потрібно, перш ніж проводити елімінацію кванторів, розширити сигнатуру. Наведений приклад формули підказує, яке розширення нам необхідно. Розглянемо рахункове сімейство двомісних предикатних символів 2″′, 3″′, 4″′,.... Символ С″′ буде інтерпретуватися як рівність по модулю С. Іншими словами, формула Х буде істинною в нашій інтерпретації, якщо порівняти з по модулю (залишки по модулю рівні; кратно).
Важливо мати на увазі, що індекс в не є змінною: у нас не триміснийпредикат, а рахункове сімейство двомісних предикатів.
Таке розширення не міняє класу виразність предикатів, оскільки, наприклад, можна виразити як . Зате після цього всяка формула еквівалентна бескванторной, як показує наступна теорема (звана теоремою про елімінації кванторів в Арифметика Прессбургера).
Аксіоми
Мова арифметики Пресcбургера включає константи 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) є формалізацією принципу математичної індукції. Вона не може бути еквівалентно замінена ніякою кінцевою системою аксіом. Таким чином арифметика Преcсбургера не є звичайно аксіоматичною.
Властивості
Мозес Прессбургер довів що арифметика Пресcбургера є:
- несуперечливою: Не існує такого твердження в арифметиці Преcсбургера яке може бути виведене з аксіом, разом з своїм запереченням.
- повною: Для кожного твердження в алфавіті арифметики Пресcбургера, незалежно від того чи можливо довести його з аксіом чи можна довести його заперечення.
- розвязною: Існує алгоритм який дозволяє сказати чи дане твердження буде істинним або хибним.
Розв'язність арифметики Преcсбургера може бути показана за допомогою елімінації кванторів, доповненим аргументацією про арифметичні рівняння.
Арифметика Пеано, яка являє собою арифметику Пресcбургера доповнену операцією множення, не є розв'язною, внаслідок негативної відповіді Задачі розв'язності. За теоремою Геделя про неповноту, арифметика Пеано є неповною і її несуперечливість не є внутрішньо доведеною.
Див. також
- Аксіоми Пеано
- Арифметика Робінсона
- Логіка першого порядку
Література
- Верещагин Н.К., Шень А. — Языки и исчисления стор. 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,".
- Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320–325.