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

формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Ф. А. Содержит константу 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 переменных, что формула ∀x1. ∀x9 (P ≠ Q) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф.

А. Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф. А. Непротиворечивость Ф. А. Доказана с помощью трасфинитной индукции до ординала ε0 (наименьшее решение уравнения ωε = ε). Поэтому схема индукции до ε0 недоказуема в Ф. А., хотя там доказуема схема индукции до любого ординала α < ε0. Класс доказуемо рекурсивных функций Ф. А. (т. Е. Частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф. А.) совпадает с классом ординально рекурсивных функций с ординалами < ε0. Не все теоретико-числовые предикаты выразимы в Ф. А. Примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (⌈А⌉) ↔ А, где ⌈А⌉ – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям.

Присоединение к Ф. А. Символа Т с аксиомами типа Т (⌈А & B⌉) ↔ Т (⌈А⌉) & Т (⌈B⌉), выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. А. Похожая конструкция (но уже внутри Ф. А.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. А. Корректна и полна относительно формул вида ∃x1. ∃xk (P = Q). Замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. А. Алгоритмически неразрешима. При задании Ф. А. В виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств.

На этом пути было получено первое доказательство непротиворечивости Ф. А. Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В → ∀xA (x) из В → A (0), B → A (1),. Понятие ω-вывода (т. Е. Вывода с ω-правилом) высоты < ε0 выразимо в Ф. А., поэтому переход к ω-выводам позволяет устанавливать в Ф. А. Многие метаматематические теоремы, в частности полноту относительно формул вида ∃x1. ∃xk (P = Q) и ординальную характеристику доказуемо рекурсивных функций. Лит. Клини С. К., Введение в метаматематику, пер. С англ., М., 1957. Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.

Г. Е. Минц.