ФОРМАЛЬНАЯ АРИФМЕТИКА

ФОРМАЛЬНАЯ АРИФМЕТИКА формулировка
арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический
метод). Язык Ф. а. содержит константу 0, числовые переменные, символ
равенства, функциональные символы +, • ,' (прибавление 1) и логические
связки (см. Логические операции). Постулатами Ф. а. являются аксиомы
и правила вывода исчисления предикатов (классического или интуиционистского
в зависимости от того, какая Ф. а. рассматривается), определяющие равенства
для арифметических операций: а + 0 = а, а + b' = (а + b),

Средства Ф. а. достаточны
для вывода теорем элементарной теории чисел. В настоящее время, по-видимому,
неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной
без привлечения средств анализа, к-рая не была бы выводима в Ф. а. В Ф.
а. изобразимы рекурсивные функции и доказуемы их определяющие равенства.
Это позволяет, в частности, формулировать суждения о конечных множествах.
Более того, Ф. а. эквивалентна аксиоматической теории множеств Цермело
- Френкеля без аксиомы бесконечности: в каждой из этих систем может быть
построена модель другой.

Ф. а. удовлетворяет условиям
обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р,
Q
от 9 переменных, что формула Vxне =Q) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость
Ф. а. Поэтому неразрешимость диофан-това уравнения Р - Q = 0 недоказуема
в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции
до ординала ее=
е). Поэтому схема индукции до едоказуема схема индукции до любого ординала а <еКласс
доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций,
обще-рекурсивность к-рых может быть установлена средствами Ф. а.) совпадает
с классом ординально рекурсивных функций с ординалами <е

Не все теоретико-числовые
предикаты выразимы в Ф. а.: примером является такой предикат Т, что для
любой замкнутой арифметической формулы А имеет место Т(А )<->А,
где А -номер формулы А в нек-рой фиксированной нумерации,
удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т
с аксиомами типа

выражающими его перестановочность
с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая
конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя
заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно
формул вида Еx= Q); замкнутая формула
из этого класса доказуема тогда и только тогда, когда она истинна. Так
как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует,
что проблема выводимости в Ф. а. алгоритмически неразрешима.

При задании Ф. а. в виде
генценовской системы осуществима нормализация выводов, причём нормальный
вывод числового равенства состоит только из числовых равенств. На этом
пути было получено первое доказательство непротиворечивости Ф. а. Нормальный
вывод формулы с кванторами может содержать сколь угодно сложные формулы.
Полная подфор-мульность достигается после замены схемы индукции на w-правило,
позволяющее вывести .В >*VхА(х)изВ>А(0), В>А(1),... Понятие w-вывода
(т. е. зывода с w-правилом) высоты <епоэтому переход к w-выводам позволяет устанавливать в Ф. а. многие метаматематические
теоремы, в частности полноту относительно формул вида Еx= Q) и ординальную характеристику доказуемо рекурсивных функций.

Лит.: Клини С. К.,
Введение в метаматематику, пер. с англ., М., 1957; Нi1bеrt D., Веrnауs
P., Grundlagen der Mathematik, 2 Aufl., Bd 1 - 2, В., 1968 - 70.

Г. Е. Минц.