Субрекурсивная реализуемость и логика предикатов

• Автор: Пак Бен Ха
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2003
• Место защиты: Москва
• Количество страниц: 83 с.

Содержание
1 Введение
2 Основные определения
2.1 Примитивно рекурсивные и настично-рекурсивные функции
2.2 Интуиционистское исчисление предикатов
2.3 Интуиционистская формальная арифметика
3 Примитивно рекурсивная реализуемость
3.1 Иерархии примитивно рекурсивных функций
3.2 Строго примитивно рекурсивная реализуемость
3.3 Неарифметичность предикатной логики строго примитивно рекурсивной реализуемости
3.4 Строго примитивно рекурсивно неопровержимые предикатные формулы
4 Минимальная реализуемость
4.1 Примитивно рекурсивные функционалы
4.2 Минимальная реализуемость арифметических формул .
4.3 Неарифметичность предикатной логики минимальной реализуемости
4.4 < вц-неопровержимые предикатные формулы

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

тематической логики.
Основная идея введенного Клини понятия рекурсивной реализуемости состоит в том, что информация об интуиционистской истинности арифметического утверждения кодируется натуральным числом, которое называется реализацией этого утверждения. При этом, например, реализацией импликации Ф 3 Ф считается гёделевский номер частично-рекурсивной функции, которая каждую реализацию утверждения Ф переводит в некоторую реализацию утверждения Ф, что соответствует интуиционистскому пониманию истинности утверждения вида Ф Э Ф как существования эффективного способа, позволяющего из обоснования утверждения Ф получить обоснование утверждения Ф. Реализацией универсального утверждения УхФ(х) считается гёделевский номер частично-рекурсивной функции, которая каждое натуральное число п переводит в некоторую реализацию утверждения Ф(п), что соответствует интуиционистскому пониманию истинности утверждения вида УхФ(х) как существования эффективного способа, позволяющего для любого п получить обоснование утверждения Ф(п). Таким образом, интуиционистское понятие эффективности уточняется с помощью частично-рекурсивных функций. Однако в математике рассматриваются и другие, более узкие классы вычислимых функций — так называемые субрекурсивные классы. Представляет интерес рассмотрение и изучение вариантов реализуемости, основанных на использовании различных субрекурсивных классов функций. Этот интерес стимулируется и некоторыми известными метаматематическими результатами. Так, Нельсон [20] доказал корректность формальной системы интуиционистской арифметики НА относительно клиниевской рекурсивной реализуемости в следующем смысле: если замкнутая арифметическая формула Ф выводима в системе НА, то Ф рекурсивно реализуема. Из этого результата вытекает такой факт: если в интуиционистской арифметике выводима формула вида УхЗуФ(х, у), то существует такая рекурсивная функция /, что для любого натурального числа т истинна формула Ф(т, /(т)). В том случае, когда Ф(х,у) — примитивно рекурсивная формула, соответствующая функция / называется доказуемо рекурсивной. Таким образом, всякая доказуемо рекурсивная функция является рекурсив-

3. Каковы бы ни были натуральные числа т и п, если т. ф п, то
Н <21 Э Ух([тг](ж) Э ->[ш](г)). (24)
4- Каково бы ни было натуральное число п,
Ь <21 Э Уж([п](ж) V -1[п](а:)). (25)
5. Каково бы ни было натуральное число п,
Р (?1 3 Зж[п](ж). (26)
6. Каковы бы ни были арифметическая формула Ф(у1,..., уп) и на-
туральные числа к,..., кп,
Ы Ф(&ъ. • .,кп) э Уу% ■ ■ ■ УуД^Кгц) к ... к[кп}(уп) э Ф'(Уь •

Доказательство. Все эти утверждения немедленно следуют из (14) и (15) - (20). Предложение 10 доказано.
Ряд арифметических формул
Ф = 5(ж1,ж2), А(х1,х2,х3),М(х1,х2,х3),М'(х1),£(а;их2),
допустимый для подстановки в формулу А,М,И, Е), будем на-
зывать интерпретацией формулы ($, если формула <21 (5, А, АЛ, Лг, £) является строго примитивно рекурсивно реализуемой.
Пусть фиксирована некоторая интерпретация Ф формулы (^1. Если Е — предикатная формула, не содержащая предикатных букв, отличных от 5, А, М, К, Е, будем для краткости вместо д’дя’л" £ писать Е. Именно этот смысл будут иметь выражения <21, [п](ж) и Ф', если Ф — арифметическая формула.
Предложение 11 Каковы бы ни были интерпретация Ф формулы <21 и замкнутая арифметическая формула Ф, если предикатная формула <21 Э Ф; выводима в интуиционистском исчислении предикатов, то арифметическая формула Ф' является строго примитивно рекурсивно реализуемой.