|
АРИФМЕТИКА ФОРМАЛЬНАЯРасстановка ударений: АРИФМЕ`ТИКА ФОРМА`ЛЬНАЯ АРИФМЕТИКА ФОРМАЛЬНАЯ, арифметическое исчисление, - логико-математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы +, ⋅, ' (прибавление 1) и логич. связки. Термы строятся из константы 0 и переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида 0'... '. Атомарные формулы - это равенства термов; остальные формулы строятся из атомарных с помощью логич. связок &, ∨, →, ⌉, ∀, ∃. Формулы в языке А. ф. наз. арифметическими формулами. Постулатами А. ф. являются постулаты предикатов исчисления (классического или интуиционистского в зависимости от того, какая А. ф. рассматривается), аксиомы Пеано и схема аксиом индукции где А - произвольная формула, наз. индукционной формулой. Средства А. ф. оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е гг.), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, к-рая не была бы выводима в А. ф. Запись и доказательство таких теорем в А. ф. требует выявления ее выразительных возможностей. Особенно существенна выразимость в А. ф. многих теоретико-числовых функций. В частности, в А. ф. можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этом оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство f(x') = g(x, f(x)) выражается формулой где F и G - формулы, изображающие графики функций f и g, соответственно. В А. ф. можно формулировать суждения о конечных множествах. Более того, классич. А. ф. эквивалентна аксиоматической теории множеств Цермело-Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой. Дедуктивная сила системы А. ф. характеризуется ординалом ε0 (наименьшее решение уравнения ωε = ε): в А. ф. выводима схема трансфинитной индукции до любого ординала α < ε0, но не выводима схема индукции до ε0 . Класс доказуемо рекурсивных функций системы А. ф. (т. е. частично рекурсивных функций, общерекурсивность к-рых может быть установлена средствами А. ф.) совпадает с классом ординально рекурсивных функций с ординалами < ε0 . Это позволяет погружать в А. ф. нек-рые ее расширения, напр. А. ф. с символами для всех примитивно рекурсивных функций и соответствующими дополнительными постулатами. А. ф. удовлетворяет условиям обеих Гёделя теорем о неполноте. В частности, имеются такие полиномы Р, Q от нескольких переменных, что формула ∀ X(Р (Х) ≠ Q(X)) невыводима, хотя и выражает истинное утверждение, а именно непротиворечивость системы А. ф. При исследовании структуры А. ф. (в частности, вопросов непротиворечивости) используется ее формулировка без кванторов, но с гильбертовским ε-символом. При построении формул этой системы не допускается употребление кванторов, но разрешается использование термов вида εx А (х) (нек-рое х, удовлетворяющее условию А, если такие х существуют, и 0 в противном случае). Постулаты ε-системы - это постулаты исчисления высказываний, правила для равенства, правило подстановки вместо свободной числовой переменной, аксиомы для функций +, ⋅, ', pd (вычитание 1 из положительных чисел) и следующие ε-аксиомы: Кванторы вводятся как сокращения: аксиома индукции оказывается выводимой. Формулы А. ф., содержащие свободные переменные, задают теоретико-числовые предикаты. Формулы, не содержащие свободных переменных (замкнутые формулы), выражают суждения, k-местный предикат от натуральных чисел наз. арифметическим, если найдется такая арифметич. формула Р(x1, ..., xk), что для любых натуральных чисел n1, ..., nk имеет место Это определяет классификацию арифметич. предикатов по типу префикса в предваренной форме соответствующей формулы. Класс ∑n (класс Пn) состоит из предикатов Р(α), изобразимых формулой вида где f - примитивно рекурсивная функция, Q1 есть ∃ (соответственно ∀) и Qi - чередующиеся кванторы (т. е. Qi + 1 есть Q→i, где ∀¯ есть ∃, а ∃¯ есть ∀). Каждый из этих классов содержит универсальный предикат, т. е. такой предикат Т(е, а), что для всякого одноместного предиката Р из того же класса имеется число еP, для к-рого верно ∀ х((Т(еP, х) ≡ Р(х)). Многоместные предикаты сводятся к одноместным с помощью функций, нумерующих системы натуральных чисел. При каждом n > 0 справедливо неравенство ∑n ≠ Пn, и класс с меньшим индексом есть собственная часть любого класса с большим индексом. Классификация предикатов порождает классификацию арифметич. функций на основе классификации соответствующих графиков. Не все теоретико-числовые предикаты арифметические: примером неарифметич. предиката является такой предикат Т(х), что для любой замкнутой арифметич. формулы А имеет место Т (⌜ А⌝) = А, где ⌜ А⌝ - номер формулы А в нек-рой фиксированной нумерации, удовлетворяющей естественным условиям. Предикат Т играет существенную роль в исследованиях структуры А. ф., в частности вопроса о независимости ее аксиом. Присоединение к А. ф. символа T с аксиомами типа T(⌜ A&B⌝) = T(⌜ А⌝)&T(⌜ B⌝), выражающими его перестановочность с логич. связками, позволяет доказать непротиворечивость А. ф. Та же конструкция (но уже внутри А. ф.) проходит для подсистемы A[n] системы А. ф., в к-рой схема индукции ограничена условием: индукционная формула имеет сложность ≤ n, т. е. принадлежит ∑n ∪ Пn . Роль T здесь успешно исполняет, напр., универсальный предикат для ∑n + 1 и соответствующее доказательство проводится в системе A[n + 1] . В силу второй теоремы Гёделя о неполноте отсюда следует, что A[n + 1] сильнее A[n], так что А. ф. не совпадает ни с одной из систем A[n] и схему индукции нельзя заменить никаким конечным множеством аксиом. А. ф. оказывается полной относительно формул из класса ∑1 : замкнутая формула из этого класса выводима в А. ф. тогда и только тогда, когда она истинна. Так как класс ∑1 содержит алгорифмически неразрешимый предикат, отсюда следует, что проблема выводимости в А. ф. алгорифмически неразрешима. При задании А. ф. в виде Генцена формальной системы обычного типа сечение оказывается неустранимым. Устранение сечения становится возможным, если заменить схему индукции правилом бесконечной индукции (ω-правило): На этом пути было получено одно из первых доказательств непротиворечивости А. ф. При фактическом построении системы с ω-правилом основным оказывается предикат «число е есть номер общерекурсивной функции, описывающей вывод длины < ε0 с ω-правилом (ω-вывод)». Этот предикат принадлежит классу П2, и получающаяся система оказывается не формальной, а лишь полуформальной. Каждому выводу формулы A в А. ф. удается сопоставить такое число е, что суждение «e есть ω-вывод формулы A без сечения» истинно (и даже доказуемо в А. ф.). Так как ω-вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость А. ф. Применение второй теоремы Гёделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в А. ф. не может быть доказана средствами А. ф. ; тем не менее это может быть доказано в А. ф. при любом фиксированном N для любого вывода с индукциями сложности ≤ N. Переход к ω-выводам позволяет устанавливать многие метаматематич. теоремы о системе А. ф., в частности полноту относительно формул из ∑1 и ординальную характеристику доказуемо рекурсивных функций. Лит. : [1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Нilbеrt D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1-2, В., 1968-70; [3] Hовиков П. С., Элементы математической логики, 2 изд., М., 1973; [4] Kreisel G., «J. Symbolic Logic», 1968, v. 33, № 3, p. 321 - 88; [5] Гёдель К., в сб. : Математическая теория логического вывода, М., 1967, с. 299 - 310. Г. Е. Минц. Источники:
|
|
|||
© MATHEMLIB.RU, 2001-2021
При копировании материалов проекта обязательно ставить ссылку на страницу источник: http://mathemlib.ru/ 'Математическая библиотека' |