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

Оглавление
I Введение. З
II Примитивно рекурсивная реализуемость. 13
1. Интуиционистские и базисные формальные системы. 13
1.1. Язык логики предикатов...................................... 14
1.2. Интуиционистское исчисление предикатов НРС.................. 13
1.3. Секвенциальное интуиционистское исчисление предикатов К^С. 16
1.4. Язык формальной арифметики.................................. 13
1.5. Интуиционистская формальная арифметика НА................... 18
1.6. Базисная логика предикатов ВС^С............................. 19
1.7. Базисная арифметика ВА...................................... 21
1.8. Связь базисной логики с интуиционистскими системами......... 22
2. Примитивно рекурсивная реализуемость. 28
2.1. Определения и основные факты................................ 28
2.2. РИ-реализуемость ”по Салехи”................................ 31
2.3. РИ-реалиэуемость япо Клини”................................. 37
2.4. Понятие РИ-реадиэуемости для предикатных формул............. 49
2.5. Обшая схема доказательства основного результата............. 32
3. Формализация теоремы Тенненбаума 33
3.1. Теория Т.................................................... 33
3.2. Теория Г.................................................... 57
3.3. Теория Ґ1................................................... 57
3.4. РН-реализуемость усилении аксиомы индукции.................. 73
4. Неарифметичность множества всех РГ1-реализуемых предикатных формул. 86
5. Неарифметичность множества всех РИ-пеопровержимых предикатных формул. 97
III Конструктивная теория моделей. 1°3
6. Обобщенные предикаты и обобщенные системы. ЮЗ
і
7. Конструктивные теории нумерованных моделей. 112
8. Конструктивная теория равенства. 130
8.1. Рефлексивные системы....................................130
8.2. Конструктивные теории разрешимого равенства.............131
8.3. Неполнота теорий неразрешимого равенства................143
2
Часть 1
Введение.
Диссертация посвяшена исследованию некоторых вопросов конструктивном математической логики.
В начале XX века в математике возникло интуиционистское направление как положительным аспект предпринятой Брауэром [1] критики классической математики в связи с обнаружением в последней теоретико-множественных парадоксов. Интуиционистская критика затронула и классическую логику. Начиная с работ А. Н. Колмогоров.!, Гейтннга, В. И. Глнвенко, относящихся к концу 20-х — началу 30-х годов, большое внимание уделяется построению и исследованию логических систем, корректных с точки зрения интуиционизма. По мере развития математики и математической логики исследования по интуиционистской логике не только не утратили свою актуальность, но, напротив, наполнялись новым содержанием. Так, еще в 30-е годы А. Н. Колмогоров [2] показал, что интуиционистская логика имеет реальный смысл, не связанный с философскими установками Брауэра, если рассматривать ее как логику решения задач. В 40-е годы американский математик С. К. Клинп (3] предложил интерпретацию ряда специфических интуиционистских понятий на основе разработанных к тому времени концепций теории алгоритмов. В частности, Клннн ввел понятие рекурсивной реализуемости для формул языка арифметики первого порядка с целью уточнения интуиционистского смысла арифметических суждений на основе теории рекурсивных функций (см. [5. § 82]). Это понятие послужило отправной точкой для разработки конструктивной семантики математических утверждений, использованной в рамках конструктивного подхода к математике в работах А. А. Маркова и его школы [4]. Развитие конструктивной математики в свою очередь вызвало необходимость исследования соответствующей ей конструктивной логики. Наконец, исследования последи их лет в области теоретического программирования выявили особую роль конструктивной логики в вопросах синтеза программ, поскольку использование этой логики в математических построениях позволяет сделать явными их алгоритмические ч вычислительные аспекты. Процедуры извлечения алгоритмов из интуиционистских доказательств обычно используют конструктивные сехиштпки логпко-математических языков. Поэтому конструктивная логика считается одним из актуальных направлений современной математической логики.
В конструктивной логике (как и в клиниевском определении реализуемости) интуиционистское понятие эффективности уточняется с помощью рекурсивных функций. В математике рассматриваются также другие, более уз-
з
кие классы вычислимых функции, например, примитивно рекурсивные функции. По аналогии с клиниевской реализуемостью можно определить понятие примитивно рекурсивной реализуемости. В первой части диссертации рассматривается семантика арифметических и предикатных формул, основанная на примитивно рекурсивной реализуемости. Исследуется множество примитивно рекурсивно реализуемых предикатных формул и доказывается его неарифме-тичность.
В последние годы в работах В. Е. Плиско [12] была начата разработка теории моделей, основанной на конструктивной семантике типа рекурсивной реализуемости. Во второй части диссертации эти результаты обобщаются для других типов конструктивной семантики, в частности, для примитивно рекурсивной реализуемости. Средствами конструктивной теории моделей исследуются конструктивные теории нумерованных алгебраических систем, в частности, конструктивные теории так называемых обобщенных алгебраических систем в минимальной сигнатуре е, содержащей лишь символ равенства. Определяются условия совпадения таких конструктивных теорий с классической теорией равенства.
Введем необходимые определения.
Примитивно рекурсивными называются функции, которые можно получить с помощью операций подстановки и рекурсии из следующих исходных функций: константы I), операции прибавления единицы 6' и семейства функций проекции Гт (т = 1. 2,..., 1 < I < г?»).
Функции, получающиеся из исходных функций с помощью операторов подстановки. примитивной рекурсии н минимизации, называются частично-рекурсивными.
Определим способ описания и геделевской нумерации частично-рекурсивных п примитивно рекурсивных функций. Как и в работе [13]. будем обозначать частично-рекурсивные и примитивно рекурсивные функции как слова в алфавите
О, 8, ^ (ш = 1,2,..., 1<1<га), С, II, М, которые строятся по следующим правилам:
1) 0 есть 0-ыестный функциональный символ;
2) 5 есть одноместный функциональный символ;
3) 1]п есть т-местнын функциональный символ (т = 1,2,..., 1 < * < т);
4) если / есть т-местнын функциональный символ (т > 1). а 51,______</,„
4
суть п-местные функциональные символы (п > 0), то С/$ц ...дт есі'ь п-местный функциональный символ;
5) если / есть п-местнын функциональный символ, а д есть (г* + 2)-местный функциональный символ (п > 0), то Rfg есть (п + 1)-местный функциональный символ;
6) если / есть (и + 1)-местньга функциональный символ (n > 1). то М/ есть п-местнын функциональный символ.
Символы 0. S и 1^ считаются обозначениями соответствующих исходных примитивно рекурсивных функций. Запись вида Cfgi. ..дт — ото обозначение функции, полученной суперпозицией из функций, обозначенных посредством /* Функциональный символ Rfg есть обозначение для функции, по-
лученной рекурсией из функций, обозначенных через / и д. Функциональный символ М/ есть обозначение для функции, полученной операцией минимизации из функции /, т. с.
M/(*i*/iy(/(y,xi“О].
Если оператор минимизации не использовался (т. с. буква М не входит в состав * кодирующего” слова), то выражаемая таким словом частично-рекурсивная функция является примитивно рекурсивной.
Зафиксируем геделевскую нумерацию частично (примитивно) рекурсивных функций, как слов в описанном выше алфавите. Примитивно рекурсивную функцию с геделевским номером X обозначаем через фТ.
Часто для обозначения функций и их геделевскнх номеров мы будем использовать так называемые Л-обоэначения (см. [о, § 10]), а именно:
• Пусть /(.т) есть числовая форма от одной переменной х (например. .г2+3х}. Будем обозначать через Аа\/(х) функцию, которая каждому ,г сопоставляет значение f{x). Аналогично, если /(jcj, ... ,г„) еегь числовая форма от н переменных, то будем обозначать через
АХ! ...Х„./(хЬ...,Хл) функцию, которая каждому кортежу :Г[,... ,х„ сопоставляет значение
f{x
♦ Пусть примитивно рекурсивная функция Ax.f(x) задана с помощью Л-обозначения, причем сама форма /(х) дает примитивно рекурсивное описание этой функции. Тогда через Лх./(;г) будем обозначать геделевский номер этого описания функции Ax.f(x). Аналогично определяется
ЛХі ...*п./(*1»-••.*«)
ь
ДЛЯ функции Хх\ . .. xn.f(x 1,. . ., .Гя).
Отмстим также несколько определений, относящихся к нумерованным множествам и моделям.
Пусть а = (Р"1,... ,Р**) — конечная чисто предикатная сигнатура узкого исчисления предикатов, причем верхний индекс п, означает валентность (число аргументов) предикатного символа Р"‘ (і = 1,..., А-). Язык первого порядка в сигнатуре а будем обозначать La. Будем считать, что в языках первого порядка используются предметные переменные из фиксированого счетного множества Var = {то, її, *2____}-
Нумерованной алгебраической системой (сигнатуры о) назовем пару (М,і/), где М (Л/,Po,Pi,...) — алгебраическая система сигнатуры гг, a v : N -> М — нумерация основного множества А/ алгебраической системы М.
В первой части диссертации рассматривается семантика арифметических и предикатных формул, основанная на понятии примитивно рекурсивной реализуемости.
В разделе 1 приводятся используемые п дальнейшем аксиоматики интуиционистского исчисления предикатов гнльбертовского типа НРС, секвенциального интуиционистского исчисления предикатов 1QC, интуиционистской формальной арифметики НА и, наконец, секвенциального исчисления так называемой базисной логики, основанной на более сильном понятии конструктивности, чем изучавшиеся ранее конструктивные логики. По сравнению с интуиционистской логикой, в оазисной логике ослабляется правило вывода Modus Ponens (в частности, в базисной логике не выводится секвенция Т -> А => .4). Базисная логика предикатов BQC строится в языке логики предикатов с равенством. Понятие формулы несколько отличается от того, которое используется в интуиционистской логике предикатов, а именно, отличается употребление квантора всеобщности, который возникает только в формулах вида Vx(.4 —* В), где х — список переменных. Иногда вместо Vx(.4 -» ß) нсполь эуется запись Vx : A.B. На основе базисной логики естественным образом строится базисная арифметика ВА. Базисная арифметика корректна относительно классической семантики. Приводится техника "перевода“ произвольной формулы языка первого порядка с языка IQC d язык BQC’ и обратно (соответственно, .4і и .4'). Ввозится понятие "п-ослаблення" (,4)п и ”п-усиленпя" (.4)„ формулы А. Фактически, ослабление формулы означает замену некоторых подформул исходной формулы с А на
Т (Т -> ...(Т -» /1)...).
б
Раздел 2 посвящен исследованию РІІ-реализуемости (т. е. примитивно рекурсивной реализуемости). Вводится понятие Р11-реализуемостн для арифметических формул н секвенции: .гг^Л (см. подраздел 2.1). Имеет место теорема Салехи о корректности базисной арифметики ВА относительно примитивно рекурсивной реализуемости, доказанная п работе (20):
Теорема 2. Если В А Ь А =Ф В, то ВА Ь пг1"(А =*• В) для некоторого натурального числа п.
Арифметическая формула называется негативной, если она не содержит СИМВОЛОВ дизъюнкции и кванторов существования. Доказывается, что если А — замкнутая негативная арифметическая формула, то .4 PH-реализуема тогда и только тогда, когда она классически истинна.
Далее понятие примитивно рекурсивной реализуемости распространяется на предикатные формулы. Замкнутая предикатная формула Р называется РГ{-реалнзусмой, если любой ее замкнутый арифметический пример РЛ-реализуем (обозначение: г,,гр). В конце раздела приводится общая схема доказательства основного результата о неарифметичности множества всех РК-реализуемых предикатных формул.
В разделе 3 доказываются предложения, носящие технический характер и необходимые для доказательства основного результата. При этом используется теория Т2 (см. [13]). С помощью подходящей формализации доказательства теоремы Тенненбаума [б] о несуществовании рекурсивных нестандартных моделей арифметики, В. Е. Плиско [13] доказал, что для негативных замкнутых арифметических формул Г справедливо Т2 Н /’ = Р (предикатная формула Г строится по каждой арифметической формуле ґ путем исключения функциональных символов и замены их предикатными). В разделе 3.4 доказывается, при каких условиях формулы, являющиеся усилениями формул, используемых в этом выводе, являются РК-реализуемыми. В частности, приходится тщательно следить за использованием аксиомы индукции, так как в обшем виде усиление аксиомы индукции не РИ-реализуемо.
В разделе 4, доказывается основной результат первой части:
Теорема 5. Множество всех РП-реализуелшх предикатных формул не-арифметично.
Система арифметических формул
Ф](х, X],.. ., Х„.),..., Ф„(х, X),..., Хпц)
7
называется РЯ-опровержением формулы А{1\........Р*), где Р — поместный
предикатный символ, если арифметическая формула Ух : Т..4(ФЬ..., Ф„) не РЯ-реализуема. Если у формулы А нет РЯ-опроверженкя, то она называется РЯ-неопровсржимой. В разделе 5 доказывается
Теорема 6. Множество всех РЯ-неопровержимых предикатных формул не арифметично.
Аналогично вводится понятие РІІ-неопровержіїмой секвеншш и доказывается
Теорема 7. Множество всех Р Я-неопровержимых секвенций не арифметично.
Приводится пример интуиционистски выводимой секвенции, которая валяется РЯ-опровержішом.
Вторая часть диссертации посвящена исследованию конструктивной теории моделей и, в частности, конструктивной теории равенства. При атом используются идеи рекурсивной реализуемости по Клини и примитивно рекурсивной реализуемости. Будем использовать язык базисной логики предикатов в сиг натуре о, который будем обозначать Ьь„.
В разделе б вводится понятие обобщенного предиката (см. [9].[12]). которое с теоретико-множественной точки зрения отражает особенности конструктивного способа действии с предикатами. А именно, п-местным обобщенным
предикатом на множестве натуральных чисел N = {0.1.2________} называется
функция (в теоретико-множественном смысле) типа И" —> 2К.
Логические операции над обобщенными предикатами трактуются в диссертации конструктивно, в соответствии с идеями реализуемости, определенной относительно произвольного класса вычислимых функций V с вычислимой нумерацией р : N -» V, обладающего следующими свойствами:
• класс V' замкнут относительно операции суперпозиции;
• класс V содержит все примитивно рекурсивные функции:
• для класса V верна я-ш-п теорема: для любых чисел ш и н существует (щ + 1)-местная функция #",(«, Уі— , Ут) из этого класса такая, что если а
номер (т+п)-местной функции/(уь...,ут,гі,...,гй) из этого класса и кі,. ..,кт — произвольные числа, то А-|,..., А-т) есть номер п-местной функции /(&!,...с параметрами г,, ...,
з
Класс всех примитивно рекурсивных функций и класс всех частично рекурсивных функций удовлетворяют этим условиям. Понятия реализуемости, определяемые с помощью этих классов, являются, соответственно, клнниевской рекурсивной реализуемостью и примитивно рекурсивной реализуемостью.
Обобщенной алгебраической системой (или обобщенной моделью) в сигнатуре о = (Р"1,..., Р"*) (здесь Р?1 есть п,-местный предикатный символ) называется упорядоченный набор (Р),.. • .Р*)> где Vi — п,-местный обобщенный предикат (* = 1,2,..., к).
Пусть А = (Р],... ,Р*} — обобщенная (7-система. Всякое ^-высказывание Ф, т. е. замкнутая формула в языке первого порядка Ььа сигнатуры о. естественным образом задает операцию над обобщенными предикатами Р],..., Р*, результатом которой является множество натуральных чисел (значение высказывания Ф), обозначаемое [Ф]£. Более точное определение дается индуктивным способом; приведем определение для случая квантора всеобщности:
[Уи(Ф0(и) -» Ф1(ч))]£ ^
^ {т|Уа,и(о€ (Фо(и)]* -^!рг«о,и))Лрх({о,и» б (Ф^и)#))};
Будем говорить, что натуральное число е У-А-реаднзует высказывание Ф, если е € (Ф](/. Высказывание Ф языка Ьь„ будем называть У-истинкьш в обобщенной «т-снстеме А, если существует число, которое У-А-реалиэует высказывание Ф. V-теория обобщенной системы А — это множество Т1ц-(А) всех высказываний, У-истинных в А.
Обобщенные ст-системы А| = (Р'ь... ,Р'«) и Аг = (Р"ь— Р"т) назовем У-эквивалентными, если для любого * существуют такие вычислимые функции /, и <?, из класса У, что для любых чисел а, к 1, А-Л(
О 6 .....А-,,))?' => №....*„,,«) 6 [(*'№.<ч))г’;
о 6 [/?(*,,)Р =#■ 9,1*, кЩ}а) € №,.**)]£'.
Предложение 44. Если обобщенные о-системы А! и А2 У-эквивалентны. то их V-теории совпадают, т. е.
тмао = тма2).
В разделе 7 исследуются конструктивные теории нумерованных алгебраических систем. Обобщенная алгебраическая система А = {Рь... ,Р*) сигнатуры а = (Р,”1,..., Р^*) согласована с нумерованной алгебраической системой (М. и) сигнатуры <т, если для любого I = 1.... Д- и любых чисел Сь..выполняются следующие условия:
1) Р,(сь...,сП1} ф 0 «=? М \= Р*(ис1,...
9
2) если числа <li,...,dni таковы, что vc-} — i/âj для любого j = 1...п,-, то
Ti(ci,... ,Сщ) = Ti{dl,...,dn,).
Будем говорить, что высказывание Ф языка I* конструктивно V-нстинно в нумерованной 17-системе (М,г/), если и только если Ф Г-нстинно в любой обобщенной сг-снстеме, согласованной с (M,i/). Обозначение: |=V;con Ф-
Множество высказывании языка Ü. конструктивно V'-истинных в нумерованной алгебраической системе (М, и) будем обозначать Thi-;corl(M,j/) и называть конструктивной V-теорией этой нумерованной алгебраической системы.
Нумерованные алгебраические системы (Mi,i/() и (Мг,^) назовем У'Эквивалентными (обозначение: «у (Ma,j/j)), если существует такое взаимно-
однозначное отображение р основного множества Mi системы Mj на основное множество Л/j системы Mj, ЧТО Ц является изоморфизмом систем Ml и М2, и при этом существуют такпе одноместные вычислимые функции / п g из класса V', что
(Vn 6 N)/j(j/i(h)) = Ы/(п));
(Vn g N)ц~1(ъ(п)) = J/j(p(n)).
Теорема 8. Если нумерованные системы (Мi, гч) и (Mj.t/j) ^-эквивалентны, то Th^;con(Mbi/t) = Thi/itenfMî,«^).
Формула Ф языка Lbc называется атомарно-отрицательной, если в Ф всякое вхождение каждого предикатного символа находится в области действия некоторого знака отрицания не содержащей квантора всеобщности V (под формулой —>А подразумевается формула А —» ±). Формула Ф языка L* называется универсально-отрицательной, если в Ф область действия любого квантора V является атомарно-отрицательной формулой.
Предложение 53. Пусть (М.//) — нумерованная алгебраическая система сигнатуры о. А и В — произвольные согласованные с ней обобщенные о-системы. Тогда, каковы бы ни были универсально-отрицательная формула
Ф(у1,____J/.i) лзыка L*. не содержащая свободных, переменные, отличных от.
Уь... ,уп, и числа ci,...,c„. шкет место
|Ф{с,,....с.)1^0«[Ф(с,.........с„)]Р # 0.
В частности. во всех обобщенных а-системах, согласованны г с данной нумерованной ст-системой (М. и). V -истинны одни и те же универсально-отри нательные высказывания языка
В разделе 8 исследуется конструктивная теория равенства. Рассматривается язык первого порядка в минимальной сигнатуре г. Обобщенную е-снстему А назовем V-рефлекейвпой, если формула Vx(T -» (г = л-)) V-нстинна в А.
10
Теорема 9. Если А] и А2 — рефлексивные обобщенные г-системы, согласованные с одной и той же нумерованной г-системой, то
ТМА^ТМАз).
Обобщенную г-снстему А будем называть обобщенной 5-системой с V-разрешимым равенством, если формула
Ут, у(Т -+ (т = у V -»і = у))
принадлежит теории ТЬу(А).
Пусть К — произвольный класс обобщенных систем данной сигнатуры о. Будем называть V-теорией класса К- множество ТЬу(АС) высказываний сигнатуры о, V-истинных во всех ^-системах из класса К.. Тогда справедлива
Теорема 10. Пусть £п — класс всех обобщенных е-систем с V-разрешимым равенством, согласованных с нумерованной г-системой (А/, о), где а Є N или п = и>, |Л/1 = п. Тогда V-теория ТЬу(£") совпадает с классической теорией равенства и, следовательно, полна.
Расс?.іатрнваются обобщение 5-системы с V-неразрешимым равенством, т. е. такие, в которых Ф'-истннна формула
^Уг,у(Т -» {х = у V -чс = у)).
Доказывается, что свойства конструктивных теорий ^-неразрешимого равенства зависят от свойств нумерации основного множества. Очевидно, что нумерация одноэлементного множества тривиальна {и : N -* {ао}), и равен ство в данном случае разрешимо. Оказывается, что уже в случае двухэлементного носителя Л/ ситуация меняется: в зависимости от свойств нумерации V и теории обобщенной г-системы может быть ^-истинна как формула УтДТ -> Зх2—*л*і = 2а)- так и ее отрицание.
Теорема 11. Пусть Тп — класс всех обобщенных г-систем с V-неразрешимым равенством, согласованных с нумерованной г-системой (Л/, о), где мощность основного множества \М\ равна п (п > 2 или п = ы). Тогда V-теория Тііу(^) неполна.
Основные результаты диссертации опубликованы в работах [21], [22]. [23]. [24].
Автор выражает глубокую благодарность своему научному руководителю кандидату физико-математических наук Валерию Егоровичу Плиско за поста-
11
новку задачи, постоянное внимание к работе, поддержку и ценные обсуждения. Автор также выражает благодарность коллективу кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ им. М. В. Ломоносова за плодотворную обстановку и стимулирующее общение.
12