АРИФМЕТИКА ФОРМАЛЬНАЯ это:

АРИФМЕТИКА ФОРМАЛЬНАЯ

арифметическое исчисление,- логико-математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы (прибавление 1) и логич. связки. Термы строятся из константы 0 п переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида Атомарные формулы - это равенства термов; остальные формулы строятся из атомарных с помощью логич. связок Формулы в языке А. ф. наз. арифметическими формулами. Постулатами А. ф. являются постулаты предикатов исчисления (классического пли интуиционистского в зависимости от того, какая А. ф. рассматривается), .аксиомы Пеано


я схема аксиом индукции


где А - произвольная формула, наз. индукционной формулой.

Средства А. ф. оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е гг.), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, к-рая не была бы выводима в А. ф. Запись и доказательство таких теорем в А. ф. требует выявления ее выразительных возможностей. Особенно существенна выразимость в А. ф. многих теоретико-числовых функций. В частности, в А. ф. можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этой оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство выражается формулой ,


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

Дедуктивная сила системы А. ф. характеризуется ординалом (наименьшее решение уравнения ): в А. ф. выводима схема трансфинитной индук ции до любого ординала , но не выводима схема индукции до . Класс доказуемо рекурсивных функций системы А. ф. (т. е. частично рекурсивных функций, общерекурсивность к-рых может быть установлена средствами А. ф.) совпадает с классом ординально рекурсивных функций с ординалами . Это позволяет погружать в А. ф. нек-рые ее расширения, напр. А. ф. с символами для всех примитивно рекурсивных функций и соответствующими дополнительными постулатами. А. ф. удовлетворяет условиям обеих Гёделя теорем о неполноте. В частности, имеются такие полиномы от нескольких переменных, что формула невыводима, хотя и выражает истинное утверждение, а именно непротиворечивость системы А. ф.

При исследовании структуры А. ф. (в частности, вопросов непротиворечивости) используется ее формулировка без кванторов, но с гильбертовским e-символом. При построении формул этой системы не допускается употребление кванторов, но разрешается использование термов вида (нек-рое х, удовлетворяющее условию А, если такие хсуществуют, и 0 в противном случае). Постулаты -системы - это постулаты исчисления высказываний, правила для равенства, правило подстановки вместо свободной числовой переменной, аксиомы для функций (вычитание 1 из положительных чисел) и следующие -аксиомы:


Кванторы вводятся как сокращения:


аксиома индукции оказывается выводимой.

Формулы А. ф., содержащие свободные переменные, задают теоретико-числовые предикаты. Формулы, не содержащие свободных переменных (замкнутые формулы), выражают суждения, fe-местный предикат от натуральных чисел наз. арифметически м, если найдется такая арифметич. формула что для любых натуральных чисел имеет место


Это определяет классификацию арифметич. предикатов по типу префикса в предваренной форме соответствующей формулы. Класс (класс ) состоит из предикатов , изобразимых формулой вида


где - примитивно рекурсивная функция, есть (соответственно .) и - чередующиеся кванторы (т. е. есть , где есть , а есть ). Каждый из этих классов содержит универсальный предикат, т. е. такой предикат , что для всякого одноместного предиката Риз того же класса имеется число , для к-рого верно ). Многоместные предикаты сводятся к одноместным с помощью функций, нумерующих системы натуральных чисел. При каждом справедливо неравенство и класс с меньшим индексом есть собственная часть любого класса с большим индексом. Классификация предикатов порождает классификацию арифметич. функций на основе классификации соответствующих графиков. Не все теоретико-числовые предикаты арифметические: примером неарифметич. предиката является такой предикат , что для любой замкнутой арифметич. формулы Аимеет место - номер формулы Ав нек-рой фиксированной нумерации, удовлетворяющей естественным условиям.

Предикат Тиграет существенную роль в исследованиях структуры А. ф., в частности вопроса о независимости ее аксиом. Присоединение к А. ф. символа с аксиомами типа , выражающими его перестановочность с логич. связками, позволяет доказать непротиворечивость А. ф. Та же конструкция (но уже внутри А. ф.) проходит для подсистемы системы А. ф., в к-рой схема индукции ограничена условием: индукционная формула имеет сложность , т. е. принадлежит Роль Тздесь успешно исполняет, напр., универсальный предикат для , и соответствующее доказательство проводится в системе В силу второй теоремы Гёделя о неполноте отсюда следует, что сильнее , так что А. ф. не совпадает ни с одной из систем и схему индукции нельзя заменить никаким конечным множеством аксиом. А. ф. оказывается, полной относительно формул из класса : замкнутая формула из этого класса выводима в А. ф. тогда и только тогда, когда она истинна. Так как класс содержит алгорифмически неразрешимый предикат, отсюда следует, что проблема выводимости в А. ф. алгорифмически неразрешима.

При задании А. ф. в виде Генцена формальной системы обычного типа сечение оказывается неустранимым. Устранение сечения становится возможным, если заменить схему индукции правилом бесконечной индукции.( -правило):


На этом пути было получено одно из первых доказательств непротиворечивости А. ф. При фактическом построении системы с -правилом основным оказывается предикат "число еесть номер общерекурсивной функции, описывающей вывод длины с -правилом ( -вывод)". Этот предикат принадлежит классу ,и получающаяся система оказывается не формальной, а лишь полуформальной. Каждому выводу формулы Ав А. ф. удается сопоставить такое число е, что суждение "е есть -вывод формулы Абез сечения" истинно (и даже доказуемо в А. ф.). Так как -вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость А. ф. Применение второй теоремы Гёделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в А. ф. не может быть доказана средствами А. ф.; тем не менее это может быть доказано в А. ф. при любом фиксированном для любого вывода с индукциями сложности . Переход к -выводам позволяет устанавливать многие метаматематич. теоремы о системе А. ф., в частности полноту относительно формул из и ординальную характеристику доказуемо рекурсивных функций.

Лит.:[1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Нi1bеrt D., Веrnауs P., Grundlagen der Mathematik, 2 Aufl., Bd 1-2, В., 1968-70; [3] Новиков П. С., Элементы математической логики, 2 изд., М., 1973; [4] Kreisel G., "J. Symbolic Logic", 1968, v. 33, №3, p. 321-88; [5] Гёдель К., в сб.: Математическая теория логического вывода, М., 1967, с. 299-310. Г. Е. Минц.


Математическая энциклопедия. — М.: Советская энциклопедия. . 1977—1985.

Смотреть что такое "АРИФМЕТИКА ФОРМАЛЬНАЯ" в других словарях:

  • Арифметика — Ганс Себальд Бехам. Арифметика. XVI век Арифметика (др. греч. ἀ …   Википедия

  • ФОРМАЛЬНАЯ ФИЛОСОФИЯ — существующая в течение тысячелетий тенденция философии к фундаментальному обобщению понятий и законов, присущих формальным аспектам частных философских наук: формальной логики, формальной онтологии, формальной этики (см. в наст. словаре ст. с… …   Современный философский словарь

  • Формальная система — (формальная теория, аксиоматическая теория)  результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причем все условия, регулирующие употребление этих слов в теории, явно высказаны… …   Википедия

  • Формальная логика — Формальная логика  конструирование и исследование правил преобразования высказываний, сохраняющих их истинностное значение безотносительно к содержанию входящих в эти высказывания понятий. Формальная логика, в отличие от неформальной,… …   Википедия

  • Формальная арифметика — Аксиомы Пеано одна из систем аксиом для натуральных чисел. Аксиомы Пеано позволили формализовать арифметику. После введения аксиом стали возможны доказательства многих свойств натуральных и целых чисел, а также использование целых чисел для… …   Википедия

  • Формальная арифметика —         формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Ф. а. содержит константу 0, числовые переменные, символ равенства, функциональные символы +, •, (прибавление 1) и логические связки (см …   Большая советская энциклопедия

  • ЭЛЕМЕНТАРНАЯ АРИФМЕТИКА — тоже, что арифметика формальная …   Математическая энциклопедия

  • ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА — Гейтипга исчисление, название трех формальных систем конструктивной логики, предложенных А. Рейтингом [1]. Первая из них гейтинговское, или интуиционистское, исчисление высказываний формализация принципов конструктивной логики высказываний;… …   Математическая энциклопедия

  • ЛОГИКО-МАТЕМАТИЧЕСКИЕ ИСЧИСЛЕНИЯ — прикладные исчисления, формализации математич. теорий. Л. м. и. задается своим языком и перечнем постулатов (эти элементы образуют синтаксис).и в большинстве случаев снабжается семантикой. Существенными чертами, отличающими Л. м. и. от аксиоматич …   Математическая энциклопедия

  • БЕСКОНЕЧНАЯ ИНДУКЦИЯ — правило Карнапа, w правило, неэлементарное вывода правило с бесконечным числом посылок. Точнее, пусть в нек ром логико математич. языке переменная x рассматривается как пробегающая натуральные числа и формула этого языка. Если доказана… …   Математическая энциклопедия

Книги



Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»