Формальна арифметика — це формулювання арифметики у вигляді формальної (аксіоматичної) системи.
Мова формальної арифметики містить константу , числові змінні, символ рівності, функціональні символи , , (збільшення 1) і логічні зв'язки. Постулатами формальної арифметики є аксіоми і правила виводу числення предикатів, що визначають рівність для арифметичних операцій. Засоби формальної арифметики достатні для виведення теорем елементарної теорії чисел. На даний момент невідомо жодної змістовної теоретико-числової теореми, доведеної без залучення засобів аналізу, яка не виводилася б у формальну арифметику. У формальній арифметиці змальовані рекурсивні функції і їх визначена рівність. Це дозволяє формулювати думки про скінченну множину. Більш того, формальна арифметика еквівалентна аксіоматичній теорії множин Цермела – Френкеля. Без аксіоми нескінченності у кожній з цих систем може бути побудована інша модель.
Формальна арифметика задовольняє умовам обох теорем Геделя про неповноту. Зокрема, є такі поліноми , від 9 змінних, що формула " " не виводиться, хоча і виражає дійсну думку, а саме несуперечність формальної арифметики. Тому нерозв'зність діофантового рівняння Р-Q=0 недоказова у формальній арифметиці. Несуперечність формальної арифметики доведена за допомогою трансфінітної індукції до ординала е0 (найменший розв'язок рівняння ). Тому схема індукції до е0 недоказова у формальній арифметиці, хоча там доказова схема індукції до будь-якого ординала а<e0. Класу доказово рекурсивних функцій формальної арифметики (тобто частково рекурсивних функцій, загальна рекурсивність яких може бути встановлена засобами формальної арифметики) збігається з класом ординально-рекурсивних функцій з ординалами <e0.
Не всі теоретико-числові предикати виражаються у формальній арифметиці: прикладом є такий предикат , що для будь-якої замкнутої арифметичної формули має місце Т (é А ù) , де é А ù – номер формули в деякій фіксованій нумерації, що задовольняє природним умовам. Приєднання до формальної арифметики символу , що виражають його перестановку з логічними зв'язками, що дозволяє довести не суперечність формально арифметики. Схожа конструкція доводить, що схему індукції не можна замінити жодною кінцевою безліччю аксіом. Формальна арифметика коректна і повна відносно формул вигляду "" до ; замкнута формула з цього класу доказова тоді і лише тоді, коли вона достеменна. Оскільки цей клас містить алгоритмічно нерозв'язний предикат, звідси випливає, що проблема вивідності у формальній арифметиці алгоритмічно нерозв'язна.
При заданні формальної арифметики у вигляді гензенівської системи реалізована нормалізація виводу, причому нормальне виведення числової рівності складається лише з числової рівності. На цьому шляху було отримано перший доказ несуперечності формальної арифметики. Нормальне виведення формули з кванторами може містити скільки завгодно складних формул. Повна підформульність досягається після заміни схеми індукції на со-правило. Поняття -виведення (тобто виводу з -правилом) висоти <e0 виражається у формальній арифметиці, тому перехід до -виводів дозволяє встановлювати у Ф. а. багато метаматематичних теорем, зокрема повноту і ординальну характеристику рекурсивних функцій.
Означення Формальна арифметика – це числення предикатів, в якому є: Предметна константа . Двомісні функціональні символи та , одномісний функціональний символ . Двомісний предикат ( позначатимемо через ). Власні схеми аксіом: .
Тут – довільна формула, а , , – довільні терми теорії . Схема аксіом виражає принцип математичної індукції.
Класифікація Формальна арифметика поділяється на такі види: класична формальна арифметика з D-оператором; класична формальна арифметика з P-опера тором; конструктивна формальна арифметика.
Див. також Теоретична арифметика Числення висловлень Квантор Правило резолюцій Числення секвенцій Логіка другого порядку Теорема Льовенгейма—Сколема Нормальна форма Сколема
Джерела Формальна арифметика Основи математичної логіки Класична формальна арифметика з P-оператором формальна арифметика з D-оператором Конструктивна формальна арифметика Числення предикатів
Список літератури
Арнольд І. В. Теоретична арифметика. К., 1939;
Беллюстин В. К. Как постепенно дошли люди до настоящей арифметики. М., 1940; Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947 Клини С. К. Введение в метаматематику. М., 1957 Мендельсон Э. Введение в математическую логику. М., 1976 Новиков П. С. Элементы математической логики. М., 1959 Черч А. Введение в математическую логику, т. I. М. 1960