|
|
Большая Советская Энциклопедия (цитаты)
|
|
|
|
|
Формальная арифметика | Формальная арифметика (далее Ф) формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Ф содержит константу 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 ( ¹ Q) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф Непротиворечивость Ф доказана с помощью трасфинитной индукции до ординала e0 (наименьшее решение уравнения we = e). Поэтому схема индукции до e0 недоказуема в Ф, хотя там доказуема схема индукции до любого ординала a < e0. Класс доказуемо рекурсивных функций Ф (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф) совпадает с классом ординально рекурсивных функций с ординалами < e0.
Не все теоретико-числовые предикаты выразимы в Ф: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (éАù) " А, где éАù – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф символа Т с аксиомами типа
Т (éА & ù) " Т (éАù) & Т (éù),
выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф Похожая конструкция (но уже внутри Ф) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф корректна и полна относительно формул вида $x1... $xk ( = Q); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф алгоритмически неразрешима.
При задании Ф в виде генценовской системы осуществима нормализация выводов, причем нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Ф Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В ® "xA (x) из В ® A (0), ® A (1),... Понятие w-вывода (т. е. вывода с w-правилом) высоты < e0 выразимо в Ф, поэтому переход к w-выводам позволяет устанавливать в Ф многие метаматематические теоремы, в частности полноту относительно формул вида $x1... $xk ( = Q) и ординальную характеристику доказуемо рекурсивных функций.
Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays ., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.
Г. Е. Минц.
|
Для поиска, наберите искомое слово (или его часть) в поле поиска
|
|
 |
 |
 |
|
