Формальна арифметика

Формальна арифметика — це формулювання арифметики у вигляді формальної (аксіоматичної) системи. Мова формальної арифметики містить константу ${\displaystyle {\mbox{0}}}$, числові змінні, символ рівності, функціональні символи ${\displaystyle {\mbox{+}}}$, ${\displaystyle \times }$, (збільшення 1) і логічні зв'язки. Постулатами формальної арифметики є аксіоми і правила виводу числення предикатів, що визначають рівність для арифметичних операцій. Засоби формальної арифметики достатні для виведення теорем елементарної теорії чисел. На даний момент невідомо жодної змістовної теоретико-числової теореми, доведеної без залучення засобів аналізу, яка не виводилася б у формальну арифметику. У формальній арифметиці змальовані рекурсивні функції і їх визначена рівність. Це дозволяє формулювати думки про скінченну множину. Більш того, формальна арифметика еквівалентна аксіоматичній теорії множин Цермела – Френкеля. Без аксіоми нескінченності у кожній з цих систем може бути побудована інша модель.

Підручник з арифметики Леонтія Магницького, 1703 рік

Джузеппе Пеано в 1889 році сформулював аксіоми натуральних чисел

Ганс Себальд Бехам. Арифметика. XVI век

Формальна арифметика задовольняє умовам обох теорем Геделя про неповноту. Зокрема, є такі поліноми ${\displaystyle {\mbox{P}}}$ , ${\displaystyle {\mbox{Q}}}$ від 9 змінних, що формула " ${\displaystyle {\mbox{x1...x9}}}$ " ${\displaystyle {\mbox{(P1Q)}}}$ не виводиться, хоча і виражає дійсну думку, а саме несуперечність формальної арифметики. Тому нерозв'зність діофантового рівняння Р-Q=0 недоказова у формальній арифметиці. Несуперечність формальної арифметики доведена за допомогою трансфінітної індукції до ординала е0 (найменший розв'язок рівняння ${\displaystyle {\mbox{we=e}}}$). Тому схема індукції до е0 недоказова у формальній арифметиці, хоча там доказова схема індукції до будь-якого ординала а<e0. Класу доказово рекурсивних функцій формальної арифметики (тобто частково рекурсивних функцій, загальна рекурсивність яких може бути встановлена засобами формальної арифметики) збігається з класом ординально-рекурсивних функцій з ординалами <e0.

Не всі теоретико-числові предикати виражаються у формальній арифметиці: прикладом є такий предикат ${\displaystyle {\mbox{T}}}$, що для будь-якої замкнутої арифметичної формули ${\displaystyle {\mbox{A}}}$ має місце Т (é А ù) , де é А ù – номер формули ${\displaystyle {\mbox{A}}}$ в деякій фіксованій нумерації, що задовольняє природним умовам. Приєднання до формальної арифметики символу ${\displaystyle {\mbox{T}}}$, що виражають його перестановку з логічними зв'язками, що дозволяє довести не суперечність формально арифметики. Схожа конструкція доводить, що схему індукції не можна замінити жодною кінцевою безліччю аксіом. Формальна арифметика коректна і повна відносно формул вигляду "${\displaystyle {\mbox{x 1 ... x}}}$" до ${\displaystyle {\mbox{( P=Q )}}}$; замкнута формула з цього класу доказова тоді і лише тоді, коли вона достеменна. Оскільки цей клас містить алгоритмічно нерозв'язний предикат, звідси випливає, що проблема вивідності у формальній арифметиці алгоритмічно нерозв'язна.

При заданні формальної арифметики у вигляді гензенівської системи реалізована нормалізація виводу, причому нормальне виведення числової рівності складається лише з числової рівності. На цьому шляху було отримано перший доказ несуперечності формальної арифметики. Нормальне виведення формули з кванторами може містити скільки завгодно складних формул. Повна підформульність досягається після заміни схеми індукції на со-правило. Поняття ${\displaystyle {\mbox{w}}}$-виведення (тобто виводу з ${\displaystyle {\mbox{w}}}$-правилом) висоти <e0 виражається у формальній арифметиці, тому перехід до ${\displaystyle {\mbox{w}}}$-виводів дозволяє встановлювати у Ф. а. багато метаматематичних теорем, зокрема повноту і ординальну характеристику рекурсивних функцій.