Примитивно рекурсивная реализуемость и конструктивная теория моделей

• Автор: Витер, Дмитрий Александрович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2001
• Место защиты: Москва
• Количество страниц: 150 с.

Оглавление

I Введение. З

II Примитивно рекурсивная реализуемость.

1. Интуиционистские и базисные формальные системы.

1.1. Язык логики предикатов

1.2. Интуиционистское исчисление предикатов НРС

1.3. Секвенциальное интуиционистское исчисление предикатов ЩС.

1.4. Язык формальной арифметики............................... • • •

1.5. Интуиционистская формальная арифметика НА

1.6. Базисная логика предикатов ВС^С

1.7. Базисная арифметика В А

1.8. Связь базисной логики с интуиционистскими системами
2. Примитивно рекурсивная реализуемость.
2.1. Определения и основные факты
2.2. Р11-реализуемость ”по Салехи”
2.3. Р11-реализуемость ”по Клини”
2.4. Понятие РИ-реализуемости для предикатных формул
2.5. Общая схема доказательства основного результата
3. Формализация теоремы Тенненбаума
3.1. Теория Т
3.2. Теория Т'
3.3. Теория Т
3.4. Р 11-реализуемость усилений аксиомы индукции
4. Неарифметичность множества всех РИ-реализуемых предикатных формул.
5. Неарифметичность множества всех РИ-неопровержимых предикатных формул.
III Конструктивная теория моделей. ЮЗ
6. Обобщенные предикаты и обобщенные системы. ЮЗ

7. Конструктивные теории нумерованных моделей.
8. Конструктивная теория равенства.
8.1. Рефлексивные системы
8.2. Конструктивные теории разрешимого равенства
8.3. Неполнота теорий неразрешимого равенства

Часть I Введение.
Диссертация посвящена исследованию некоторых вопросов конструктивной математической логики.
В начале XX века в математике возникло интуиционистское направление как положительный аспект предпринятой Брауэром [1] критики классической математики в связи с обнаружением в последней теоретико-множественных парадоксов. Интуиционистская критика затронула и классическую логику. Начиная с работ А. Н. Колмогорова, Гейтинга, В. И. Гливенко, относящихся к концу 20-х — началу 30-х годов, большое внимание уделяется построению и исследованию логических систем, корректных с точки зрения интуиционизма. По мере развития математики и математической логики исследования по интуиционистской логике не только не утратили свою актуальность, но, напротив, наполнялись новым содержанием. Так, еще в 30-е годы А. Н. Колмогоров [2] показал, что интуиционистская логика имеет реальный смысл, не связанный с философскими установками Брауэра, если рассматривать ее как логику решения задач. В 40-е годы американский математик С. К. Клини [3] предложил интерпретацию ряда специфических интуиционистских понятий на основе разработанных к тому времени концепций теории алгоритмов. В частности, Клини ввел понятие рекурсивной реачизуемости для формул языка арифметики первого порядка с целью уточнения интуиционистского смысла арифметических суждений на основе теории рекурсивных функций (см. [о. § 82]). Это понятие послужило отправной точкой для разработки конструктивной семантики математических утверждений, использованной в рамках конструктивного подхода к математике в работах А. А. Маркова и его школы [4]. Развитие конструктивной математики в свою очередь вызвало необходимость исследования соответствующей ей конструктивной логики. Наконец, исследования последних лет в области теоретического программирования выявили особую роль конструктивной логики в вопросах синтеза программ, поскольку использование этой логики в математических построениях позволяет сделать явными их алгоритмические и вычислительные аспекты. Процедуры извлечения алгоритмов из интуиционистских доказательств обычно используют конструктивные семантики логико-математических языков. Поэтому конструктивная логика считается одним из актуальных направлений современной математической логики.
В конструктивной логике (как и в клнниевском определении реализуемости) интуиционистское понятие эффективности уточняется с помощью рекурсивных функций. В математике рассматриваются также другие, более уз-

2) Пусть Ф = А А В.
Очевидно, что в ВА выводимо
хгрг(А(х) Л В(х)) Ь 7Г1(г)гр,’А(х); хгрг(А(х) А В(х)) Ь тг2(г)гргБ(х).
По (8) и (9),
тг!(а;)гртА(х) Н /л(тт1(т),х)г|гаг.4(х); тг2(х)гргВ(х) Ь /в(тг2(х),хУ3га1В(х).
}ф{х,х) = {/л(7Г1(гс),х),/в(7г2(а:),х)). Поэтому,
тгрт(А(х) Л В{х)) 1- (/л(7Г1(т),х),/в(7г2(ж),х))г|га,(А(х)ЛВ(х)),
откуда получаем (6) для Ф = А А В. Аналогично доказывается справедливость (7) для Ф = А А В.
3) Пусть Ф = АУ В. По определению, в системе ВА выводится а,трг(А(х) V В(х)) 1- (яд(ж) = О Л 7Г2(.г')грТ4(х))/
/(~ 7Г1(т) = О Л 7г2(ж)гртП(х)).
По (8) и (9),
(тгх(а’) = О Л тг2(.т)гргА(х)) Н (яд(ж) = О Л /л(тг2(.г),х)г^а,.4(х)):
(~ Яд(ж) = О Л тг2(.г)грг£(х)) Ь (~ Яд(ж) = О Л /в(п2(х),х)гр5га1В{х)).
fф(x,x) = (яд(ж),58(яд(ж)) • /л(тг2(.г-),х) +88-(тг1(.т)) • /в(-2(.т),х)).
Аналогично доказывается справедливость (7) для Ф = А V В.
По определению,
Тогда