ФОРМАЛЬНАЯ АРИФМЕТИКА, формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Ф. а. содержит константу 0, числовые переменные, символ равенства, функциональные символы +, • ,‘ (прибавление 1) и логические связки (см. Логические операции). Постулатами Ф. а. являются аксиомы и правила вывода исчисления предикатов (классического или интуиционистского в зависимости от того, какая Ф. а. рассматривается), определяющие равенства для арифметических операций: а + 0 = а, а + b‘ = (а + b),
Средства Ф. а. достаточны для вывода теорем элементарной теории чисел. В настоящее время, по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, к-рая не была бы выводима в Ф. а. В Ф. а. изобразимы рекурсивные функции и доказуемы их определяющие равенства. Это позволяет, в частности, формулировать суждения о конечных множествах. Более того, Ф. а. эквивалентна аксиоматической теории множеств Цермело - Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.
Ф. а. удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р, Q от 9 переменных, что формула Vx1...Vx9,(P не =Q) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф. а. Поэтому неразрешимость диофан-това уравнения Р - Q = 0 недоказуема в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции до ординала еО (наименьшее решение уравнения wе= е). Поэтому схема индукции до е0 недоказуема в Ф. а., хотя там доказуема схема индукции до любого ординала а <е0. Класс доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций, обще-рекурсивность к-рых может быть установлена средствами Ф. а.) совпадает с классом ординально рекурсивных функций с ординалами <е0.
Не все теоретико-числовые предикаты выразимы в Ф. а.: примером является такой предикат Т, что для любой замкнутой арифметической формулы А имеет место Т(А )<->А, где А -номер формулы А в нек-рой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т с аксиомами типа
выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно формул вида Еx1..Ехk(P = Q); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. а. алгоритмически неразрешима.
При задании Ф. а. в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Ф. а. Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подфор-мульность достигается после замены схемы индукции на w-правило, позволяющее вывести .В >*VхА(х)изВ>А(0), В>А(1),... Понятие w-вывода (т. е. зывода с w-правилом) высоты <е0 выразимо в Ф. а., поэтому переход к w-выводам позволяет устанавливать в Ф. а. многие метаматематические теоремы, в частности полноту относительно формул вида Еx1...Еxк(P = Q) и ординальную характеристику доказуемо рекурсивных функций.
Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Нi1bеrt D., Веrnауs P., Grundlagen der Mathematik, 2 Aufl., Bd 1 - 2, В., 1968 - 70.
Г. Е. Минц.