Схемы рефлексии в формальной арифметике тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Российская Академия Наук Математический институт им, В.А. Стсклова

РГ6 од

На правах рукописи

п , , . УДК 510.64

БЕКЛЕМИШЕВ Лев Дмитриевич

Схемы рефлексии в формальной арифметике

01.01.06 — математическая логика, алгебра и теория чисел

Автореферат

диссертации на соискание учёной степени доктора физико-математических наук

Москва 1998

Работа выполнена в математическом институте им. В.А. Стек-лова Российской Академии Наук

Официальные оппоненты:

чл.-корр. РАН, доктор физико-математических наук Матиясевич Юрий Владимирович;

доктор физико-математических наук, профессор Семёнов Алексей Львович;

доктор физико-математических наук, профессор Успенский Владимир Андреевич.

Ведущая организация — Институт Математики Сибирского отделения Российской Академии Наук.

Защита состоится 24" сеитлЯрл Ю98 г. в на за-

седании специализированного совета Д.002.38.02 по защите диссертаций на соискание учёной степени доктора физико-математических наук при Математическом институте им. В.А. Стеклова Российской Академии Наук по адресу: Москва, ул. Губкина, д. 8, 4 этаж, конференц-зал.

С диссертацией можно ознакомиться в библиотеке МИ РАН.

Автореферат разослан " " Ш-ОНЛ, 1998 г.

Учёный секретарь

специализированного совета Д.002.38.02 доктор физ.-мат. наук

И.Г. Лысёнок

Общая характеристика работы

Настоящая диссертация посвящена исследованию схем рефлексии для фрагментов формальной арифметики Пеано и применению этих схем к вопросам сравнения и классификации арифметических теорий.

Схемы рефлексии возникли в математической логике вскоре после доказательства Гёделем его фундаментальных теорем о неполноте [5, 12]. Для данной теории Т эти схемы представляют собой варианты формализации утверждения "если формула <р доказуема в Т, то уз истинна". Они дают примеры истинных, но недоказуемых утверждений, обобщающих первый известный пример такого рода — гёделевскую формулу непротиворечивости теории Т.

Тьюринг [15] ввёл в рассмотрение прогрессии теорий, получаемые итерированием процесса пополнения теории схемой рефлексии, и предложил возможный подход к ординальной классификации арифметических теорий на основе таких прогрессий. В дальнейшем этот подход был проанализирован и развит Феферманом в [4]. Построенные Тьюрингом и Феферманом примеры показали, что на пути подобной классификации встают существенные трудности, связанные, в частности, с проблемой естественного представления ординалов в арифметике.

Крайзель и Леви в [8] показали, что схемы рефлексии являются удобным инструментом для изучения вопросов сложности аксиоматизации формальных теорий. Ими была доказана дедуктивная эквивалентность так называемой равномерной схемы рефлексии для примитивно рекурсивной арифметики и полной схемы индукции, откуда, в частности, вытекает невозможность задания арифметики Пеано множеством аксиом ограниченной кванторной сложности. В этой же работе была доказана эквивалентность схемы трансфинитной индукции до ординала ео и равномерной схемы рефлексии для арифметики Пеано. В дальнейшем были установлены тесные связи между схемами рефлексии и другими истинными невыводимыми утверждениями, включая известные комбинаторные принципы Париса-Харрингтона.

В диссертации получено решение ряда важных вопросов о схемах рефлексии, что позволило сделать аппарат этих схем уни-

нереальным инструментом анализа и ординальной классификации арифметических теорий. Описание исследуемой теории в терминах схем рефлексии позволяет использовать свойства таких схем для получения разнообразных результатов о её строении и соотношении с другими теориями, в частности, результатов о независимости, аксиоматизируемости, (частичной) консервативности и харак-теризации классов доказуемо тотальных вычислимых функций.

Одно из наиболее активно развивающихся в последнее время направлений математической логики связано с изучением подсистем, или фрагментов, формальной арифметики Пеано РА. Интерес к этим вопросам был вызван прежде всего обнаружившимися связями с теорией сложности вычислений и попытками формализации понятия эффективного (feasible) доказательства. Монография [6] содержит накопленные в этой области к 1993 году основные результаты и обширную библиографию.

В настоящей работе подход, основанный на схемах рефлексии, применён к исследованию иерархий фрагментов РА. Изучены взаимосвязи схем рефлексии и основных форм индукции ограниченной арифметической сложности. Кале следствие получен ряд новых результатов, относящихся к иерархиям фрагментов РА, определяемых правилом индукции и схемой индукции без параметров ограниченной арифметической сложности.

К основным результатам диссертации можно отнести следующие.

1) Точная характеризация правил индукции ограниченной арифметической сложности в терминах схем рефлексии.

Существенной чертой полученной характеризации является её инвариантность, то есть независимость от выбора базисной теории достаточно широкого класса, над которой эти правила рассматриваются. В частности, это позволяет получить естественную аксиоматизацию с помощью схем аксиом замыканий произвольных достаточно сильных арифметических теорий относительно правил индукции.

2) Точная характеризация схем беспараметрической индукции ограниченной арифметической сложности в терминах схем рефлексии.

Возникающие при этом так называемые локальные схемы рефлексии в простейшем случае были известны еще со времени ра-

боты Тьюринга. Однако, их связь с фрагментами РА или другими формальными системами, определяемыми независимым образом, ранее не была известна.

3) Детально изучено строение иерархии локальных схем рефлексии над произвольной достаточно сильной арифметической теорией. В частности, получены оптимальные в смысле арифметической сложности результаты о консервативности для иерархии схем локальной рефлексии, а также результаты о связи равномерной и локальной схем рефлексии.

Вместе с результатами 2) это позволяет дать ответ на ряд вопросов о схемах беспараметрической индукции в арифметике, а также получить новое конструктивное доказательство некоторых результатов об этих схемах, для которых ранее было известно лишь неконструктивное теоретико-модельное доказательство.

4) Получен ответ на стоявший в области фрагментов арифметики вопрос о доказуемо тотальных вычислимых функциях теории, аксиоматизируемой схемой индукции для Щ-формул без параметров. Показано, что класс таких функций совпадает с примитивно рекурсивными функциями. Расширение этой теории схемой индукции для Х^-формул с параметрами имеет более широкий класс доказуемо тотальных вычислимых функций, совпадающий с классом дважды рекурсивных функций в смысле Р. Петер. Эти результаты, по-видимому, являются наиболее интересными приложениеми результатов 2) и 3).

5) Построение иерархий итерированных схем рефлексии с естественными свойствами, позволяющее обобщить на такие схемы результаты о консервативности из 3). В частности, показано, что для таких иерархий а раз итерированная схема локальной рефлексии, где а — конструктивный ординал, доказывает те же П г -предложения , что и ша раз итерированное утверждение о непротиворечивости.

В отличие от традиционного подхода, связанного с ординальными границами доказуемости трансфинитной индукции в формальных теориях (см., например, [11]), изложенный в диссертации подход дает более тонкую классификацию, позволяющую различить теории уже на уровне их Последствий. На основе этого подхода получено обобщение на более широкий класс теорий теоремы Шмерля [13] о тонкой структуре иерархии итерированных

схем равномерной рефлексии над примитивно рекурсивной арифметикой и вычислены ординалы основных фрагментов РА. Также получены обобщения результатов 4) на схемы беспараметрической индукции арифметической сложности П„ для произвольного п > 2.

Применяемые в диссертации методы можно разделить на три группы. К первой группе относятся широко известные методы структурной теории доказательств, используемые при получении харак-теризаций 1) и 2), такие как техника устранения сечения и сколе-мизация. Отметим, что применяемый нами для анализа правила Х„-индукции вариант техники сколемизации является усовершенствованием техники "операторных теорий" работы [14].

Ко второй группе относится нетрадиционная техника, используемая для анализа схем локальной рефлексии. Ключевую роль здесь играет логика доказуемости и связанные с ней модели Крип-ке. Первые применения подобной техники к анализу схем рефлексии содержатся в работах [3, 1].

Наконец, подход, предлагаемый нами для построения иерархий итерированных схем рефлексии, использует некоторые идеи работ [4,13]. Введенное в диссертации понятие гладкой прогрессии теорий позволяет существенно упростить построение итерированных схем рефлексии, делая ненужным использование языка теории рекурсии и его формализации в арифметике, а также использование так называемых фундаментальных последовательностей ординальных обозначений. При этом достигается большая общность результатов и, в некотором смысле, каноничность определяемых посредством этой конструкции схем. Понятие гладкой прогрессии возникло при изучении полимодальных логик доказуемости для иерархий итерированных схем рефлексии в работах [16, 18].

Диссертация имеет теоретический характер. Ее результаты могут применяться в исследованиях в области математической логики и теории алгоритмов.

Все результаты диссертации являются новыми. Они докладывались на семинарах механико-математического факультета МГУ им. М.В. Ломоносова, университетов г. Амстердама, г. Утрехта (Нидерланды), г. Вены (Австрия), г. Мюнстера (ФРГ), университета Париж VII (Франция), и были изложены в приглашенном докладе на Обществе Курта Гёделя (Вена, 1996 г.). Они также были доложены на ряде международных конференций, в том чис-

ле: ежегодная конференция ассоциации символической логики Logic Colloquium (Хайфа, 1995 г.); Конгресс немецкого математического общества (Иена, 1996 г.); Логические основания информатики LFCS'97 (Ярославль, 1997 г.); 14th Weak arithmetic days (Санкт-Петербург, 1997 г.); Мальцевские чтения (Новосибирск, 1994 г., 1997 г.). Результаты диссертации вошли в курсы лекций, прочитанных автором на механико-математическом факультете МГУ в 1995-97 гг. и 9-й европейской летней школе по языку, логике и информатике ESSLLI'97 (Экс-ан-Прованс, 1997 г.).

Основные результаты диссертации опубликованы в работах автора [16] - [24].

Диссертация насчитывает 149 страниц, список литературы содержит 54 наименования.

Содержание диссертации

Диссертация состоит из введения и 7 разделов, разбитых на параграфы. В разделе 1 вводятся основные понятия диссертации и излагается необходимая для дальнейшего техника. Параграфы 1.1, 1.2 и 1.3 посвящены, соответственно, введению в элементарную арифметику, арифметизацию синтаксиса формальных теорий и логику доказуемости. Приведем некоторые определения.

Мы рассматриваем теории первого порядка в арифметическом языке, содержащем явно символы для функций 5, +, •, 2х, предикатов = и < и константу 0. Элементарные формулы — это формулы, все вхождения кванторов в которые имеют вид Vz (х < t <р{х)) или Эх (х < t А <р(х)) для некоторого терма t, не зависящего от х. £„-формулы получаются из элементарных формул добавлением префикса из п чередующихся блоков однотипных кванторов, начинающегося с 3. Пп-формулы определяются двойственным образом. В(Е„) означает множество булевых комбинаций Е„-формул.

Элементарная арифметика ЕА задается конечным списком стандартных аксиом для базисных функций и предикатов арифметического языка и схемой индукции для элементарных формул. Ниже будет также рассматриваться теория ЕА+, представляющая собой расширение ЕА Пг-аксиомой, выражающей определенность функций 2* при любых значениях аргументов п и х, где 2g = х и 2®+1 = 22". ЕА и ЕА+ являются достаточно слабыми фрагментами арифметики Пеано и играют роль базисных минимальных теорий.

Пусть Т — перечислимая теория в арифметическом языке, а □т(зт) означает естественную Si-формулу, выражающую предикат "ж есть гёделев номер выводимой в Т формулы". Мы используем следующие стандартные обозначения. г<р~> означает гёделев номер формулы íp. Замкнутые термы вида S(S{... 5(0)...)) (п раз), где S — функция следования, называются нумералами и обозначаются п. Если ц> — формула, мы пишем От'-р вместо □x(rV~1)- Символ 1 означает логическую связку "ложь", a Con (Г) есть формула непротиворечивости теории У, определяемая как ->Oy-L Выражение ra(xi,..., i*)"1 означает естественный определимый терм для элементарной функции, сопоставляющей последовательности ni,.,.,nf¡ гёделев номер rcr(ñi,... результата подстановки нумералов щ.. вместо переменных xi,. ..,Xk в формулу а. Мы также пишем Üxcíii,... ,i:n) вместо Clx(rcr(á;i, • • •, in)"1)-

Результаты раздела 2 можно отнести к общей теории схем рефлексии. В §2.1 вводятся основные формы схем рефлексии. Локальной схемой рефлексии Rfn(jT) называется схема От<Р —> <р, для всех арифметических предложений ip. Равномерная схема рефлексии RFN (Т) определяется как

Vsi...Va;n (□Tv?(¿1,.. .,¿n) <p(xi,.. .,£„)),

для всех арифметических формул f{xi,..., хп). Схемы частичной рефлексии получаются из локальной и равномерной схем наложением ограничения, состоящего в том, что формула <р пробегает лишь некоторый подкласс Г класса всех арифметических предложений (формул). Такие схемы обозначаются Rfnr(r) и RFNr(T), соответственно, а в качестве Г обычно рассматривается один из классов £п или П„ арифметической иерархии. Важная роль равномерной и локальной схем рефлексии объясняется тем, что большинство других форм рефлексии оказывается эквивалентным одной из этих двух.

В §2.2 излагаются уточнённые версии известных теорем Край-золя и Леви о неограниченности, являющихся основой для применения схем рефлексии к вопросам сложности аксиоматизации теорий. Мы сопровождаем их усовершенствованным доказательством, применимым, как это требуется в дальнейшем, к достаточно слабым фрагментам РА. В §2.3 детально исследуются иерархии схем локальной и равномерной рефлексии ограниченной арифметической

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

Теорема 1. Для любого п > 1

(г) в теориях Т + и Т + РМт1п„(Т) доказуемы одни и те

же Пп-предложения;

(И) в теориях Т + Шп(Т) и Т + (Т) доказуемы одни и те же Еп-предложения;

(Ш) в Т + 1^п(!Г) иТ + (Т) доказуемы одни и те же В(£ 1)-предложения.

Результаты первых двух пунктов этой теоремы являются оптимальными в том смысле, что консервативность для двойственных классов арифметических предложений уже не имеет места. Результат пункта (111) является оптимальным в том смысле, что для рассматриваемых теорий не имеет места консервативность ни для класса П2, ни для класса £2-предложений. Для каждого из этих трёх случаев ранее была известна консервативность лишь для класса Щ-предложений [2].

Разделы 3-5 диссертации посвящены применению схем рефлексии для анализа фрагментов арифметики, в частности, правил индукции и схем беспараметрической индукции ограниченной арифметической сложности.

В разделе 3 вводятся основные формы индукции в арифметике — схема аксиом 1А и правило 1Я — и анализируются сравнительно простые случаи схем индукции с параметрами и правила индукции для Пп-формул.

IA: ip(0) Л Vx (<p(x) ip(x + 1)) Vxip(x) Vxip(x)

Схема и правило индукции для формул 95, пробегающих некоторый подкласс Г класса арифметических формул, обозначается Г-IA и Г-IR, соответственно. /Е„ означает теорию, аксиоматизированную над ЕА схемой En-IA; /Е" аксиоматизируется над ЕА правилом S„-IR; теория /S" аксиоматизируется схемой IA для Еп-формул (р(х) с единственной свободной переменной х. Л1п, /П^ и определяются аналогично.

В §3.2 воодится необходимая техника, связанная с секвенциальным исчислением Тейта. В §3.3 на основе теоремы об устранении сечения доказывается эквивалентность теорий /£„, Ш„ и ЕА + RFMsn+l (ЕА) при n > 1 и извлекаются известные следствия, касающиеся оптимальной арифметической сложности аксиоматизации теорий 1Т,П (см. [9]). Основная лемма из приводимого в диссертации доказательства этой теоремы была получена в [22] для характеризации правила IIn-IR и также используется в §3.5.

В §3.4 с общей точки зрения рассматриваются правила вывода в арифметике. Мы называем правилам произвольное множество примеров, то есть выражений вида

где <рх,..., (рп и ф — арифметические формулы. Выводы с использованием правил определяются стандартным образом; Т + R означает замыкание теории Т относительно правила R и правил вывода логики первого порядка modus ponens и обобщения. [Т, R] означает замыкание Т относительно однократного применения правила R, то есть теорию, аксиоматизированную над Т всеми формулами ф такими, что для некоторых формул щ ,ipn, выводимых в Т, есть пример R.

Правило Äi называется выводимым из если для любой теории Т, содержащей ЕА, Т + J2i С Т + Дг- Правило Ri сводимо к R2, если для любой теории Т, содержащей ЕА, [T,iZi] С [Т, /¿2]. Ri и R2 конгруэнтны, если они взаимно сводимы (обозначается Ri Для теории U, содержащей ЕА, мы говорим, что Ri и Дг

конгруэнтны по модулю II, если для любого расширения Т теории и, [Г, Лх] = [Т, Дг]- Правило II конгруэнтно множеству аксиом А, если Д конгруэнтно А как правилу с пустой посылкой, то есть если для любой теории Т, содержащей ЕА, [Г, Щ = Т + А.

В §3.4 отношения сводимости и конгруэнтности правил вывода в арифметике исследуются для наиболее естественных форм правила индукции. Показывается, что наиболее естественные формы правила индукции ограниченной арифметической сложности являются конгруэнтными одной из трех основных: правилу £П-1Р?, правилу ПП-1Р или схеме ЕП-1А.

В §3.5 мы даем инвариантную характеризацию правила ПП-1И в терминах схем рефлексии. Для данной теории Т вводится правило ■метпарефлексии

ККпАТ): *

ЮН^Т + уУ

Ит-ЯРп„(Т) обозначает это же правило с ограничением </? 6 Пт. Основным результатом является

Теорема 2. ({) ПП-1И &! П„+1-ЯРПп(ЕА), для п > 1;

(И) ПНИ й П2-РНП1(ЕА) по модулю ЕА+.

Эта теорема позволяет получить ряд интересных следствий об аксиоматизации замыканий теорий относительно правила ПгГ!Н.

Следствие 3.18. Для конечных^-аксиоматизированных теорий Т, содержащих ЕА+,

Т + Пх-т = Т + Соп(Г) + Соп(Т + Соп(Т)) + ...

Аналогичный результат имеет место и для правила Пп-1(} при п > 1. Обозначим через (Г)£ теорию Т + (}р1\1п„(г) + +

(Т)) + ...

Следствие 3.16. Если Т — конечная П„4-1 -аксиоматизированная теория, содержащая ЕА, то Т + ПП-1Я = (Т1)"-

Следствие 3.19. Для Пп+1-аксиомат,изированных теорий Т, содержащих ЕА (или ЕА+ при п= 1), теория Т + ПП-1Р не является конечно аксиоматизируемой при условии ее непротиворечивости.

Так как замыкание произвольной теории Т относительно П„-Ш является объединением теорий вида Р + для всех конечных

Пп+1-аксиоматизированных подтеорий Р С Т, то следствие 3.16 фактически дает характеризацию замыканий произвольных содержащих ЕА теорий относительно ПП-1К.

Раздел 4, в котором излагаются необходимые для дальнейшего сведения из теории доказуемо тотальных рекурсивных функций (д.т.р.ф.), также служит необходимой подготовкой к анализу правила £„-индукции в разделе 5. Функция /(жь... ,жп) называется доказуемо тотальной рекурсивной в теории Т, если график / представим в стандартной модели Их-формулой ф(хг,... ,хп,у) такой, что

Т Ь VII,. - ■ Ф{х1, хп,у).

Класс д.т.р.ф. теории Т обозначается Т(Т) и представляет собой важную характеристику теории Т.

В §4.1 характеризуются классы д.т.р.ф. для Пг-аксиоматизированных расширений ЕА и показывается, что оператор примитивной рекурсии на классах д.т.р.ф. в точности соответствует правилу ЕНР?, применяемому к таким теориям. В §4.2 и §4.3 доказывается, что для таких теорий Т универсальную функцию для класса Р(Т) можно ввести в консервативном расширении теории [Г, £х-113] и при этом верифицировать естественные свойства такой функции. Это позволяет в теории [Г, ЕНЯ] построить определение истинности для бескванторных формул языка Т, обогащенного символами для функций из Т{Т).

В РАЗДЕЛЕ 5 на основе этих результатов дается точная харак-теризация правила £„-113 в терминах правила метарефлексии. В §5.1 получена следующая теорема.

Теорема 3. ЕНЯ £ П2-13Ки3(ЕА).

В §5.3 на основе варианта техники сколемизации, излагаемого в §5.2, характеризация правила ЕНЯ распостраняется на правила £га-1ГЗ для произвольного п > 1.

Теорема 4. £„-11? = Пп+1-(Шп„+1(ЕА) по модулю /£„_ 1 для любого п > 1.

Следствием этой теоремы является взаимная выводимость правил и Пп+1-ВНпп+1(ЕА). Отсюда также получаются следующие следствия 5.24 и 5.25 (для п > 1).

Следствие 5.24. Для любой конечной Пп+1 и "£п+1-аксиомати-зированной теории Т, содержащей ЕА, Т + £П-1К = (Т)"+1.

Следствие 5.25. Для любой П„4-1 и Е„+1 -аксиоматизированной теории Т, содержащей ЕА,

(г) Т + Еп-\И = Т + Пп+1-1Я;

(п) Т + Еге-1И пе является конечно аксиоматизируемой теорией при условии ее непротиворечивости.

Отметим, что первая часть предыдущего следствия обобщает известный результат Парсонса [10] об эквивалентности теорий /Е^

По-видимому, наиболее интересные применения результатов о правилах индукции получаются в РАЗДЕЛЕ 6, посвященном анализу схем беспараметрической индукции. Оказывается, что такие схемы тесно связаны с релятивизированными схемами локальной рефлексии. Релятивизированным предикатом доказуемости для теории Т называется каноническая формула (ж), выражающая доказуемость в £п-|_1-полной теории, аксиоматизированной над Т множеством всех истинных Пп-предложений. Схема (^¿Ь (Т) есть множество всех формул а, где а есть Ет-предложение. В

§6.1 получена следующая характеризация.

Теорема 5. Для любого п > 1 следующие теории эквивалентны:

(г) /Е-=ЕА + Я^+1(ЕА); " (и) /Пп+1ееЕА + РЦ1:+2(ЕА);

(Иг) ЕА+ + Л1г~ = ЕА+ + (^(ЕА) = ЕА+ + Н^н2(ЕА+).

Эта теорема, вместе с обобщением результатов о консервативности для локальных схем рефлексии на релятивизированные схемы, позволяет в §6.2 доказать Пп+1-консервативность теории /П~+1 над /Е^ и получить следующее важное следствие (га > 1).

Следствие 6.9. Классы доказуемо тотальных рекурсивных функций теорий и совпадают. В частности, РЦЩ) совпадает с множеством всех примитивно рекурсивных функций.

Здесь также получен ряд других следствий о консервативности и аксиоматизируемости для схем беспараметрической индукции, из которых можно выделить получаемое на основе релятивизации теоремы 1 (ш)

Следствие 6.11. Для любого п> 1, теория Ш~+1 консервативна над относительно В(Еп+1)-предложений.

В §6.3 рассматривается связь между равномерными и локальными схемами рефлексии, а также введенным выше правилом ме-тарефлексии. С помощью техники устранения сечения в формализме исчисления Тейта и подходящей секвенциальной формулировки правила метарефлексии доказывается следующая теорема (для п > 1).

Теорема 6. Пусть II —Ип+1-аксиоматизированное расширение ЕА. Тогда для любой теории Т, содержащей ЕА, теория II + К^1\|£П(Т) Ип-консервативна над 17 + Пп-РЯп„ {Т).

Из этой теоремы вытекают следующие результаты о консервативности для равномерных и локальных схем рефлексии.

Предложение 6.27. Если Т — Пп+1 -аксиоматизированное расширение ЕА, то теория Т + есть Ип-консервативное расширение (Т)£..

Предложение 6.28. Если и — Т1п+1-аксиоматизироваиное расширение ЕА, то теория II + есть Т,п+1-консервативное расширение II +

Предложение 6.27 обобщает теорему Парсонса [10] о -консервативности /Х„ над /Х". В частности, отсюда вытекает тот известный факт (независимо установленный также Г. Минцем и Г. Такеути), что совпадает с классом примитивно рекур-

сивных функций. Предложение 6.28 обобщает доказанную Кэйе, Парисом и Димитракопулосом [7] неконструктивно теорему о £п+2~ консервативности теории 1ЕП над . Отметим, что вместе с теоремой 5 предложение 6.28 даёт независимое конструктивное доказательство этой теоремы.

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

Т1. То = Т, где Т — данная "начальная" теория; Т2. Та+1=Та + Соп{Т0);

ТЗ. Та — Ц3<аТр, где а — предельный ординал.

Эта последовательность теорий используется в диссертации для того, чтобы сопоставить ординал огс1г(С) любому расширению II теории Т следующим образом:

от(]т(и) — наименьший а такой что IIК Соп(Га).

Для наиболее естественных расширений теории Т обычно можно установить, что Топ}т(£г) исчерпывает все арифметические Щ-следствия II. Таким образом, огс1т([7) может рассматриваться как ординал, измеряющий "силу" теории V относительно Т в смысле доказуемости Пх-предложений.

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

РА и РА + Соп(РА) имеют одни и те же классы д.т.р.ф. и одинаковые ординальные границы доказуемости трансфинитной индукции (равные £о)- Однако (см. следствие 7.25 (i) диссертации), огё^д(РА) = Со, в то время как ог<1^д(РА + Con (РА)) = ео ■ 2.

Хорошо известная трудность на пути вышеописанной программы классификации теорий состоит в том, что условия Т1-ТЗ не определяют последовательность Та однозначно, то есть теория Та зависит от формального представления ординала а в арифметике, а не только от самого порядкового типа, а также от конкретного способа арифметизации условий Т1-ТЗ.

Для небольших ординалов понятие "естественных систем" конструктивных ординальных обозначений было уже выработано в теории доказательств. Однако, удовлетворительного ответа на вопрос о наиболее естественной арифметизации условий Т1-ТЗ, по-видимому, не было. В разделе 7 диссертации мы предлагаем простой и общий подход к определению таких "естественных" иерархий схем рефлексии с помощью вводимого здесь понятия гладкой прогрессии, основанной на итерации формулы непротиворечивости (или любой другой из рассмотренных выше схем рефлексии) вдоль заданного элементарного линейного порядка. Доказанные в §7.1 и §7.2 теоремы о существовании и единственности гладких прогрессий говорят о том, что для любой фиксированной начальной теории и фиксированного элементарного линейного порядка существует, и притом единственная с точностью до доказуемой в ЕА эквивалентности, гладкая прогрессия, основанная на итерации формулы непротиворечивости. Тем самым понятие гладкости даёт удовлетворительный ответ на вопрос об арифметизации условий Т1-ТЗ и их аналогов для других схем рефлексии.

В §7.3 рассматриваются гладкие прогрессии, основанные на итерации схем рефлексии в некотором смысле близкой силы, и показывается, что ряд полученных нами ранее результатов о консервативности для таких схем рефлексии можно распостранить на итерированные схемы рефлексии.

В §7.4 вводится понятие хорошего вполне упорядочения, которое выделяет некоторые необходимые для дальнейшего естественные свойства элементарных вполне упорядочений. Отмстим, что эти свойства являются достаточно слабым набором требований "естественности". В §7.9, играющем роль приложения, показано,

что для любого конструктивного е-ординала а существует хорошее элементарное вполне упорядочение, имеющее порядковый тип а.

Если Ф('Г) — любая из рассмотренных ранее в диссертации схем рефлексии для теории Т, и фиксировано некоторое элементарное вполне упорядочение, то через Ф (Т)а будем обозначать гладкую прогрессию, основанную на итерации схемы Ф. Мы сохраняем введенные ранее обозначения Та = Соп(Т)а и (Г)" = КЯГ\!пп (Т)а. Для данных теорий Т, 17 и класса формул Г выражение Т ~г и обозначает взаимную консервативность Т и 17 относительно предложений из Г.

В §7.5 доказывается теорема о сравнении гладких прогрессий, основанных на итерации формулы непротиворечивости я локально й схемы рефлексии вдоль одного и того же хорошего вполне упорядочения.

Теорема 7. Доказуемо в ЕА для любых ординалов а,/3, где а > 1, имеют место следующие соотношения:

(г) (Шп(Т)а)р =Пп (1+0); йЫТ^а =Пг Тр+Шс.; (И) =пг Тыа.

Этот результат играет ключевую роль и при сравнении гладких прогрессий, основанных на итерации других типов схем рефлексии. В §7.6 на основе теоремы 7 и результатов §7.3 получается нижеследующее обобщение теоремы Шмерля о тонкой структуре иерархии итерированных схем равномерной рефлексии над примитивно рекурсивной арифметикой.

Определим ординальные функции ип (а) формулой

щ{а) := а,

и обозначим и>п := и>„(1), £о 8ир{с^п | п < о;}.

Теорема 8. Для любых п,тп> 1, для любого П„+1 -расширения Т теории ЕА (доказуемо в ЕА+) имеет место:

(») va > 14p mi+mn =nn re^Mi+fl-

Шмерль [13] установил аналогичное утверждение лишь для специальных прогрессий типа (PRA)", где PRA — примитивно рекурсивная арифметика, при более ограничительных условиях на рассматриваемый класс вполне упорядочений.

Как следствие в диссертации вычисляются ординалы фрагментов РА, определяемых ограничением схемы индукции на классы арифметической иерархии, относительно элементарной арифметики.

Следствие 7.25. Для любого п > 1

(г) IЕп =п2 ЕАа,,,.^, таким образом

ordEA(/En) = w„+1;

(И) РА =п„ (ЕА)"0, таким образом огс1^д(РА) = е0.

В §7.8 на основе нашего подхода дается характеризация классов д.т.р.ф. основных иерархий фрагментов арифметики в терминах известной иерархии классов функций Гжегорчика £а для a < eq. В частности, опираясь на некоторые результаты Р. Сомме-ра и теорему 8 мы доказываем известное утверждение о том, что Т{1 Е„) = . В силу результатов раздела 5 отсюда следует, что с этим же классом функций совпадают и классы д.т.р.ф. теорий /Е^, /Е~ и Ш~+1. В заключение, на основе результатов раздела 5 получается следующее предложение.

Предложение 7.29. Для любого п > 1

В частности, F(IT>\ 4- 1Щ) = £ш2.

Таким образом, класс д.т.р.ф. теории /Ех + 1Щ" совпадает с классом дважды рекурсивных функций в смысле Р. Петер. Этот результат интересен тем, что каждая из теорий /Ei и /П J, взятая отдельно, имеет строго меньший класс д.т.р.ф., совпадающий с классом примитивно рекурсивных функций.

Литература

[1] С.Н. Артёмов. Расширения арифметики и модальные логики. Канд. дисс., Математический институт им. В.А. Стеклова РАН, Москва, 1979.

[2] С.В. Горячев. Об интерпретируемости некоторых расширений арифметики. Математические заметки, 40:561-572, 1986.

[3] G. Boolos. Reflection principles and iterated consistency assertions. Journal of Symbolic Logic, 44:33-35, 1979.

[4] S. Feferman. Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic, 27:259-316, 1962.

[5] K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsheße für Mathematik und Physik, 38:173-198, 1931.

[6] P. Hájek and P. Pudlák. Metamathematics of First Order Arithmetic. Springer-Verlag, Berlin, 1993.

[7] R. Kaye, J. Paris, and C. Dimitracopoulos. On parameter free induction schemas. Journal of Symbolic, Logic, 53(4):1082-1097, 1988.

[8] G. Kreisel and A. Levy. Reflection principles and their use for establishing the complexity of axiomatic systems. Zeitschrift f. math. Logik und Grundlagen d. Math., 14:97-142, 1968.

[9] D. Leivant. The optimality of induction as an automatization of arithmetic. Journal of Symbolic Logic, 48:182-184, 1983.

[10] С. Parsons. On n-quantifier induction. Journal of Symbolic Logic, 37(3):466-482, 1972.

[11] W. Pohlers. Proof Theory. An Introduction. Lecture Notes in Mathematics 1407. Springer-Verlag, Berlin, 1989.

[12] J.B. Rosser. Gödel Theorems for non-constructive logics. Journal of Symbolic Logic, 2:129-137, 1937.

[13] U.R. Schmerl. A fine structure generated by reflection formulas over Primitive Recursive Arithmetic. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium'78. North Holland, Amsterdam, 1979, pages 335-350.

[14] W. Sieg. Fragments of arithmetic. Annals of Pure and Applied Logic, 28:33-7f, 1985.

[15] A.M. Turing. System of logics based on ordinals. Proc. London Math. Soc., ser. 2, 45:161-228, 1939.

Работы автора по теме диссертации

[16] Л.Д. Беклемишев. Независимые нумерации теорий и рекурсивных прогрессий. Сибирский математический журнал, 33(5):22-46, 1992.

[17] Л.Д. Беклемишев. Об ограниченном правиле индукции и итерированных схемах рефлексии над кальмаровской элементарной арифметикой. В сб. Теоретические и прикладные аспекты математических исследований, под ред. О.Б.Лупанова. Москва, МГУ, 1994, стр. 36-39.

[18] L.D. Beklemishev. On bimodal logics of provability. Annals of Pure and Applied Logic, 68:115-160, 1994.

[19] L.D. Beklemishev. Iterated local reflection versus iterated consistency. Annals of Pure and Applied Logic, 75:25-48, 1995.

[20] L.D. Beklemishev. Notes on local reflection principles. Logic Group Preprint Series 133, University of Utrecht, 1995, 8 p.

[21] L.D. Beklemishev. Remarks on Magari algebras of PA and /Д0 + EXP. In Logic and Algebra, P.Agliano, A.Ursini, eds., pages 317325. Marcel Dekker, New York, 1996.

[22] L.D. Beklemishev. Induction rules, reflection principles, and provably recursive functions. Annals of Pure and Applied Logic, 85:193-242, 1997.

[23] L.D. Beklemishev. Parameter free induction and reflection. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory. Lecture Notes in Computer Science 1289. Springer-Verlag, Berlin, 1997, pp. 103-113.

[24] L.D. Beklemishev. A proof-theoretic analysis of collection. Archive for Mathematical Logic, 34(4-5):216-238, 1998.

- i

у/ м ^ H//ir

Ч»? - Г я 9 - &

Российская Академия Наук Математический институт имени В.А. Стеклова

На правах рукописи УДК 510.64

БЕКЛЕМИШЕВ Лев Дмитриевич

Схемы рефлексии в формальной

арифметике

01.01.06 — математическая логика, алгебра и теория чисел

Диссертация на соискание учёной степени доктора физико-математических наук

Москва - 1998 г.

Моим дорогим родителям Дмитрию Владимировичу и Людмиле Анатолиевне

Содержание

Введение 5

1 Основные понятия 9

1.1 Элементарная арифметика.......................9

1.2 Арифметизация синтаксиса......................12

1.3 Логика доказуемости..........................................18

2 Общие свойства схем рефлексии 20

2.1 Схемы рефлексии..............................................20

2.2 Теоремы о неограниченности................................23

2.3 Иерархии схем частичной рефлексии...................26

3 Индукция и рефлексия 36

3.1 Основные формы индукции .....................36

3.2 Исчисление Тейта ........................37

3.3 Схемы индукции и их характеризация......................40

3.4 Правила индукции, сводимости....................44

3.5 Характеризация правила Пп-индукции .................50

4 Доказуемо тотальные рекурсивные функции 55

4.1 Базисные результаты........ ..................55

4.2 Элементарное замыкание......................................60

4.3 Универсальная функция.........................66

4.4 Определение истинности......................................71

5 Характеризация правила Еп-индукции 74

5.1 Правило Хх-индукции..........................................74

5.2 Релятивизация..................................................78

5.3 Правило Еп-индукции..........................................83

5.4 О правиле ¿3(Еп)-индукции....................................91

6 Беспараметрическая индукция и рефлексия 92

6.1 Характеризация схем беспараметрической индукции ... 92

6.2 Результаты о консервативности и аксиоматизируемости 95

6.3 Схемы и правила рефлексии...........................100

7 Итерированные схемы рефлексии 107

7.1 Построение итерированных схем рефлексии................109

7.2 Единственность................................................113

7.3 Прогрессии близкой силы ......................117

7.4 Хорошие вполне упорядочения................................120

7.5 Композиция прогрессий . . ...................................122

7.6 Итерированная непротиворечивость и локальная рефлексия........................................................123

7.7 Итерированная равномерная рефлексия ....................134

7.8 Беспараметрическая индукция и быстрорастущие

функции ............ ..................................137

7.9 Приложение ..............................140

Введение

Настоящая диссертация посвящена исследованию схем рефлексии для фрагментов формальной арифметики Пеано и применению этих схем к вопросам сравнения и классификации арифметических теорий.

Схемы рефлексии возникли в математической логике вскоре после доказательства Гёделем его фундаментальных теорем о неполноте [17].1 Для данной теории Т эти схемы представляют собой варианты формализации утверждения "если формула (р доказуема в Т, то (р истинна". Они дают примеры истинных, но недоказуемых утверждений, обобщающих первый известный пример такого рода — гёделевскую формулу непротиворечивости теории Т.

Тьюринг [43] ввёл в рассмотрение прогрессии теорий, получаемые итерированием процесса пополнения теории схемой рефлексии, и предложил возможный подход к ординальной классификации арифметических теорий на основе таких прогрессий. В дальнейшем этот подход был проанализирован и развит Феферманом в [15]. Построенные Тьюрингом и Феферманом примеры показали, что на пути подобной классификации встают существенные трудности, связанные с проблемой канонического выбора итерированных схем рефлексии и связанным с ней вопросом о естественном представлении ординалов в арифметике.

Крайзель и Леви в [20] показали, что схемы рефлексии являются удобным инструментом для изучения вопросов сложности аксиоматизации формальных теорий. Ими была доказана дедуктивная эквивалентность так называемой равномерной схемы рефлексии для примитивно рекурсивной арифметики и полной схемы индукции, откуда, в частности, вытекает невозможность задания арифметики Пеано множеством аксиом ограниченной кванторной сложности. В этой же работе была доказана эквивалентность схемы трансфинитной индукции до ординала со и равномерной схемы рефлексии для арифметики Пеано. В дальнейшем были установлены тесные связи между схемами рефлексии и другими истинными невыводимыми утверждениями, включая известные комбинаторные принципы Париса-Харрингтона.

В диссертации получено решение ряда важных вопросов о схемах рефлексии, что позволило сделать аппарат этих схем универсальным

1 Схемы рефлексии появились впервые, по-видимому, в работе Россера 1937 г. [34]. При этом Россер ссылается на неопубликованные результаты Клини, рассмотревшего в 1935 г. вариант логического правила, эквивалентный, в современной терминологии, равномерной схеме рефлексии (см. ниже §2.1).

инструментом анализа и ординальной классификации арифметических теорий. Описание исследуемой теории в терминах схем рефлексии позволяет использовать свойства таких схем для получения разнообразных результатов о её строении и соотношении с другими теориями, в частности, результатов о независимости, аксиоматизируемости, (частичной) консервативности и характеризации классов доказуемо тотальных вычислимых функций.

Одно из наиболее активно развивающихся в последнее время направлений математической логики связано с изучением подсистем, или фрагментов, формальной арифметики Пеано РА. Интерес к этим вопросам был вызван прежде всего обнаружившимися связями с теорией сложности вычислений и попытками формализации понятия эффективного (feasible) доказательства. Монография [18] содержит накопленные в этой области к 1993 году основные результаты и обширную библиографию.

В настоящей работе подход, основанный на схемах рефлексии, применён к исследованию иерархий фрагментов РА. Изучены взаимосвязи схем рефлексии и основных форм индукции ограниченной арифметической сложности. Как следствие получен ряд новых результатов, относящихся к иерархиям фрагментов РА, определяемых правилом индукции и схемой индукции без параметров ограниченной арифметической сложности.

К основным результатам диссертации можно отнести следующие.

1) Точная характеризация правил индукции ограниченной арифметической сложности в терминах схем рефлексии (теоремы 2, 3, 4 диссертации) .

Существенной чертой полученной характеризации является её инвариантность, то есть независимость от выбора базисной теории достаточно широкого класса, над которой эти правила рассматриваются. В частности, это позволяет получить естественную аксиоматизацию с помощью схем аксиом замыканий произвольных достаточно сильных арифметических теорий относительно правил индукции (следствия 3.16, 3.18 и 5.24).

2) Точная характеризация схем беспараметрической индукции ограниченной арифметической сложности в терминах схем рефлексии (теорема 5).

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

мами, определяемыми независимым образом, ранее не была известна.

3) Детально изучено строение иерархии локальных схем рефлексии над произвольной достаточно сильной арифметической теорией. В частности, получены оптимальные в смысле арифметической сложности результаты о консервативности для этой иерархии (теорема 1), а также результаты о связи равномерной и локальной схем рефлексии (теорема 6, предложения 6.27 и 6.28).

Вместе с результатами 2) это позволяет дать ответ на ряд вопросов о схемах беспараметрической индукции в арифметике, а также получить новое конструктивное доказательство некоторых результатов об этих схемах, для которых ранее было известно лишь неконструктивное теоретико-модельное доказательство.

4) Получен ответ на стоявший в области фрагментов арифметики вопрос о доказуемо тотальных вычислимых функциях теории, аксиоматизируемой схемой индукции для Пг-формул без параметров. Показано, что класс таких функций совпадает с примитивно рекурсивными функциями (следствие 6.9). Расширение этой теории схемой индукции для Егформул с параметрами имеет более широкий класс доказуемо тотальных вычислимых функций, совпадающий с классом дважды рекурсивных функций в смысле Р. Петер (предложение 7.29). Эти результаты, по-видимому, являются наиболее интересными приложениеми результатов 2) и 3).

5) Построение иерархий итерированных схем рефлексии с естественными свойствами, позволяющее обобщить на такие схемы результаты о консервативности из 3). В частности, показано, что для таких иерархий а раз итерированная схема локальной рефлексии, где а — конструктивный ординал, доказывает те же Пх-предложения, что и иа раз итерированное утверждение о непротиворечивости (теорема 7).

В отличие от традиционного подхода, связанного с ординальными границами доказуемости трансфинитной индукции в формальных теориях (см., например, [29]), изложенный в диссертации подход дает более тонкую классификацию, позволяющую различить теории уже на уровне их Последствий. На основе этого подхода получено обобщение на более широкий класс теорий теоремы Шмерля [35] о тонкой структуре иерархии итерированных схем равномерной рефлексии над примитивно рекурсивной арифметикой и вычислены ординалы основных фрагментов РА (теорема 8, следствие 7.25). Также получены обобщения результатов 4) на схемы беспараметрической индукции арифметической сложности Пп для произвольного п > 2 (предложение 7.29).

Применяемые в диссертации методы можно разделить на три группы. К первой группе относятся широко известные методы структурной теории доказательств, используемые при получении характеризаций 1) и 2), такие как техника устранения сечения и сколемизация. Отметим, что применяемый нами для анализа правила Еп-индукции вариант техники сколемизации является усовершенствованием техники "операторных теорий" работы [37].

Ко второй группе относится нетрадиционная техника, используемая для анализа схем локальной рефлексии. Ключевую роль здесь играет логика доказуемости и связанные с ней модели Крипке. Первые применения подобной техники к анализу схем рефлексии содержатся в работах [11, 1].

Наконец, подход, предлагаемый нами для построения иерархий итерированных схем рефлексии, использует некоторые идеи работ [15, 35]. Введенное в диссертации понятие гладкой прогрессии теорий позволяет существенно упростить построение итерированных схем рефлексии, делая ненужным использование языка теории рекурсии и его формализации в арифметике, а также использование так называемых фундаментальных последовательностей ординальных обозначений. При этом достигается большая общность результатов и, в некотором смысле, каноничность определяемых посредством этой конструкции схем.

1 Основные понятия

1.1 Элементарная арифметика

Язык элементарной арифметики — это язык первого порядка, содержащий бинарные предикатные символы = и <; бинарные функциональные символы + и •; унарные функциональные символы S и ехр и константу 0. Стандартная модель арифметики — это модель с унивесумом N = {0,1,2,...}, на котором все символы интерпретируются естественным образом: = есть отношение равенства; < есть отношение порядка; + и • суть операции сложения и умножения; S есть функция следования S(x) = х + 1; ехр есть показательная функция ехр (ж) = Iх.

Формулы этого языка называются арифметическими. Мы будем следовать обычным соглашениям об опускании излишних скобок в формулах; использовать инфиксное написание =, <, + и • (то есть будем писать, например, х < у вместо <(х, у)); будем писать 2х вместо ехр(ж) и так далее, х < у есть сокращение для х < у Л ~>х = у.

Выражения \/х < t А{х) и Зх < t А(х) являются сокращениями для формул \/х (х < t —> А{х)) и Зх (х < t Л А(х)), соответственно (где t — любой терм, не содержащий переменной х). Вхождения кванторов такого вида называются ограниченными; ограниченными или элементарными формулами называются арифметические формулы, все вхождения кванторов в которые ограничены. Заметим, что по определению бескванторные формулы являются элементарными. Аналогично определяются выражения \/х < t А(х) и Зх < t А(х). Элементарные предикаты или отношения — это отношения, определимые элементарными формулами в стандартной модели арифметики.

Арифметические формулы классифицируются по своей логической сложности в классическую арифметическую иерархию. Для п > 0 классы £n- and Пп- формул определяются индуктивно следующим образом. Е0- и По-формулы — это элементарные формулы. Еп+х-формулы — это формулы вида Зх\... 3xmA(xi,..., хт), где А — некоторая Пп-формула. Пп+1-формулы — это формулы вида Vxi... VxmA(xi,..., хт), где А — некоторая £п-формула. Другими словами, Еп-фор мулы — это ограниченные формулы с префиксом из п чередующихся блоков однотипных кванторов, начинающиеся с 3, а Пп-формулы определены двойственным образом. Классы Еп- and Пп-формул будем обозначать Еп и Пп, соответственно.

По теореме о предваренной нормальной форме, всякая арифметичес-

кая формула логически эквивалентна Еп-формуле для некоторого п. Допуская вольность речи, мы будем иногда называть Е„,-формулами также и формулы, логически эквивалентные Еп-формулам в смысле нашего официального определения. По модулю логической эквивалентности

1. Классы Еп и Пп замкнуты относительно V, А.

2. А 6 Еп пЛ £ П„ и двойственно.

3. Для п > 1, класс П„ замкнут относительно V, класс Еп замкнут относительно 3.

С вычислительной точки зрения, наиболее важным классом формул является Ех. Предикат является Е 1-определимым, если и только если он (рекурсивно) перечислим.

Элементарные предикаты разрешимы, причем грубая оценка сложности разрешающей процедуры дает верхнюю оценку порядка на число её шагов, где п — некоторая константа, а х — размер входа. Здесь 2^ означает суперэкспоненциалъную функцию двух аргументов:

ох — 2х „ — 22"

¿0 п+1^ •

Функции вида для фиксированного п называются мулътиэкспонен-циалъными, таким образом всякий элементарный предикат разрешим за мультиэкспоненциальное время. Обратное также верно: всякий предикат, разрешимый за мультиэкспоненциальное время, элементарен (см. [4]).

Арифметика Пеано РА — теория первого порядка с равенством, сформулированная в арифметическом языке и задаваемая следующими математическими аксиомами:

Р1. -5(а) = 0

Р2. ^(а) = 5(6) а = 6

РЗ. а + 0 = а

Р4. а + 5(6) = 5(а + 6)

Р5. а- 0 = 0

Р6. а ■ 5(6) = а • 6 + а

Р7. ехр(О) = 5(0) Р8. exp(S(a)) = ехр(а) + ехр(а) Р9. а < 0 а = О PIO. а < S(b) a<bVa = S{b))

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

IA : <р(0) Л Vz (ср(х) (p(S(x))) ->> Ух(р(х).

Элементарная арифметика ЕА аксиоматизируется над Р1-Р10 схемой индукции для элементарных формул ip{x).

Элементарная арифметика представляет собой достаточно слабый фрагмент РА. Хорошо известно, что, аналогично РА, ЕА имеет эквивалентную формулировку в языке арифметики без символа экспоненты. Теория /До задается в этом языке аксиомами Р1-Р6, Р9, Р10 вместе со схемой индукции для До-формул (т.е. ограниченных формул языка без ехр). Известно, что график функции 2х можно естественным образом определить некоторой Ад-формулой Ехр(ж, у) ([18], с. 299). Для этой формулы в /До выводимы аналоги аксиом Р7, Р8 и свойства функциональности и монотонности. Формула Ехр(х,у) определяет интерпретацию ЕА в теории /Ао + Ехр, где Ехр есть аксиома УхЗу Ехр(ж, у), выражающая тотальность экспоненты ([18], с. 37). Фактически, ЕА дедуктивно эквивалентна консервативному дефинициальному расширению /Ао + Ехр с помощью символа для функции ехр. Нетрудно убедиться в том, что эта интерпретация сохраняет классы £п и Пп-формул при п > 1 по модулю выводимости в /До + Ехр. (Класс элементарных отношений, однако, строго шире, чем класс До-отношений. Элементарные отношения совпадают с доказуемо Ai-отношениями для теории /До + Ехр.)

В отличие от РА, /Ао + Ехр и ЕА являются конечно аксиоматизируемыми теориями ([18], с. 366). Нетрудно убедиться, что ЕА аксиоматизируема формулами сложности Пх в арифметической иерархии, а /До + Ехр имеет сложность аксиоматизации Щ (в языке без ехр).

Элементарными (по Кальмару) функциями называются функции, которые могут быть получены из функций Z(x) = 0, S, +, •, 2Ж, функ-

ции

О, если х < у

х

х — у, иначе

и проектирующих функций /"(жь • •., хп) = хг с помощью операций композиции и ограниченной минимизации [32]:

(у, если у < г и Шу,х) Л < у-^Шг.х) [О, если чг <

(Здесь Я — предикат вида д(1,х) = 0 для некоторой ранее определенной функции д.)

Класс элементарных функций обозначается Е и совпадает с классом функций, вычислимых по Тьюрингу за мультиэкспоненциальное время (см. [4]). Класс £ замкнут относительно операций ограниченного суммирования, ограниченного умножения и ограниченной примитивной рекурсии. Фактически, по модулю композиции и достаточно большого набора начальных функций каждая из этих операций эквивалентна ограниченной минимизации (см. [32], гл. 5).

Символы для всех элементарн�