![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/0/0e/Magnitsky.djvu/page1-640px-Magnitsky.djvu.jpg&w=640&q=50)
Формальна арифметика
З Вікіпедії, безкоштовно encyclopedia
Формальна арифметика — це формулювання арифметики у вигляді формальної (аксіоматичної) системи.
![]() | Цю статтю потрібно повністю переписати відповідно до стандартів якості Вікіпедії. (серпень 2018) |
![]() | Ця стаття є сирим перекладом з іншої мови. Можливо, вона створена за допомогою машинного перекладу або перекладачем, який недостатньо володіє обома мовами. (січень 2014) |
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/0e/Magnitsky.djvu/page3-640px-Magnitsky.djvu.jpg)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/3/3a/Giuseppe_Peano.jpg/320px-Giuseppe_Peano.jpg)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/0c/Arithmetria.jpg/640px-Arithmetria.jpg)
Мова формальної арифметики містить константу , числові змінні, символ рівності, функціональні символи
,
, (збільшення 1) і логічні зв'язки. Постулатами формальної арифметики є аксіоми і правила виводу числення предикатів, що визначають рівність для арифметичних операцій. Засоби формальної арифметики достатні для виведення теорем елементарної теорії чисел. На даний момент невідомо жодної змістовної теоретико-числової теореми, доведеної без залучення засобів аналізу, яка не виводилася б у формальну арифметику. У формальній арифметиці змальовані рекурсивні функції і їх визначена рівність. Це дозволяє формулювати думки про скінченну множину. Більш того, формальна арифметика еквівалентна аксіоматичній теорії множин Цермела – Френкеля. Без аксіоми нескінченності у кожній з цих систем може бути побудована інша модель.
Формальна арифметика задовольняє умовам обох теорем Геделя про неповноту. Зокрема, є такі поліноми ,
від 9 змінних, що формула "
"
не виводиться, хоча і виражає дійсну думку, а саме несуперечність формальної арифметики. Тому нерозв'зність діофантового рівняння Р-Q=0 недоказова у формальній арифметиці. Несуперечність формальної арифметики доведена за допомогою трансфінітної індукції до ординала е0 (найменший розв'язок рівняння
). Тому схема індукції до е0 недоказова у формальній арифметиці, хоча там доказова схема індукції до будь-якого ординала а<e0. Класу доказово рекурсивних функцій формальної арифметики (тобто частково рекурсивних функцій, загальна рекурсивність яких може бути встановлена засобами формальної арифметики) збігається з класом ординально-рекурсивних функцій з ординалами <e0.
Не всі теоретико-числові предикати виражаються у формальній арифметиці: прикладом є такий предикат , що для будь-якої замкнутої арифметичної формули
має місце Т (é А ù) , де é А ù – номер формули
в деякій фіксованій нумерації, що задовольняє природним умовам. Приєднання до формальної арифметики символу
, що виражають його перестановку з логічними зв'язками, що дозволяє довести не суперечність формально арифметики. Схожа конструкція доводить, що схему індукції не можна замінити жодною кінцевою безліччю аксіом. Формальна арифметика коректна і повна відносно формул вигляду "
" до
; замкнута формула з цього класу доказова тоді і лише тоді, коли вона достеменна. Оскільки цей клас містить алгоритмічно нерозв'язний предикат, звідси випливає, що проблема вивідності у формальній арифметиці алгоритмічно нерозв'язна.
При заданні формальної арифметики у вигляді гензенівської системи реалізована нормалізація виводу, причому нормальне виведення числової рівності складається лише з числової рівності. На цьому шляху було отримано перший доказ несуперечності формальної арифметики. Нормальне виведення формули з кванторами може містити скільки завгодно складних формул. Повна підформульність досягається після заміни схеми індукції на со-правило. Поняття -виведення (тобто виводу з
-правилом) висоти <e0 виражається у формальній арифметиці, тому перехід до
-виводів дозволяє встановлювати у Ф. а. багато метаматематичних теорем, зокрема повноту і ординальну характеристику рекурсивних функцій.