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

РГб од

- 6 СЕН 2000

Министерство образования Российской Федерации Удмуртский государственный университет Математический факультет

На правах рукописи

Яшин Александр Данилович

Полнота и аксиоматизируемость неклассических логик с дополнительными логическими связками

01.01.06 — математическая логика, алгебра и теория чисел

Автореферат диссертации на соискание ученой степени доктора физико-математических наук

Ижевск 2000

Работа выполнена в Удмуртском государственном университете

Официальные оппоненты:

доктор физико-математических наук профессор Пальчунов Д.Е. доктор физико-математических наук профессор Рыбаков В.В. доктор физико-математических наук профессор Захарьящев М.В. Научный консультант — доктор физико-математических наук профессор Артемов С.Н.

Ведущая организация: Институт проблем передачи информации РАН (Москва)

Защита состоится " 8 "сентября 2000 года на заседании специализированного Совета Д.064.61.02 по защите диссертаций на соискание ученой степени доктора физико-математических наук при Красноярском государственном университете по адресу:

660041, Красноярск, пр. Свободный, 79

С диссертацией можно ознакомиться в библиотеке КГУ по адресу 660041, Красноярск, пр. Свободный, 79

Автореферат разослан " У * 2000 года

Ученый секретарь специализированного Совета У

кандидат физико-математических наук Голованов М.И.

В (23^03

Общая характеристика работы.

Исследование какого-либо объекта (или класса объектов), первоначально успешно продвигающееся в "глубину", на некоторой стадии достигает "предельной точки", когда обычные усилия уже не приводят к отысканию существенно новых свойств этого объекта.

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

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

Следующие примеры непосредственно связаны с математической логикой: булевы алгебры с операторами; булевы алгебры с выделенными идеалами; языки более высокого порядка; относительно элементарная определимость и др.

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

Согласно гильбертовской концепции основное назначение идеальных понятий (другое название — экстрапонятия) — либо получение новых реальных знаний об изучаемых объектах, либо более простое обоснование уже известных свойств. Например, к числу реальных утверждений Гильберт относил арифметические формулы вида Vi(/(i) = g(x)) для вычислимых функций / и д.

При этом первичным требованием к вводимым экстрапонятиям является консервативность, т.е. введенные экстрапонятия не должны изменять объем реальных знаний.

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

Вместе с тем за эту универсальность первопорядкового языка пришлось расплачиваться. Неполнота и неразрешимость — наиболее известные последствия.

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

Здесь уместно упомянуть современную модальную логику, которая получается из классической двузначной логики введением дополнительных модальных операторов [1, 40]. В рамках модальной логики удается описать чисто логические аспекты разных прикладных теорий, от формальной арифметики Пеано до вопросов прикладной информатики.

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

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

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

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

языке этот оператор представляется как дополнительная одноместная связка.

К настоящему моменту в литературе накопилось большое число примеров логик, полученных из Int расширением языка дополнительной связкой (или связками). Выбор тех или иных связок основывался на различных соображениях. Чаще всего новая связка возникала из некоторого "интересного" или "полезного" понятия, определимого в языке описания конкретной семантики Int. Главный упор в последующих исследованиях делался на построении аксиоматики, изучении свойств и приложений получающихся логик. К этому типу можно отнести работы по следующим направлениям:

модальности (аналоги классических модальностей) в Int: Булл1966, Божич к Дошен1984, Эвальд1986, Серви1977, Сотиров1984, Виллиамсон1992, Вольтер & Захарьящев1997;

временные связки в Int: Каминский1988, Габбай1975, Лопес-Эскобар1985, Нут1975, Раушер1974,1977;

слабая дизъюнкция в логике финитных задач Медведева: Скворцов1983; сильная конъюнкция Поттингера (Лопес-Эскобар1985); связки, определимые в интуиционистском второпорядковом пропозициональном исчислении: Габбай1977, Крайзель1981, Трулстра1981; работа де Йонга1980 о классе интуиционистских связок; оператор Крайзелп: Гоад1978, Селлуцци1974, Войтыляк1984.

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

сильное отрицание в Int: Земан1968, Гуревич1977, Шаталов1977; связки, определяемые секвенциальными исчислениями: Боуэн1971; Санчис-1973; Кучера1968;

немонотонные операторы: возможность (Габбай1982) и следование (Сер-ви1992);

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

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

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

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

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

Подход П.С.Новикова был впервые изложен в статьях Я.С.Сметанича [3, 4]: формвиьная система L определяет новую связку по П.С.Новикову, если L консервативна над Int и не допускает присоединения явных сотношений для дополнительной связки. Первый пример новой связки по Новикову найден Сметаничем, при этом связка оказывается константной, т.е. не зависящей от аргумента.

А.В.Бессонов [5] привел пример исчисления с новой неконстантной связкой и установил континуальность семейства логик, определяющих новую связку по Новикову.

Ссылка на лемму Цорна показывает, что всякая консервативная над Int логика содержится в некоторой полной по Новикову логике, однако такая ссылка ничего не дает в плане эффективного описания как конкретных примеров полных логик, так и всего семейства полных логик.

Проблема Новикова изначально была сформулирована для языка с однсй дополнительной одноместной связкой следующим образом: построить явный (т.е. конечно аксиоматизируемый) пример полной логики с новой связкой.

В случае нескольких дополнительных связок понятие новизны естественным образом трансформируется в понятие независимости связок, а сама проблема Новикова переформулируется следующим образом: для данного набора связок построить явный пример полной логики, в которой эти связки были бы независимы.

Для конкретной логики проблема Новикова заключается в описании всех ее полных расширений.

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

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

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

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

Однако в случае интуиционистской логики высказываний конечный адекватный набор истинностных значений невозможен, что было установлено еще К.Гёделем [23]. В связи с этим возникает т.н. проблема характеризации логических связок [26), заключающаяся в отыскании внешнего определения класса связок, в котором изначально подразумеваемый набор оказался бы функцио-

нально полным.

Применительно к модальной логике Д.Скотт [24] пишет: "Имея подходящее определение ..., мы, без сомнения, сможем показать, что единственными логическими операторами (одноместными — прим. авт.) являются -I, ->->, О, О".

С другой стороны, А.Трулстра в статье [25] выражает некоторое сомнение по поводу функциональной полноты набора стандартных интуиционистских связок: "Каждая из этих семантик (семантик интуиционистской пропозициональной логики — прим. авт.) математически намного сложнее, нежели стандартная классическая семантика. Нет оснований полагать, что класс операторов, опре--делимых через —V, А, является дефинициально полным для какой-либо из этих семантик".

Попытка формулировки внешнего определения класса стандартных интуиционистских связок с точки зрения моделей Крипке была предпринята Д.Мак-калоу в [6]. Предложенные Д.Маккалоу определения позволяют легко доказать достаточность набора стандартных связок V, А, —>, -1, однако искусственность самих определений (имеющих чисто синтаксический характер) не дает оснований считать, что проблема характеризации этого набора в указанной работе решена удовлетворительно (отметим, что этот вывод сделан Д.Маккалоу там же). В заключительном параграфе статьи Маккалоу содержится замечание о том, что логические связки не должны различать подобные модели; но эта идея дальнейшего развития не получила.

Цели и задачи диссертации.

Исследование стандартных и нестандартных логических связок интуиционистской логики высказываний с точки зрения:

• полноты по П.С.Новикову;

• семантической полноты дедуктивной системы в данном классе моделей;

• семантической характеризации конкретных наборов связок.

Методология исследований

Первоначальные исследования по семантике неклассических логик велись исключительно на алгебраическом языке. В частности, модели интуиционистской логики и ее расширений представлялись как псевдобулевы алгебры (или алгебры Гейтинга) (Расёва Е. & Сикорский Р. [29]).

Работы С.Крипке по реляционной семантике модальных и интуиционистской логик позволили упростить и визуализировать многие понятия и результаты соответствующей теории.

Интуиционизм как раздел оснований математики нашел свое развитие в работах А.Трулстры, Г.Крайзеля, Д.ван Далена, А.Г.Драгалина и др.

В 70-е годы XX столетия объектом внимания стала чисто логическая проблематика неклассических логик. В этом контексте заметную роль сыграла книга П.С.Новикова [31].

В работах А.В.Кузнецова [32,33, 34,35] были поставлены и частично решены вопросы, специфичные именно для неклассических логик и давшие толчок последующему развитию: полнота, финитная аппроксимируемость, табличность, параметрическая выразимость, шефферовость, арифметическая доказуемость как модальная связка и др.

Усилиями ряда ученых было накоплено много фактов относительно отдельных неклассических логик (некоторые имена упомянуты в предыдущем разделе). По достижении массой фактов некоторого критического значения назрела необходимость выработки более общего взгляда на проблематику. Период первоначального накопления фактов постепенно стал уступать место систематическому анализу не отдельных логик, но всего разноообразия таковых как единого целого (Л.Л.Максимова & В.В.Рыбаков [41]).

Реляционная семантика позволила с помощью шкал строить модели, алгебраическое описание которых является практически необозримым. Мостом между алгебраической и реляционной семантикой явились теоремы о представлении произвольной псевдобулевой алгебры семейством конусов подходящей шкалы и связи между вложениями псевдобулевых алгебр и строго изотонными отображениями (р-морфизмами) соответствующих шкал (Л.Л.Максимова [42]). Эти тео-

ремы позволили исследовать вопросы интерполяции и определимости в различных неклассических логиках (см. например работы Л.Л.Максимовой [43,44,45]). В нашей работе теорема о представлении и теорема о р-морфизмах являются "краеугольными камнями" всех результатов, касающихся понятия полноты по П.С.Нсвикову.

Отмеченная в предыдущем разделе идея задавать интерпретацию дополнительных логических связок с помощью условия вынуждения в моделях Крипке была жредложена Л.Л.Максимовой (см. статью А.В.Бессонова [5]).

Следующим важным понятием является понятие т.н. п-характеристической шкалы. Это понятие с успехом применялось для решения вопросов о допустимости правил вывода в неклассических логиках, о разрешимости У-фрагментов элементарных теорий свободных псевдо- и топобулевых алгебр, решениям уравнений над такими алгебрами (В.В.Рыбаков [36, 37, 38, 39]). Эти результаты были подытожены в монографии В.В.Рыбакова [40]. В нашей работе п-характеристические шкалы непосредственно применяются для построения примеров полных по Новикову логик с несколькими новыми константами и для оценкм общего числа таких логик.

Среди большого числа вопросов, связанных с неклассическими логиками, заметное место занимают вопросы алгоритмического распознавания тех или иных свойств неклассических логик. Положительные примеры (т.е. когда изучаемое свойство Л разрешимо) достаточно редки и основываются чаще всего на явном построении семейства расширений данной логики, удовлетворяющих Л, что позволяет описать эффективный позитивный тест1 для распознавания Л■ В качестве примеров можно привести результаты о разрешимости интерполяционного свойства суперинтуиционистских логик (Максимова Л.Л. [43]), свойства анти-табличности расширений логики Геделя-Леба (А.В.Чагров & Л.А.Чагрова [50]).

Для доказательства неразрешимости тех или иных свойств логик применяется техника имитации двухленточных машин Минского (двухрегистровых абаковё). Эта техника была с успехом применена для доказательства алгоритмической неразрешимости целого ряда свойств (дизъюнктивное свойство, таб-

1 термин из книги Дж.Булоса и Р.Джеффри [46].

личность, финитная аппроксимируемость и др.) (Чагров A.B. [49], Захаръящев М.В. & Чагров А.В [47], Чагрова Л.А. [48]). Эти исследования были подытожены в монографии А.В.Чагрова и М.В.Захарьящева [1]. В нашей работе техника имитации машин Минского применяется для доказательства алгоритмической неразрешимости проблемы консервативности логик для случая двух или более дополнительных констант.

Следующей важной задачей представляется задача о разрешимости данной логики: найти алгоритм распознавания принадлежности произвольной формулы рассматриваемой логике. Одним из наиболее часто упоминаемых- критериев разрешимости является критерий Харропа [51]: если логика конечно-аксиоматизируема и финитно аппроксимируема, то она разрешима. В некоторых случаях удается доказать разрешимость и не финитно аппроксимируемых логик с помощью погружения в разрешимые слабые второпорядковые теории, такие, как слабая арифметика Бюхи или теория Рабина в языке с несколышми одноместными функциями (например, Дж.Бёрджесс [52]).

Следующим важным типом задач является построение аксиоматики логик, заданных семантически, т.е. посредством некоторого класса шкал. Результаты такого типа принято называть теоремами о (семантической) полноте исчисления относительно соответствующего класса шкал. Мы используем следующую методику: по данной непротиворечивой (относительно рассматриваемого исчисления) паре списков формул строится модель, в которой выполняются все формулы "положительной" компоненты и не выполняются все формулы "отрицательной" компоненты. В литературе имеется масса примеров применения этого метода, при этом примеры различаются по степени "участия творческого субъекта" в процессе построения моделей. Понятие канонической модели в этом смысле требует минимального "участия", т.е. все нужные свойства мадели следуют непосредственно из свойств самого исчисления. Недостатком канонических моделей является их необозримость.

Для построения обозримых моделей требуемого вида нужна более высокая степень "участия субъекта" в построении. Пример применения этого метода можно видеть в книге А.Г.Драгалина [30].

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

применяется метод фильтрации (например, Д.Габбай [57]). В нашей работе вариант метода фильтрации применяется в доказательстве разрешимости логики с константой бесконечного индекса.

Для переноса результатов с одного языка на другой широко применяется метод перевода. Под переводом понимается отображение класса формул одного языка в класс формул другого языка. Типичными примерами являются негативная интерпретация классической логики в интуиционистской, интерпретация интуиционистских формул посредством модальных (например, Максимова Л.Л & В.В;Рыбаков [41]). В нашей работе метод перевода применяется для построения новых примеров полных по П.С.Новикову логик на основе уже имеющихся.

Изучение связок, определимых в языке элементарной теории моделей Крип-ке, основано на понятии элементарного расширения и насыщенной модели (теория моделей первого порядка (Кейслер Дж. & Чэн Ч. [62]). В классической теории моделей 1-го порядка есть ряд теорем, связывающих теоретико-модельные свойства формул с их синтаксическим строением. Примеры: теорема Лося-Тарского показывает, что относительно перехода к подсистемам устойчивы универсальные формулы и только они; относительно строгих гомоморфизмов устойчивы условно экзистенциальные формулы и только они (условно экзистенциальные формулы имеют вид Ух{А(х) 3уВ[рс,у)) (С.С.Гончаров)). В нашей работе аналогичная методика применяется для получения результатов о харак-теризации некоторых наборов связок как формул, устойчивых (в обе стороны) относительно аморфизмов моделей Крипке.

Наконец, отметим, ■что с алгебраической точки зрения дополнительные интуиционистские связки представляют собой операторы на псевдобулеых алгебрах, поэтому данное направление может быть условно обозначено как "псевдобулевы алгебры с операторами". Параллельные ветви классической логики в настоящее время активно развиваются под названиями "булевы алгебры с операторами " (см., например, [56]) и "булевы алгебры с выделенными идеалами" (Д.Е.Пальчунов [53, 54, 55]).

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

Язык интуиционистской логики высказываний Int расширяется путем добавления связок ф = {pi,..., <рп}. Каждая связка уз,- имеет ki = ar(ipi) аргументных мест. В частности, связка без аргументов называется константой. Расширенный язык обозначаем через С(ф), класс формул расширенного языка — через Fm(ip). Формулы, не содержащие дополнительных связок, называем чистыми.

Назовем ф-логикой произвольное множество формул языка С{ф), включающее Int, замкнутое относительно правил modus ponens, подстановки и замены эквивалентных2 для каждой дополнительной связки. ^-Логика L называется консервативной (над Int), если для любой чистой формулы D из D 6 L следует D 6 Int.

Явным соотношением для связки ip, называем формулу вида tpiipi,... А, где А не содержит <р;.

Схемой замены эквивалентных называется множество формул вида ki

А (Pi Ч}) (£>(Pi,... ,pfc() ßfe,...,%)). i=i

Если L — ^-логика и Г — множество формул, то через L + T будем обозначать наименьшую по включению ^-логику, содержащую £ и Г.

Определение 1. ^-логика L, включающая схему замены эквивалентных, называется полной по Новикову, если она консервативна над Int и для любой формулы Аф L ip-логика L + А неконсервативна над Int.

Обратим внимание на то, что П.С.Новиков наличие аксиом замены для дополнительных связок включает в число требований к ^-логикам. Известно, что при наличии аксиом замены правила замены эквивалентных становятся излишними. По видимому, это требование возникло на основе того, что Int содержит аксиому замены эквивалентных для каждой стандартной связки.

Определение 2. Связки (pi,...,(pn независимы в консервативной ф-логике L, если для любого щ 6 ф и для любой формулы А, не содержащей вхождений

гдля одноместной СВЯЗКИ и т.п.

<Pi, (р-логика L + ifii(pi,.. .,ptt) +■» А неконсервативна над Int. Другими словами, никакое расширение L, консервативное над Int, не содержит явных соотношений.

Определение 2 можно рассматривать как обобщение известного результата о независимости стандартных связок в Int (Маккинси [7]): при присоединении к Int какого-то явного соотношения, например (р->д)ч->Л(А, V, -i)(р, q), образуется собственное расширение Int.

Заметим, что в подавляющем числе работ по нестандартным интуиционистским связкам говорится только об отсутствии явных соотношений в данной ^-логике. П.С.Новиков предложил более сильное условие: не только в данной ^-логике не должно быть явных соотношений, но также и ни в каком ее расширении, консервативном над Int.

Можно отметить аналогию с трактовкой отрицания в известном методе вы-нуждения: условие а вынуждает -<А, если никакое корректное расширение условия а не вынуждает А.

До работ автора не было известно ни одного примера полной по Новикову ^-логики.

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

Теорема 1 Логика Кузнецова имеет единственное полное пб Новикову расширение, являющееся конечно аксиоматизируемым и разрешимым.

Аналогичный факт установлен и для логики Габбая.

Для случая нескольких дополнительных констант <р с использованием понятия п-характеристической модели [40] (в нашей терминологии — универсальной (р-шкалы) установлен следующий результат.

Теорема 2 Каждый конечный конус универсальной (р-шкалы определяет полную по Новикову (р-логику. При этом разным конусам соответствуют разные полные логики.

Каждая полная по Новикову <р-логика, соответствующая конечному конусу, конечно аксиоматизируема и разрешима. Если при этом константы образуют базис псевдобулевой алгебры подконусов выбранного конуса, то эта ip-логика не содержит явных соотношений.

Полностью решен вопрос о числе полных по Новикову логик для констант.

Теорема 3 В случае двух или более дополнительных констант существует континуум полных по Новикову (р-логик, в которых эти константы независимы.

В случае единственной дополнительной константы (<р = {<р}) полные по Новикову ¡р-логики образуют явно описанную счетную последовательность. Каждая <р-логика из этой последовательности разрешима.

В связи с тем, что консервативность является краеугольным камнем в подходе П.С.Новикова, можно для данного набора связок (р сформулировать алгоритмическую проблему консервативности: по записи формулы А ^5-языка выяснить, является ли ^-логика Int + А консервативной над Int.

Ситуация с алгоритмической проблемой консервативности полностью прояснена:

Теорема 4 Для единственной дополнительной константы проблема консервативности разрешима.

Для двух и более дополнительных констант проблема консервативности неразрешима.

Для единственной одноместной дополнительной связки проблема консервативности неразрешима.

Кроме вышеперечисленного, в работе развит и семантический подход к понятию логической связки, намеченный в работах Маккалоу [6], Скотта [8] и Трулстры [9].

В рамках элементарной теории реляционных моделей в терминах монотонности и устойчивости при определенных отображениях моделей получена ха-рактеризация следующих наборов интуиционистских логических связок:

{v,л,{v,л,->,-.,a}, {v, л, г, А}, {V, л, ->, i, г, А, □}

(здесь О — модальный оператор типа универсальной необходимости, г — связки, дуальные связкам —соответственно)3.

Апробация работы.

Различные разделы работы докладывались на следующих мероприятиях:

• Всесоюзные конференции по математической логике (1984, 1986, 1988, 1990, 1992)

• 2 Всесоюзная конф. по прикладной логике (Новосибирск 1988)

• Научно-исследовательский семинар кафедры математической логики и теории алгоритмов МГУ

• Logic Colloquium'94 (Clermont-Ferrande, Prance)

• Logic Colloquium'96 (San-Sebastian, Spain)

• Всероссийская конференция по логике'96 (Санкт-Петербург)

• Goedel'96 (Brno, Czech Republic)

• Computer Science Logic'96 (Utrecht, Netherlands)

• Advances in Modal Logics'96 (Berlin, Germany)

• Logic Collloquium'97 (Leeds, UK)

• Мальцевские чтения'97 (Новосибирск)

• Мальцевские чтения'98 (Новосибирск)

• Алгебраический семинар КГУ (Красноярск, 1998)

• Международная конференция памяти А.И.Мальцева (Новосибирск, 1999)

• Международная конференция "Логика и приложения" (Новосибирск, 2000)

3Точные формулировки ниже.

Содержание диссертации.

1. ^-Логики.

В этой главе

• излагаются необходимые понятия и результаты метаматематики чистой интуиционистской логики высказываний. Часть из них непосредственно может быть найдена в литературе, остальные легко получаются переформулировкой известных понятий и результатов метаматематики модальной логики [1, 40, 61];

• эти понятия переносятся на язык с дополнительными связками;

• анализируется ряд примеров, главным образом с точки зрения подхода П.С.Новикова; в некоторых случаях излагаются "попутные" результаты, могущие представлять самостоятельный интерес.

Интуиционистская логика высказываний Int формулируется в языке, содержащем счетное множество пропозициональных переменных VAR = {pi,...}, набор стандартных логических связок А, V, —Эквиваленция вводится общепринятым способом А++В # (А->В)Л(В—*А). Иногда вводятся стандартные логические константы 0 — "ложь" и 1 — "истина".

Шкалой называется непустое частично упорядоченное множество. Если W

— шкала, то конусом называется ее подмножество, замкнутое относительно увеличения: х € X$¿x < у =>- у 6 X. Множество конусов шкалы W обозначаем посредством ConW. На ConW определены т.н. операции Крите U, Л, Э, —, превращающие Con W в псевдобулеву алгебру (п.б.а). Такие алгебры являются моделями интуиционистской логики точно так же, как булевы алгебры — моделями классической двузначной логики.

Обобщенной шкалой называется объект вида ц = (W, S), где W — шкала и S

— подалгебра Con W. Использование обобщенных шкал мотивируется известной теоремой о представлении псевдобулевых алгебр: всякая п.б.а. изоморфна подалгебре алгебры Con W для некоторой шкалы W.

Предположим, что язык интуиционистской логики высказываний расширен путем добавления связок ф = {<Р\,--., ¥>п}- Каждая связка р,- имеет к, = ar(tpi) аргументных мест. В частности, связка без аргументов называется константой. Рвсширенный язык обозначаем через £{ф), класс формул расширенного языка — через Fm{(p). Формулы, не содержащие дополнительных связок, называем чистыми.

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

Обобщенной ф-шкалой называется объект вида у, = где

(W,S) — обобщенная шкала, и для каждого i = 1,...,п Ф; : S** —> S — k{-местный оператор на S. Если tpi — константа, то Ф¡ представляет собой фиксированный конус в S.

Оценкой на обобщенной ^-шкале /х = {W, 5, Ф) называется отображение v : VAR —» 5.

На произвольные формулы оценка v распространяется по индукции: для стандартных связок и стандартных констант

v(AVВ) v(A)Uv(B),v(AäB) Ф v(A)nv(B), v(A —> В) ^ v(A)Dv{B),v(-<A) ^ -v(A), v(0) ^ 0,r(l) ^ W, для дополнительных — посредством соответствующих операторов:

Для констант: v(ipi)

Обьнным образом определяются понятия: модель — обобщенная р-шкала с оценкой переменных; истинность формулы в модели — (р, v)\=- А ф «(>1) = Wp, общезначимость формулы в одной <£-шкале и в классе ^-шкал. Обожначим ЬФ{Ш) # {i€ Fm{ip) | V/i 6 М : ц (= А}. Следующее правило называется правилом замены эквивалентных для связки

<Pi-

(¿i+>Bi).....(Ль.ч^ДО

Назовем ф-логикой произвольное множество формул языка С{ф), включающее Int, замкнутое относительно правил modus ponens, подстановки и замены

эквивалентных для каждой дополнительной связки. В частности, явля-

ется ^-логикой.

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

^-Логика L называется консервативной над Int, если для любой чистой формулы D из D € L следует D б Int.

Явным соотношением для связки <pi называем формулу вида

где А не содержит <pi.

Аксиомой замены для связки ipt называется формула ki

А (р, Я]) (v.(pi. • • -,?*.) <-» vMu- • ■, Як,))-j=1

Для каждой стандартной связки аксиома замены содержится в Int.

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

Если L — (^-логика и Г — множество формул, то через L + Г обозначаем наименьшую по включению ^-логику, включающую L и Г.

Скажем, что множество формул Г присоединимо к консервативной ^-логике L, если L 4- Г тоже консервативна над Int.

Перечислим примеры ^-логик, анализируемые в связи с подходом П.С.Новикова, и полученные для них результаты.

Логика Сметанича.

Логика Сметанича Sm задается в языке с единственной дополнительной константой tp следующим образом:

Sm Jni+i

[ ip->(AV-iA)

с правилом вывода modus ponens. Sm определяет новую константу по Новикову.

Теорема 5 Sm характеризуется классом конечных шкал при следующей интерпретации <р: а <р т^ тах(а).

Логика регулярной константы.

Логика регулярной константы Reg определяется в языке с единственной дополнительной константой ip следующим образом:

Reg определяет новую константу по Новикову и несовместима с Sm.

Пусть F — конечная шкала. Выберем подмножество Ф С MAX(F), удовлетворяющее условию

(всякая немаксимальная точка "видит" по крайней мере одну максимальную уточку и хотя бы одну максимальную -уточку).

Конечную шкалу с надлежащим образом выбранным Ф назовем Н-шкалой.

Теорема в Яед Ь А, т.и т.т. А общезначима в классе конечных И-шкал. Логика Бессонова.

Логика Бессонова [5] определяется в языке с единственной дополнительной одноместной связкой посредством

с правилом вывода modus ponens. Эта логика определяет новую одноместную связку по П.С.Новикову.

Для логики Бессонова разработана адекватная окрестностная семантика. Эта логика используется для анализа взаимосвязи между подходами П.С.Новикова и Д.Габбая (подход Д.Габбая описан в [28]).

Логика Каминского.

Для формализации свойств модализированного временного оператора (другое название — сильный оператор будущего времени) в рамках интуиционистской логики высказываний Int М.Ка-

Va i MAX{F) : П Ф / 0& П (MAX(F) \ Ф) ^ 0

Bea = Int + <

vW

<p(0) -t(AV -vi)

минский предложил исчисление [10] в языке с одной одноместной связкой ¥>(•):

Кат = Int + >

+

. wCP) <р(Р)

Логика Каминского не удовлетворяет условиям, сформулированным в подходе П.С.Ношкова, т.к. к ней присоединимо каждое из двух явных соотношений уг(р) «ри <р(р) +■►

Стандартная интерпретация связки <р в логике Каминского:

х (= 1р(А) т.и т.т. когда на любом пути, проходящем через точку х, найдется точка у, такая, что у\=А.

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

Шкалой с отмеченными точками называем пару (IV, О), где — шкала, И С № — некоторое фиксированное подмножество (отмеченные точки). Вынуждение для кр определяем следующим образом:

Шкалы вида (IV, D) с конфинальным D назовем К-шкалами. Теорема 7 Кат Ь А А общезначима в классе конечных К-шкал. Построены примеры расширений Кат, по прежнему консервативные над Int.

Прецедентное отрицание

Связка г, двойственная к -i, интерпретируется в обычных моделях Крипке следующим образом: х\= г А Ф Эд <хА

Связка г является частью синтаксиса т.н. логики. Гейтинга-Брауэра, [11, 12]. Указанной интерпретации связки г естественным образом соответствует оператор Л {у | Зх < у : х $ X) иа алгебре конусов любой шкалы, поэтому множество Lr общезначимых формул г-языка замкнуто относительно правила замены эквивалентных, т.е. является ^-логикой.

Рассмотрим следующий фрагмент логики Гейтинга-Брауэра:

с правилами modus ponens, подстановки и замены эквивалентных.

Консервативность L над Int вытекает из общезначимости 1° и 2° в произвольной шкале.

Теорема 8 L не допускает присоединения явных соотношений для г; Вместе с тем аксиома замены для г: (p++g) (гр о rg) также неприсоединима к L.

Другими словами, связка г не соответствует подходу Новикова.

х[=<р(А) ^ Уу>х(у€Л ==> у |= А).

pVrp -.rl

Модальный оператор "универсальная необходимость"

Проблеме введения в интуиционистскую логику модальностей, подобных традиционным О (необходимость) и О (возможность) посвящен ряд работ (например [13,16,17,14,18,15,19].

Базисные системы оказываются очень бедны и потому допускают присоединение явных соотношений.

Рассмотрим связку □ типа "универсальной истинности":

х\=ОА VV: у\=А.

Нетрудно проверить, что общезначимы следующие формулы: 1°. DpV -.Dp; 2°. Dl; 3°. Op-tp.

Обозначим La = Int + 1° + 2° + 3° с правилами подстановки, modus ponens и замены эквивалентных. Указанная интерпретация связки □ показывает, что La консервативна над Int.

Предложение 9 La не допускает присоединения явных соотношений для D; тем не менее аксиома замены для О: (р ++ q) (Цр-Н Dg) также неприсоединима к La.

Связка D тоже не соответствует подходу Новикова. Оператор Крайзеля

Оператором Крайзеля [20,21] называется одноместная связка 0, интерпретируемая в инфини-тарном языке посредством бесконечной дизъюнкции

0(Р) «* у

*<оо

где Ei (р) — последовательность Нишимуры от переменной р. Интерпретация в инфинитарном языке показывает, что аксиома однозначности для 0 содержится в £0.

Тем не менее следующее предложение говорит, что £« не является примером логики, определяющей новую связку по Новикову.

Теорема 10 Lt допускает присоединение явного соотношения 0(р) «-> 1. Антиимпликация Боуэна

К.Боуэн рассмотрел в [22] секвенциальное исчисление LJg, полученное из обычного секвенциального исчисления Int с односукцедентными секвенциями расширением языка двухместной связкой <£. и добавлением правил

Г, Л =» Г => В Г, В =» А Г А£В V,A<£B =>

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

Множество формул, выводимых в этом исчислении, обозначим через Bow. Оно не замкнуто относительно правила замены эквивалентных для т.е. не является ^-логикой. Тем не менее Bow применяется для построения примера полной по Новикову логики с новой двухместной связкой (глава 3).

2. Новые константы в Int.

В этой главе рассматривается язык с пропозициональными константами <р = {<Ри ■■■,<Рп}-

ф-шкалой будет называться объект вида (W, S, Ф1(..., Ф„), где (W, S) — обобщенная шкала и Ф< — фиксированные конусы в S.

Конечную порожденную (р-шкалу 7 = (F, Ф) называем правильной, если Ф является базисом алгебры Con F.

В правильной <£-шкале любой конус X является значением некоторой константной формулы £{Х). Через П обозначаем наибольший неединичный элемент алгебры CcmF.

Константную характеристическую формулу правильной ^-шкалы Т определяем следующим образом:

((J0 ** ° £00 S(X * К)) е(П),

конъюнкция в посылке пробегает по всем конусам X, Y е ConF и парам (о, *) е {(-+,:>), (A, n),(V,U)>.

Через и обозначаем посылку и заключение формулы соответственно.

Пусть G — конечная шкала, F — произвольная шкала. Строим шкалу G[F], размещая над каждой максимальной точкой шкалы G "нарост", изоморфный F.

Пусть Т — (F, Ф) — ^-шкала. Тогда шкала G[F] естественным образом превращается в шкалу <?[.?].

Фиксируем правильную ^-шкалу Т = (F, Ф). Пусть

ВД ^ {G[f[ | G е н}

(здесь Н — класс всех конечных порожденных шкал). Основные объекты изучения — (^-логики вида

I? ^ L4НИ).

Теорема 11 Пусть Т = (F, Ф) — конечная порожденная (р-шкала, удовлетворяющая условиям:

(а) Ф — система образующих алгебры ConF;

(б) root F i

Тогда LT — полная по Новикову (р-логика. Если Т является правильной, то I? же содержит явных соотношений.

С помощью т.н. универсальной (р-шкалы установлена мощность семейства всех полных по Новикову логик для нескольких констант:

Теорема 12 При \<р\ > 2 существует континуум полных по Новикову (р-логик с независимыми константами.

Для языка с единственной дополнительной константой <р установлен следующий классификационный результат:

. Теорема 13 Полные по Новикову <р-логики исчерпываются последовательностью L\ L2, L3, Ьъ, L7,..., Ln+\

В этой последовательности индексы — номера дизъюнктивно неразложимых формул из последовательности Нишимуры. Логики Ьх и Ь2 содержат явные соотношения <р «-» 0 и tp ++1 соответственно. Каждая из оставшихся логик определяет новую константу. При этом Sm с £3 и Reg С L& (оба включения строгие). Аксиоматика для уг-логики Lf строится следующим образом. Фиксируем:

• правильную (¿ыпкалу Т — (F, Ф);

• о = root F — корень шкалы;

• Í2 — наибольший неединичный элемент алгебры ConF;

• для каждого конуса X € ConF константную формулу £(Х), определяющую этот конус.

Определим дедуктивную систему Ах(Р) следующим образом. Схемы аксиом:

Ati: стандартные схемы аксиом интуиционистского пропозиционального исчисления; Ах2:

Ах3: £{Та) -)• L(Fa) для каждого а € F \ {о} (здесь L(Fa) — схема, аксиоматизирующая чистую табличную логику шкалы

Ах 4: ( У {А ++ £{Х) Л В о £(Г))) £(П) Л. Л (Я V í(í2))->„

(.A-+B)V£(SI)

дизъюнкция V пробегает по всем конусам X, Y С П, таким, что X % Y;

Ах5: ((У(Л £(*)) 5(П)) А (Л £(íl)) -.Л V £(П) дизъюнкция в посылке пробегает по всем непустым конусам X С Sí.

Теорема 14 А е Lr <=> Ах{Т) Ь Л.

В доказательстве используется конструкция из статьи С.Н.Артёмова & Л.Д.Век-лемишева [59]. Из этой теоремы сразу вытекают хорошие свойства ^-логики такие, как разрешимость, дизънктивное свойство. В частности, все полные по Новикову логики конечного индекса в языке с единственной дополнительной константой разрешимы.

^-Логика Va также разрешима, что, однако, доказывается с использованием варианта метода фильтрации и теоремы Бюхи о разрешимости слабой арифметики второго порядка.

Пусть <р-логика задана в виде Int + А, где Л — некоторая формула (¡¿-языка. 5стественно формулируется алгоритмическая проблема консервативности ф-огик такого вида над Int.

Нетрудно заметить следующее: L = Int+A неконсервативна над Int тогда и олько тогда, когда существует вывод в L некоторой чистой формулы D £ Int.

Поскольку понятие вывода в явно заданной логике является разрешимым, и сама Int разрешима, семейство всех неконсервативных ^-логик рассматриваемого вида перечислимо.

Теорема 15 Для языка с единственной дополнительной константой проблема консервативности алгоритмически разрешима.

Перечислимость семейства всех консервативных р-логик основана на классификационной теореме для полных по Новикову ^з-логик:

Int + А консервативна над Int тогда и только тогда, когда Int + А содержится в некоторой полной по Новикову ^-логике. Это равносильно За € {1,2, S, 5,..., 2п 4-1,..., оо} : А 6 La. Здесь отношение А 6 L" является разрешимым.

Для языка с несколькими дополнительными константами ситуация иная.

Теорема 16 При \(р\ > 2 алгоритмическая проблема консервативности неразрешима.

3. Неконстантные связки и полнота по Новикову. В этой главе

• решается проблема Новикова для логик Кузнецова и Габбая;

• с помощью некоторого варианта метода перевода строится пример полной ^-логики с несколькими независимыми одноместными связками;

• строится пример полной <р-логики с новой двухместной связкой, существенно зависящей от обоих аргументов;

• доказывается неразрешимость алгоритмическай проблемы консервативности исчислений в языке с дополнительной одноместной связкой, с правилами modus ponens, подстановки и замены эквивалентных.

Логика Кузнецова [35] формулируется в языке с дополнительной одноместной связкой ¡р(•) следующим образом:

Логика Габбая [28] задается в языке с дополнительной связкой %[>(-) посред-

Правила вывода в обоих случаях — подстановка и modus ponens. Обе логики содержат схему замены эквивалентных.

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

Kz семантически полна в классе конечных деревьев при следующей интерпретации связки <р: a f= ¡р(р) ^ Vb > в : Ь (= р.

Gab семантически полна в классе конечных деревьев при следующей интерпретации ф:

Теорема 17 Каждая из логик Kz и Gab определяет новую связку по Новикову.

Для описания полных по Новикову расширений логик Кузнецова и Габбая используется понятие w-шкалы, введенное С.Н.Артёмовым в [58].

По данному конечному дереву F строим ш-шкалу Fu = Fx {..., 2,1} с лексикографическим упорядочением. Наглядно Fu получается из F заменов каждой точки на убывающую последовательность порядкового типа из.

Пусть Fu = {Fu | F — конечное дерево}.

Kz=zlnt+' (ср(р) ->• р) р

<p(p)-*(qV(q->p))

ством

Gab = Int -f <

V ^(р) ■ф{р)

Vy > х : у f= р, если х не максимальна; х 1= Р, иначе.

Обозначим Кг+ = Lv(Fw), Gab+ = Ьф(Fw).

Теорема 18

(a) Kz+ — единственное полное по Новикову расширение Kz.

(b) Gab+ — единственное полное по Новикову расширение логики Gab.

Следующая теорема описывает явную аксиоматику: Теорема 19

Kz+ = Kz+ V2(p) ((р-* q) V (q р)); Gab+ = Gab+ ф2(р) ((р q) V (q -*■ р));

Следствие 20 Логики Kz+ и Gab+ разрешимы.

Отмегим также, что Kz+ и не являются финитно аппроксимируемыми.

4. Элементарная теория моделей Крипке и логические связки

Элементарная теория моделей Крипке К формулируется в языке, содержащем двухместный предикатный символ < для отношения достижимости, константу о для выделенного элемента (актуальный мир [60]) и счетную серию одноместных предикатов Р<(-) для интерпретации пропозициональных переменных pj.

Логические связки языка К обозначаем посредством V, &, =>• , ~ (отрицание), .

Аксиомы теории К:

• частичный порядок; • монотонность: Р{(х)&х < у =$> Р<(у). В дальнейшем мы будем рассматривать следующие примитивные связки: V, Л, —-I, г (прецедентное отрицание), (дуал импликации), □ (универсальная необходимость). Для произвольной пропозициональной формулы А определяем формулу [А] (г) языка К с одной свободной переменной:

№) ^ вд,

^ [А](х)&[В](х), HvßjM т* [А](х) V [£](*)> [А-*В](х) * Vy>x([A](y) [В]{у)),

Ь4](я) # Уу>1(~И](2/)), [А*-В]{х) # Зу<*([Л](у)&~[ВД)>

[г А}(х) ^ Эу < [ЕХА](®> ** УуИ]^).

Лемма 21 (монотонность) К Н [А](х)кх < у => \А]{у).

В дальнейшем будем рассматривать следующие классы пропозициональных формул (сокращенно ПФ):

Гто — ПФ, содержащие только стандартные связки; Рт1 — ПФ, содержащие стандартные связки и О; Гт2 — ПФ, содержащие все указанные выше связки. Ртпз — ПФ, содержащие стандартные связки и {А, г}; Соответствующие наборы примитивных связок обозначаем посредством Со, ..., С3.

Характеризация связок V,Л,—

Пусть М1, Мг —модели Крипке. Отображение Л : Л/х М2 будем называть р-морфизмом моделей, если выполнены следующие условия: 1. =

2. а < Ь => Л(а) < Л(Ь) (монотонность);

3. Л(а) < с 3Ь>а: Л(6) = с (сохранность верхнего конуса);

4. Л(ох) = 02 (согласованность актуальных миров);

5. а |= р Л(а) ¡= р для всех переменных р (согласованность оценок). Модели Мх,Мч называем подобными, если существует конечная цепочка моделей М1 —> N1 ч— ЛГ2...№т = Мг, в которой каждые два соседних члена жибо элементарно эквивалентны, либо находятся в отношении р-морфизма в ту или другую, сторону.

Пусть А(х) — формула языка теории К, не содержащая константу о. А монотонна, если К I- Л(х)&2 < у => А[у). А устойчива, если для любого £о-морфизма И: М2

М1\=А(о)<=>М2^А(о).

Монотонную устойчивую формулу называем логической связкой.

Теорема 22 Для пропозициональной формулы А 6 Рт(£о) формула [^4] (х) является логической связкой. Для всякой связки А(х) найдется ПФ А' такая, что К Ь А{х) [Л'](аО.

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

Характеризация набора \/,Л, □

Теорема 23 Набор связок \/,А,—характеризуется следующими условиями:

(a) монотонность;

(b) устойчивость относительно всюду определенных сюръективных р-мор-физмов моделей.

Характеризация связок логики Гейтинга—Брауэра с □

Теорема 24 Набор связок V, Л, —>, -ч, О, г характеризуется следующими условиями:

(a) монотонность;

(b) устойчивость относительно всюду определенных сюръективных р-мор-физмов, удовлетворяющих дополнительному условию сохранности нижнего конуса: Н(а) > с 36 < а: к(Ь) = с.

Характеризация связок логики Гейтинга-Брауэра

Отношением связности на частично упорядоченном множестве называется транзитивное замыкание отношения аЯЪ # а < Ь V 6 < а. Связной компонентой точки называется множество точек, связанных с данной.

Теорема 25 Набор связок V, Л,-4,-1, А, г характеризуется следующими условиями:

(a) монотонность;

(b) устойчивость относительно р-морфизмов, определенных на связной компоненте актуального мира и удовлетворяющих условию сохранности нижнего конуса h(a) > с БЬ < а : h(b) — с.

Характеризация связок модальной логики S4

Элементарная теория модальных моделей Крипке Kmod формулируется в одко-сортном языке с равенством, со следующими нелогическими символами: константой о для актуального мира, двухместным предикатом Л для отношения достижимости между мирами, одноместными предикатами Ри Р2, ...для интерпретации пропозициональных переменных.

Аксиомы теории Ктоа: предпорядок с корнем о, т.е.

oRx; xRyhyRz xRz\ xRx.

Модели теории Kmod характеризуют известную модальную логику 54.

Пусть Мг. и Мг — модели теории KmDd. Отображение h: Мг~+М2 называется р-морфизмом моделей, если выполнены следующие условия: сюръективность: h{Mi) = Мг\ монотонность: aRib =Ф- h(a)R2h(b); конусность: h(a)R2c =Ф- 36: aRib8ih(b) =с;

согласованность оценок: Мх f= Pi{a) М2 f= Pj(/i(o)) (»s= 1,2,___

Пропозициональные формулы строятся из переменых р; посредством пропозициональных связок Л, -1. Дизъюнкция V и импликация -4 вводятся обычным для классической двузначной логики образом.

Теорема 26 Набор связок {л, ->, □} характеризуется в теории Km0d следующими условиями:

(a) релятивизованность на верхний конус актуального мира;

(b) устойчивость относительно р-морфизмов моделей.

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

[1] Chagrov A., Zakharyaschev М. Modal Logic. Clarendon Press, Oxford, 1S97.

[2] Solovay R. Provability interpretations of modal logic.// Israel J. of Math., 1976, v.25, p.287-304.

[3] Сметанич Я.С: О полноте исчисления высказываний с дополнительной операцией от одной переменной.// Труды Моск. матем. об-ва, 1960, т.9, с.357-371.

[4] Сметанич Я.С. Об исчислениях высказываний с дополнительной операцией.// ДАН СССР, 1961, т. 139, № 2, с.309-312.

[5] Бессонов А.В. О новых операциях в интуиционистском исчислении.// Матем. заметки, 1977,1 т.22, вып.1, с.23-28.

[6] McCullough DJP. Logical connectives for intuitionistic propositional logic.// Journal of Symb. bogie, 1971, v.36^61, p.15-20.

[7] McKinsey J.C.C. Proof of the independence of the primitive symbols of Heyting's calculus of propositions. // J. of Symb. Logic, 1939, v.4, p.155-158.

[8] Скотт Д. Советы по модальной логике.// В кн.: Семантика модальных и интенсиональных логик, М.: Прогресс, 1981, с.280-317.

[9] 3>oeIstra A.S. On a second order propositional operators in intuitionistic logic.// Studia Logica, 1981, v.40^62, p.l 13-139.

[10] Kaininski M. Nonstandard connectives for intuitionistic propositional logic.// Notre Dame J. on Formal Logic, 1988, v.29, №3, p.309-331.

[11] Rauszer C. Applications of Kripke models to Heyting-Brouwer logic.// Studia Logica, 1977, T.36^sl-2, p.61-71;

[12] Lopez-Escobar E.G.K. On intuitionistic sentential connectives I.// Revista Colomb. Mat., 1985, v.19^1-2, p.117-130.

[13] Bull R.A. MIPC as the formalization of an intuitionistic concept of modality.//Journal Symb. Logic, 1966, v.31^6 4, p.60&-616.

[14] Ewald W.B. Intuitionistic tense and modal logic.// Jornal of Symb. Logic, 1986, v.51^61, p.166-179.

[15] Krivtsov V.N. Creative subject, Beth models and neighbourhood functions.// Archive for Mathematical Logic, 1996, v.35, p.89-102.

[16] Servi G.F. On modal logic with intuitionistic base.// Journal Symb. Logic, 1977, v.36^63, p.141-149.

[17] Sotirov V.H. Modal theories with intuitionistic logic.// Proc. of Conf. on Math. Logic, Sofia, 1984, p.139-171.

[18] Williamson T. On intuitionistic modal epistemic logic.// J. PhiL Log., 1992, v.21, ?61, p.63-89.

[19] Вольтер Ф., Захарьящев M. Об отношении между интуиционистскими и классическими модальными логиками. // Алгебра и логика, 1997, т.Зб, №2, с.121-155.

[20] Celluca С. Un connettivo per 1а logica intuitionista.// Le Matematiche, 1974, v.28, pu274-290;

[21] Goad C.A. Monadic infititary propositional logic: a special operator.//'Reports on Math. Logic, 1978, v.10, p.43-50.

[22] Bowen K.A. An extension of the intuitionistic prepositional calculus.// Indag. Math., 1971, v.33, №3, p.287-293.

¡23] Godel K. Zum intuitionisticschen Aussagenkaliffl.// Altad. der Wissenschaften in Wien, Math.-naturwissenschaftlische Basse, 1932, S.65-fi6.

[24] Скотт Д. Советы по модальной логике.// В кн.: Семантика модальных и интенсиошаль-ных логик, М.: Прогресс, 1981, с.280-317.

[25] Ttoelstra A.S. On a second order propositional operators in intuitionistic logic.// Studia Logica, 1981, v.40, №2, pЛ13-139.

[26] Zucker J.I., Tragesser R.S. The adequacy problem for inferential lope.// J. Philos. Lope, 1978, v.7, №4, p.501-516.

[27] Дарджания Г.К. Секвенциальный вариант модальной системы 1А.// В кн.: Металогические исследования, М., 1985, с.59-72.

[28] Gabbay D.M. On some new intuitionistic propositional connectives I.// Stadia Logica, Ю77, v.36^« 1-2, p.127-139.

[29] Расёва Б., Сикорский P. Математика метаматематики. М.: Наука, 1972.

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

31] Новиков П.С. Конструктивная математическая логика с точки зрения классической. М.: Наука, 1977.

[32] Кузнецов A.B. О неразрешимости общих проблем полноты, разрешения и эквивалентности для исчислений высказываний.// Алгебра и логика, 1963, т.2, вып.4, с.47-66.

[33] Кузнецов A.B. Аналоги штриха Шеффера в конструктивной логике.// ДАН СССР, 1S65, Т.Х60, №2, с.274-277.

[34] Кузнецов A.B. О средствах для обнаружения невыводимости или невыразимости..// В кн.: Логический вывод, М.: Наука, 1979, с.5-33.

[ЗЬ] Кузнецов A.B. О доказуемостно-интуиционистском пропозициональном исчислении.// ДАН СССР, 1985, т.283,№ 1, с.27-30.

¡36] Рыбаков В.В. Допустимые правила предтабличных модальных логик.// Алгебра и логика, 1981, т.20, вып.4, с.440-464.

[37] Рыбаков В.В. Базисы допустимых правил модальной системы Grz и интуиционистской логики.// Матем. сборник, 1985, т.128, №3, с.321-338.

[38] Рыбаков В.В. Уравнения в свободной топобулевой алгебре и проблема подстановки.// ДАН СССР, 1986, т.287, вып. 3, с 554-557.

[39] Рыбаков В.В. Допустимость правил вывода с параметрами в интуиционистской логике и интуиционистские модели Крипке.// ДАН СССР, т.312, вып.1, с.42-45.

[40] Rybakov V.V. Admissibility of logical inference rules. Studies on Logic and Foundations of Mathematics, vol.136,1997,617 pp.

[41] Максимова Л.Л., Рыбаков B.B. О решетке нормальных модальных логик.// Алгебра и логика, 1974, т.13, выл.2, с.188-216.

[42] Максимова Л.Л. Предтабличные суперинтуиционистские логики.// Алгебра и логика, 1972, т. 11, вып.5, с.558-570.

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

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

[45] Максимова Л.Л. Интерполяционные теоремы в модальных логиках. Достаточные условия.// Алгебра и логика, 1980, т.19, №2, с.194-213.

[46] Булос Дж., Джеффри Р. Вычислимость и логика.// М.: Мир, 1993.

[47] Chagrov A., Zakharyaschev M. The undecidability of the disjunction property of propositions! logics and other related problems.// Journal Symb. Logic, 1993, v.58,№3, p.967-1002.

[48] Chagrova L.A. An undecidable problem in correspondence theory.// Journal Symb. Logic, 1991, v756,№4, p.1261-1272.

[49] Чагров A.B. Неразрешимые свойства расширений логики доказуемости, часть 1, Алгебра и логика, 1990, т.29, с.350-367; часть 2, Алгебра я логика, с.614-623.

[50] А.В. Чагров, Л.А.Чагрова. Разрешимость проблемы антитабличности расширений логики Гёд&пя-Лёба. // Логические методы построения эффективных алгоритмов. Калинин, КГУ, 1986, с. 126-129.

[51] R-Harrop. On the existence of finite models and decision procedures for prepositional calculi. // Proc. Cambridge Philos. Soc., 1958, v. 54, p. 1-13.

[52] Burgess J. Decidability for brandling time.// Studia Logica, 1980, v.39, № 2-3, p.203-218.

[53] Пальчунов Д.Е. Конечно-аксиоматизируемые булевы алгебры с выделенными идеалами.// Алгебра и логика, 1987, г.26, вып.4, с.121-135.

[54] Pal'chunov D.E. Coustably-Categorical Boolean algebras with Distinguished Ideals.// Studia Logica, 1987, v.XLVI, №2, p.121-135.

[55] Пальчунов Д.Е. О псевдобулевых алгебрах с конечным числом плотных элементов... В сб.: Вычислимые инварианты в теории алгебраических систем. Новосибирск, ВЦ СО АН СССР, 1987, с.35-45.

[56] Maddux R.D. Open problems.// In: Colloquia Mathematica Societatis J£nos Bolyai, Algebraic Logic, 1988, p.727-746.

[57] Габбай Д.М. Общий метод фильтрации для модальных логик.// В кн.: Семантика модальных и интенсиональных логик, М.: Прогресс, 1981, с.205-211.

[58] Артёмов С.Н. Вопросы аксиоматизируемости и полноты модальных логик доказуемости.// Дисс... доктора фиэ.-матем. наук, М.: МИАН СССР, 1988, 158с.

[59] Artemov S.N., Beklemishev L.D. On prepositional quantifiers in provability logic.// Notre Dame Journal on Formal Logic, 1993, V.34J&3, p.401-419.

[60] Zakharyaschev M. Canonical formulas for К4. Part 1: Basic results.// Journal of Symb. Logic, 1992, v.57,№4, p.1377-1402.

61] Kracbt M. Tools and techniques in modal logic. IVeie Universitat, Berlin, 1996.

[62] Кейслер Дж., Чэн Ч.Ч. Теория моделей. М.: Мир, 1977.

Публикации автора по теме диссертации:

[1] Яшин А.Д. Формулы Нишимуры как одноместные логические связки в эле-гментарной теории моделей Крипке.// Вестник Моск. ун-та, Сер.1 матем., механ., 1984, № 5, с.12-15.

[2] Яшин А.Д. Семантическая характеризация интуиционистских логических связок.// Матем. заметки, 1985, т.38, №1, с.157-167.

[3] Яшин А.Д. Семантическая характеризация модальных логических связок.// Матем. заметки, 1986, т.40, №4, с.519-526.

[4] Яшин А.Д. Семантическая характеризация некоторых наборов интуиционистских логических связок.// Матем. заметки, 1989, т.45, №5, с.103-113.

[5] Яшин А.Д. Логика Сметанича Т* и два определения новой интуиционистской связки.// Матем. заметки, 1994, т.56, № 1, с.135-142.

[6] Яшин А.Д. О полноте одной новой интуиционистской связки.// Матем. заметки, 1996, т.60, №3, с.423-433.

[7] Яшин А.Д. Новая регулярная константа в интуиционистской логике высказываний.// Сибирский матем. журнал, 1996, т.37, №6, с.1413-1432.

[8] Ншин А.Д. О количестве новых логических констант в интуиционистском исчислении высказываний.// Вестник Моск. ун-та, Сер.1 матем., механ., 1997, №1, с.7-10.

[9] Ншин А.Д. Континуальность семейства полных по Новикову логик с новой одноместной связкой.// Вестник Моск. ун-та, Сер.1 матем., механ., 1997, *БЗ , с.22-25.

[10] Яшин А.Д. Модифицированная окрестностная семантика для логики Каминского.// Вестник Моск. ун-та, Сер.1 матем., механ., 1998, №2, с.8-11.

[11] Яшин А.Д. О новой константе в интуиционистской логике высказыввне-ий.// Фунд. и прикл. матем., 1999, т.5, №3, с.903-926.

[12] Яшин А. Д. Об одном расширении логики Габбая.// Сибирский матем. журнал, 1998, т.39, №1, с.224-235.

[13] Yashin A. On a semantical approach to the notion of the intuitionistic logical connective.// Proc. of VIII-th Congress on LMPS, Moscow, 198T, vol.1, p.73-74.

[14] Yashin A.D. On Novikov's approach to the notion of the intuitionistic logjcal connective: two negative examples.// Bulletin Sec. Log., 1996, v.725, №2, pJ84-88.

[15] Yashin A.D. New intuitionistic logical constants: undecidability of the conser-v&tiveness problem.// In: Lecture Notes in Computer Science, 1997, v.1258, p.460-471.

[16] Yashin A.D. New solutions to Novikov's problems for intuitionistic connectives.// Journal of Logic and Computations, 1998, v.8, №5, p.637-664.

[17] Yashin A.D. Lrreflexive modality in the intuitionistic prepositional logic and Novikov completeness.// Journal of Phil. Log., 1999, v.28, p.175-197.

[18] Yashin A.D. New intuitionistic logical constants and Novikov completeness^/ Studia Logica, 1999, v.63, p.151-180.

Подписано в печать 2£. О 9.2 ООО. Тираж 100 экз. Заказ № 1382. Типография Удмуртского госуниверситета. 426034, Ижевск, ул. Университетская, 1, корп. 4.