Арифметика Пресбургера — Вікіпедія

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

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

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

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

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

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

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

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

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

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

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

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

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

• Аксіоми Пеано
• Арифметика Робінсона
• Логіка першого порядку