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

• Автор: Беклемишев, Лев Дмитриевич
• Шифр специальности: 01.01.06
• Научная степень: Докторская
• Год защиты: 1998
• Место защиты: Москва
• Количество страниц: 149 с.

Содержание
Введение
Основные понятия
1.1 Элементарная арифметика
1.2 Арифметизация синтаксиса
1.3 Логика доказуемости
Общие свойства схем рефлексии
2.1 Схемы рефлексии
2.2 Теоремы о неограниченности
2.3 Иерархии схем частичной рефлексии
Индукция и рефлексия
3.1 Основные формы индукции
3.2 Исчисление Тейта
3.3 Схемы индукции и их характеризация
3.4 Правила индукции, сводимости
3.5 Характеризация правила Пп-индукции
Доказуемо тотальные рекурсивные функции
4.1 Базисные результаты
4.2 Элементарное замыкание
4.3 Универсальная функция
4.4 Определение истинности
Характеризация правила Еп-индукции
5.1 Правило X 1-индукции
5.2 Релятивизация
5.3 Правило Хи-индукции
5.4 О правиле Б(Х„)-индукции
Беспараметрическая индукция и рефлексия
6.1 Характеризация схем беспараметрической индукции
6.2 Результаты о консервативности и аксиоматизируемости
6.3 Схемы и правила рефлексии

Теорема 1. Для п >
(г) в теориях Т + РДп(Т) и Т + (ДппДТ1) доказуемы одни и те же Пп-предложения;
(и) в теориях Т + И(Т) и Т + РД)£П(Т) доказуемы одни и те же Лп-предложения;
(иг) в Т + 1-Дп(Т) иТ + РДпДТ) доказуемы одни и те же 8(1)-предложения.
Доказательство. Допустим
/™=1 Ф») 7Г-
В силу условий Лёба мы также имеем
Т I- □Г(Д™=1(С]Г1—у ц>ф) —у 7Г).
Рассматривая арифметическую реализацию, которая сопоставляет переменной р предложение 7г, а рг предложение рг для всех г, по лемме 2.18 заключаем, что
Т Л™1 {ПтФг -> Фг) 7Г,
где фг означает арифметическую интерпретацию модальной формулы Qi. Заметим теперь, что если тг 6 Г1„ для п > 1. то фг е Пга для всех г. Значит
Т + (Т) 7Г.
Аналогично, £п-следствия РДДТ) содержатся в РДп£п(Т), и #(£1)-следствия Я1п(Т) содержатся в теории которая эквивалентна
РДпеДТ) по лемме 2.17, ц.е.ф
Следующее утверждение показывает, что доказанная выше теорема оптимальна в смысле арифметической сложности.
Лемма 2.27. При условии непротиворечивости Тш, дляп > 1 найдется £„- (соответственно, ППу) предложение, доказуемое в Т + (Дп(Т), но не доказуемое в Т + РДпДГ) (соотв., Т + №г%п(Т)).
Доказательство. По 2.16 в качестве такого предложения можно взять соответствующий частный случай схемы [ДпзДТ) (соотв., (ДпщС1)), п.е.Н,
В заключение отметим следующее усиление следствия 2.10.