Формальна арифметика, формулювання арифметики у вигляді формальної (аксіоматичною) системи (див. Аксіоматичний метод ) . Мова Ф. а. містить константу 0, числові змінні, символ рівності, функціональні символи +, •, '' (збільшення 1) і логічні в'язки (див. Логічні операції ) . Постулатами Ф. а. є аксіоми і правила виводу числення предикатів (класичного або інтуїционістського залежно від того, яка Ф. а. розглядається), що визначають рівність для арифметичних операцій:
а + 0 = а , а + b’ = ( а + b ),
а •0 = 0, а • b’ = ( а • b ) + а ,
аксіоми Пеано:
ù( а’ = 0), а’ = b’ ® а = b ,
( а = b & а = з ) ® b = з , а = b ® а '' = b ''
і схема аксіом індукції:
А (0) & " x ( А ( х ) ® А ( x '')) ® " ха ( x ).
Засоби Ф. а. достатні для виведення теорем елементарної теорії чисел. В даний час, мабуть, невідомо жодної змістовної теоретіко-числової теореми, доведеної без залучення засобів аналізу, яка не виводилася б у Ф. а. У Ф. а. змальовані рекурсивні функції і доказова їх визначальна рівність. Це дозволяє, зокрема, формулювати думки про кінцеву безліч. Більш того, Ф. а. еквівалентна аксіоматичної теорії безлічі Цермела – Френкеля без аксіоми нескінченність: у кожній з цих систем може бути побудована модель інший.
Ф. а. задовольняє умовам обох теорем Геделя про неповноту. Зокрема, є такі поліноми Р , Q від 9 змінних, що формула " x 1 ... " x 9 ( P ¹ Q ) не виводиться, хоча і виражає дійсну думку, а саме несуперечність Ф. а. Тому нерозв'зність діофантова рівняння Р - Q = 0 недоказова у Ф. а. Несуперечність Ф. а. доведена за допомогою трасфінітной індукції до ордінала e 0 (найменше вирішення рівняння w e = e). Тому схема індукції до e 0 недоказова у Ф. а., хоча там доказова схема індукції до будь-якого ордінала а < e 0 . Клас доказово рекурсивних функцій Ф. а. (тобто частково рекурсивних функцій, общерекурсивность яких може бути встановлена засобами Ф. а.) збігається з класом ордінально рекурсивних функцій з ордіналамі < e 0 .
Не всі теоретіко-числові предикати виразіми у Ф. а.: прикладом є такий предикат T, що для будь-якої замкнутої арифметичної формули А має місце Т (é А ù) « А, де é А ù – номер формули А в деякої фіксованої нумерації що задовольняє природним умовам. Приєднання до Ф. а. символу Т з аксіомами типа
Т (é А & B ù) « Т (é А ù) & Т (é B ù),
що виражають його перестановочность з логічними в'язками, дозволяє довести несуперечність Ф. а. Схожа конструкція (але вже усередині Ф. а.) доводить, що схему індукції не можна замінити жодним кінцевим безліччю аксіом. Ф. а. коректна і повна відносно формул вигляду $ x 1 ... $ x до ( P = Q ); замкнута формула з цього класу доказова тоді і лише тоді, коли вона достеменна. Оскільки цей клас містить алгоритмічно нерозв'язний предикат, звідси витікає, що проблема виводимості у Ф. а. алгоритмічно нерозв'язна.
При завданні Ф. а. у вигляді генценовськой системи осуществіма нормалізація виводів, причому нормальне виведення числової рівності складається лише з числової рівності. На цій дорозі було отримано перший доказ несуперечності Ф. а. Нормальне виведення формули з кванторами може містити скільки завгодно складні формули. Повна подформульность досягається після заміни схеми індукції на со-правіло, що дозволяє вивести В ® " xa ( x ) з В ® A (0), B ® A (1)... Поняття w-віведення (тобто виводу з w-правілом) висоти < e 0 виразимий у Ф. а., тому перехід до w-віводів дозволяє встановлювати у Ф. а. багато метаматематичних теорем, зокрема повноту відносно формул вигляду $ x 1 ... $ x до ( P = Q ) і ордінальную характеристики доказово рекурсивних функцій.
Літ.: Кліні С. До., Введення в метаматематику, пер.(переведення) з англ.(англійський), М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, Ст, 1968–70.
