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

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

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

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

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

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

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

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

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

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

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

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