Примитивно рекурсивная реализуемость и конструктивная теория моделей тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

I Введение.

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

1. Интуиционистские и базисные формальные системы.

1.1. Язык логики предикатов.

1.2. Интуиционистское исчисление предикатов HP С.

1.3. Секвенциальное интуиционистское исчисление предикатов IQC.

1.4. Язык формальной арифметики.

1.5. Интуиционистская формальная арифметика НА.

1.6. Базисная логика предикатов BQC.

1.7. Базисная арифметика ВА.

1.8. Связь базисной логики с интуиционистскими системами.

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

2.1. Определения и основные факты.

2.2. PR-реализуемость "по Салехи".

2.3. PR-реализуемость "по Клини".

2.4. Понятие PR-реализуемости для предикатных формул.

2.5. Общая схема доказательства основного результата.

3. Формализация теоремы Тенненбаума

3.1. Теория Т.

3.2. Теория Т.

3.3. Теория Т2.

3.4. PR-реализуемость усилений аксиомы индукции.

4. Неарифметичность множества всех PR-реализуемых предикатных формул.

5. Неарифметичность множества всех PR-неопровержимых предикатных формул.

III Конструктивная теория моделей. ЮЗ

6. Обобщенные предикаты и обобщенные системы. ЮЗ

Часть I

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

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

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

В последние годы в работах В. Е. Плиско [12] была начата разработка теории моделей, основанной на конструктивной семантике типа рекурсивной реализуемости. Во второй части диссертации эти результаты обобщаются для других типов конструктивной семантики, в частности, для примитивно рекурсивной реализуемости. Средствами конструктивной теории моделей исследуются конструктивные теории нумерованных алгебраических систем, в частности, конструктивные теории так называемых обобщенных алгебраических систем в минимальной сигнатуре £, содержащей лишь символ равенства. Определяются условия совпадения таких конструктивных теорий с классической теорией равенства.

Введем необходимые определения.

Примитивно рекурсивными называются функции, которые можно получить с помощью операций подстановки и рекурсии из следующих исходных функций: константы 0, операции прибавления единицы S и семейства функций проекции Гт [т — 1,2,., 1 < i < т).

Функции, получающиеся из исходных функций с помощью операторов подстановки, примитивной рекурсии и минимизации, называются частично-рекурсивными.

Определим способ описания и геделевской нумерации частично-рекурсивных и примитивно рекурсивных функций. Как и в работе [13]. будем обозначать частично-рекурсивные и примитивно рекурсивные функции как слова в алфавите

О, S, (т = 1,2,., 1 < i < т), С, R, М, которые строятся по следующим правилам:

1) 0 есть 0-местный функциональный символ;

2) S есть одноместный функциональный символ;

3) есть m-местный функциональный символ (ш — 1,2,., 1 < г < т);

4) если / есть m-местный функциональный символ (т > 1). а gi,.,gm суть n-местные функциональные символы (п > 0), то Cfgi. дт есть п-местный функциональный символ;

5) если / есть n-местный функциональный символ, а д есть (п + 2)-местный функциональный символ (п > 0), то Rfg есть (п + 1)-местный функциональный символ;

6) если / есть (п + 1)-местный функциональный символ (n > 1), то М/ есть n-местный функциональный символ.

Символы 0, S и 1[п считаются обозначениями соответствующих исходных примитивно рекурсивных функций. Запись вида C/gi. дт — это обозначение функции, полученной суперпозицией из функций, обозначенных посредством /, . дт. Функциональный символ Rfg есть обозначение для функции, полученной рекурсией из функций, обозначенных через / и д. Функциональный символ М/ есть обозначение для функции, полученной операцией минимизации из функции /, т. е.

Uf{xh.,xn) ~fJLy[f(y,Xl,.,Xn) =0].

Если оператор минимизации не использовался (т.е. буква М не входит в состав "кодирующего" слова), то выражаемая таким словом частично-рекурсивная функция является примитивно рекурсивной.

Зафиксируем геделевскую нумерацию частично (примитивно) рекурсивных функций, как слов в описанном выше алфавите. Примитивно рекурсивную функцию с геделевским номером х обозначаем через фх.

Часто для обозначения функций и их геделевских номеров мы будем использовать так называемые А-обозначения (см. [5, § 10]), а именно:

• Пусть / (ж) есть числовая форма от одной переменной х (например, х2+3х). Будем обозначать через Xx.f(x) функцию, которая каждому х сопоставляет значение f(x). Аналогично, если f(xi,. ,хп) есть числовая форма от п переменных, то будем обозначать через

Azi .xn.f(xh.,xn) функцию, которая каждому кортежу xi,.,xn сопоставляет значение f(xi,.,xn).

• Пусть примитивно рекурсивная функция Ax.f(x) задана с помошью А-обозначения, причем сама форма f(x) дает примитивно рекурсивное описание этой функции. Тогда через Ax.f(x) будем обозначать геделевскии номер этого описания функции Ax.f(x). Аналогично определяется

Ажх. xn.f(xi,., хп) для функции Xxi. xn.f(x 1, .,£„).

Отметим также несколько определений, относящихся к нумерованным множествам и моделям.

Пусть а = (Р"1, ■ ■ ■, P]?h} — конечная чисто предикатная сигнатура узкого исчисления предикатов, причем верхний индекс п,- означает валентность (число аргументов) предикатного символа (г = 1,., к). Язык первого порядка в сигнатуре а будем обозначать La. Будем считать, что в языках первого порядка используются предметные переменные из фиксированого счетного множества Var = {жо, xi: х2■ • • •}•

Нумерованной алгебраической системой (сигнатуры а) назовем пару (М, и), где М v^ (М, Pq, Pi, .} — алгебраическая система сигнатуры а, а и : N —> М — нумерация основного множества М алгебраической системы М.

В первой части диссертации рассматривается семантика арифметических и предикатных формул, основанная на понятии примитивно рекурсивной реализуемости.

В разделе 1 приводятся используемые в дальнейшем аксиоматики интуиционистского исчисления предикатов гильбертовского типа НРС, секвенциального интуиционистского исчисления предикатов IQC, интуиционистской формальной арифметики НА и, наконец, секвенциального исчисления так называемой базисной логики, основанной на более сильном понятии конструктивности, чем изучавшиеся ранее конструктивные логики. По сравнению с интуиционистской логикой, в базисной логике ослабляется правило вывода Modus Ponens (в частности, в базисной логике не выводится секвенция Т —> А .4). Базисная логика предикатов BQC строится в языке логики предикатов с равенством. Понятие формулы несколько отличается от того, которое используется в интуиционистской логике предикатов, а именно, отличается употребление квантора всеобщности,- который возникает только в формулах вида \/х(Л —у В), где х •— список переменных. Иногда вместо Vx(,4 —> В) используется запись Vx : А.В. На основе базисной логики естественным образом строится базисная арифметика ВА. Базисная арифметика корректна относительно классической семантики. Приводится техника перевода" произвольной формулы языка первого порядка с языка IQC в язык BQC и обратно (соответственно, Аь и Аг). Вводится понятие "п-ослабления" (.4)" и "п-усиления1" {А)п формулы А. Фактически, ослабление формулы означает замену некоторых подформул исходной формулы с А на

Т -> (Т -> .(Т А).).

Раздел 2 посвящен исследованию PR-реализуемости (т. е. примитивно рекурсивной реализуемости). Вводится понятие PR-реализуемости для арифметических формул и секвенций: хгргА (см. подраздел 2.1). Имеет место теорема Салехи о корректности базисной арифметики ВА относительно примитивно рекурсивной реализуемости, доказанная в работе [20]:

Теорема 2. Если ВА b А => В, то ВА Ь пгрТ(А В) для некоторого натурального числа п.

Арифметическая формула называется негативной, если она не содержит символов дизъюнкции и кванторов существования. Доказывается, что если А — замкнутая негативная арифметическая формула, то А PR-реализуема тогда и только тогда, когда она классически истинна.

Далее понятие примитивно рекурсивной реализуемости распространяется на предикатные формулы. Замкнутая предикатная формула F называется PR-реализуемой, если любой ее замкнутый арифметический пример PR-реализуем (обозначение: гprF). В конце раздела приводится общая схема доказательства основного результата о неарифметичности множества всех PR-реализуемых предикатных формул.

В разделе 3 доказываются предложения, носящие технический характер и необходимые для доказательства основного результата. При этом используется теория Т2 (см. [13]). С помощью подходящей формализации доказательства теоремы Тенненбаума [6] о несуществовании рекурсивных нестандартных моделей арифметики, В. Е. Плиско [13] доказал, что для негативных замкнутых арифметических формул F справедливо Т2 Ь F = F' (предикатная формула F' строится по каждой арифметической формуле F путем исключения функциональных символов и замены их предикатными). В разделе 3.4 доказывается, при каких условиях формулы, являющиеся усилениями формул, используемых в этом выводе, являются PR-реализуемыми. В частности, приходится тщательно следить за использованием аксиомы индукции, так как в обшем виде усиление аксиомы индукции не PR-реализуемо.

В разделе 4, доказывается основной результат первой части:

Теорема 5. Множество всех PR-реализуемых предикатных формул не-арифметично.

Система арифметических формул

•£) ,., хП1),., Фп(ж, Х\,., хПк^) 7 называется PR-опровержением формулы А(Р\,., Р*.), где Р— п,-местный предикатный символ, если арифметическая формула Vrc : Т.А(Ф1,., Ф„) не PR-реализуема. Если у формулы А нет PR-опровержения, то она называется PR-неопровержимой. В разделе 5 доказывается

Теорема 6. Множество всех PR-неопровержимых предикатных формул неарифметично.

Аналогично вводится понятие PR-неопровержимой секвенции и доказывается

Теорема Т. Множество всех PR-неопровержимых секвенций неарифметично.

Приводится пример интуиционистски выводимой секвенции, которая является PR-опровержимой.

Вторая часть диссертации посвящена исследованию конструктивной теории моделей и, в частности, конструктивной теории равенства. При этом используются идеи рекурсивной реализуемости по Клини и примитивно рекурсивной реализуемости. Будем использовать язык базисной логики предикатов в сигнатуре (7, который будем обозначать Lba.

В разделе 6 вводится понятие обобщенного предиката (см. [9],[12]), которое с теоретико-множественной точки зрения отражает особенности конструктивного способа действий с предикатами. А именно, п-местным обобщенным предикатом на множестве натуральных чисел N = {0,1,2.} называется функция (в теоретико-множественном смысле) типа N" 2N.

Логические операции над обобщенными предикатами трактуются в диссертации конструктивно, в соответствии с идеями реализуемости, определенной относительно произвольного класса вычислимых функций V с вычислимой нумерацией р : N —» V. обладающего следующими свойствами:

• класс V замкнут относительно операции суперпозиции;

• класс V содержит все примитивно рекурсивные функции:

• для класса V верна s-m-n теорема: для любых чисел т и п существует (т + 1)-местная функция г/ь ., ут) из этого класса такая, что если а — номер (т+п)-местной функции /(г/i,., г/т, z\,., zn) из этого класса и &1,., кт — произвольные числа, то ., кт) есть номер п-местной функции f(k\,., кт. Zi,., zn) с параметрами zi, ., zn.

Класс всех примитивно рекурсивных функций и класс всех частично рекурсивных функций удовлетворяют этим условиям. Понятия реализуемости, определяемые с помощью этих классов, являются, соответственно, клиниевской рекурсивной реализуемостью и примитивно рекурсивной реализуемостью.

Обобщенной алгебраической системой (или обобщенной моделью) в сигнатуре о — (Pi1,. •, ) (здесь Р-1' есть пг-местный предикатный символ) называется упорядоченный набор ('Pi,., Pk), где Pi — пг-местный обобщенный предикат (г — 1,2,. ,к).

Пусть А = (Pi,. ,Vk) — обобщенная сг-система. Всякое сг-высказывание Ф, т. е. замкнутая формула в языке первого порядка Ььа сигнатуры о, естественным образом задает операцию над обобщенными предикатами V\,. ,Vk, результатом которой является множество натуральных чисел (значение высказывания Ф), обозначаемое [Ф]у. Более точное определение дается индуктивным способом; приведем определение для случая квантора всеобщности: [Уп(Ф0(и) Ыи))}$ {s|Va,u(a G [Ф0(и)]^ ->!рх((а, и)) А рх((а,.и)) G [*i(u)#))};

Будем говорить, что натуральное число е V-A-реализует высказывание Ф, если е G [Ф]у • Высказывание Ф языка Ььа будем называть V-истинным в обобщенной а-системе А, если существует число, которое V'-A-реализует высказывание Ф. V-теория обобщенной системы А — это множество Thy (А) всех высказываний, У-истинных в А.

Обобщенные <т-системы Ai = (P'i,. ,V'm) и А2 = (P"i, ■ ■ ■ ,Р"т) назовем V-эквивалентными, если для любого i существуют такие вычислимые функции fi и gi из класса V, что для любых чисел ci, /q,., кщ a G [Pi'(ku ., кщ)р ^дг{къ. ,кщ,а) G [РЦк{,., kni)p.

Предложение 44. Если обобщенные о-системы А\ и А2 V-эквивалентны, то их V-теории совпадают, т. е.

Thv(A1)=Thv(A2).

В разделе 7 исследуются конструктивные теории нумерованных алгебраических систем. Обобщенная алгебраическая система А = (Pi,. ,Pk) сигнатуры а = (Pi1,., Pj!k) согласованас нумерованной алгебраической системой (Мл/) сигнатуры о, если для любого г = 1,., к и любых чисел ci,., сщ выполняются следующие условия:

1) Рг(си ., О ф 0 М Н P?'(vch ., исп.);

2) если числа d\,., dni таковы, что ucj = vdj для любого j = 1,., щ. то Vi(ci,.,cni) =Vi(db.,dni).

Будем говорить, что высказывание Ф языка Ььа конструктивно V'-истинно в нумерованной сг-системе (M,z/), если и только если Ф V'-истинно в любой обобщенной сг-системе, согласованной с (M,i/). Обозначение: (М,^) Ц';соп Ф. Множество высказываний языка l)a конструктивно V'-истинных в нумерованной алгебраической системе (M,z/) будем обозначать Thvr;Con(M, и) и называть конструктивной V-теорией этой нумерованной алгебраической системы.

Нумерованные алгебраические системы (Mi, и\) и (М2, щ) назовем V'-эквива-лентными (обозначение: (Mi,z/i) «у (Мг,^)), если существует такое взаимнооднозначное отображение /i основного множества М\ системы Mi на основное множество Мч системы М2, что ц является изоморфизмом систем Mi и М2, и при этом существуют такие одноместные вычислимые функции / и д из класса У, что

Упе%Мп)) = ^(/(п));

Vn6N)/r1(/y2(n)) = ;y1(^(n)).

Теорема 8. Если нумерованные системы (Mi,z/i) и (Мг,^) V-эквивалентны, то Th^;co„(Mi, vi) - Th7;con(M2,i/2)

Формула Ф языка Ььа называется атомарно-отрицательной, если в Ф всякое вхождение каждого предикатного символа находится в области действия некоторого знака отрицания ~>. не содержащей квантора всеобщности V (под формулой -\А подразумевается формула А —> ±). Формула Ф языка Lba называется универсально-отрицательной, если в Ф область действия любого квантора V является атомарно-отрицательной формулой.

Предложение 53. Пусть (М,/у) — нумерованная алгебраическая система сигнатуры с. А и В — произвольные согласованные с ней обобщенные а-системы. Тогда, каковы бы ни были универсально-отрицательная формула Ф(у\,. ,уп) языка Lba. не содержащая свободных переменных, отличных от г/i,., уп, и числа ci,., сп, имеет место

Ф(сь ., сп)]£ ф 0 [Ф(сь ., сп)$ ф 0.

В частности, во всех обобщенных а-системах, согласованных с данной, нумерованной а-системой (М,и), V-истинны одни и те же универсально-отрицательные высказывания языка 1?

В разделе 8 исследуется конструктивная теория равенства. Рассматривается язык первого порядка в минимальной сигнатуре с. Обобщенную е-систему А назовем V-рефлекс-йеной, если формула \/ж(Т —>• (х = х)) У-истинна в А.

Теорема 9. Если А\ и А-2 — рефлексивные обобщенные е-системы, согласованные с одной и той же нумерованной е-системой, то

Thy(Ai) = Thy(A2).

Обобщенную c-систему А будем называть обобщенной е-системой с У-разрешимым равенством, если формула

Vx, у(Т (ж = у V ^х = у)) принадлежит теории Thy (А).

Пусть К, — произвольный класс обобщенных систем данной сигнатуры а. Будем называть V-теорией класса /С множество Thy (/С) высказываний сигнатуры о", У-истинных во всех сг-системах из класса /С. Тогда справедлива

Теорема 10. Пусть £п — класс всех обобщенных е-систем с V-разрешимым равенством, согласованных с нумерованной е-системой (М, и), где п 6 N или п = ш, \М\ = п. Тогда V-теория Thy(£") совпадает с классической теорией равенства и, следовательно, полна.

Рассматриваются обобщеные c-системы с У-неразрешимым равенством, т. е. такие, в которых V'-истинна формула у(Т ->• (х = у V -ire = у)).

Доказывается, что свойства конструктивных теорий У-неразрешимого равенства зависят от свойств нумерации основного множества. Очевидно, что нумерация одноэлементного множества тривиальна (и : N —> {fto}); н равенство в данном случае разрешимо. Оказывается, что у лее в случае двухэлементного носителя М ситуация меняется: в зависимости от свойств нумерации v в теории обобщенной c-системы может быть У-истинна как формула Vrci(T —> 3^2= Ж2). так и ее отрицание.

Теорема 11. Пусть Тп — класс всех обобщенных е-систем с V-неразрешимым равенством, согласованных с нумерованной е-системой (М,и), где мощность основного множества \М\ равна п (п > 2 или п = со). Тогда V-теория Thy(^r") неполна.

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

Автор выражает глубокую благодарность своему научному руководителю кандидату физико-математических наук Валерию Егоровичу Плиско за поста

Часть II

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

Интуиционистское понятие эффективности уточняется в клиниевском определении (рекурсивной) реализуемости с помощью рекурсивных функций. В математике рассматриваются также другие, более узкие классы вычислимых функций, например, примитивно рекурсивные функции. По аналогии с клини-евской реализуемостью можно определить понятие примитивно рекурсивной реализуемости, а именно, рассмотреть понятие реализуемости, основанное на использовании только примитивно рекурсивных функций как способа получения одних реализаций из других. Эти идеи связаны с критическим пересмотром интуиционистских взглядов на природу "доказательства", что привело к появлению в 80-х годах так называемой базисной логики (Basic Logic), основанной на интерпретации А —> В как конструкции, использующей "допущение" об истинности А для построения "доказательства" В. Так, например, формула (Т —» А) —> А не может считаться истинной при такой интерпретации. Действительно, допущение об истинности формулы Т —> А означает, что существует метод построения доказательства А. Однако сам этот метод остается неизвестным. Таким образом не существует конструкции, позволяющей по допущению об истинности формулы Т —»• А построить доказательство формулы А.

Аксиоматика базисной логики высказываний BPL (Basic Prepositional Logic) была представлена А. Виссером в 1981 году [И]. В. Руйтенбург [14] расширил BPL до базисной логики предикатов BQC (Basic Predicate Calculus). С. Салехи [18] представил реализуемость в языке базисной арифметики ВА (Basic Arithmetic) как клиниевскую рекурсивную реализуемость, ограниченную использованием только примитивно рекурсивных функций, доказав корректность ВА относительно такого определения реализуемости. Перейдем к формальным определениям.

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

2. A. H. Колмогоров, Zur Deutung der intuitionisticshen Logik. Math. Z., 1932, 35, p. 58 — 65.

3. S. K. Kleene, On the interpretation of intuitionistic number theory. Journ. Symbolic Logic, 1945, vol. 10, p. 109 — 124.

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

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

6. S. Tennenbaum, Non-archimedean systems of arithmetic. Notices Amer. Math. Soc., 1959, 6, № 3, p. 270 — 283.

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

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

9. В. Е. Плиско, Некоторые варианты понятия реализуемости для предикатных формул. ДАН, 1976, т. 226, № 1, с. 61 — 64.

10. Ю. Л. Ершов, Проблемы разрешимости и конструктивные модели. Москва, Наука, 1980.

11. A. Visser, A propositional logic with explicit fixed points. Studia Logica, 1981, 40, p. 155 — 175.

12. В. E. Плиско, О языках с конструктивными логическими связками. ДАН, 1987, т. 296, № 1, с. 35 — 38.

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

14. W. Ruitenburg, Basic Logic and Fregean set theory. H. Barendregt, M. Bezem, J. W. Klop (eds.), Dirk Van Dalen Festschrift, Quaestions Infinitae, Department of Philosopy, Utrecht University, 1993, vol.5, p. 121 — 142.

15. Ю. Л. Ершов, Определимость и вычислимость. Новосибирск, "Научная книга, 1996.

16. В. Е. Плиско, Об арифметической сложности предикатных логик полных конструктивных арифметических теорий. Фундаментальная и прикладная математика, 1999, т. 5, № 1, с. 221 — 255.

17. М . Ardeshir, A Translation of Intuitionistic Predicate Logic into Basic Predicate Logic. Studia Logica, 1999, 62, p. 341 — 352.

18. S. Salehi, A Generalized Realizability for Constructive Arithmetics. Abstracts of Contributed papers LC2000 and ELSS 2000, Paris, La Sorbonne, 23 — 31 juillet 2000.

19. S. Salehi, Primitive Recursive Realizability and Basic Arithmetic. 2000, Manuscript.

20. S. Salehi, Primitive Recursive Realizability and Basic Arithmetic. The Bulletin of Symbolic Logic, 2001, vol. 7, № 1, p. 147 — 148.

21. V. Plisko, D. Viter, Equality from the constructive point of view. The Bulletin of Symbolic Logic, 2001, vol. 7, № 1, p. 143.• В работе 22. постановка задачи и определения принадлежат Плиско В. Е.; Витеру Д. А. принадлежат основные результаты.

22. Д. А. Витер, О конструктивной теории равенства. Вестн. Моск. ун-та. Сер. 1. Математика. Механика, 2001, № 6, с. 61 — 63.

23. Д. А. Витер, Примитивно рекурсивная реализуемость и логика предикатов. Рукопись депонирована в ВИНИТИ, 06.08.2001, Ш 1830 В2001, 86 с.