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

• Тишковский, Дмитрий Евгеньевич
• кандидат физико-математических наук
• 1999

Оглавление диссертации кандидат физико-математических наук Тишковский, Дмитрий Евгеньевич

Содержание

Введение

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

1.1. Суперинтуиционистские предикатные логики и теории

1.2. Суперинтуиционистские дедуктивные системы

1.3. Адекватность суперинтуиционистских дедуктивных систем суперинтуиционистским логикам

1.4. Суперинтуиционистские дедуктивные системы как дедуктивные системы полимодальных логик

1.5. Свойства логик и свойства дедуктивных систем

2. Квазицилиндрические алгебры

2.1. Определение и примеры

2.2. Размерность элементов

2.3. Алгебры локально-конечной размерности

2.4. Означивания формул

2.5. Алгебры Расёвой—Сикорского

2.6. Алгебры Линденбаума—Тарского

2.7. Теорема о полноте

3. Алгебраические эквиваленты некоторых свойств логик

3.1. Дизъюнктивное свойство

3.2. Экзистенциальное свойство

3.3. Свойство Бета

3.4. Проективное свойство Бета

3.5. Интерполяционное свойство

3.6. Соотношение свойств дедуктивных систем и свойств логик

Литература

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

Введение

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

Как известно, одной из ключевых теорем теории моделей является теорема Гёделя о полноте классической логики предикатов, связывающая синтаксическое и семантическое понятия истинности формул. Благодаря этой теореме становится возможным изучение свойств классических теорий семантическими методами. Таким образом, наличие для изучаемой логики семантики, связанной с данной логикой при помощи некоторой теоремы о полноте, во многом облегчает исследование свойств логики, так как становится возможным использовать в дополнение к синтаксическому аппарату ещё и аппарат этой семантики. В частности, если логика полна относительно некоторого класса алгебр, то это позволяет исследовать логику при помощи мощного и развитого аппарата универсальной алгебры.

Хорошим подспорьем в изучении свойств решётки однотипных логик является наличие единой семантики для этих логик. Так, например, решётке пропозициональных суперинтуиционистских логик соответствует решётка многообразий псевдобулевых алгебр. К сожалению, в случае предикатных логик такого удачного соответствия нет. Известно [25], что существует континуум суперинтуиционистских предикатных логик, которые неполны относительно семантики шкал Крипке, и существует континуум суперинтуиционистских предикатных логик, которые неполны относительно семантики псевдобулевых моделей Е. Расёвой и Р. Си-корского [8].

В связи с вышесказанным возникает проблема построения такого класса К однотипных структур, чтобы всякая суперинтуиционистская предикатная логика была бы полной относительно некоторого подкласса класса К. Естественно требовать, чтобы класс К был классом алгебр. Таким образом, проблема построения единой семантики для суперинтуиционистских предикатных

логик становится проблемой их единой алгебраизации.

Алгебраическая логика берёт начало с работы Тарского [32]. В этой работе Тарский ввёл понятие алгебры пропозициональных формул. Он определил отношение = на множестве формул условием

А = В «$=>• Ь А э I? и \-BdA

и показал, что это отношение является конгруэнцией на алгебре формул. Тарский доказал, что соответствующая фактор-алгебра является булевой алгеброй, а множество всех классических тавтологий совпадает с множеством формул, эквивалентных Т. Фактор-алгебры, полученные факторизацией алгебры формул по конгруэнции указанного выше вида, получили позднее название алгебр Линденбаума—Тарского и играют важную роль в алгебраизации логик.

Позднее метод Тарского был применён к алгебраизации пропозициональных модальных, суперинтуиционистских и многих других логик. Большой вклад в развитие алгебраческих методов исследования неклассических логик был внесён Е. Расёвой и Р. Си-корским [29,8]. Сам Тарский возглавил обширную исследовательскую программу по алгебраизации классической логики 1-го порядка [17]. Позднее эта программа была подхвачена различными школами алгебраической логики, среди которых следует особо отметить венгерскую школу [11,12,18,19,23,24,31].

В 1989 году метод Тарского был обобщён Блоком и Пигоц-ци [13] на случай алгебраизации произвольных пропозициональных логик. В указанной работе использовалось представление логик дедуктивными системами, и было введено понятие алгебраиз-уемости пропозициональной дедуктивной системы. Было доказано, что алгебраизуемой дедуктивной системе соответствует единственная эквивалентная алгебраическая семантика — некоторое квазимногообразие алгебр. В диссертации также используется представление предикатных логик дедуктивными системами.

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

примерах. Рассмотрим правило введения квантора всеобщности

А Э В(х) Ь Л э УхВ(х).

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

УхА(х) Э А(у),

где х не попадает в область действия квантора по переменной у в А(х), имеет недостаток той же природы. Действительно, выражения А{х) и А(у) формально различны, но их нельзя трактовать как различные переменные для формул. Наиболее полно сложность предикатных логик отражена в правиле подстановки формул 1-го порядка (см. параграф 1.1). Это правило, по сравнению с пропозициональным случаем, существенно усложнено условиями, которые не допускают коллизий переменных при использовании правила подстановки.

Как следует из приведённых выше примеров, проблема заключается в том, что мы имеем дело с операциями замены свободных вхождений переменных, которые не всегда явно присутствуют в языке 1-го порядка, но используются в метаязыке.

Существует несколько решений этой проблемы [13, Приложение С], [23]. Первое состоит в том, чтобы строить дедуктивную систему для предикатной логики в языке, в который непосредственно введены символы для всевозможных операций замены переменных. Следуя по этому пути при алгебраизации классической логики 1-го порядка, приходим к понятиям полиадических и квазиполиадических алгебр [16].

Второе решение состоит в том, чтобы выразить операцию замены переменных в самом языке 1-го порядка. Это становится возможным, если в языке 1-го порядка присутствует символ равенства Тогда указанную выше аксиому можно заменить, например, на VхА(х) э Зх{х & у а Следуя в этом на-

правлении, при алгебраизации классической логики 1-го порядка получим многообразие цилиндрических алгебр [17].

Если же в языке нет символа равенства, но есть бесконечное количество предметных переменных, то существует промежуточное решение — выразить операции замены нескольких переменных через операции замены одной переменной. Исходя из этой предпосылки, алгебраизуя классическую логику предикатов, получим многообразие (цилиндрических) алгебр Пинтера (с подстановками) [27]. Указанные алгебры являются наиболее простыми алгебрами, которые годятся в качестве алгебраического эквивалента для классической логики 1-го порядка [23]. В данной работе мы используем именно такой подход.

Несмотря на множество подходов к алгебраизации предикатных логик (см. [12,17,23]), суперинтуиционистские предикатные логики до сих пор не были алгебраизованы.

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

если логика Ь полна относительно класса К алгебр, то Ь имеет свойство V тогда и только тогда, когда К обладает свойством А1д(Г).

Через А1д(V) здесь обозначен алгебраический эквивалент свойства V, формулируемый на языке алгебр и гомоморфизмов.

Большой вклад в теорию алгебраизации свойств пропозициональных логик внесён Максимовой Л. Л. В работах [5-7,21,22] найдены и изучены алгебраические эквиваленты для многих свойств пропозициональных суперинтуиционистских и мономодальных логик. В частности, алгебраизованы дизъюнктивное свойство, свойство Бета, проективное свойство Бета и интерполяционное свойство пропозициональных суперинтуиционистских логик. Близкие результаты в области алгебраической характери-зации свойств определимости Бета и интерполяционного свойства различных логик были получены сравнительно недавно учеными

венгерской школы [18-20,31].

Таким образом, естественна постановка задачи об алгебраиз-ации свойств суперинтуиционистских предикатных логик. В диссертации при трансляции свойств суперинтуиционистских предикатных логик на алгебраический язык взяты за основу методы, использованные Максимовой Л. Л. при доказательстве аналогичных теорем эквивалентности.

В последнее время в алгебраической логике классическую логику 1-го порядка связывают с пропозициональными полимодальными логиками [24,33]. Во многом подобная связь мотивирована представлением логики дедуктивной системой, которая в случае предикатных логик может трактоваться и как дедуктивная система для пропозициональных полимодальных логик. В работе также исследуется этот вопрос. Устанавливается связь между суперинтуиционистскими предикатными логиками и пропозициональными интуиционистскими полимодальными логиками [1]. Параллельно алгебраизации свойств суперинтуиционистских предикатных логик, проведённой в диссертации, могут быть алгебраизова-ны и соответствующие свойства интуиционистских полимодальных логик, такие как дизъюнктивное свойство, свойство Бета, проективное свойство Бета, интерполяционное свойство выводимости и импликативное интерполяционное свойство.

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

Цель работы — построить единую алгебраическую семантику для всех суперинтуиционистских предикатных логик и транслировать основные свойства указанных логик на алгебраический язык.

В диссертации использованы семантические методы теории не-

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

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

Основные результаты диссертации:

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

2) Введён и исследован класс квазицилиндрических алгебр. Доказано, что каждая суперинтуиционистская предикатная логика сильно полна относительно некоторого многообразия указанных алгебр.

3) Для дизъюнктивного, экзистенциального свойств, свойства Бета, проективного свойства Бета, интерполяционного свойства выводимости и импликативного интерполяционного свойства суперинтуиционистских предикатных логик найдены эквивалентные алгебраические свойства.

Работа носит теоретический характер. Ее методы и результаты могут использоваться специалистами в области неклассических логик и теоретической информатики, для чтения лекций и спецкурсов в Московском, Новосибирском, Красноярском, Новосибирском педагогическом и др. госуниверситетах.

Основные результаты, полученные в диссертации, докладывались на:

• заседаниях семинаров "Алгебра и логика" и "Нестандартные логики" кафедры алгебры и математической логики механико-математического факультета НГУ,

• русско-японском коллоквиуме по нестандартным логикам и логическим аспектам информатики N81/95 (Иркутск, 1995),

• международной конференции "Универсальная алгебра и теория решеток" (Сегед, Венгрия, 1996),

• международной конференции " Логика, алгебра и информатика", посвященной памяти Елены Расевой (Варшава, 1996),

• международной конференции "Мальцевские чтения" (Новосибирск, 1998),

• международных научных студенческих конференциях "Студент и научно-технический прогресс" (Новосибирск, 1993,1995,1996),

• логическом коллоквиуме ЬС'98 (Прага, 1998).

Результаты диссертации опубликованы в девяти работах автора [34-42].

Остановимся более подробно на содержании работы. В главе 1 исследуются синтаксические аспекты суперинтуиционистских предикатных логик.

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

В параграфе 1.2 вводятся понятие суперинтуиционистской дедуктивной системы и понятие вывода формулы 1-го порядка в дедуктивной системе. Следует отметить, что язык дедуктивных систем заранее фиксируется, и все рассматриваемые в работе дедуктивные системы записаны в едином пропозициональном языке. Пропозициональные переменные этого языка служат буквами для обозначения произвольных формул 1-го порядка. Поэтому формулы языка дедуктивных систем названы схемами формул, что согласуется с известными понятиями схемы аксиом и частного случая схемы аксиом [3]. Обычным образом определяется понятие вывода схемы формул в дедуктивной системе.

Сведение предикатной логики к пропозициональной дедуктивной системе позволяет обойти многие проблемы алгебраизации предикатных логик, связанные с подстановками формул и операциями замены переменных. Дедуктивная система называется

адекватной логике, если данная логика совпадает с множеством формул, выводимых в данной дедуктивной системе. Возникает вопрос: для всякой ли суперинтуиционистской предикатной логики существует ей адекватная дедуктивная система? В параграфе 1.3 изучается подобное отношение между дедуктивными системами и суперинтуиционистскими предикатными логиками и теориями. Приводятся примеры логик и адекватных им дедуктивных систем. Всякой суперинтуиционистской предикатной логике можно поставить в соответствие наибольшую суперинтуиционистскую дедуктивную систему .05(1,), включив в схемы аксиом все схемы формул, любые частные случаи которых принадлежат логике Ь. Доказана важная теорема о существовании для произвольно взятой суперинтуиционистской предикатной логики адекватной ей дедуктивной системы:

ТЕОРЕМА 1.21. Для любой предикатной суперинтуиционистской логики Ь дедуктивная система ПБ(Ь) адекватна Ь.

Ключевую роль в доказательстве указанной теоремы играет построение трансляции А Ф[А] формул 1-го порядка в схемы формул, обладающей двумя "хорошими" свойствами. Во-первых, одним из частных случаев схемы Ф[А] является сама формула А. Во-вторых, если формула А принадлежит логике Ь, то все частные случаи схемы Ф[А] также принадлежат данной логике Ь.

В параграфе 1.4 проводится параллель между суперинтуиционистскими дедуктивными системами и интуиционистскими полимодальными пропозициональными логиками. Отмечается, что язык рассматриваемых дедуктивных систем является пропозициональным языком полимодальных логик с модальностями V*, 3* и (г,] < и). Доказывается, что множества схем формул, выводимых в расширениях некоторой фиксированной базовой дедуктивной системы I (которая адекватна интуиционистской предикатной логике), являются интуиционистскими полимодальными логиками в смысле [1] с регулярными модальностями. Доказывается, что все модальности V* в указанных полимодальных логиках являются П-нормальными, модальности 3; — О-нормальными, модальности в) являются □- и О-нормальными, а пары модаль-

ностей (N/¿,3$) хорошо мотивированы (см. [1]). Для этих полимодальных логик формулируются теорема о дедукции и теорема о замене, доказательства которых стандартны и потому не приводятся. Заметим, что из теоремы о замене следует алгебраизуе-мость в смысле [13] расширений базовой системы I.

В параграфе 1.5 формулируются основные свойства суперинтуиционистских предикатных логик и пропозициональных полимодальных логик (суперинтуиционистских дедуктивных систем). Кроме того, с использованием свойств трансляции А Ф[А] доказывается теорема о том, что если наибольшая суперинтуиционистская дедуктивная система БЗ(Ь), адекватная данной логике Ь, обладает дизъюнктивным или интерполяционным свойством, то и логика Ь обладает этим свойством.

В главе 2 изучаются квазицилиндрические алгебры и их соотношение с суперинтуиционистскими предикатными логиками.

В параграфе 2.1 определяется многообразие квазицилиндрических алгебр, приводятся примеры указанных алгебр и доказываются некоторые важные тождества и соотношения, верные в этих алгебрах.

В параграфе 2.2 определяется и изучается понятие размерности А а элемента а квазицилиндрической алгебры. Размерность — важная характеристика элемента алгебры. Эта характеристика является алгебраическим аналогом множества свободных переменных в формуле 1-го порядка.

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

ТЕОРЕМА 2.20. Класс локально-финитарных алгебр замкнут относительно взятия подалгебр, гомоморфных образов и конечных прямых произведений.

Кроме того, строится пример, показывающий, что класс локально-финитарных алгебр не является многообразием.

В параграфе 2.4 вводится понятие означивания формул в квазицилиндрической алгебре как отображения из множества формул 1-го порядка в алгебру, подчинённого некоторым условиям. Доказывается важная теорема о продолжении отображений до означиваний формул:

ТЕОРЕМА 2.25. Пусть Л — квазицилиндрическая алгебра, А1 — множество всех атомарных формул вида р(х{0,... где

Х{0,... , Хгп — некоторая закреплённая за данным (п + 1)-арным предикатным символом р последовательность различных переменных. Пусть г>о — отображение множества А1 в носитель алгебры Л.

Если для всех р(х{0,... , Х{п) из At выполнено Ауор(х{0, ... , Хгп) С {го ,...,гп}; то г>о единственным образом продолжается до означивания V формул в алгебре Л.

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

В параграфе 2.5 исследуется связь известной семантики псевдобулевых моделей Расёвой и Сикорского с квазицилиндрическими алгебрами. Указывается способ построения по произвольно взятой псевдобулевой модели некоторой квазицилиндрической алгебры. Доказывается, что множества общезначимых формул исходной модели и построенной алгебры совпадают. Это позволяет заключить, что логики, полные относительно классов псевдобулевых моделей, полны относительно некоторых классов квазицилиндрических алгебр, или, другими словами, семантика квазицилиндрических алгебр не слабее семантики псевдобулевых моделей.

В параграфе 2.6 определяется понятие квазицилиндрической алгебры Линденбаума—Тарского интуиционистской теории Т 1-го порядка. Ввиду важности этого понятия, оно подвергнуто

тщательному изучению. Доказаны следующие теоремы.

ТЕОРЕМА 2.40. Всякая локально-финитарная алгебра изоморфна алгебре Линденбаума—Тарского подходящей интуиционистской теории.

ТЕОРЕМА 2.42. Пусть Ь — суперинтуиционистская логика, А — локально-финитарная квазицилиндрическая алгебра. Если в А общезначимы все формулы из Ь, то А является гомоморфным образом подходящей алгебры Линденбаума—Тарского логики Ь.

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

По всякой дедуктивной системе 1)5 легко построить многообразие алгебр V(-¿)5), включив в это многообразие только те квазицилиндрические алгебры, в которых верны все тождества Ф = Т, где Ф — схема аксиом дедуктивной системы 1)5. Заметим, что У(1)5) является эквивалентной алгебраической семантикой в смысле [13] дедуктивной системы, в схемы аксиом которой помимо схем аксиом системы 1)5 включены схемы аксиом базовой системы I. Доказана важная

ТЕОРЕМА 2.46. Если 1)5 адекватна логике Ь, то для любой Ь-теории Т имеет место £ V(1)5).

Эта теорема имеет два важных следствия. Первое из которых — независимость класса У(1)5)И алгебр локально-конечной размерности из многообразия V (1)5) от выбора дедуктивной системы 1)5:

СЛЕДСТВИЕ 2.48. Для любой суперинтуиционистской дедуктивной системы /)5; адекватной логике Ь, класс У(1)5)^ совпадает с классом всех локально-финитарных алгебр, в которых общезначимы формулы из Ь, и не зависит от дедуктивной системы 1)5.

Это следствие показывает, что действительным алгебраическим эквивалентом логики Ь является класс алгебр локально-конечной размерности, в которых общезначимы все формулы из Ь. Другое

следствие — теорема о сильной полноте логики L относительно многобразия V(DS) — является одним из основных результатов диссертации и вынесено в параграф 2.7:

ТЕОРЕМА 2.49 (о полноте). Если суперинтуиционистская дедуктивная система DS адекватна суперинтуиционистской предикатной логике L, то логика L сильно полна относительно многообразия V(DS).

В главе 3 изучаются алгебраические эквиваленты известных свойств суперинтуиционистских предикатных логик. В параграфах 3.1-3.5 формулируются алгебраические эквиваленты дизъюнктивного, экзистенциального свойств, свойства Бета (СБ), проективного свойства Бета (ПСБ), интерполяционного свойства выводимости (ИСВ) и импликативного интерполяционного свойства (ИС). Доказываются соответствующие теоремы об эквивалентности. В частности доказано, что алгебраическими эквивалентами свойства Бета, проективного свойства Бета являются соответственно известные [22] свойства ES* и SES сюръективности эпиморфизмов локально-финитарной части соответствующего логике многообразия, а свойств ИСВ и ИС — соответственно свойства амальгамируемости (АР) и сверхамальгамируемости (SupAP) [5] указанного класса локально-финитарных алгебр.

В параграфе 3.6 формулируются алгебраические эквиваленты СБ, ПСБ, ИСВ и ИС суперинтуиционистских дедуктивных систем как систем интуиционистских полимодальных логик. Доказана теорема о том, что алгебраическими эквивалентами свойства Бета, проективного свойства Бета интуиционистских полимодальных логик являются соответственно свойства ES* и SES сюръективности эпиморфизмов всего многообразия, соответствующего полимодальной логике, а свойств ИСВ и ИС — соответственно свойства АР и SupAP указанного многообразия. Доказательство этой теоремы почти дословно повторяет доказательства уже доказанных в данной главе теорем для суперинтуиционистских логик и потому не приводится. Легко доказывается, что если многообразие квазицилиндрических алгебр обладает свойством ES*, SES, АР или SupAP, то его локально-финитарная часть также

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

ТЕОРЕМА 3.15. Если суперинтуиционистская дедуктивная система И5 адекватна логике Ь и обладает свойством СБ (ПСБ, ИСВ, ИС), то и логика Ь обладает свойством СБ (ПСБ, ИСБ, ИС соответственно).

Приведены примеры применений этой теоремы для опровержения СБ и ИСВ в полимодальных логиках.

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

1. Дедуктивные системы

для суперинтуиционистских предикатных логик

В этой главе исследуется представление суперинтуиционистских предикатных логик с помощью дедуктивных систем для пропозициональных полимодальных логик. Основным результатом данной главы является теорема о существовании для произвольной суперинтуиционистской предикатной логики адекватно её представляющей дедуктивной системы.

1.1. Суперинтуиционистские предикатные логики и теории

Будем рассматривать языки 1-го порядка, не содержащие функциональных символов, предметных констант и символа равенства. Предполагаем, что логические символы любого рассматриваемого языка 1-го порядка состоят из нульместных символов Т ("истина"), _1_ ("ложь"), стандартных символов-связок: А, V, Э, ->, V, 3 и вспомогательных символов: (,), ? ("запятая"). При этом множество предметных переменных рассматриваемого языка предполагается равным фиксированному счётному множеству Уаг — {х{ | г < и}. Так как при вышеуказанных соглашениях множество предикатных символов однозначно определяет язык 1-го порядка, будем отождествлять множество предикатных символов и соответствующий ему язык, используя для них одно и то же обозначение. Пусть Р — некоторое множество предикатных символов. Функция # : Р ш каждому р из Р ставит в соответствие его арность, т.е. всякий риз Р есть фр- арный предикатный символ. Обозначаем через Рог(Р) множество всех формул языка Р. Для каждой формулы А обозначаем через FУ(A) множество свободных переменных формулы А, а через Р(А) — множество всех предикатных символов, встречающихся в формуле А. Через Ух А будем обозначать универсальное замыкание формулы А. Для любых двух формул А и В выражение А = В служит сокра-

щением формулы (А D В) Л (В D А).

Пусть Рг— некоторое фиксированное множество предикатных символов, удовлетворяющее следующему условию:

для каждого т < и> существует q из Рг такой, что > т. (*)

Суперинтуиционистской логикой [26] будем называть всякое множество формул языка Рг, содержащее интуиционистскую предикатную логику и замкнутое относительно правила подстановки, modus ponens и правила обобщения. Далее будут рассматриваться только суперинтуиционистские логики, поэтому будем опускать в указанном словосочетании слово "суперинтуиционистская" . Определение правила подстановки легко найти в [4]. Так как в этой работе правило подстановки будет использоваться по существу, целесообразно привести его явно.

Пусть ро,... ,рп — различные предикатные символы, арностей то,... , тп соответственно, Bq, ... ,Вп — некоторые формулы. Для каждого г = 0,... , п пусть уг0,... , у1т. — произвольные различные переменные. Пометим в каждой Bi (г = 0,... , п) свободные вхождения переменных ylQ,... , угт.. Будем говорить, что подстановка (формул) Sßo • • • А допустима, если для каждого i = 0,... , п выполнены следующие условия:

1) для каждого вхождения Pi(zo,... , zrni) в Л ни одно свободное вхождение переменной у\ в Bi не находится в области действия квантора по соответствующей переменной zs]

2) ни одно вхождение Pi(zo,... ,zmJ в А не находится в области действия квантора ни по какой свободной переменной формулы Bi, отличной от переменных Уо,... , угт..

Замечание 1.1. Несмотря на то, что переменные у1- не входят в обозначение подстановки формул, сама подстановка зависит от их выбора. В обозначении подстановки формул предполагается, что указанные переменные уже выбраны и закреплены за соответствующими формулами Bi.

Через Sßo •• - Pßn А будем обозначать результат указанной подстановки, т.е. формулу, которая получена из А одновременной для всех % — 0,... ,п заменой каждого вхождения вида

Pi(zo,.. - , zmi) в А на формулу, полученную из Д одновременной заменой свободных вхождений переменных уг0,... , уг в Д на соответствующие Zq, . . . , Zm.

Таким образом, чтобы совершить подстановку формул Bq, ... , Вп в А вместо ро,... ,рп соответственно, необходимо закрепить у каждой Bi свободные переменные уг0,... , уггщ. Каждая переменная усоответствует j-му месту для переменной при предикатном символе pi. При подстановке каждое вхождение pi с приписанными переменными будет заменено на соответствующую формулу Bi. При этом свободные вхождения ylj (в данном вхождении Bi в результат подстановки) будут заменены на ту переменную, которая стоит на этом j-м месте при указанном вхождении Pi в А.

Говорим, что формула С получена по правилу подстановки из формулы А, если С является результатом некоторой допустимой подстановки формул в А.

Пусть L — некоторая логика, Р — некоторое множество предикатных символов. L-теорией в языке Р называем всякое множество формул указанного языка Р, содержащее все формулы языка Р, являющиеся подстановочными частными случаями формул логики L, и замкнутое относительно правил modus ponens и обобщения. Ясно, что множество всех формул языка Р, являющихся подстановочными частными случаями формул логики L, образует наименьшую L-теорию в языке Р. Будем обозначать эту теорию через L(P).

Пусть L — логика, Р — некоторый язык 1-го порядка, Г U {А} с For(P). Пишем Г \~ь А и говорим "в L из Г выводима Ä\ если формула А принадлежит наименьшей L-теории в языке Р, содержащей множество Г. В случае если Г — пустое множество, пишем L Ь А и говорим "в L выводима А".

Стандартным образом доказываются следующие известные теоремы.

ТЕОРЕМА 1.2 (Теорема о дедукции). Пусть L — суперинтуиционистская предикатная логика, Г — последовательность формул, А и В — формулы.

Тогда Т,А\-Ь В ГЬ^УжАэЯ.

ТЕОРЕМА 1.3 (Теорема о замене). Пусть L —суперинтуиционистская предикатная логика, А, В и С — формулы. Если D — результат замены в С некоторого вхождения подформулы А на формулу В и L\- А = В, то L Ь С = D.

Пусть А — формула, г0,... , гп, j0,... , j„ < ш, и все г0,... , гп различны. Если для каждого к = 0,... , п ни одно из свободных вхождений переменной Xik в А не находится в области действия кванторов по переменной Xjk, то говорим, что допустимо применение к А операции замены переменных s^...^ (или, короче: замена переменных s^'^A допустима) и обозначаем через s^'.'^A формулу, полученную в результате одновременной замены всех свободных вхождений .. ,Х{п в формуле А на Xj0,... , Xjn соответственно. В противном случае говорим, что указанная замена недопустима.

ЛЕММА 1.4. Пусть L — суперинтуиционистская предикатная логика, А — формула. Если L\- А и замена s^A допустима, то L h SjA.

Доказательство. Действительно, по правилу обобщения из L Ь А следует L b Va^A Поскольку Int b Ух^А Э s^A, применяя modus ponens, имеем L\- slj А. □

В интуиционистской логике верны следующие известные эквивалентности: Vrrр(х) = Мур(у) и Зхр(х) = 3ур(у), гдер — унарный предикатный символ, х и у — переменные. Эти эквивалентности, используя теорему о замене, несложно обобщить на случай произвольной формулы и получить в результате известный принцип замены связанных переменных [3], который часто будет использоваться в данной работе для построения интуиционистски эквивалентных формул. Говорим, что формула В получена из формулы А заменой связанной переменной, если В получается из А заменой некоторого вхождения подформулы Ух{А' (3Х{А') на подформулу VxjSjA' (3XjSjA' соответственно), при этом предполагается, что замена переменных s^A' допустима, и переменная Xj не входит свободно в А'. Формулы А и В называем конгруэнтными (пишем: А ~ В), если существует такая последова-

тельность формул Aq,... ,Ап, что Л о = А, Ап = В, и для всякого к = 0,... , п—1 формула Afc+i получается из А^ заменой связанной переменной. Очевидно, что отношение конгруэнтности является отношением эквивалентности на классе формул.

ТЕОРЕМА 1.5 (Принцип замены связанных переменных).

Для любых формул А и В если А ~ В, то Int b А = В.

1.2. Суперинтуиционистские дедуктивные системы

Будем рассматривать следующий язык М.С для дедуктивных систем. Пусть алфавит языка Л4.С содержит бесконечное множество Рт = символов пропозициональных переменных, пропозициональные константы Т,±, одноместные символы (i,j < и), двуместные символы: V,A ,Э.

Замечание 1.6. Символы 3* (VJ соответствуют операциям связывания квантором существования (всеобщности) переменной в формулах 1-го порядка. Символы slj соответствуют операциям замены свободных вхождений переменной Х{ на переменную Xj в формулах 1-го порядка. (Символы для указанных операций замены не присутствуют в языке 1-го порядка. Но эти операции неявно используются для отражения связи, например, между такими формулами, как р(хо), р(х\), \/х2р(х2) и т.п. Примеры такого использования вышеуказанных операций можно встретить не только в формулировках метатеорем об изучаемых логиках, но и в формулировках аксиом и правил вывода для предикатных логик.)

Формулу Ф языка ЛЛС будем называть схемой формул. Множество всех схем формул обозначим Fm.

Пусть П — множество формул языка (Xj | j € J) —

список всех символов из Рт,, которые имеют вхождение в какую-нибудь из схем множества П. Будем писать ü(Xj | j £ J) вместо П если требуется явное указание на Xj. Если (Xj | j 6 J) = (Xq,... ,ХП), то есть список таких Xj конечен, то пишем:

П(Хо,... ,Хп), вместо П(Х5- | ^ £ </). Если же П состоит из одной формулы Ф, то есть П = {Ф}, то в этом случае будем писать Ф(Ху | з £ «/) и Ф(Х0,... ,Х„) вместо | з £ 7) и {Ф}(Хо,... ,Хп) соответсвенно.

Правилом вывода называем конструкцию П Ь Ф, где П и {Ф} — конечное множество схем формул. Дедуктивной системой называем пару (5, Я), где 5 с Рт (элементы ¿> будем называть схемами аксиом) и й — некоторое множество правил вывода.

Пусть Ф(Хо, • • • , Хп) — схема формул, ... ,Ап — формулы. Говорим, что формула С является частным случаем схемы формул Ф при подстановке Л0,... , А п вместо Хо,... , Хп соответственно, если выполнено какое-нибудь из следующих условий:

1) Ф = Х{ и С совпадает с Д-;

2) Ф = Т (_1_) и С = Т (соответственно: С = _1_);

3) ф = -,ф (\^ФДФ) и С = -уИ соответственно), где формула Б является частным случаем схемы формул Ф(Хо,... , Хп) при подстановке Ао,... ,Ап вместо Хо,... ,Хп соответственно;

4) Ф = в^Ф, г,] < и) и С = в^В, где замена переменных в^И допустима, а формула В конгруэнтна некоторому частному случаю схемы формул Ф(Хо,... , Хп) при подстановке Ао,... , Ап вместо Хо,... ,Хп соответственно;

5) Ф - Ф Л Ф' (Ф V Ф',Ф Э Ф') и С = £> Л У (£> V В', В Э В' соответственно), где И и И' — частные случаи схем формул Ф и, соответственно, Ф' при подстановках формул Ао,... , Ап вместо Хо,... , Хп.

Через Ф(Д), ...,Ап) будем обозначать произвольный частный случай схемы формул Ф при подстановке Ао,... ,Ап вместо Хо,... ,ХП соответственно. Если П(Х^- | ] £ </) — множество схем формул, а А^ {] £ </) — формулы, то через П(Ау | ] £ 3) будем обозначать множество частных случаев схем формул из П, полученных при подстановке формул Авместо соответствующих

X,.

Пусть Ф(Хо,... , Хп) — произвольная схема формул, Aq, ... , Ап, Bq, ... ,Вп — формулы. Индукцией по построению Ф нетрудно доказать следующую лемму:

ЛЕММА 1.7. Пусть С и D — частные случаи схемы Ф(Хо,... , Хп) при подстановках формул Ао,... ,Ап и, соответственно, Bq, ... ,Вп вместо Xq, ... , Хп.

Если Int I- Ао = В0,... , Int b Ап = Вп, то Int b С = D.

Пусть Xq, ... , Хт все символы из Рт, которые имеют вхождение в правило вывода Фо> • • • > ^n-i Ь

Говорим, что формула Ап является непосредственным следствием формул Aq,... , Ап-\ по правилу вывода • • • > ^п-1 I- Фп, если для некоторых формул Bq, ... , Вт каждая А\ является частным случаем соответствующей схемы при подстановке формул Bq, ... , Вт вместо соответствующих Х0, • • • , Хт.

Выводом формулы А в дедуктивной системе DS из множества формул Г называем всякую последовательность формул Bq, ... ,Вп такую, что А = Вп, и каждая формула В( данной последовательности либо есть частный случай некоторой схемы аксиом дедуктивной системы DS, либо принадлежит Г, либо является непосредственным следствием некоторых предыдущих формул по какому-либо правилу вывода указанной дедуктивной системы. Пишем Г \~£,s А если существует вывод формулы А в DS из Г. Говорим, что А выводима в DS, и пишем DS b А, если 0 \~ds А-

Обычным образом можно определить понятие вывода схемы формул в дедуктивной системе. Говорим, что схема формул Фп является непосредственным следствием схем формул Фо,... , Фп-1 по правилу вывода Фо№> • • • , Хт),... , Фп_ i(X0, •. • , Хт) b ФП(Х0,... , Хт), если для некоторых схем формул ©о, • • • , От каждая Фг- является частным случаем соответствующей схемы при подстановке схем ©о,... , @то вместо соответствующих Хо,... , Хт.

Выводом схемы формул Ф в дедуктивной системе DS из мноэюества схем формул П называем всякую после-

довательность схем формул Фо, • • • , Фп такую, что Ф = Фп, и каждая схема формул Ф« данной последовательности либо есть частный случай некоторой схемы аксиом дедуктивной системы DS, либо принадлежит П, либо является непосредственным следствием некоторых предыдущих схем по какому-либо правилу вывода указанной дедуктивной системы. Пишем П \\~ds Ф, если существует вывод схемы формулы Ф в DS из П. Правило П Ь Ф называем выводимым в системе DS, если П Ibps Ф. Говорим, что Ф выводима в DS, и пишем DS Ib Ф, если 0 II-ds Ф-

Говорим, что дедуктивные системы эквивалентны, если множества выводимых в них схем формул совпадают.

Суперинтуиционистской дедуктивной системой называем всякую дедуктивную систему, множество выводимых формул которой содержит интуиционистскую логику, а множество правил вывода совпадает с множеством Rq = {X, X Э Y b Y} u {X h | i < üj}.

Пример 1.8. Примером суперинтуиционистской дедуктивной системы является следующая дедуктивная система Iq для интуиционистской логики. Множеством правил вывода системы /о является множество Rq (т.е. modus pones и правила навешивания квантора всеобщности по каждой переменной), а множество схем аксиом Iq состоит из следующих групп схем (i,j Е со):

(h) ± Э X;

(h) X Э Т;

(h) XD(YD X);

(h) (XDY)D ((X D (Y D Z)) D (X D Z)); (h) (X A Y)D X; (16) (X a Y) d Y;

(h) {X э Y) D ((X D Z) D (X D (Y A Z)));

(Is)XD(XVY);

(I9)XD(YVX);

(1ю) (Хэг)э ((у ЭЯ)Э ((х У¥)э г)); (1ц) (Хэ¥)э ((X э -У) 3 --Х);

(1и) УгХ Э 3)Х; (1гя) з)Х э ^Х;

(1и) ЧХ э з)У) э &Х э 4-у) (г ф 3);

(115) ЩХ Э У) Э (4-Х Э У,-У) (г ф з).

Нетрудно обобщить доказательство А. Чёрча [9] о допустимости правила подстановки в интуиционистском исчислении предикатов (см. также [4]) на случай произвольной суперинтуиционистской дедуктивной системы и доказать следующую теорему:

ТЕОРЕМА 1.9. Множество формул, выводимых в произвольной суперинтуиционистской дедуктивной системе, замкнуто относительно правила подстановки.

В дальнейшем мы ограничимся изучением суперинтуиционистских дедуктивных систем и поэтому будем часто опускать в вышеуказанном словосочетании слово "суперинтуиционистская" и отождествлять суперинтуиционистскую дедуктивную систему с множеством её схем аксиом.

1.3. Адекватность суперинтушщонистских дедуктивных систем суперинтуиционистским логикам

Будем говорить, что дедуктивная система 1>5 адекватна логике Ь, если множество формул выводимых в ББ совпадает с Ь.

Легко доказать следующее

ПРЕДЛОЖЕНИЕ 1.10. Если суперинтуиционистская дедуктивная система Ив адекватна логике Ь, то для любого множества формул Г и любой формулы А верна эквивалентность Г \-ьА <=> Г 1-Д5 А.

Легко доказывается

ТЕОРЕМА 1.11. Пусть ЩХ, | j 6 J) U {Ф(Хj | j 6 J)} — множество схем формул, DS — дедуктивная система. Если П 11-д5 Ф, то для любого списка формул (Aj | j Е J) выполнено

п (Aj I jeJ) \-DS ф {Aj | jeJ).

Таким образом, если DS адекватна логике L, то все доказуемые в DS схемы формул являются метатеоремами логики L.

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

Рассмотрим следующие простые примеры.

Пример 1.12. 1) Дедуктивная система Iq из примера 1.8 адекватна интуиционистской логике предикатов. Действительно, нетрудно проверить, что все частные случаи схем аксиом Iq являются интуиционистски верными. Более того, все аксиомы интуиционистской предикатной логики из [2] являются частными случаями схем аксиом Iq.

2) Другим примером дедуктивной системы, адекватной интуиционистской логике предикатов, служит система I, дополненная по сравнению с Iq следующими группами схем аксиом (i, j, к < и):

(he 4X = X;

(hi 3iX d уд-х;

(hs s)\/iX = МгХ;

(h9 3iS)X Ds)X(i^ j);

(ho s)3kX = 3ks)X (к ф i,j);

(hi sfikX = Vks)X (к ф i, j);

(h2 s)sfX = skjS)X;

(hs s)s{X = sfs)X (к ф i,j и

(124 s)(X DY) = s)X d s)Y;

(hb) S)(X AY) = s)X Л s)Y; (J26J s)(X\/Y) = s)Xy s)Y; (I27) s)^X =

Схемы аксиом (Iw)~(h7) формализуют некоторые общие принципы, отражающие свойства языка 1-го порядка или же выводимые в интуиционистской логике с использованием особенностей языка 1-го порядка. К таким принципам относятся, например, принципы сокращения и перестановки кванторов в интуиционистски верных формулах, а также принципы работы с операциями замены свободных переменных.

Нетрудно видеть, что частные случаи схем (I\§)-(hi) при подстановке вместо пропозициональных переменных X и Y каких-либо формул 1-го порядка являются интуиционистски верными. Таким образом, добавление к Iq схем (I\q)~(Iti) не испортило нам дедуктивной системы, и I также адекватна интуиционистской логике.

3) Логике с элиминацией кванторов QE ^ Int + 3хр(х) D Ухр(х) (где р — унарный предикатный символ, ах — произвольная переменная) адекватна дедуктивная система D(QE) I u {3iX DViX\i< и).

Легко проверить, что D(QE) адекватна логике QE.

4) Логике константных областей CD — Int + Уг(А V В) D (А V УхВ) (где А и В — произвольные формулы и х 0 FV(A)) будет адекватна дедуктивная система D(CD) = IU {Уг'^Х V Y)D(s)XV\/iY)\i^j}.

Очевидно, что все частные случаи схем вида Уi(sljX V Y) D (s)X V У ¿У) (г ф j) имеют вид У х(А У В) Э (А V У хВ), где х $ FV{Ä). Обратно, для любого г, если Х{ 0 FV(A), то s'jA — А и, значит, всякая формула У xi{A V В) D (А V Ух ¡В), где Х{ £ FV(A), является частным случаем схемы аксиом УД^ХУУ) э (4ХУУгУ).

5) Построение адекватных дедуктивных систем для логик из предыдущих пунктов не представляет трудностей ввиду про-

стоты их аксиом. Рассмотрим логику Int3 ^ Int + Fq2 [37], где

Fq2 ^ (3xqi(x) Л 3xq2{x) Л \/x^(qi(x) Л q2(x)) Л Vx(qi(x) D р(х)) Л Vx(q2(x) D р{х))) D (3xri(x) Л 3xr2(x) Л Vx^(ri(x) Л r2(x)) Л

\/x(ri(x) D -*p(x)) Л Vx(r2(x) D ->р(ж))).

Чтобы отразить в соответствующей схеме аксиом, что, например, переменная х входит и в q\(x), ив р(х) в подформуле q\{x) Э р{х), необходимы символы slj. Рассмотрим схему аксиом

вц ^ {3jS)X Л 3js)Y Л y3slr(X Л У) Л

Щ(Х D Z) AVjS)(Y D Z)) D (3jS)X' Л 3]S)Y' Л \fjs)^(X' Л У') Л

Vjs)(X' D ~>Z) л yjS){Y' d iz)).

Нетрудно доказать, что дедуктивная система D(Inta) I U {Gjj | i ф j} адекватна логике Intß. Ясно, что все частные случаи схем вида Qij (i ф j) при подстановке p{xi) вместо Z, q\{xi) вместо X, q2(xi) вместо Y, r\(xi) вместо X' и г2(х{) вместо Y' дают нам аксиому

(3xjqi(xj) Л 3xjq2(xj) Л Vxj->(qi(xj) Л q2(xj)) Л

(*j) D p{xj)) r\Mxj(q2(xj) D p(xj))) D (3xjri(xj) Л 3xjr2(xj) Л Mxj-y(r\(xj) Л r2(xj)) Л

Mxjir^xj) D ~>p(xj)) Л \/xj(r2(xj) D ~ip(xj))).

Таким образом, для проверки адекватности достаточно проверить, что все частные случаи дополнительных схем аксиом D(Intß) будут являться подстановочными частными случаями аксиомы Fq2. Действительно, пусть А — частный случай

схемы для некоторых г ф Тогда А имеет вид

(Зх^Вх А ЗхуВ2 А Мх^(Вх А В2) л

Ух^Вг Э £>) Л \fxjiB2 Э £>)) Э (3x^1 А 3х,С2 А А С2) Л

Ух^Сх э --£>) Л Уз,-(С2 Э ->£>)).

Пометим в формулах В\, В2, С\, С2 и В переменную Ху Легко видеть, что

А = ЗвХсгс2о((3хМ*з) Л А ф^) А

э р(х^) А Ух^2(ху) Э р{хэ))) Э (3хуг\(х^) А Зх^г2(х^) А Уа^—'(п(^) А г2(х^) А

Уа^г^-) э ->р(х,)) А Ух,(г2(ху) Э ~<р(хз))))-

Замечание 1.13. 1) Системы 1о и I из пунктов 1)-2) приведённого выше примера не являются эквивалентными. Можно доказать, что схема аксиом (1\ъ) не выводима в системе /о. Таким образом, для фиксированной логики может существовать несколько адекватных ей неэквивалентных дедуктивных систем.

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

2) Используя принцип замены связанных переменных, нетрудно доказать, что для любых фиксированных индексов i и ] следующие дедуктивные системы также будут адекватны логикам ЕС}, СБ и 1г^з соответственно: I и {3{Х э I и V У) э {з)Х V у4У)} и / и {еу}.

Целью этого параграфа является теорема о существовании дедуктивной системы, адекватной произвольно взятой суперинтуиционистской логике. Для достижения этой цели понадобятся некоторые дополнительные построения и леммы.

Пусть Т — 1п1;-теория. Через £>5(Т) обозначим множество всех таких схем формул Ф, что если формула А является частным случаем Ф, то А £ Т. Аналогичный В в (Г) объект для классических теорий Т первого порядка с равенством был введён В. В. Рыбаковым в [30], где этот объект назван логикой схем теории Т и обозначен через Ь5(Т).

Рассмотрим суперинтуиционистскую дедуктивную систему

(Р5(Т);До).

Доказательство следующей леммы опущено из-за его тривиальности.

ЛЕММА 1.14. Для всякой формулы А, если 1>5(Т) Ь А, то А £ Т.

Из теоремы 1.9 немедленно следует, что утверждение, обратное к утверждению леммы 1.14, неверно для суперинтуиционистских теорий, не замкнутых относительно правила подстановки.

Далее будет доказано, что если теория Т является логикой, то обращение леммы 1.14 имеет место. Как будет доказано ниже, для этого достаточно указать способ построения по произвольной формуле А, верной в логике некоторой схемы формул Ф[А] из частным случаем которой являлась бы исходная формула А. Для простоты будем рассматривать только те формулы, чьи связанные переменные имеют индексы большие, чем любая арность предикатных символов, входящих в эту формулу. Такие формулы будем называть простыми. В силу принципа замены связанных переменных (теорема 1.5) любая формула интуиционистски эквивалентна некоторой простой формуле.

Далее приведён один из многих таких способов построения схемы Ф[А] по простой формуле А.

Пусть каждому предикатному символу р, имеющему вхождение в А, взаимно-однозначно поставлена в соответствие некоторая пропозициональная переменная X из Рт. Также поставим в соответствие символу р последовательность 0,... , т (т + 1 = фр) индексов переменных. Заметим, что £()>••• , хт не встречаются в формуле А связанно, так как А — простая формула.

Пусть Ао,... , А/ — последовательность различных индексов

всех тех переменных, в область действия кванторов по которым попадает символ р в А. Пусть vq, ... — произвольная последовательность различных индексов, не встречающихся среди индексов переменных в формуле А и среди 0,... , т. Будем говорить в дальнейшем, что vs соответствует \s в схеме Ф[А]. Последовательность vо? • • • , Щ будем называть дополнительной последовательностью индексов для данного символа р в А. Для большей простоты обозначений будем считать, что для любых двух дополнительных последовательностей (для некоторых р и q в А) одна из этих последовательностей является начальным сегментом другой.

Пусть индексы ко, • • • i кт различны и не встречаются среди индексов переменных в формуле А и среди индексов Ло,... , Л/, fo,... , щ, 0,... , т. Последовательность ко,... , кт будем называть вспомогательной последовательностью индексов для данного символа р в А. Также как и в случае дополнительных последовательностей считаем, что для любых двух вспомогательных последовательностей для А одна из этих последовательностей является начальным сегментом другой.

Построение схемы Ф[А] состоит в замене каждого вхождения p(xi0,... , Xim) в формуле А на следующую схему формул:

fco . . . „fcm „О т Xо . . . САI у

¿0 im, fco bkmöV„ bViЛ J

а вхождений вида Vasj и Зх{ на символы \/г- и 3^ соответственно, где X из Рт и последовательности индексов Ло,... , Л;, Ро,... , ui, fco, • • • , кт выбраны для данного р указанным выше образом.

Замечание 1.15. Поясним на неформальном уровне роли последовательностей индексов, участвующих в построении схемы Ф[А]. На формальном уровне роли этих последовательностей прояснятся в доказательстве леммы 1.17.

1) Громоздкость построения схемы Ф[А] (в том числе обилие индексов в указанной схеме) отчасти вызвана тем, что в языке АЛ С отсутствуют символы модальностей, которые соответствовали бы операциям одновременной замены свободных вхождений нескольких переменных в формулах языка С. Из-за

отсутствия этих символов приходится вводить последовательность к8.

В построении Ф[-А] интуитивно использовались следующие факты:

а) Если множества переменных {жл0,... , и {хщ,... , х^} не пересекаются, то для всякой формулы А имеем

• ■ • з^А = в^.'.'^'А. Это метаравенство может не выполняться, если указанные множества пересекаются. Например: хг) = р(х2, х2), а ¿р(ж0, хг) = р(х2, х0).

б) Если переменные хко,... ,хкт не встречаются среди свободных переменных формулы А и среди переменных

т>. <т>. г • т ■ ФП Л . . . с^т с30 ¿т Л — „30"'3т Л

2) Роль выделенной последовательности 0,... , га состоит в том, чтобы фиксировать соответствие между пропозициональной переменной X языка Л4.С и некоторой фиксированной атомарной формулой языка С, а именно: р(хо,... , хт).

Более точно, каждой подстановке произвольной формулы В вместо X в Ф[А] будет соответствовать подстановка (см. стр. 18) в формулу А вместо р формулы В с помеченными переменными хо,... , хт.

3) Роль последовательностей А«,. и гл, состоит в том, чтобы явно указать в схеме Ф [А] те индексы переменных, под квантор по которым попадает символ р в А.

Как сказано в 2), подстановке вместо X в Ф[А] некоторой формулы языка С соответствует некоторая подстановка формул в А вместо р. Чтобы эта подстановка формул была допустимой, и необходимы блоки вида й^0 ■ • • в определении Ф[А].

Например, пусть некоторое вхождение р(хг0,... , Х{т) в А находится под действием квантора по х\, но х\ не встречается среди хг0,... , хгт и среди хо,... ,хт. Если в построении Ф[А] опустить блоки вида • • • , то при подстановке в схему Ф[А] вместо X некоторой формулы В со свободным вхождением х\ переменная х\ в В окажется связанной указанным вы-

ше квантором, что повлечёт недопустимость подстановки в А вместо р формулы В с помеченными переменными хо,... , хт.

Отметим, что при построении схемы Ф[А] допускается большой произвол в выборе X из Рт и указанных последовательностей индексов для каждого предикатного символа р в А.

Пример 1.16. Пусть

А ^ Ухз(ро(хз, XI) Э р\{х2)) Э (Зх2р0(х2, хг) Э р1(х2)).

Выбор индексных последовательностей осуществляем в соответствии с таблицей:

к vs ks

Ро PI 2,3 3 4,5 4 6,7 6

Тогда в качестве Ф[А] можно взять следующую схему формул:

э s62s°6slY) э (32sWA*7*14X 444У)-

JIEMMA 1.17. Пусть А — простая формула. Для любой п.с.и. логики L, если А 6 L, то Ф[А] € DS(L).

Доказательство. Пусть Ф[А] = Ф(ХРо,... ,ХРп), Aq, ... , Ап £ For и определена формула Ф(Ао,... , Ап).

Доказательство леммы будет осуществлено в несколько этапов. Сначала по Ао,... , Ап будут построены некоторые формулы Bq, ... , Вп такие, что Int Ь Ф(Ао,... , Ап) = Ф(Бо>... , Вп). Затем будут построены две подстановки формул, последовательное применение которых к формуле А даст формулу Ф(Д), • • • > Дг)- Тогда в силу того, что множество L замкнуто относительно правила подстановки, получим: L Э Ф(-Во> • • • > Дг)- Из того, что L Э Int, получим Ф(Ао,... , Ап) £ L. Следовательно, в силу произвольности Ао,... , Ап, Ф[А] будет принадлежать DS(L).

Пользуясь принципом замены связанных вхождений переменных (см. стр. 20), по каждой формуле А{ строим формулу Bi, заменяя все связанные вхождения переменных в формуле Aj на некоторые новые различные переменные, индексы которых не встречаются в Ф[А] и не имеют вхождений ни в одну из

формул А, Aq, ... , An, Во,... , Bi-1, Д+ь ... ,Вп (причём, каждая новая переменная встречается в двух местах в формуле Bi тогда и только тогда, когда заменяемая ею переменная имеет вхождения в соответствующих местах формулы Ai). Ясно, что Int b Aq ее Во, ... ,Int Ь Ап = Вп. По лемме 1.7 получаем, что Ш^Ф(А0,... ,Ап) = Ф(В0,... ,Вп).

Для каждого г пусть ш,; + 1 = фрг, ко,.. • , кт — вспомогательная последовательность индексов для pi и Ад,... , А}. — (различные) индексы переменных, в область действия кванторов по которым попадает pi в формуле А, а щ,... , щ. им соответствующие индексы в схеме Ф[А]. Поставим взаимно-однозначно в соответствие каждому pi некоторый предикатный символ qi такой, что арность qi больше или равна суммы арности pi с длиной последовательности Aq, ... , А], т.е. #qi > #pi + ^ + 1. (Такие qi существуют в силу условия (*) для Р.) Положим:

Di — 0) • • • > xmi, xVo,... , xVl, xVlr,... , х

"и,

Для дальнейшего можно считать, что = #Рг + /г- +1. Пометим в каждой Д свободные переменные хо,... ,хт. Очевидно, что подстановка формул • • • ^ А допустима. Обозначим через В результат этой подстановки. Очевидно, что в В входят лишь те переменные, индексы которых встречаются в схеме Ф[А|.

Заменим теперь в каждой Д все свободные вхождения переменных хко,... , Хкт. на переменные хо,... , хт. соответственно. В результате таких замен во всех Д получим формулы Со,... ,Сп. Пометим в каждой из С г свободные переменные хо,... , хт, Хуо,... , Хц и рассмотрим подстановку • • • дспВ.

Пусть г = 0,... ,п произвольно. По построению В получаем, что любое вхождение ^ в В имеет вид:

Список литературы диссертационного исследования кандидат физико-математических наук Тишковский, Дмитрий Евгеньевич, 1999 год

Литература

[1] Вольтер Ф., Захарьящев М. Об интуиционистских модальных логиках//Алгебра и логика. —1997. — Т.36, №2. — С. 121-155.

[2] Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М.: Наука, 1979.

[3] Ершов Ю. JI., Палютин Е. А. Математическая логика. — М.: Наука, 1979.

[4] Клини С. К. Введение в метаматематику. — М.: ИЛ, 1957.

[5] Максимова Jl. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых ал-гебр//Алгебра и логика. — 1977. — Т.16, №6. — С.643-681.

[6] Максимова JI. Л. Интерполяционные теоремы в модальных логиках и амальгамируемые многообразия топобулевых ал-гебр//Алгебра и логика. — 1979. — Т.18, №5. — С.556-586.

[7] Максимова Л. Л. Модальные логики и многообразия модальных алгебр: свойства Бета, интерполяция и амальгамируе-мость//Алгебра и логика. — 1992. — Т.31, №2. — С.145-166.

[8] Расёва Е., Сикорский Р. Математика метаматематики. — М.: Наука, 1972.

[9] Чёрч А. Введение в математическую логику. Т.1. — М.: ИЛ, 1960.

[10] Шрайнер П. А. Интерполяция и определимость в логиках конечных областей: дис...канд.физ.-мат.наук: 01.01.06. — Новосибирск,1998.

[11] Andréka Н. Algebraizable logics, and algebraizable semantic logics; a unified theory//Workshop on Abstract Algebraic Logic, Centre de Recerca Matemática, Bellaterra, Spain, july 1997: Abstracts of talks. — P.7-8.

[12] Andréka H., Németi I., Sain I. Abstarct model theoretic approach to algebraic logic. — Manuscript, 1984.

[13] Blok W. J., Pigozzi D. Algebraizable logic//Memoirs Amer. Math. Soc. — 1989. — Vol.77, №396.

[14] Craig W. Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory//J. symbol, log. — 1957. — Vol.22. — P. 269-285.

[15] Czelakowski J. Logical matrices and the amalgamation proper-ty//Stud. log. — 1982. — Vol.41, №4. — P.329-341.

[16] Halmos P. R. Algebraic Logic. — New York: Chelsea Publ. Co., 1962.

[17] Henkin L., Monk J. D., Tarski A. Cylindric algebras. — Amsterdam: North Holland, 1971, 1985. — Pts 1,2.

[18] Hoogland E. Algebraic characterizations of two beth definability properties//Workshop on Abstract Algebraic Logic, Centre de Recerca Matemática, Bellaterra, Spain, july 1997: Abstracts of talks. — P.48-52.

[19] Madarász J. X. Craig interpolation in algebraizable log-ics//Workshop on Abstract Algebraic Logic, Centre de Recerca Matemática, Bellaterra, Spain, july 1997: Abstracts of talks. — P.69-70.

[20] Madarász J. X. The Craig Interpolation Theorem in multi-modal logics//Bull, of the Section of Logic. — 1995. — Vol.24, №3. — P. 147-154.

[21] Maksimova L. On maximal intermediate logics with disjunction property//Stud. log. — 1986. — Vol.45, №1. — P.69-75.

[22] Maksimova L. Explicit and Implicit Definability in Modal and Related Logics//Bull. of the Section of Logic. — 1998. — Vol.27, №1/2. — P.36-39.

[23] Németi I. Algebraization of quantifier logics, an introductory overview//Stud. log. — 1991. — Vol.50, №3/4. — P.485-570.

[24] Németi I. Multi-modal logics and algebraization of quantifier logics//Workshop on Abstract Algebraic Logic, Centre de Recerca Matemática, Bellaterra, Spain, july 1997: Abstracts of talks. — P.76-77.

[25] Ono H. A study of intermediate predicate logics//Publ. Res. Inst, math. sci. — 1973. — №8. — P.619-649.

[26] Ono H. Some problems in intermediate predicate logics//Rept. math. log. — 1987. — Vol.21. — P.55-67.

[27] Pinter C. Cylindric algebras and algebras of substitutions//Trans. Amer. Math. Soc. — 1973. — Vol.175. — P.167-179.

[28] Pinter C. A simple algebra of first order logic//Notre Dame J. form. log. — 1973. — Vol.14, №3. — P.361-366.

[29] Rasiowa H. An Algebraic Approach to Non-Classical Logics. — Amsterdam: North-Holland, 1974. — (Studies in Logic and the Foundation of Mathematics: Vol.78).

[30] Rybakov V. V. Logics of schemes for first-order theories and poly-modal propositional logic//Advanced in Intentional Logic. — Kluwer Acad. Publ., 1996. — P.93-106.

[31] Sain I. On algebraic characterizations of some definability properties//Workshop on Abstract Algebraic Logic, Centre de Recerca Matemática, Bellaterra, Spain, july 1997: Abstracts of talks. — P. 108-116.

[32] Tarski A. Grundzüge des Sistematikalküls. Erster Teil//Fund. Math. — 1935. — Vol.25. — P.503-526.

[33] Venema Y. Many-Dimensional Modal Logic: PhD thesis. — Institute for Logic, Language and Information, Universiteit van Amsterdam, 1989.

[34] Тишковский Д. E. Алгебраизация суперинтуиционистских предикатных логик//Материалы XXXIII международной научной студенческой конференции "Студент и научно-технический прогресс", Новосибирск, 1995. — С.32.

[35] Тишковский Д. Е. Об алгебраизации предикатных суперинтуиционистских логик//Материалы XXXIV международной научной студенческой конференции "Студент и научно-технический прогресс", Новосибирск, 1996. — С.84.

[36] Тишковский Д. Е. Алгебраические эквиваленты некоторых свойств суперинтуиционистских предикатных логик. — Новосибирск, 1998. — 15 с. — (Препринт/НИИ МИОО НГУ; №38).

[37] Тишковский Д. Е. Интерполяционное свойство и суперинтуиционистские предикатные логики//Сиб. мат. журн. — 1998.

— Т.39, №1. — Р. 172-180.

[38] Тишковский Д. Е. Об алгебраической семантике для суперинтуиционистских предикатных логик//Алгебра и логика. — 1999. — Т.38, №1. — Р.68-95.

[39] Tishkovsky D. On Algebraic Counterpart of Beth Property of Superintuitionistic Predicate Logics//Logic Colloquium'98 (the 1998 ASL European Summer Meeting), Prague, Czech Republic, aug. 9-15 1998: Book of abstracts. — P. 106.

[40] Tishkovsky D. E. Some Superintuitionistic Predicate Logics without Interpolation Property//Second Workshop on Non-Standard Logics and Logical Aspects of Computer Science, Irkutsk, Russia, june 1995: Abstract of Papers. — P.80.

[41] Tishkovsky D. E. Constructing total algebraic semantics for superintuitionistic first-order logics//Conference on Universal Algebra and Lattice Theory, Szeged, Hungary, july 1996: Abstracts.

— P.59.

[42] Tishkovsky D. E. On algebraic semantics for superintuitionistic first-order logics//Minisemester on Logic, Algebra and Computer Science (Helena Rasiowa in memoriam), Warsaw, Poland, dec. 1996: Abstracts. — P.32.