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

Определение "Формальная арифметика" в Большой Советской Энциклопедии

Формальная арифметика, формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Формальная арифметика содержит константу 0, числовые переменные, символ равенства, функциональные символы +, •, " (прибавление 1) и логические связки (см. Логические операции). Постулатами Формальная арифметика являются аксиомы и правила вывода исчисления предикатов (классического или интуиционистского в зависимости от того, какая Формальная арифметика рассматривается), определяющие равенства для арифметических операций:
а + 0 = а, а + b’ = (а + b),
а •0 = 0, а •b’ = (а•b) + а,
аксиомы Пеано:
ù(а’ = 0), a’= b’ ® а = b,
(a = b & а = с) ® b = с, а = b ®a" = b"
и схема аксиом индукции:
А (0) & "x (А (х) ® А (x")) ® "xa (x).

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

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

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

Т (éА & Bù) « Т (éАù) & Т (éBù),

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

При задании Формальная арифметика в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Формальная арифметика Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В ® "xA (x) из В ® A (0), B ® A (1),... Понятие w-вывода (т. е. вывода с w-правилом) высоты < e₀ выразимо в Формальная арифметика, поэтому переход к w-выводам позволяет устанавливать в Формальная арифметика многие метаматематические теоремы, в частности полноту относительно формул вида $x₁... $x_k (P = Q) и ординальную характеристику доказуемо рекурсивных функций.

Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.
  Г. Е. Минц.