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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук


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

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

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

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

Аксіоми[ред.ред. код]

Мова арифметики Пресcбургера включає константи 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) є формалізацією принципу математичної індукції. Вона не може бути еквівалентно замінена ніякою кінцевою системою аксіом. Таким чином арифметика Преcсбургера не є звичайно аксіоматичною.

Властивості[ред.ред. код]

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

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

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

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

Див. також[ред.ред. код]

Література[ред.ред. код]

  • Верещагин Н.К., Шень А. — Языки и исчисления стор. 114, 121, 224
  • Барвайс Д. — Справочная книга по математической логике. Часть 3: теория рекурсии