арифметическое исчисление,- логико-математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы (прибавление 1) и логич. связки. Термы строятся из константы 0 п переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида Атомарные формулы - это равенства термов; остальные формулы строятся из атомарных с помощью логич. связок Формулы в языке А. ф. наз. арифметическими формулами. Постулатами А. ф. являются постулаты предикатов исчисления (классического пли интуиционистского в зависимости от того, какая А. ф. рассматривается), .аксиомы Пеано
я схема аксиом индукции
где А - произвольная формула, наз. индукционной формулой.
Средства А. ф. оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е гг.), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, к-рая не была бы выводима в А. ф. Запись и доказательство таких теорем в А. ф. требует выявления ее выразительных возможностей. Особенно существенна выразимость в А. ф. многих теоретико-числовых функций. В частности, в А. ф. можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этой оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство выражается формулой ,
где - формулы, изображающие графики функций , соответственно. В А. ф. можно формулировать суждения о конечных множествах. Более того, классич. А. ф. эквивалентна аксиоматической теории множеств Цермело - Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.
Дедуктивная сила системы А. ф. характеризуется ординалом (наименьшее решение уравнения ): в А. ф. выводима схема трансфинитной индук ции до любого ординала , но не выводима схема индукции до . Класс доказуемо рекурсивных функций системы А. ф. (т. е. частично рекурсивных функций, общерекурсивность к-рых может быть установлена средствами А. ф.) совпадает с классом ординально рекурсивных функций с ординалами . Это позволяет погружать в А. ф. нек-рые ее расширения, напр. А. ф. с символами для всех примитивно рекурсивных функций и соответствующими дополнительными постулатами. А. ф. удовлетворяет условиям обеих Гёделя теорем о неполноте. В частности, имеются такие полиномы от нескольких переменных, что формула невыводима, хотя и выражает истинное утверждение, а именно непротиворечивость системы А. ф.
При исследовании структуры А. ф. (в частности, вопросов непротиворечивости) используется ее форм
…
Перейти к полному виду статьи
Свернуть