Конструктивные семантики логических языков, основанные на обобщенной вычислимости тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат наук Коновалов Александр Юрьевич

• Коновалов Александр Юрьевич
• кандидат наук
• 2018

Оглавление диссертации кандидат наук Коновалов Александр Юрьевич

Введение

Глава 1. Основные определения и вспомогательные утверждения

1.1 Гиперарифметические отношения

1.1.1 [Рр-описания

1.1.2 Нумерация частично-рекурсивных функций

1.1.3 Гиперарифметические отношения и Д^-индексы

1.1.4 Алгоритм Тарекого - Куратовского

1.1.5 Гинерарифметическая иерархия

1.2 Формальные языки

1.2.1 О языках первого порядка

1.2.2 Язык формальной арифметики 1_д и его расширения

1.2.3 Язык логики предикатов 1_Р

1.3 Формальные дедуктивные системы

1.3.1 Интуиционистское исчисление предикатов 1РС

1.3.2 Классическое исчисление предикатов СРС

1.3.3 Формальная арифметика РА

1.3.4 Формальная арифметика РА'

1.4 Определимость в расширениях языка 1_д

1.4.1 Определимость в языке 1_н

1.4.2 Предикаты истинности для расширений языка 1_д

1.4.3 Нумерация функций, определимых в расширениях языка 1_д

1.4.4 Отношения на множестве метаобозначений С

Глава 2. Обобщенная реализуемость для расширений языка арифметики

2.1 Понятие реализуемости для расширений языка 1_д

2.2 Классическая семантика и реализуемость

Глава 3. Реализуемость и логика предикатов

3.1 Варианты понятия реализуемости дня языка логики предикатов

3.2 Классическая логика и реализуемость

3.3 Интуиционистская логика и реализуемость

3.4 Базисная логика предикатов ВРС

3.5 Базисная логика и реализуемость

Глава 4. Реализуемость и теория множеств

4.1 Язык теории множеств 1_Б

4.2 Универсум А

4.3 Понятие реализуемости для языка теории множеств 1_Б

4.4 Теории \2Р, С1Р

4.5 Теория и реализуемость

4.6 Теория и реализуемость

4.7 Теория и реализуемость

Заключение

Указатель обозначений

Список литературы

Введение

Введение диссертации (часть автореферата) на тему «Конструктивные семантики логических языков, основанные на обобщенной вычислимости»

Актуальность темы.

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

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

Развитие конструктивной математики в свою очередь вызвано необходимость исследования соответствующей ей конструктивной логики. В математической логике логические законы выражаются посредством предикатных форму::. Имеются различные варианты понятия реализуемости для таких форму,:: (см, |11|). Семантика предикатных форму,::, основанная на понятии рекурсивной реализуемости, предполагает, что вместо предикатных церемонных подставляются формулы языка формальной арифметики. Однако было доказано |5|, что при расширении языка арифметики за счет предиката истинности для него класс реализуемых предикатных форму,:: сужается. Попытки решения проблемы выработки адекватного понятия реализуемости для предикатных форму,::, независимого от языка, в котором формулируются предикаты, подставляемые вместо предикатных церемонных, привели к понятию абсолютно реализуемой предикатной формулы |7|, Оказалось, что множество всех абсолютно реализуемых предикатных формул является П}-полнь:м. П-множества соответствуют перечислимым множествам в контексте так называемой гинерарифмотической вычислимости. Как отмечается в |4, § 16,5|, гинерарифмотическая вычислимость может служить фундаментом для естественного расширения конструктивной точки зрения. Поэтому представляет интерес рассмотрение конструктивных семантик, основанных на различных видах обобщенной вы чис л имоети,

Интуиционистская критика классической математики затронула и понятие множества, С точки зрения интуиционизма приемлемы следующие два способа определения множества: 1) посредством задания способа порождения его элементов; 2) посредством указания свойства, которое характеризует элементы множества. Если множество определяется посредством указания свойства, характеризующего элементы этого множества, то соответствующее свойство называется видом, а всякий объект, обладающий этим свойством, называется членом данного вида, В связи с построением конструктивной математики представляет интерес рассмотрение конструктивных семантик дня теории множеств, основанных на видах, разрешимых с точки зрения обобщенной вычислимости.

Цели и задачи работы.

Определить и исследовать понятие реализуемости дня форму:: языка арифметики и его расширений, основанное на использовании вычислимых в обобщенном смысле функций как конструктивного способа получения одних реализаций из других. Определить и исследовать понятие реализуемости предикатных форму::, основанное на обобщенной вычислимости. Определить и исследовать понятие реализуемости форму,:: языка теории множеств, основанное на гинерарифметических предикатах.

Основные результаты.

Для уточнения понятия (обобщенной) вычислимости в диссертации фигурируют следующие классы функций:

— Р[ класс всех примитивно рекурсивных функций;

— [[ — класс всех частично-рекурсивных функций;

— [[[/]— класс всех функций, частично-рекурсивных относительно /, оде f — произвольная всюду определенная функция типа N ^ N

А

— А[Х] — класс всех функций, определимых в формальной арифметике, расширенной при помощи предиката Рх (х) ^ х € X, оде X — произвольное подмножество N.

— Н — класс всех гиперарифметических функций.

Для каждого такого класса функций V фиксируется гёделева нумерация и вводятся обозначения: — множество всех гёделевых номеров всех п-местных функций из класса V, <£>у'п — п-местная функция из класса V с гёделевым номером г. Для каждого класса Ш € {А, Н} и |А[Х ] | X С ^определяется расши рение языка формальной арифметики, в котором выразимыми оказываются в точности функции из класса Ш. По аналогии с клиниевской реализуемостью [ ] определяется условие «натуральное число е У-реализует замкнутую формулу Ф языка обозначаемое так: е тущ Ф- При этом случай, когда формула Ф является импликацией или начинается с квантора всеобщности, разбирается в духе Р[

— е г Ухх,... ,хп (Ф(жь ... ,хп) ^ Ф(жь ... ,хп)) ^

[е € и для всех натуральных чисел з и а\,... ,ап имеет место

5 гу№ Ф(аь ... ,ап) !у>е'п+1 («ъ ... ,ап,в) и ру'п+1(а1,... ,ап, в) гу№ Ф(аь ..., ап)],

если п ^ 0;

— е Ух\,... ,хп Ф ^ [е гущ ... ,хп (Т ^ Ф)], если п > О, формула Ф не начинается с квантора V, и логическая связка ^ не является глав ной в Ф,

Понятие У-реализуемости распространяется на предикатные формулы. Замкнутая предикатная формула называется V-реализуемой относительно Ш-оценок, если любой ее замкнутый пример в языке оказывается У-реализуем, По аналогии с абсолютной рекурсивной реализуемостью (см, [ ]) определяется абсолютная У-реализуемость, Зафиксируем 0 = М С N и временно обогатим язык логики предикатов константами из множества М. Пусть задано условие «натуральное число е У-ре^изует фор мулу Ф» для всех атомарных Ф

ременных множество М, это условие распространяется на остальные высказывания Ф языка логики предикатов по аналогии с определением У-реализуемости для арифметических формул, Замкнутая предикатная формула называется абсолютно V-реализуемой в области М, если она оказывается У-ре^изуемой независимо от того, как была задана У-реализуемость для атомарных высказываний при обогащении языка логики предикатов константами из М. Замкнутая предикатная формула называется абсолютно V-реализуемой, если она абсолютно У-реализуема в любой области. Абсолютно У-реализуемая (в области М) предикатная формула называется равномерно абсолютно У-ре^изуемой (в области М), если существует единая реализация этой формулы для всех способов задания У-реализуемости на атомарных высказываниях при обогащения языка логики предикатов константами (из М).

Понятие У-реализуемости распространяется на формулы языка теории множеств. Определяется множество А С М, называемое универсумом, которое обладает следующими свойствами:

А

— если г — гиперарифметический индекс отношения И (в, х), то имеет ме сто г € А тогда и только тогда, когда все натуральные числа ж, удовлетворяющие условию Зв И(8,х),

А

АФ

этого языка определяется условие «натуральное число е У-ре^изует Ф в универсуме А»:

— е гД (а = Ь) ^ [а = &];

— е гД (а € Ь) ^ Оь(е, а),

где Дг(в, х) — гиперарифметическое отношение, гиперарифметический индекс которого есть г. Полагая областью значений связанных переменных множество А, это условие распростра-

Ф

У-реализуемости для арифметических формул.

Базисная логика предикатов ВРС определяется в [ ], Конструктивная теория множеств С7Р описана в [21], Интуиционистская теория С7Р- определяется как С7Р без аксиомы объемности. Модификацию теории С7Р-, в которой вместо интуиционистской логики используется базисная, обозначим С7Р-,

Результаты диссертации состоят в следующем:

1, Пусть Ш есть или А, или А[Х] для некоторого X, или Н, а V есть или А, или А [У] для некоторого У, или Н, или Щ}'] для некоторого /, и при этом класс V содержит

все функции из класса Ш. Тогда для расширения языка арифметики 1_ щ семантика У-реализуемости совпадает с классической семантикой (теорема ),

2, Пусть Ш есть или А, или А[Х] для некоторого X, или Н, а V есть или А, или А [У] для некоторого У, или Н, или [/] для некоторого /, и при этом класс V содержит все функции из класса Ш. Произвольная замкнутая предикатная формула является У-ремизуемой относительно ^-оценок тогда и только тогда, когда она выводится в классическом исчислении предикатов (теорема 3).

3, Пусть V есть или А, или А[Х] для некоторого X, или Н, или для такой функции /, что класс содержит все арифметические функции. Тогда всякая (равномерно) абсолютно У-ремизуемая (в области N предикатная формула выводится в классическом исчислении предикатов (теорема 4), Отметим, что в случае обычной рекурсивной реализуемости это не так (см, |3|, |6, теорема 3|),

Р[ А

не выводится в классическом исчислении предикатов (теорема 5),

5, Пусть V есть или А, или А[Х ] (для некотор ого X), ил и Н, Тогда высказывание Ух ((Т ^ Р(ж)) ^ Р(х)) не является абсолютно У-реадизуемым в области N (теорема 6), Это означает, что интуиционистское исчисление предикатов некорректно относительно абсолютной У-реализуемости (теорема ),

6, Пусть V есть или Р[ или [или [/] для некоторого /, или ^^и А[Х] для некоторого X, ил и Н, Тогда принцип Маркова в форме

Ух (Т ^ Р(х) V -Р(х)) ^ (--Эх Р(х) ^ Эх Р(х))

является абсолютно У-реализуемым (теорема ), и не является равномерно абсолютно У-реализуемым (теорема ),

7, Пусть V есть или ^^и ] для некотор ого /, ил и А, или А[Х ] для некотор ого X,

Н

Ух (Т ^ Р(х) V -Р(х)) ^ (--Эх Р(х) ^ Эх Р(х))

является равномерно абсолютно У-ремизуемым в области N (теорема ), Это означает, что существует такая замкнутая предикатная формула, которая не выводима в интуиционистском исчислении предикатов, однако, является абсолютно У-ремизуемой и равномерно абсолютно У-ремизуемой в об ласти N (теорема ),

8, Пусть V есть или [или [/] для некоторого /, или А, или А[Х] для некоторого X, или Н, Всякая замкнутая предикатная формула, выводимая в базисной логике предикатов ВРС, является равномерно абсолютно У-реализуемой (теорема ),

9, Пусть V есть или [или ] для некоторой гиперарифметическо й функции f. Тогда всякая замкнутая формула языка теории множеств, выводимая в теории С7Р-, является У-ремизуемой в универсуме Д (теорема ),

10, Пусть V есть или А, или А[Х] для некоторого гиперарифметического множества X. Найдется замкнутая формула языка теории множеств, выводимая в теории С7Р-, которая не является У-ремизуемой в унив ерсуме Д (теорема ),

11. Пусть V есть или А, или А[Х] для некоторого гиперарифметического множества X. Тогда всякая замкнутая формула языка теории множеств, выводимая в теории С7Р-, является У-ре^низуемой в универсуме А (теорема ),

12. Пусть V есть или Р[ или или [[[/] для некоторого ^и ^^и А[Х] для некоторого X, или Н. Тогда высказывания Ух, у (Vz (г € х о г € у) ^ х = у) (аксиома объемности) и Уу ЗгУх (х € г о V« (и € х ^ и € у)) (аксиома степени) не являются У-ре^изуемыми в унив ерсуме А (теорема ),

Теоретическая и практическая ценность.

Работа имеет теоретический характер и представляет научный интерес дня занимающихся неклаееическими логиками и вопросами реализуемости. Техника, разработанная автором, может быть использована и в других аналогичных случаях.

Апробация работы и публикации автора.

Основные результаты работы докладывались па международных конференциях «Восьмые Смирновские чтения но логике» (Москва, июнь 2013 г.), «Конструктивная теория доказательств» (Москва, февраль 2014 г.), «Десятые Смирновские чтения но логике» (Москва, июнь 2017 г.) и па семинарах «Научно-исследовательский семинар по математической логике», «Вычислимость и некласеичеекие логики» (Механико-математический факультет МГУ им, М. В, Ломоносова),

Основные результаты но теме диссертации изложены в 6 печатных изданиях |12, 13, 14, 15, 16, 17|, 4 из которых изданы в журналах, рекомендованных ВАК 113, 14, 15, 16|, 2 — в тезисах докладов 112, 17|,

Благодарности.

Автор выражает глубокую благодарность своему научному руководителю Валерию Егоровичу Плиско за постановку задачи, постоянное внимание, поддержку в работе, обсуждения и цепные советы.

Автор благодарен В, Б, Шехтману, В, Н, Крунскому, Л, Д. Бсклсмишсчзу, Т, Л, Яворской и другим сотрудникам кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ им, Ломоносова за преподавание основ математической логики и стимулирующее общение.

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

Автор выражает благодарность своему школьному учителю математики Лилии Николаевне Пановой, которая пробудила в нем интерес к занятию математической логикой.

Автор благодарен протоиерею Сергию Правдолюбову, иерею Владимиру Мандзюк-Пль-пицкому, иерею Максиму Крижевскому и всему приходу Храма Живоначалыюй Троицы в Троице-Голенищево за поддержку.

Структура диссертации.

Диссертация состоит из введения, четырех гнав, заключения, указателя обозначений и списка литературы из 25 наименований, включая 6 работ автора. Общий объем диссертации составляет 137 страниц, включая 131 страницу основного текста.

Глава 1. Основные определения и вспомогательные утверждения 1.1 Гиперарифметические отношения 1.1.1 [р-описания

Будем использовать следующую общеупотребительную символику дня замены слов и словосочетаний естественного языка: ^ — «есть по определению»; У — «для всех»; Э — «существует»; — «тогда и только тогда, когда»; ... ... — «если ..., то ...»•, - — «неверно, что»; ^ — «тогда и только тогда, когда»; ... ^ ... — «если ..., то ...»•, Л — «и»; V — «или». Символ □ означает конец доказательств. По средством N обозначаем множество натуральных чисел {0,1, 2,...}. Через V(^ обозначим множество всех подмножеств множества N. Если / — частичная функция типа ^ N и к]_,... ,кп — натуральные числа, то тот факт, что определено / (к1,..., кп), обозначаем так: !f(к1,..., кп).

Частичная функция типа ^ N называется частично-рекурсивной (п ^ 0), если она может быть получена с помощью операций подстановки, рекурсии и минимизации из следующих исходных функций: константы 0, функции прибавления единицы Б и семейства функций проекции 1гт (т = 1, 2,,,., 1 ^ г ^ т). Частично-рекурсивные функции, которые могут быть получены из исходных функций без использования операции минимизации, называются примитивно рекурсивными. Всюду определенные частично-рекурсивные функции называются

[

Р[

Частичная функция типа ^ N (п ^ 0) называется частично-рекурсивной относительно ... Д, оде f1,..., ¡к — всюду определенные функции натурального аргумента, если она может быть получена с помощью операций подстановки, рекурсии и минимизации из функций Д,... Д и исходных функций. Посредством Т обозначаем множество всех всюду определенных функций типа N ^ N. Для всех / € Т функции, частично-рекурсивные относительно /, будем называть [[[/]-функциями.

Как и в |8|, будем обозначать примитивно рекурсивные функции словами в алфавите

Лрн = {0, Я, 4 (т =1, 2,..., 1 ^ г ^ т), С, И,}, а частично-рекурсивные функции — словами в алфавите

Лк = Лрк и {М}.

Кроме этого, если фиксирована функция $ € Т, то [[/]-функции будем обозначать словами в алфавите

Л = Лк и {Г}.

Дня этого введем следующие определения.

Определение 1. Для всех натуральных чисел п индукцией то длине слова 7 алфавита Л определим условие «7 есть п-местное Rp-опиеание»:

— 0 есть 0-местное Rp-описание;

— F есть 1-местное Rp-описание;

— S есть 1-мест ное Rp-описание;

— 1гт есть m-местное RP-onncaHne;

— если а есть m-местное RP-onHcanие (т ^ 1), а ßi,..., ßm суть n-местные RP-onncanHH (п ^ 0), то Caßi... ßm есть n-местное RP-onHcaHHe;

— если а есть n-местное RP-onHcanие (п ^ 0), a ß есть (п + 2)-местное RP-onHcanne, то Käß есть (п + 1)-местное RP-onncaHne;

— если а есть (п + 1)-местное RP-onHcanие (п ^ 0), то Мо есть n-местное RP-onHcanHe, Будем говорить, что а — RP-onwcaHwe, если для некоторого натурального числа п, которое назовем валентностью RP-onncaHия о, а является n-местным RP-onncaHneм, RP-onHcaHHH,

F R R

торых нет символа М, будем называть PR-описаниями.

Определение 2. Пусть f е Т. Для каждого n-местного RP-onHcanия 7 (п ^ 0) определим n-местную частичную функцию 7^ следующим индуктивным образом:

— F/ ^ /;

— 0/ ^ 0;

- Sf есть функция прибавления единицы S, т, е, Sf (х) — х + 1;

f f _ (Im) есть функция проекции Т, е■ (Im) (ЖЬ . . . ,Xm) — xi]

- (C aß-,... ßm) f есть функция, пленная суперпозицией из фу икцпй а-, ß( ,...,ßL т, е, имеет место условное равенство

(Caßi. ..ßm )f (xi,... ,xn) — af (ßf (xu ... ,xn),..., ßfm (жь ... ,xn)),

где n — валентность RP-onncaHия Caßi... ßm',

— (Roß)f есть функция, полученная из функций of и ßf примитивной рекурсией, т. е. выполняются соотношения

('Raß)f (xi,..., xn, 0) — af (xi,..., xn),

(Roß)f(xi,... ,Xn,Xn+1 + 1) — ßf(xi,... ,Xn,Xn+1, (Raß)f(xx,... ,xn,xn+1)),

где n — валентность RP-onHcaHия Roß;

— (Ma)f есть функция, полученная из функции af операцией минимизации, т. е. имеет место условное равенство

(Ma)f (жь ... ,х,п) — ßy [af (хг, ...,х,п,у) = 0],

где п — валентность RP-onncanия Мо,

Как видно из приведенного выше определения, если [-описание 7 не содержит символа Г (т. е. является [описанием), то для всех /ь/2 € Т имеет место ^^ = 'у^2. Следовательно,

для всех [описаний 7 корректно определение 7* ^ 7 где f € Т. Будем говорить, что а есть [описание (Р[описание) фун кции если а ест ь [описание (Р[описание) на* = <р.

Связь между [-описаниями и частично-рекурсивными функциями устанавливается при помощи следующих предложений, которые легко могут быть доказаны индукцией по построению соответствующих объектов,

Предложение 1. Пусть f € Т. Справедливы следующие утверждения.

1. Если а — [-описание, то а? — ]-функция.

2. Если, ф — }-функция, то найдется такое [р-описание а, что ф = а?.

Предложение 2. Справедливы следующие утверждения.

1. Если а — [-описание, то а* — [функция.

2. Если ф — [-функция, то найдется такое [описан ие а, что ф = а*.

Предложение 3. Справедливы следующие утверждения.

1. Если а — Р[описание, то а* — Р[-функция.

2. Если ф — Р[-функция, то найдется такое Р[-опи,сание а, что ф = а*.

Фиксируем примитивно рекурсивную взаимно-однозначную функцию с, кодирующую пары натуральных чисел натуральными числами. Например, определим с как в [ , §5,3]:

с(и, ь) ^ и2 + 2иу + V2 + 3и + ь).

Тогда «обратные» одноместные функции р1 и р2, оде р1(ж) и р2(х) суть первая и вторая компоненты пары с кодом ж, т. е.

с(Р1 (x), Р2(^)) = ж,

также примитивно рекурсивны. Для любого натурального п > 0 с помощью функции с индуктивно определяется функция сга, взаимно-однозначно отображающая N на N

с1(х) ^ х; сп+1(х1,... ,хп+1) ^ с(сп(х1,... ,хп),хп+1).

Посредством р™,..., р™ обозначим одноместные функции, «обратные» к сга, т. е.

сп(рпг(х),..., рпп(х)) = X, (1.1)

которые также примитивно-рекурсивны,

В выражениях вида р1 (¿), р2(£), р™(£) и т. п. обычно будем опускать скобки. На множестве Т определим двухместную операцию ф, положив

(/1 Ф /2)М ^ с(/1(т),/2(т))

для всех натуральных чисел т. Вместо ((... ф ...) ф /га-1) Ф ¡п будем пнеать /1 ф ... ф ¡п. Таким образом, для всех /)_,...,/„, € Т имеет место:

(/1 ф ... ф и)(х) = сп(Ш,..., Ш). (1.2)

Нетрудно видеть, что для всех ..., /п € Т класс всех [[/1 ф ... ф /га]-функций совпадает с классом всех функций, частично-рекурсивных относительно ..., Из этого факта и предложения 1 получаем следующее утверждение.

Предложение 4. Пусть ..., /п € Т. Справедливы следующие утверждения.

1. Если а — [Р-описание, то а^1®---®^ — функция, частично-рекурсивная относительно ¡1,...,!п-

2. Если ф — функция, частично-рекурсивная относительно ..., ¡п, то найдется такое [,Р-описание а, что ф есть аЛ®---®.

1.1.2 Нумерация частично-рекурсивных функций

Пусть фиксирована гёделева нумерация Rp-описаний, Это означает, что фиксирован алгоритм, который каждому Rp-описанию сопоставляет некоторое натуральное число, называемое его гёделевым номером, причем по каждому натуральному числу г можно алгоритмически проверить, является ли оно гёделевым номером какого-либо Rp-описания, и найти это Rp-описани е. Rp-описание, гёделев номер кото poro есть z, обозначаем через 7z, Есл и а — Rp-описание, то его гёделев номер обозначаем через Таким образом, если г есть гёделев номер RP-onncaHия а, то z = гоп, и = а.

Для всех натуральных чисел п ^ 0 определим следующие множества:

Gp ^ |г«п | а — RP-onncaHие n-местной функции}, GR ^ |г«п | а — R-описан ие n-местной фун кции}, GpR ^ |г«п | а — PR-описан ие n-местной фун кции}.

Очевидно, что все эти множества перечислимы (и даже разрешимы), В силу тезиса Черча дня всех натуральных чисел п ^ 0 найдутся одноместные общерекурсивные функции gp, g^ , gp r, которые осуществляют бесповторный пересчет множеств Gp, GR, GpR соответственно.

Для всех натуральных чисел п, z определим частичную функцию ^pR'n типa Nn ^ N следующим образом:

</z ^^Ъ ...,Хп) ^ 7*п^)(ЖЬ . ..,хп).

Из предложения следует, что частичная функция р тап a Nn ^ N является примитивно

« « PR п

рекурсивной тогда и только тогда, когда найдется такое натуральное число z, что р = R'n, Будем говорить, что натуральное число z есть примитивно рекурсивный индекс (сокращенно PR-индекс) функ ции р тап a Nn ^ N если имеет м есто р = ^pR'n.

Для всех натуральных чисел п, z определим частичную функцию pR'n тап a Nn ^ N следующим образом:

. . . , Xn) ^ lgr^(z) (xl, . . . , Xn).

Из предложения следует, что частичная функция <р тап a Nn ^ N является R-функцией

R n

тогда и только тогда, когда имеет место р = для некоторого натурально го числа г. Будем говорить, что натуральное число z есть частично-рекурсивный индекс (сокращенно R-индекс) функ ции р тап a Nn ^ N если имеет м есто р = <pR'n.

Замечание 1. Введенная выше нумерация частично-рекурсивных функций является допустимой в смысле терминологии из |4, упр. 2-10|. Из |4, упр. 2-10, 11-121 следует, что такие результаты из книги [ ], как теорема о нумерации (см, [ , §1,8 теорема IV]), ( s—т—п)-теорема (см, |4, §1,8 теорема V|), теорема о рекурсии (см, |4, §11.2 теорема Ш|), остаются справедливыми при замене нумерации частично-рекурсивных функций, принятой в |4|, на нумерацию, введенную выше.

Для всех f е Т и натуральных чисел п, z определим частичную функцию типа

Nn ^ N следующим образом:

pR[/ í'n(x1, ...,Xn) ^ Т^^ь ...,Xn). Из предложения следует, что частичная функция p типа Nn ^ N является Rf/J-функцией

R[ f ],n

тогда и только тогда, когда имеет место p = pz для некоторого натурального числа г. Будем говорить, что натуральное число г есть R[/]-индекс функции p тап а Nn ^ N, если

R[ f ],n

имеет место p = pz .

Замечание 2. В [ ] R^-функциям имеется соответствие в виде А-частичнорекурсивных функций (А С N), А именно, произвольная функция p являет ся R[/]-фyнкциeй тогда и только тогда, когда p есть X[/]-частичнорекурсивная функция, где X[/] = {c(x, у) | f(x) = у}. R[ ] R[ ]

X[ ]

X[ ] R[ ]

А

сят от принятой в |4| нумерации, естественным образом преобразуются в утверждения о R[ ] R[ ]

R[ ]

( — т — п)

типизованный аналог теоремы III из |4, §11.2| (теоремы о рекурсии).

Для каждых натуральных чисел к^ 1, п ^ 0и z е G^ определим частичную функцию pk,n типа тк х Nn ^ N следующим образом:

pkz'n( fi,..., fk ,Xi,...,Xn) ^ (Xl, ...,Xn).

Частичная функция p тап а Тк х Nn ^ N (к ^ 1, п ^ 0) называется частично-рекурсив-нои, если найдется такое натуральное число г е G^, что p есть p'k'n. В этом случае говорят, что z является частично-рекурсивным индексом (сокращенно R-нндексож) функции p.

Замечание 3. В |4| принята нумерация частично-рекурсивных функций с функциональными переменными (см. |4, §15.2|), основанная на специфической формализации понятия относительной рекурсивности в |4, §9.2|. В |4, §9.21 описываются также альтернативные, эквивалентные принятой в качестве основной в |4|, формализации понятия относительной рекурсивности, среди которых присутствует и формализация с помощью машин с оракулом. Используя предложение 4 и |2, §69 Теорема XXX|, можно показать, что класс частично-рекурсивных

функций типа Тк х N ^ N (к ^ 1, п ^ 0) не зависит от того, определяется ли он при помо-

[Р

машип с оракулами.

Определим множество метаобозначений Ск следующим образом:

Ск ^ {Р[ [} и {[[/] | f €Т}.

В выражениях вида р1к'п, и т- п- обычно будем опускать второй верхний

индекс там, где он может быть восстановлен из контекста.

Предложение 5 (теорема о нумерации). Пусть V € Ск и V = Р[ Для, каждого натурального числа п найдется такая (п + 1)-местная V-функция ф, что имеет место

ф{г,хъ ... ,хп) — рух (жь ... ,хп). (1.3)

Доказательство. См, [ , §1,8 теорема IV], □

Предложение 6 ((в — т — п)-теорема). Пусть V € Ск и V = Р[ Для, всех натуральных чисел т, п найдется такая общерекурсивная функция б™, что имеет место

<Рц?(2,у1 ---.,ym)(xl,...,хп) - (У\,...,Уш ,^,...,Хп). (1.4)

□

Предложение 7 (теорема о рекурсии). Пусть V € V = Р[ и f — общерекурсивная, функция типа Мш+1 ^ N Для, каждого натурально го числа п найдется такая общерекурсивная функция д тип а, ^ N что имеет место

v,n _ v,n /-1 r\

^f(g(ki,...,km),ki,...,km) ^g(ki,...,km) V " >

для, всех натуральных чисел k\,... ,km.

Доказательство. См, [ , §11,2 теорема III], □

1.1.3 Гиперарифметические отношения и Д{-индексы

Всякий раз, когда мы говорим об отношениях на Тк х Мп, подразумевается, что для натуральных чисел к, п выполняется соотношение к + п > 0, т. е, натуральные числа к, п могут быть равны нулю, но не оба одновременно. Отношения на Тк х Мп будем записывать при помощи предикатных форм вида Д(/ь ..., ¡к,Х\,..., хп). Выражение Д(/,ж) используем как сокращение для Д(/ь ..., ¡к,Х\,..., хп), подразумевая, что f = ¡\,..., ¡к ш х = Х\,... ,хп для некоторых натуральных чисел кип.

Характеристическая функция хя произвольного отношения Я на Тк х Мга определяется следующим образом:

I 1, если Я( ¡ъ..^ ¡к ,хг,...,хп); Хя( h,..., !к ,х1,...,хп) ^ <

Список литературы диссертационного исследования кандидат наук Коновалов Александр Юрьевич, 2018 год

Список литературы

|1| Н, А. Шанин. О некоторых логических проблемах арифметики. Тр. МИАН, 1955, т. 43, стр. 1—112.

|2| С. К. Клини. Введение в метаматематику. М.: ИЛ, 1957.

|3| В. П. Оревков, Связь конструктивной общезначимости с выводимостью в классическом исчислении, предикатов. Всесоюзный симпозиум но матом, логике (тезисы докладов), Алма-Ата, 1969, стр. 35.

|4| X. Роджерс. Теория рекурсивных функций и эффективная вычислимость. М,:«Мир», 1972.

|5| В. Е. Плиско. Рекурсивная, реализуемость и конструктивная, логика предикатов. ДАН, 1974, т. 214, Л» 3, стр. 520-523.

|6| В. Е. Плиско. Неарифметичпостъ класса реализуемых предикатных формул. Изв. АН СССР. Сер. мат., 1977, т. 41, Л» 3, стр. 483-502.

|7| В. Е. Плиско. Абсолютная, реализуемость предикатных формул. Изв. АН СССР, Сер. матем, 1983, т. 47, .К2 2, стр. 315—334.

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

|9| Д. А. Витер, Примитивно-рекурсивная, реализуемость и логика предикатов. Депонировано в ВИНИТИ, Л» 1830-В2001. М., 2001.

|10| Д. А. Витер. Примитивно-рекурсивная реализуемость и конструктивная теория моделей: Канд. дис. М,, 2001.

|11| В. Е. Плиско. Обзор предикатной логики реализуемости. Тр. Матем. ип-та им. В. А. Стеклова, М.: МАИК «НАУКА/ИНТЕРПЕРИОДИКА», 2011, т. 274, стр. 222-251.

|12| А. Ю. Коновалов. Понятие арифметической реализуемости. Восьмые Смирновские чтения: материалы Между нар. науч. конф., Москва, 19-21 июня 2013 г.

|13| А. Ю. Коновалов, В. Е. Плиско. О гиперарифметической реализуемости. Матем. заметки, 2015, т. 98, JY2 5, стр. 725—746. (основные результаты принадлежат .лично А. Ю. Коновалову; постановка задачи и определения принадлежат В. Е. Плиско.) D01:10.4213/mzml0735.

|14| А. Ю. Коновалов. Арифметическая реализуемость и базисная, логика. Вести. Моск. ун-та. Матем. Мехап., 2016, Л* 1, стр. 52-56. D01:10.3103/S0027132216010071.

|15| А. Ю, Коновалов. Арифметическая реализуемость и примитивно-рекурсивная, реализуемость. Вести. Моск. ун-та. Матем, Механ,, 2016, JY2 4, стр. 60-64. DOI: 10.3103/S002 7132216040069.

|16| А. Ю. Коновалов. Семантика реализуемости для, конструктивной теории ,множеств, основанная, на гиперарифметический предикатах. Вести. Моск. ун-та. Матем. Механ., 2017, Л* 3, стр. 59-62. D01:10.3103/S0027132217030068.

|17| A. Yu. Konovalov, V. Е. Plisko. Realizability Semantics for the. Predicate Formulas Based on Generalized Computability. Десятые Смирновские чтения: материалы Между нар. науч. конф., Москва, 15-17 июня 2017 г.

|18| L. Е. J. Brouwer, De onbe.trouwbaarhe.id de.r logische. principes (Недостоверность принципов логики). Tijdsehrift voor wijsbegeerte, 1908, 2, 152—158.

|19| A. H. Колмогоров. Zur Deutung de.r intuitionisticshen Logik. Math. Z. 1932, 35, 58-65.

1201 S. K. Kleene. On the interpretation of intuitionistic number theory. Journ, Symbolic Logic. 1945, 10, 109-124.

|21| P. Aczel. The type, theoretic interpretation of constructive, set theory. Log. Coll. 1978, 77, 55-66.

1221 W, Ruitenburg. Basic, predicate, calculus. Xotre Dame J. Formal Logic. 1998, 39, X 1. 18-46.

1231 M. Ardeshir, A Translation of Intuitionistic Predicate Logic, into Basic Predicate Logic. Stud. Log. 1999, 62, 341-352.

|24| S. Salehi, Primitive, recursive realizability and basic arithmetic. Bull. Symbol. Logic. 2001, 7, X 1, 147-148.

|25| S. Salehi. Provably total functions of basic arithmetic. Math. Log. Quart. 2003, 49, X 3, 316-322.