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

• Яшин, Александр Данилович
• доктор физико-математических наук
• 1999

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

1 Метаматематика <£-логик.

1.1 Шкалы и модели.

1.2 Порожденные шкалы.

1.3 Р- морфизмы.

1.4 Обратная теорема о р-морфизмах и изоморфных вложениях

1.5 Характеристические формулы. Обратная теорема о сравнении логик.

1.6 Разное.

1.7 (^-Шкалы и (^-логики

1.8 Схема замены эквивалентных и порожденные c/3-шкалы

1.9 Р^-морфизмы.

1.10 О включении ^-логик

1.11 О присоединимости формул.

1.12 Подход П.С.Новикова.

1.13 Подход Д.Габбая.

1.14 Прямая схема построения примеров полных по Новикову нормальных </>логик.

1.15 Схема построения примеров полных <р-логик методом перевода . •

1.16 Анализ известных примеров.

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

1.16.2 Регулярная константа в Int

1.16.3 Логика Бессонова

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

1.16.5 Сильное отрицание.

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

1.16.7 Универсальная необходимость.

1.16.8 Немонотонная возможность

1.16.9 Оператор Крайзеля.

1.16.10Антиимпликация Боуэна.

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

2.1 0 конечных (^-шкалах.

2.2 Шкалы с наростами.

2.3 ¡^-логики I?

2.4 Основная лемма и ее следствие.

2.5 О полных (^-логиках с явными соотношениями.

2.6 Универсальная <£-шкала.

2.7 О числе полных ф-логик при \ф\> 2.

2.8 О (^-напарнике чистой табличной логики.

2.9 Формулы Нишимуры

2.10 ^-логики La.

2.11 Полнота по Новикову <£>-логики L

2.12 О логиках с неравномерно ограниченными константными формулами

2.13 ¡¿ыюгики L1 и L2.

2.14 Классификационная теорема.

2.15 Аксиомы логики Ьт.

2.16 Вырожденный случай теоремы о семантической полноте

2.17 Непротиворечивые пары

2.18 Построение основы.

2.19 Невырожденный случай теоремы о семантической полноте

2.20 Разрешимость ц>-логик Vх

2.21 Разрешимость алгоритмической проблемы консервативности для \ф\ — 1.

2.22 Неразрешимость алгоритмической проблемы консервативности для \<р\ > 2.

3 Неконстантные связки и полнота по Новикову

3.1 Логика Кузнецова и логика Габбая.

3.2 Шкалы с конечными хвостами.

3.3 о>шкалы.

3.4 Аксиоматика логик Kz+ и Gab+.

3.5 О числе полных логик с новой одноместной связкой

3.6 О полных расширениях логики Бессонова.

3.7 Пример полной по Новикову логики с несколькими одноместными независимыми связками.

3.8 Пример полной по Новикову логики с новой двухместной связкой.

3.9 Неразрешимость алгоритмической проблемы консервативности в языке с одной одноместной связкой

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

4.1 Семантический подход к понятию интуиционистской логической связки.

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

4.3 Пропозициональные типы.

4.4 Характеризация стандартных связок.

4.5 Характеризация набора стандартных связок с универсальной необходимостью.

4.6 Характеризация связок логики Гейтинга

Брауэра с универсальной необходимостью.

4.7 Характеризация связок логики

Гейтинга-Брауэра.

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

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

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

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

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

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

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

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

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

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

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

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

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

При переходе к прикладным интуиционистским теориям, например, арифметике Гейтинга, базисной логической системой становится интуиционистская пропозициональная логика 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 о понятии классической t"-логической связки. ' "

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

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

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

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

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

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

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

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

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

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

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

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

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

Применительно к модальной логике Д.Скотт [27] пишет:

Имея подходящее определение ., мы, без сомнения, сможем показать, что единственными логическими операторами (одноместными — прим. авт.) являются -1, —< —», □, О.

С другой стороны, А.Трулстра в статье [113] выражает некоторое сомнение по поводу функциональной полноты набора стандартных интуиционистских связок:

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

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

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

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

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

Aj^Bi,., Aki ++ Bki для каждой дополнительной связки

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

Явным соотношением для связки </?г- называем формулу вида где А не содержит щ.

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

А (.Pj Qj) (£>(Ръ • • • ,Рь) D{qu ., qki)).

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

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

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

Определение 2. Связки <pi,. ,<рп независимы в консервативной (р-логике L, если для любого (pi б (р и для любой формулы А, не содержащей вхождений ipi, (^-логика L + <pi{p\,. -Н- А неконсервативна над Int. Другими словами, никакое расширение L, консервативное над Int, не содержит явных соотношений.

Определение 2 можно рассматривать как обобщение известного факта о независимости стандартных связок в Int [98]: при присоединении к Int какого-то явного соотношения, например (р—V, д), образуется собственное расширение Int.

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

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

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

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

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

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

Для случая нескольких дополнительных констант (р установлен следующий результат:

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

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

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

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

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

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

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

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

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

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

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

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

V, А, {V, А, -!,□},

V, А,г, А}, {V, А,г,А,П} здесь □ — модальный оператор типа универсальной необходимости, А, г — связки, дуальные связкам —>, соответственно).

Название диссертации отражает различные виды полноты, которые будут расматриваться:

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

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

• дефинициальная полнота набора данных связок.

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

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

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

3. Ершов Ю.Л., Палютин Е.А. Математическая логика. // М.: Наука, 1987.

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

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

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

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

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

9. Мальцев А.И. Алгебраические системы. М.: Наука, 1970.

10. Муравицкий А.Ю. О финитной аппроксимируемости исчисленияи немоделируемости некоторого его расширения.// Матем. заметки, 1981, т.29,№6, с.907-916.

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

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

13. Сакс Дж. Теория насыщенных моделей.// М.: Мир, 1976.

14. Сегерберг К. Модальные логики с линейными отношениями альтернативности.// В кн.: Семантика модальных и интенсиональных логик. М.: Прогресс, 1981, с.180-204.

15. Скворцов Д.П. Об интуиционистском исчислении высказываний с дополнительной логической связкой.// В кн.: Исследования по неклассическим логикам и формальным системам, М.: Наука, 1983, с.154-173.

16. Скворцов Д.П. О структуре расширений пропозиционального фрагмента логики Аккермана.// В кн.: Исследования по неклассическим логикам и формальным системам, М.: Наука, 1983, с.209-221.

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

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

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

20. Соболев С.К. Об интуиционистском исчислении высказываний с кванторами.// Матем. заметки, 1977, т.22, №1, с.69-76.

21. Чагров A.B. Два новых вида мультимодальных логик.// В кн.: Неклассические логики и пропозициональные установки, М., 1987, с.48-59.

22. Чагров A.B. Континуальность множества максимальных суперинтуиционистских логик со свойством дизюнктивности.// Матем. заметки, 1992, т.51, вып.2, с.117-123.

23. Шавруков В.Ю. О двух расширениях логики доказуемости GL.// Матем. сборник, 1990, т.181, №2, с.240-255.

24. Шаталов В.В. Топологические модели для интуиционистской логики и спекутр опровержений формулы в логике Фитча.// В сб.: Теория множеств и топология, Ижевск, 1977, с.93-95.

25. Шехтман В.Б. Лестницы Ригера-Нишимуры.// ДАН СССР, 1978, т.241, №6, с.1288-1291.

26. Шехтман В.Б. Применение моделей Крипке к исследованию суперинтуиционистских и модальных логик.// Дисс. канд. физ.-матем. наук, М., 1984.

27. Шютте К. Полные системы модальной и интуиционистской логики.// В кн.: Фейс Р. Модальная логика, М.: Наука, 1974, с.324-421.

28. Эсакиа Л.Л. К теории модальных и суперинтуиционистских систем.// В кн.: Логический вывод, М.: Наука, 1979, с.147-172.

29. Эсакиа Л.Л. Алгебры Гейтинга. Тбилиси: Мецниереба, 1985.

30. Янков В.А. О связи между выводимостью в интуиционистском исчислении высказываний и конечными импликативными структурами.// ДАН СССР, 1963, т.151, №6, с.1293-1294.

31. Янков В.А. Построение последовательности сильно независимых суперинтуиционистских пропозициональных исчислений.// ДАН СССР, 1968, т.181, №1, с.33-35.

32. Яшин А.Д. О выразимости логических связок в неклассических логиках.// Дисс.канд. физ.-мат. наук, М., 1984.

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

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

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

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

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

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

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

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

41. Яшин А.Д. Континуальность семейства полных по Новикову логик с новой одноместной связкой.// Вестник Моск. ун-та, Сер.1 матем., механ., 1997, №3, с.22-25.

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

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

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

45. Artemov S.N., Beklemishev L.D. On prepositional quantifiers in provability logic.// Notre Dame Journal on Formal Logic, 1993, v.34,№3, p.401-419.

46. Baker K.A. Finite equational bases for finite algebras in a congruence distributive equational classes.// Advances in Math., 1977, v.24, p.207-243.

47. Bossi S., Meloni G. Representation of Hey ting algebras with covering and propositional intuitionistic logic with local operator.// Boll. Unione mat. ital., 1980, v.A17,№3, p.436-442.

48. Bozic M., Dosen K. Models for normal intuitionistic modal logics.// Studia Logica, 1984, v.43,№3, p.217-245.

49. Bowen K.A. An extension of the intuitionistic propositional calculus.// Indag. Math., 1971, v.33,№3, p.287-293.

50. Bull R.A. MIPC as the formalization of an intuitionistic concept of modality.//Journal Symb. Logic, 1966, v.31,№4, p.609-616.

51. Burgess J.P. Decidability for branching time.// Studia Logica, 1980, v.39, №2/3, p.203-218.

52. Cellucci C. Un connettivo per la logica intuitionista.// Le Matematiche, 1974, v.28, p.274-290.

53. Chagrov A., Zakharyaschev M. Modal companions of intermediate propositional logics.// Studia Logica, 1992, v.51,№l, p.49-82.

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

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

56. Chagrov A., Zakharyaschev M. Modal Logic. Clarendon Press, Oxford, 1997.

57. Couturat L. Алгебра логики.// Одесса: Матезис, 1909.

58. Dubashi D.P. On decidable varieties of Heyting algebras.// Journal Symb. Logic, 1992, v.57,№3, p.988-991.

59. Dummett M. A propositional calculus with denumerable matrix.// Journal Symb. logic, 1959, v.24,№ 1, p.97-106.

60. Ewald W.B. Intuitionistic tense and modal logic.// Jornal of Symb. Logic, 1986, v.51,№ 1, p.166-179.

61. Fitting M.C. Many-valued modal logics.// Fundam. Informatik, 1991, v.15, No 3-4, p.235-254.

62. Gabbay D.M. The decidability of the Kreisel-Putnam system.// Journal Symb. Logic, 1970, v.35,№3, p.

63. Gabbay D.M. Model theory for tense logics.// Annals of Math. Logic, 1975, v.8, №1-2, p. 185-236.

64. Gabbay D.M. On some new intuitionistic propositional connectives I.// Studia Logica, 1977, v.36,№ 1-2, p. 127-139.

65. Gabbay D.M. What is a classical connective?// Zeitschr. Math. Logik und Gründl. Math., 1978, Bd.24, H.l, S.37-44.

66. Gabbay D.M. Intuitionistic basis for non-monotonic logic.// In: Lect. Notes in Computer Science, 138, p7260-271.

67. Glivenko V.l. Sur quelques points de la logique de M.Brouwer. // Acad. Roy. Belg. Bull. Cl. Sei., 1929, v.15, p.183-188.

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

69. Gödel K. Zum intuitionistischen Aussagenkalkül.// Akad. Wiss. Wien, math.-naturw. Kl., Anzeiger 69 (1932), S.39-4Û.

70. Goldblatt R.I. Metamathematics of modal logic I;II // Reports on Math, logic, 1976, v.6, p.41-78; v.7, p.21-52.

71. Gurevich Yu. Intuitionistic logic with strong negation.// Studia Logica, 1977, v.36,№ 1-2, p.49-59.

72. Harrop R. On the existence of finite models and decision procedures for propositional calculus.// Proc. Cambridge Phil. Soc., 1958, v.54, p.1-13.

73. Heyting A. Die formalen Regeln der intuitionistischen Logik.// Sitzungsber. Preuss. Akad. Wiss., phys.-math. Kl., 1930, S.42-56.

74. Hobby D., McKenzie R. The structure of finite algebras.// Contemporary Math., 1988, v.76.

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

76. Kirk R.E. A characterization of the classes of finite tree frames which are adequate for the intuitionistic logic.// Zeitschr. Math. Logic und Gründl. Math., 1980, Bd.26, H.6, S.497-501.

77. Kracht M. Tools and techniques in modal logic.// Freie Universität, Berlin, 1996.

78. Kreisel G. Monadic operators defined by means of propositional quantification in intuitionistic logic.// Reports on Math. Logic, 1981, v.12, p. 15-19.

79. Krivtsov V.N. Cteative subject, Beth models and neighbourhood functions.// Archive for Mathematical Logic, 1996, v.35, p.89-102.

80. Kutschera V.E. Die Vollständigkeit des operatorensystems {-i, A, V, 3} für die intuitionistische aussagenlogik im rachmen der Gentzensemantik.// Archiv math, logik und Grundlagen forschung, 1968, B.ll,№ 1-2, S.3-16.

81. Lopez-Escobar E.G.K. Proof functional connectives.// Lect. Notes Math., 1985, v.1130, p.208-221.

82. Lopez-Escobar E.G.K. On intuitionistic sentential connectives I.// Revista Colomb. Mat., 1985, v.l9,№l-2, p.117-130.

83. Lukaszewicz W. Non-monotonic reasoning.// NY: Ellis Horwood, 1990.

84. McCall S. The strong future tense.// Notre Dame J. Formal Logic, 1979, v.20, No 3, p.489-504.

85. 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.

86. McCullough D.P. Logical connectives for intuitionistic propositional logic.// Journal of Symb. Logic, 1971, v.36,№l, p.15-20.

87. Minsky M. Recursive insolvability of Post's "Tag" problem and other topics in the theory of Turing machines.// Annals of Mathematics, ser.2, 1961, v.74, p.437-455.

88. Nishimura I. On formulas of one variable in intuitionistic propositional calculus.// Journal of Symb. Logic, 1960, v.25, p.327-331.

89. Nute D. Counterfactuals.// Notre Dame J. on Formal Logic, 1975, v. 16,№4, p.476-482.

90. Pitts A. On an interpretation of second order quantification in first order intuitionistic propositional logic.// Journal Symb. Logic, 1992, v.57, p.33-52.

91. Rieger L. On the lattice theory of Brouwerian propositional logic.// Acta Facultatis Rerum Naturaleum Universitatis Carolinae. Mathematica, 1949, v. 189, p. 1-40.

92. Rauszer C. A formalization of the propositional calculus of H-B logic.// Studia Logica, 1974, v.33,№l, p.23-34.

93. Rauszer C. Applications of Kripke models to Heyting-Brouwer logic.// Studia Logica, 1977, v.36,№l-2, p.61-71.

94. Rauszer C. Model theory for an extension of intuitionistic logic.// Studia Logica, 1977, v.36,№l-2, p.73-87.

95. Sanchis L. Formally defined operations in Kripke models.// Notre Dame J. Formal Logic, 1973, v. 14,№4, p.467-480.

96. Servi G.F. On modal logic with intuitionistic base.// Journal Symb. Logic, 1977, v.36,№3, p. 141-149.

97. Servi G.F. Nonmonotonic consequense based on intuitionistic logic.// Journal of Symb. Logic, 1992, v.57,№4, p.1176-1197.

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

99. Yashin A.D. New solutions to Novikov's problem for intuitionistic connectives.// Journal of logic and computations, 1998, v.8 ,№.5, p.637-664.

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

101. Zeman J.J. Some calculi with strong negation primitive.// Journal of Symb. Logic, 1968, v.33,№l, p.97-100.

102. Zucker J.I., TYagesser R.S. The adequacy problem for inferential logic.// J. Philos. Logic, 1978, v.7,№4, p.501-516.