Введение к работе
Настоящая диссертация посвящена исследованию схем рефлексии для фрагментов формальной арифметики Пеано и применению этих схем к вопросам сравнения и классификации арифметических теорий.
Схемы рефлексии возникли в математической логике вскоре после доказательства Гёделем его фундаментальных теорем о неполноте [5, 12]. Для данной теории Т эти схемы представляют собой варианты формализации утверждения "если формула <р доказуема в Т, то уз истинна". Они дают примеры истинных, но недоказуемых утверждений, обобщающих первый известный пример такого рода — гёделевскую формулу непротиворечивости теории Т.
Тьюринг [15] ввёл в рассмотрение прогрессии теорий, получаемые итерированием процесса пополнения теории схемой рефлексии, и предложил возможный подход к ординальной классификации арифметических теорий на основе таких прогрессий. В дальнейшем этот подход был проанализирован и развит Феферманом в [4]. Построенные Тьюрингом и Феферманом примеры показали, что на пути подобной классификации встают существенные трудности, связанные, в частности, с проблемой естественного представления ординалов в арифметике.
Крайзель и Леви в [8] показали, что схемы рефлексии являются удобным инструментом для изучения вопросов сложности аксиоматизации формальных теорий. Ими была доказана дедуктивная эквивалентность так называемой равномерной схемы рефлексии для примитивно рекурсивной арифметики и полной схемы индукции, откуда, в частности, вытекает невозможность задания арифметики Пеано множеством аксиом ограниченной кванторной сложности. В этой же работе была доказана эквивалентность схемы траксфинит-ной индукции до ординала єо и равномерной схемы рефлексии для арифметики Пеано. В дальнейшем были установлены тесные связи между схемами рефлексии и другими истинными невыводимыми утверждениями, включая известные комбинаторные принципы Париса-Харрингтона.
В диссертации получено решение ряда важных вопросов о схемах рефлексии, что позволило сделать аппарат этих схем уни-
нереальным инструментом анализа и ординальной классификации арифметических теорий. Описание исследуемой теории в терминах схем рефлексии позволяет использовать свойства таких схем для получения разнообразных результатов о её строении и соотношении с другими теориями, в частности, результатов о независимости, аксиоматизируемости, (частичной) консервативности и харак-теризации классов доказуемо тотальных вычислимых функций.
Одно из наиболее активно развивающихся в последнее время направлений математической логики связано с изучением подсистем, или фрагментов, формальной арифметики Пеано РА. Интерес к этим вопросам был вызван прежде всего обнаружившимися связями с теорией сложности вычислений и попытками формализации понятия эффективного (feasible) доказательства. Монография [6] содержит накопленные в атой области к 1993 году основные результаты и обширную библиографию.
В настоящей работе подход, основанный на схемах рефлексии, применён к исследованию иерархий фрагментов РА. Изучены взаимосвязи схем рефлексии и основных форм индукции ограниченной арифметической сложности. Как следствие получен ряд новых результатов, относящихся к иерархиям фрагментов РА, определяемых правилом индукции и схемой индукции без параметров ограниченной арифметической сложности.
К основным результатам диссертации можно отнести следующие.
1) Точная характеризация правил индукции ограниченной ариф
метической сложности в терминах схем рефлексии.
Существенной чертой полученной характеризации является её инвариантность, то есть независимость от выбора базисной теории достаточно широкого класса, над которой эти правила рассматриваются. В частности, это позволяет получить естественную аксиоматизацию с помощью схем аксиом замыканий произвольных достаточно сильных арифметических теорий относительно правил индукции.
2) Точная характеризация схем беспараметрической индукции
ограниченной арифметической сложности в терминах схем рефлек
сии.
Возникающие при этом так называемые локальные схемы рефлексии в простейшем случае были известны еще со времени ра-
боты Тьюринга. Однако, их связь с фрагментами РА или другими формальными системами, определяемыми независимым образом, ранее не была известна.
3) Детально изучено строение иерархии локальных схем ре
флексии над произвольной достаточно сильной арифметической те
орией. В частности, получены оптимальные в смысле арифмети
ческой сложности результаты о консервативности для иерархии
схем локальной рефлексии, а также результаты о связи равномер
ной и локальной схем рефлексии.
Вместе с результатами 2) это позволяет дать ответ на ряд вопросов о схемах беспараметрической индукции в арифметике, а также получить новое конструктивное доказательство некоторых результатов об этих схемах, для которых ранее было известно лишь неконструктивное теоретико-модельное доказательство.
-
Получен ответ на стоявший в области фрагментов арифметики вопрос о доказуемо тотальных вычислимых функциях теории, аксиоматизируемой схемой индукции для Щ-формул без параметров. Показано, что класс таких функций совпадает с примитивно рекурсивными функциями. Расширение этой теории схемой индукции для Ej-формул с параметрами имеет более широкий класс доказуемо тотальных вычислимых функций, совпадающий с классом дважды рекурсивных функций в смысле Р. Петер. Эти результаты, по-видимому, являются наиболее интересными приложсниеми результатов 2) и 3).
-
Построение иерархий итерированных схем рефлексии с естественными свойствами, позволяющее обобщить на такие схемы результаты о консервативности из 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 наименования.