Субрекурсивная реализуемость и логика предикатов тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Пак Бен Ха

• Пак Бен Ха
• кандидат физико-математических наук
• 2003

Оглавление диссертации кандидат физико-математических наук Пак Бен Ха

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 < £о-нео11РовеРжимые предикатные формулы.

Введение диссертации (часть автореферата) на тему «Субрекурсивная реализуемость и логика предикатов»

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

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

Основная идея введенного Клини понятия рекурсивной реализуемости состоит в том, что информация об интуиционистской истинности арифметического утверждения кодируется натуральным числом, которое называется реализацией этого утверждения. При этом, например, реализацией импликации Ф D Ф считается гёделевский номер частично-рекурсивной функции, которая каждую реализацию утверждения Ф переводит в некоторую реализацию утверждения Ф, что соответствует интуиционистскому пониманию истинности утверждения вида Ф D Ф как существования эффективного способа, позволяющего из обоснования утверждения Ф получить обоснование утверждения Ф. Реализацией универсального утверждения УяФ(ж) считается гёделевский номер частично-рекурсивной функции, которая каждое натуральное число п переводит в некоторую реализацию утверждения Ф(го), что соответствует интуиционистскому пониманию истинности утверждения вида УхФ(х) как существования эффективного способа, позволяющего для любого п получить обоснование утверждения Ф(п). Таким образом, интуиционистское понятие эффективности уточняется с помощью частично-рекурсивных функций. Однако в математике рассматриваются и другие, более узкие классы вычислимых функций — так называемые субрекурсивные классы. Представляет интерес рассмотрение и изучение вариантов реализуемости, основанных на использовании различных субрекурсивных классов функций. Этот интерес стимулируется и некоторыми известными метаматематическими результатами. Так, Нельсон [20] доказал корректность формальной системы интуиционистской арифметики НА относительно клиниевской рекурсивной реализуемости в следующем смысле: если замкнутая арифметическая формула Ф выводима в системе НА, то Ф рекурсивно реализуема. Из этого результата вытекает такой факт: если в интуиционистской арифметике выводима формула вида УхЗуФ(х,у), то существует такая рекурсивная функция /, что для любого натурального числа т истинна формула Ф(т, /(га)). В том случае, когда Ф(хуу) — примитивно рекурсивная формула, соответствующая функция / называется доказуемо рекурсивной. Таким образом, всякая доказуемо рекурсивная функция является рекурсивной. Впоследствии была получена более точная характеризация доказуемо рекурсивных функций: Крайзель показал ([18], [19]), что доказуемо рекурсивными являются в точности все < ед-рекурсивные функции, т. е. такие функции, которые могут быть получены из базисных функций с помощью операций композиции и трансфинитной рекурсии по ординалам < £q. Иначе класс < ^-рекурсивных функций может быть охарактризован как семейство всех примитивно рекурсивных функционалов типа 1. Таким образом, если в интуиционистской арифметике выводима формула видаУхЗг/Ф(ж,т/), где Ф(х,у) —примитивно рекурсивная формула, то существует такая < £о-рекурсивная функция /, что для любого натурального числа т истинна формула Ф(т, /(т)). Это наводит на мысль, что клиниевская рекурсивная реализуемость является в некотором смысле "избыточной" интерпретацией интуиционистской арифметики. По-видимому, для интерпретации интуиционистской семантики арифметических утверждений можно использовать не весь класс частично-рекурсивных функций, а лишь его собственный подкласс — семейство всех < £о-РекУРсивных функций. Эта идея была осуществлена Дамняновичем [13], который ввел понятие о-реализуемости, называемое также минимальной реализуемостью, аналогичное рекурсивной реализуемости Клини и отличающееся от нее именно тем, что вместо класса всех частично-рекурсивных функций рассматривается класс всех < £о-РекУРсивных функций. Формальная система интуиционистской арифметики НА оказалась корректной относительно минимальной реализуемости: если замкнутая арифметическая форм}гла Ф выводима в системе НА, то Ф является о~Реализуемой.

Наряду с формальной системой интуиционистской арифметики НА в теории доказательств рассматриваются различные ее подсистемы. Одна из них — система примитивно рекурсивной арифметики PRA. Она отличается от системы НА тем, что в ней используется правило индукции только для Ei-формул. Известно, что если в системе PRA выводима формула вида \/хЗуФ(х,у), где Ф(х,у) — примитивно рекурсивная формула, то существует такая примитивно рекурсивная функция /, что для любого натурального числа т истинна формула Ф(т, f(m)). Таким образом, можно сказать, что доказуемо рекурсивные в PRA функции являются примитивно рекурсивными. Дамняно-вич [12] ввел понятие строго примитивно рекурсивной реализуемости, отличающейся от рекурсивной реализуемости Клини тем, что вместо класса всех частично-рекурсивных функций рассматриваются только примитивно рекурсивные функции, и доказал, что система PRA корректна относительно строго примитивно рекурсивной реализуемости: если замкнутая арифметическая формула Ф выводима в системе PRA, то Ф является строго примитивно рекурсивно реализуемой.

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

Минимальная реализуемость и строго примитивно рекурсивная реализуемость, как и рекурсивная реализуемость Клини, могут рассматриваться как конструктивные семантики языка формальной арифметики. Для них, как и для любой семантики, представляет интерес исследование логических законов, приемлемых с точки зрения этих семантик. Логические законы выражаются посредством предикатных формул. Для каждого из рассматриваемых понятий субрекурсивной реализуемости замкнутую предикатную формулу А{Р\,. , Рп) будем называть реализуемой, если реализуема в соответствующем смысле любая замкнутая арифметическая формула А(Ф1,. , Ф„), полученная подстановкой в формулу А{Р\,., рп) арифметических формул Фь ., Фп вместо предикатных переменных Pi,., Рп. Основные результаты диссертации состоят в том, что множество всех минимально реализуемых предикатных формул и множество всех строго примитивно рекурсивно реализуемых предикатных формул не являются арифметическими.

В разделе 2 приводятся определения используемых в дальнейшем классов вычислимых функций и их нумераций, формулируются интуиционистское исчисление предикатов НРС, формальная система интуиционистской арифметиики НА и некоторые ее подсистемы.

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

В разделе 4 исследуются введенное Дамняновичем понятие < £q-реализуемости (или минимальнй реализуемости) для арифметических формул и основанное на нем понятие < £о~Реализуемой предикатной формулы. Основной результат состоит в том, что множество < £о-реализУемых предикатных формул неарифметично. Как и в случае строго примитивно рекурсивной реализуемости, рассматривается другой вариант понятия < £о-реализуемости для предикатных формул — понятие < £о-неопРовеРжим°й предикатной формулы, более точно отражающее представление о законе логики минимальной реализуемости. Множество всех < £о~неопР°веРжимых предикатных формул рекурсивно изоморфно множеству всех < £о~РеализУемых предикатных формул и потому также неарифметично.

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

Автор выражает глубокую благодарность своему научному руководителю доценту В. Б. Плиско за постановку задачи, постоянное внимание к работе, поддержку и ценные обсуждения. Автор благодарен также коллективу кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ им. М. В. Ломоносова за плодотворную обстановку и стимулирующее общение.

Список литературы диссертационного исследования кандидат физико-математических наук Пак Бен Ха, 2003 год

1. С. К. Клини, Введение в метаматематику. Москва, ИЛ, 1957.

2. А. Н. Колмогоров, Zur Deutung der intuitionisticshen Logik. Mathe-matische Zeitschrift, 1932, 35, 58 65.

3. Пак Бён Xa, Минимальная реализуемость и логика предикатов. Депонировано в ВИНИТИ 05.11.2002, №1896-В2002, 28 с.

4. Пак Бён Ха, Строго примитивно рекурсивная реализуемость и логика предикатов. Депонировано в ВИНИТИ 04.02.2003, №218-В2003, 30 с.

5. В. Е. Плиско, Рекурсивная реализуемость и конструктивная логика предикатов. Диссертация на соискание ученой степени кандидата физико-математических наук. М.: МГУ, 1973, 86 с.

6. В. Е. Плиско, Рекурсивная реализуемость и конструктивная логика предикатов. Доклады Академии Наук СССР, 1974, 214, № 3, 520 — 523.

7. В. Е. Плиско, Неарифметичность класса реализуемых предикатных формул. Известия АН СССР. Серия математическая, 1977, 41, №3, 483 502.

8. В. Е. Плиско, Формализация теоремы Тенненбаума и ее применения. Депонировано в ВИНИТИ, 1992, № 1853-В92, 52 с.

9. X. Роджерс, Теория рекурсивных функций и эффективная вычислимость. Москва, ИЛ, 1972.

10. P. Axt, Enumeration and the Grzegorczyk hierarchy. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 1963, 9, 53 -65.

11. L. E. J. Brouwer, De onbetrouwbaarheid der logische principes (Недостоверность принципов логики). Tijdschrift voor wijsbegeerte, 1908, 2, 152 158.

12. Z. Damnjanovic, Strictly primitive recursive realizability, I. Journal of Symbolic Logic, 1994, 59, 1210 -1227.

13. Z. Damnjanovic, Minimal realizability of intuitionistic arithmetic and elementary analysis. Journal of Symbolic Logic, 1995, 60, 1208 1241.

14. A. Grzegorczyk, Some classes of recursive functions. Rozprawy Matematyczne, 1953, 4, 1 46.

15. S. K. Kleene, On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 1945, 10, 109 124.

16. S. K. Kleene, Extension of an effectively generated class of functions by enumeration. Colloquium mathematicum, 1958, 6, 67 78.

17. G. Kreisel, On the interpretation of поп-finitist proofs, part I. Journal of Symbolic Logic, 1951, 16, 241 267.

18. G. Kreisel, On the interpretation of поп-finitist proofs, part II: Interpretation of number theory, applications. Journal of Symbolic Logic, 1952, 17, 43 58.

19. D. Nelson, Recursive functions and intuitionistic number theory. Transaction of American Mathematical Society, 1947, 61, 307 368.

20. H. Rose, Subrecursion: functions anf hierarchies. Clarendon Press, Oxford, 1984.

21. H. А. Шанин, О некоторых логических проблемах арифметики. Труды Математического института им. В. А. Стеклова АН СССР, 1955, 43, 1 112.

22. W. W. Tait, Infinitely long terms of finite type. I. In: Formal systems and recursive functions. North-Holland, Amsterdam, 1965, 176 185.