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

арифметическое исчисление,- логико-математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы [img: http://localhost:8080/file/010131-55.jpg] (прибавление 1) и логич. связки. Термы строятся из константы 0 п переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида [img: http://localhost:8080/file/010131-56.jpg] Атомарные формулы - это равенства термов; остальные формулы строятся из атомарных с помощью логич. связок [img: http://localhost:8080/file/010131-57.jpg] Формулы в языке А. ф. наз. арифметическими формулами. Постулатами А. ф. являются постулаты предикатов исчисления (классического пли интуиционистского в зависимости от того, какая А. ф. рассматривается),.аксиомы Пеано [img: http://localhost:8080/file/010131-58.jpg] я схема аксиом индукции [img: http://localhost:8080/file/010131-59.jpg] где А - произвольная формула, наз. индукционной формулой. Средства А. ф. оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е гг.), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, к-рая не была бы выводима в А. ф. Запись и доказательство таких теорем в А. ф. требует выявления ее выразительных возможностей. Особенно существенна выразимость в А. ф. многих теоретико-числовых функций. В частности, в А. ф. можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этой оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство [img: http://localhost:8080/file/010131-60.jpg] выражается формулой, [img: http://localhost:8080/file/010131-61.jpg] где [img: http://localhost:8080/file/010131-62.jpg] - формулы, изображающие графики функций [img: http://localhost:8080/file/010131-63.jpg], соответственно. В А. ф. можно формулировать суждения о конечных множествах. Более того, классич. А. ф. эквивалентна аксиоматической теории множеств Цермело - Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой. Дедуктивная сила системы А. ф. характеризуется ординалом [img: http://localhost:8080/file/010131-64.jpg] (наименьшее решение уравнения [img: http://localhost:8080/file/010131-65.jpg]): в А. ф. выводима схема трансфинитной индук ции до любого ординала [img: http://localhost:8080/file/010131-66.jpg], но не выводима схема индукции до [img: http://localhost:8080/file/010131-67.jpg]. Класс доказуемо рекурсивных функций системы А. ф. (т. е. частично рекурсивных функций, общерекурсивность к-рых может быть установлена средствами А. ф.) совпадает с классом ординально рекурсивных функций с ординалами [img: http://localhost:8080/file/010131-68.jpg]. Это позволяет погружать в А. ф. нек-рые ее расширения, напр. А. ф. с символами для всех примитивно рекурсивных функций и соответствующими дополнительными постулатами. А. ф. удовлетворяет условиям обеих Гёделя теорем о неполноте. В частности, имеются такие полиномы [img: http://localhost:8080/file/010131-69.jpg] от нескольких переменных, что формула [img: http://localhost:8080/file/010131-70.jpg] невыводима, хотя и выражает истинное утверждение, а именно непротиворечивость системы А. ф. При исследовании структуры А. ф. (в частности, вопросов непротиворечивости) используется ее формулировка без кванторов, но с гильбертовским e-символом. При построении формул этой системы не допускается употребление кванторов, но разрешается использование термов вида [img: http://localhost:8080/file/010131-71.jpg] (нек-рое х, удовлетворяющее условию А, если такие хсуществуют, и 0 в противном случае). Постулаты [img: http://localhost:8080/file/010131-72.jpg] -системы - это постулаты исчисления высказываний, правила для равенства, правило подстановки вместо свободной числовой переменной, аксиомы для функций [img: http://localhost:8080/file/010131-73.jpg] (вычитание 1 из положительных чисел) и следующие [img: http://localhost:8080/file/010131-74.jpg] -аксиомы: [img: http://localhost:8080/file/010131-75.jpg] Кванторы вводятся как сокращения: [img: http://localhost:8080/file/010131-76.jpg] аксиома индукции оказывается выводимой. Формулы А. ф., содержащие свободные переменные, задают теоретико-числовые предикаты. Формулы, не содержащие свободных переменных (замкнутые формулы), выражают суждения, fe-местный предикат [img: http://localhost:8080/file/010131-77.jpg] от натуральных чисел наз. арифметически м, если найдется такая арифметич. формула [img: http://localhost:8080/file/010131-78.jpg] [img: http://localhost:8080/file/010131-79.jpg] что для любых натуральных чисел [img: http://localhost:8080/file/010131-80.jpg] имеет место [img: http://localhost:8080/file/010131-81.jpg] Это определяет классификацию арифметич. предикатов по типу префикса в предваренной форме соответствующей формулы. Класс [img: http://localhost:8080/file/010131-82.jpg] (класс [img: http://localhost:8080/file/010131-83.jpg]) состоит из предикатов [img: http://localhost:8080/file/010131-84.jpg], изобразимых формулой вида [img: http://localhost:8080/file/010131-85.jpg] где [img: http://localhost:8080/file/010131-86.jpg] - примитивно рекурсивная функция, [img: http://localhost:8080/file/010131-87.jpg] есть [img: http://localhost:8080/file/010131-88.jpg] (соответственно [img: http://localhost:8080/file/010131-89.jpg].) и [img: http://localhost:8080/file/010131-90.jpg] - чередующиеся кванторы (т. е. [img: http://localhost:8080/file/010131-91.jpg] есть [img: http://localhost:8080/file/010131-92.jpg], где [img: http://localhost:8080/file/010131-93.jpg] есть [img: http://localhost:8080/file/010131-94.jpg], а [img: http://localhost:8080/file/010131-95.jpg] есть [img: http://localhost:8080/file/010131-96.jpg]). Каждый из этих классов содержит универсальный предикат, т. е. такой предикат [img: http://localhost:8080/file/010131-97.jpg], что для всякого одноместного предиката Риз того же класса имеется число [img: http://localhost:8080/file/010131-98.jpg], для к-рого верно [img: http://localhost:8080/file/010131-99.jpg]). Многоместные предикаты сводятся к одноместным с помощью функций, нумерующих системы натуральных чисел. При каждом [img: http://localhost:8080/file/010131-100.jpg] справедливо неравенство [img: http://localhost:8080/file/010131-101.jpg] и класс с меньшим индексом есть собственная часть любого класса с большим индексом. Классификация предикатов порождает классификацию арифметич. функций на основе классификации соответствующих графиков. Не все теоретико-числовые предикаты арифметические: примером неарифметич. предиката является такой предикат [img: http://localhost:8080/file/010131-102.jpg], что для любой замкнутой арифметич. формулы Аимеет место [img: http://localhost:8080/file/010131-103.jpg] - номер формулы Ав нек-рой фиксированной нумерации, удовлетворяющей естественным условиям. Предикат Тиграет существенную роль в исследованиях структуры А. ф., в частности вопроса о независимости ее аксиом. Присоединение к А. ф. символа [img: http://localhost:8080/file/010131-104.jpg] с аксиомами типа [img: http://localhost:8080/file/010131-105.jpg], выражающими его перестановочность с логич. связками, позволяет доказать непротиворечивость А. ф. Та же конструкция (но уже внутри А. ф.) проходит для подсистемы [img: http://localhost:8080/file/010131-106.jpg] системы А. ф., в к-рой схема индукции ограничена условием: индукционная формула имеет сложность [img: http://localhost:8080/file/010131-107.jpg], т. е. принадлежит [img: http://localhost:8080/file/010131-108.jpg] Роль Тздесь успешно исполняет, напр., универсальный предикат для [img: http://localhost:8080/file/010131-109.jpg], и соответствующее доказательство проводится в системе [img: http://localhost:8080/file/010131-110.jpg] В силу второй теоремы Гёделя о неполноте отсюда следует, что [img: http://localhost:8080/file/010131-111.jpg] сильнее [img: http://localhost:8080/file/010131-112.jpg], так что А. ф. не совпадает ни с одной из систем [img: http://localhost:8080/file/010131-113.jpg] и схему индукции нельзя заменить никаким конечным множеством аксиом. А. ф. оказывается, полной относительно формул из класса [img: http://localhost:8080/file/010131-114.jpg]: замкнутая формула из этого класса выводима в А. ф. тогда и только тогда, когда она истинна. Так как класс [img: http://localhost:8080/file/010131-115.jpg] содержит алгорифмически неразрешимый предикат, отсюда следует, что проблема выводимости в А. ф. алгорифмически неразрешима. При задании А. ф. в виде Генцена формальной системы обычного типа сечение оказывается неустранимым. Устранение сечения становится возможным, если заменить схему индукции правилом бесконечной индукции.([img: http://localhost:8080/file/010131-116.jpg] -правило): [img: http://localhost:8080/file/010131-117.jpg] На этом пути было получено одно из первых доказательств непротиворечивости А. ф. При фактическом построении системы с [img: http://localhost:8080/file/010131-118.jpg] -правилом основным оказывается предикат "число еесть номер общерекурсивной функции, описывающей вывод длины [img: http://localhost:8080/file/010131-119.jpg] с [img: http://localhost:8080/file/010131-120.jpg] -правилом ([img: http://localhost:8080/file/010131-121.jpg] -вывод)". Этот предикат принадлежит классу [img: http://localhost:8080/file/010131-122.jpg],и получающаяся система оказывается не формальной, а лишь полуформальной. Каждому выводу формулы Ав А. ф. удается сопоставить такое число е, что суждение "е есть [img: http://localhost:8080/file/010131-123.jpg] -вывод формулы Абез сечения" истинно (и даже доказуемо в А. ф.). Так как [img: http://localhost:8080/file/010131-124.jpg] -вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость А. ф. Применение второй теоремы Гёделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в А. ф. не может быть доказана средствами А. ф.; тем не менее это может быть доказано в А. ф. при любом фиксированном [img: http://localhost:8080/file/010131-125.jpg] для любого вывода с индукциями сложности [img: http://localhost:8080/file/010131-126.jpg]. Переход к [img: http://localhost:8080/file/010131-127.jpg] -выводам позволяет устанавливать многие метаматематич. теоремы о системе А. ф., в частности полноту относительно формул из [img: http://localhost:8080/file/010131-128.jpg] и ординальную характеристику доказуемо рекурсивных функций.