Логика доказуемости и доказуемостно-интуиционистская логика

После того как в начале XX в., Л. Брауэр подвергнул критике классическую логику (признаваемую математиками до тех пор как достаточно надежную основу для обоснования математических доказательств), в частности отвергая ее закон исключенного третьего, в математике стало складываться интуиционистское направление, а применявшиеся в не умозаключения стали формировать интуиционистскую логику. Как ичисление последняя в 1930 г. была сформулирована А.Гейтингом. И хотя согласно интуиционистской традиции никакое формальное оформление интуиционистской логики «никогда не дает полного и определенного ее описания, так же как недостижима полная теория других явлений» [3J, тем не менее под интуиционистской логикой принято понимать ту совокупность логических законов, которая была аксиоматизирована Гейтингом.

Желая лучше понять интуиционистскую критику или учесть ее, исходя из иных, чем интуиционисты (например, Брауэр (см.

33], с. III-II2)) философских предпосылок, были предприняты попытки описания интерпретаций законов интуиционистской логики, учитывающих эту критику. При этом большое значение, по-видимому, придавали интуиционистской идее о том, что всякое математическое высказывание «всегда требует проведения некоторого математического построения с некоторыми заданными свойствами», называемого доказательством этого высказывания, и что данное высказывание" можно утверждать, коль скоро это построение выполнено" [3]. Одной из первых была попытка В. Н. Колмогорова [603, предложившего истолкование интуиционистской логики как логики задач и связавшего истинность математического высказывания с задачей его доказательства, а ложность егос задачей его опровержения. Возникшие позже теория алгоритмов и конструктивное направление в математике связали закон исключенного третьего с задачей построения алгоритма, позволяющего установить истинность или ложность любого высказывания (т.е. доказать его или опровергнуть). При этом наличие алгоритмически неразрешимых массовых проблем подкрепляло интуиционистское сомнение в истинности этого закона.

Уточнения семантически неточной колмогоровской логики задач привели к логике рекурсивной реализуемости С. Клини и Дж. Роуоза (см. [5,703) и логике финитных задач Ю. Т. Медведева [183, отличными от интуиционистской и несравнимым между собой. Эти обстоятельства, а также сложность задания последних логик (особенно логики рекурсивной реализуемости) вынуждали к поиску новых интерпретаций, а наличие континуума логик, промежуточных между интуиционалистской логикой высказываний и классической, указывало на возможную сложность такого поиска. Между тем, выявленные трудности привели к идеи аппроксимации интуиционистской логики высказываний логиками из этого континуума, что породило устойчивый интерес ко всей совокупности этих логик. Результаты исследований их были подытожены в [58, 8].

Иное истолкование интуиционистской логики в 1933 г. было предложено К. Геделем [51]. Остановимся на этом подходе подробнее, используя более распространенные обозначения чем в [51]. С каждой из рассматриваемых ниже пропозициональных логик мы будем связывать некоторое исчисление И над языком ЯИ этого исчисления. При этом некоторая логика считается логикой данного исчисления И, если она содержит те и только те формулы языка ЯИ, которые (формально) выводимы в исчислении И (йь-ф означает, что формула Ф выводима в исчислении И). Так интуиционистская препозициональная логика ' Г рассматривается как множество формул языка Я1, которые строятся из бесконечного множества пропозициональных переменных pjC^jt,. (возможно, с индексами) на основе сигнатуры г V ^ п (4) обычным образом. Обозначая произвольные формулы языка буквами А, В, С, мы задаем логику I исчислением (которое также обозначаем буквой I), аксиомами которого служат следующие десять формул: сро с^эр", (Срэ С^эг" 1э<�ср=э^) oCpi>t)), (ргэс^эср&с^), (Cp&^)z>p), ССр^эе^), Cp^Cpvcv", (c^Cpvcv",.

— а правилами вывода — одновременная подстановка и moota* pohe.n.s Наряду с сигнатурой (I) Гедель f5l] рассмотрел пополненную сигнатуру r v 1 a f2) где модальность? («необходимо») является унарной препози-циональной связкой и предложил интерпретировать высказывание р как «р доказуемо». При этом гак расширенный язык он связал с модальной логикой Льюиса S4, задав его исчислением (которое мы будем обозначать тоже S4-), получаемым из исчисления X добавлением аксиом пртэр^ а)(арзр), б)(ар^аар), в)(а (р^)з (ар:эа<�р) (3) и одного правила вывода (усиления), позволяющего переходить от произвольной формулы ot языка ЯЭД к формуле, а <*. Заметив, что в аксиомах (3) модальность? можно истолковывать как доказуемость, Гедель (в целях погружения интуиционистской логики в модальную и тем самым предлагая новуто интерпретацию первой) высказал гипотезу, доказанную позже Мак-Кино и и Тарским [66], о том, что формула, А выводима в исчислении I тогда и только тогда, когда в исчислении выводим ее перевод «ТсА, получающийся расстановкой знака, а перед каждой подформулой формулы А. Однако Гедель заметил [51], что уточнение такого погружения, при котором модальность о понимается как доказуемость в формальной арифметике ?5] VA, которая выражается арифметическим высказыванием 6сдг ((X), означающим после проведения гедолевской арифметизации, что арифметическое высказывание выводимо в, не согласуется с аксиомой (За). Позже М. Леб, существенно используя некоторые факты из [563, установил [62], что для любых арифметических высказываний Ol ж Ol формулы беог С Ol о ОС) о (Bew (Ol) => B-eur COl'))).

Bear COL) ^ e^ С Bear COO)) w выводимы в, а формула (Bcur (Ol) «=> (X) выводима в Ф-А тогда и только тогда, когда выводимо Ol. эта последняя теорема была следующим образом усилена в [63]: для всякого арифметического высказывания Ol формула Ьеиг (WC0O «Ol) э Beur (tfO) выводима в .

Подчеркивая различие между формальной доказуемостью арифметического высказывания (X, выражаемой формулой ВедгСОО" и интуитивно понижаемой формальной доказуемостью, мы в [14] различаем две модальности: а и О , — ассоциируя л с Beur 1 а? Ol понимаем «как содержательное высказывание о том, что формально доказуемо (выводимо) в классической арифметике» С’И! В связи с этим вводим сигнатуру gr V => - л (б) и обычным образом строим формулы л, в> с,—- (возможно, с индексами или штрихами), учитывая, что знак, А играет роль унарной пропозициональной связки. Формула сигнатуры (6) называется геделевски верной [14], если при всякой подстановке в нее арифметических высказываний вместо всех переменных и расшифровки, а как бейт из нее получается арифметическое высказывание, доказуемое в*pj4. Формализация понятия геделевг ски'- верной формулы выполнена [13, 14] в виде следующего исчисления Д, аксиомами которого являются аксиомы классической логики высказываний, а также следующие три формулы а)(Д (р о (Ар => 4CJJJ, б)(Др"ДДр).в)(4С4рэр)э4р). (7).

Правилами вывода исчисления д являются подстановка, mod*" р0. гшц, а также следующие два: а) ^ (усиление), б) -^г (ослабление .(8).

Независимо похожее исчисление опубликовал Р. Соловей Е72] (но без последнего правила и в иных обозначениях —? вместо ^), обозначив его в честь Геделя буквой G. Заметим, что отбрасывая из списка постулатов исчисления Д аксиому (76) и правило (86) получаем исчисление (обозначаемое ниже буквой Q — ср. последнее исчисление с Д~из 1 М, а также с KA. W из ?711), рав-нообъемное, но не равносильное исчислению Д (см. [14]). Далее, учитывая то, что формулы (4) и (5) выводимы в, заключаем, что аксиомы (7) геделевски верны. Нетрудно также заметить, что правила (8) сохраняют геделевскую верность. Таким образом, всякая формула, выводимая в Д (и тем более в Q), геделевски верна. Соловей доказал [72] полноту исчисления Д (или G) относительно геделевской верности.

Уточняя идею Геделя из C5I] погружения логики X в, естественно прежде всего для произвольного арифметического высказывания OL представлять п Ol как арифметическое высказывание (а строя алгоритмическое погружение в согласии с идеями логики задач, надо дать алгоритм построения высказывания п Ol) так, чтобы арифметические высказывания.

Ot^Ol), сп&a (oi=*(k) были выводимы в l5-^. То, что это можно сделать средствами языка ЯА составляет содержание Основной Рабочей Гипотезы (ср.

I4-]), согласно которой существует в ft, А формула пр одной переменной р такая, что формулы сар=>р)> (ар=>Ар), п (рэр) (9) геделевски верны. Учитывая результат Соловея о полноте (см, выше), это означает, что формулы (9) выводимы в Д. Как доказано в [143, всякая формула пр, для которой формулы (9) выводимы в Д, эквивалентна в Д формуле (р&>др). Это дает основание для следующей расшифровки знака?: OL^y (CLlsACL). (10).

Называем (по аналогии с временными логиками Сб8]) м о д, а л ь-ным фрагментом логики доказуемости, заданной исчислением Д (или G) i множество формул сигнатуры (2), которые после расшифровки (10) выводимы в Д. Оказывается (лемма I.I.I), что модальный фрагмент логики доказуемости является нормальным расширением логики строгой импликаци Льюиса S^i. Поэтому естественно называть суперинтуиционистским фрагментом логики доказуемости множество формул сигнатуры (I) таких, что их перевод" ft после расшифровки (10) выводим в Д, т. е. суперинтуиционистский фрагмент логики доказуемости есть суперинтуиционистский фрагмент (в смысле [37]) модального фрагмента логики Д. Вопрос же о возможности погружения логики X в '^становится (учитывая «результат Соловея о полноте) вопросом о том, совпадает ли суперинтуиционистский фрагмент логики доказуемости с интуиционистской логикой. Положительный ответ на него дает теорема I.1, т. е. для всякой формулы, А языка 9l I при расшифровке (10) имеет место следующие эквивалентности:

X н-АФ=> G нТч-А. (п).

Рассматривая то или иное исчисление VA, называем его (нормальным) расширением такое множестсоответствующее исчислению И (для всех рассматриваемых здесь и ниже исчислений) — совокупность М VI всех тех алгебр сигнатуры исчисления 1Д, на которых верны все формулы, выводимые в И. Если Z. И — совокупность всех тех алгебр, логики которых суть расширения исчисления И, то легко показать (см. [14]), что ZHSMHh класс! И является наибольшим среди тех, которые вполне соответствуют исчислению И. Как показано в [141, ср. с равенством М s S. S^ ^ отмеченным в [26]), и класс ИД не является многообразием. На вопрос из [141, является ли класс £.Д квазимногообразием [17], отвечает теорема 1.3: ZA «не является универсально аксиоматизируемым классом.

После того, как возникла возможность (см. [141, сноска на с. 224) обобщить соотношение (II) на формулы сигнатуры (б), была сформулирована [91 доказуемостно-интуиционистская логика, которая в языке сигнатуры (б) задается [23, 24] (ср. [91) исчислением X4, аксиомами которой являются аксиомы (см. выше), а также следующие три формулы: а)(родр), б)(С^рэр)эр) fB) (лроО^с^зр))). (12).

Правила вывода исчисления I4 — те же, что у 1. Связь доказуемостно-интуиционистской логики с доказуемостной интерпретацией состоить в том, что всякая формула CL выводима в Iй тогда и только тогда, когда ее перевод «ft.А. (распространенный на формулы сигнатуры (б)) после расшифровки знака Q по (10) является геделевски верной формулой.

Реляционной семантикой доказуемостгл но-интуиционистской логики, заданной исчислением, и расшиво формул языка Я W, которое содержит все аксиомы исчисления.

1Л и замкнуто относительно всех его правил вывода. Очевидно, что всякое расширение исчисления Д является расширением исчисления G, но не обратно (ввиду неравносильности этих исчислений). Например, расширение G^-^P не замкнуто относительно правила ослабления. Вопрос о мощности расширений исчисления Д таким образом равносилен вопросу о мощности тех расширений исчисления G, которые замкнуты относительно ослабления. Ниже мы покажем (теорема 1.2), что эта мощность равна мощности континуума .

Алгебраическая семантика рассматриваемых (здесь и ниже) логик представляет из себя псевдобулевы С291 (в частности, булевы 129, 301) алгебры, возможно, с дополнительной операцией, удовлетворяющей некоторым тождествам^ Формула Ф считается верной на такой алгебре, если тождественно равна единице этой алгебры (т.е. ее наибольшему элементу), а логикой алгебры JC называем совокупность LJC/ всех формул, верных на^. Если формула ЯН/лГ, то говорим, что Я* опровержима на©-^" Считаем, что исчислению И соответствует совокупность алгебр 2. 1 если для любой формулы ^ языка ЯИ И Ь5? тогда и только тогда, когда Я* верна на всех алгебрах из ?- говорим, что И вполне соответствует 21, если для всяких формул ^ и языка ЯИ И+Фь-У тогда и только тогда, когда на всякой алгебре из, если на ней верна то на ней верна Ч** (см. [14]). Легко видеть, что если исчислению И вполне соответствует класс, то И соответствует, а также существует единственное многообразие [17], рений этого исчисления являются шкалы в виде частично упорядоченных множеств (где W — непустое множество), которые удовлетворяют условию обрыва возрастающих R-цепей. О з-н, а ч и в, а н и е м на <�а/, Я> называется бинарное отношение ^-V^CLHa W* Я14, удовлетворяющее следующим условиям: а) Сэс-Н^Г, ocR^) ^ 1= ЛГ, для любой пропозициональной переменной лпб) и в) ос. са/б)ф="> oc.*=ol или д) jl v= п cl V^CacR^ «> ложно ^ <0- ср. а) — д) с РО-Р<* из § 2 в [&Q]) е) ос. (ср. Ш).

Тройку, где Ол/> R> - шкала к ^ - означивание на ней, называем моделью для Формулу Я. считаем и стинной в точке oc^W данной модели, если и л о жн о й, если ложно (символически: <Х.

Логикой/.^ шкалы JK называется множество формул, истинных в каждой модели этой шкалы. Каждая формула из считается верной на шкале^М. Вместо будем иногда писать^д v= ос. Логика определяется классом & шкал, если она является пересечением логик шкал данного класса. Заметим, что всякая логика шкалы является расширением исчисления X (см. лемму 2.1.6). Всякое такое расширение исчисления называем моделируемым (ср. С8, 10,7 J). Ниже мы покажем, что доказуемостно-интуиционистская логика является моделируемой и даже определяется классом конечных шкал (теоретд ма 2.1), а также, что не всякое расширение исчисления является моделируемым (теорема 2.2).

Исследование пропозициональных логик в последние годы, начиная с систематического изучения суперинтуиционистских [8,7] (или промежуточных [58]) логик, устойчиво склонялось к выделению некоторой совокупности логик, являющейся совокупностью расширений какой-либо известной логики, чтобы рассмотреть в этой совокупности «отношения между логиками или некоторые структуры», выявленные в ней (см. [58]). При этом логикаэлемент такой совокупности, — понимается как «алгебраическая система, имеющая некоторое структурное сходство с логикой в обычном смысле и. не является логикой, на основе которой может или должна быть построена некоторого рода математика» [58]. Развитие этой точки зрения на примерах изучения совокупностей расширений интуиционистского исчисления I и нормальных расширений исчисления строгой импликации Льюиса привело к сравнительному их исследованию, начатому в 1461 и систематически проведенному в [22]. Именно в [22] было установлено, что существует гомоморфное отображение решетки ^ SV нормальных расширений исчисления S^j на решетку dCl расширений исчисления Г и изоморфное вложениес££ в ^ Оставаясь в рамках этой традиции, мы приводим ниже сравнительное исследование решетки всех нормальных расширений исчисления Q и решетки всех нормальных расширений исчисления X4. Заметим, что задавая логику исчисления И-i равносильным ему исчислением.

И^мы получаем изоморфные решетки «СИ* и^{Ненормальных} расширений этих исчислений. Так, например, задавая доказуемостно-ин.

ГЛг, А + v. «», а исчислением 1, получаемым из исчисления Г добавлением к постулатам последнего в качестве аксиом следующих формул:

12а), (126) и «Ср=>срэр)сэ (йЧ,=>р)) (ом. С9 3), ввиду равносильности исчислений I4 и (А.В.Кузнецов, неопубликовано) заключаем, что решетки ИЗОМОРФНЫ.

Приступая ниже к сравнительному изучению решеток и мы отметим что они имеют общий наибольший элемент (абсолютно противоречивая логика) и (единственный) общий коатомлогику СЛА, которая задается исчислением.

— причем всякое непротиворечивое расширение как исчисления G, так и исчисленияГл включено в, а сама логика непротиворечива. Сами же решетки и изоморфны, и изоморфизм устанавливается посредством отображения (теорема 3.2).

Напомним (см. [10, 14]), что логика L — расширение исчисления Q (или исчисления I4), — называется т, а б л и чн о й, если она является логикой некоторой конечной алгебрыназывается предтабличной, если она не таблична, но всякое ее собственное расширение (т.е. расширение данного исчисления, строго включающее L) уже табличнои называется финитно аппроксимируемой, если она пред-ставима в виде теоретико-множественного пересечения табличных логик. Реляционной семантикой исчисления Q и его расширений являются шкалы R>, где Ятранзитивное, иррефлексивное отношение на непустом множестве W с условием обрыва R-цепей (т.е. отношение R" «1 является фундированным). Означивание на таких шкалах в отличии от условий (13) должно удовлетворять следующим: (136), (13в), а также а) ос&Са-э в) ф*> «эс*^ cl илиос^ёб) ос m ol <==> &: (14) в) V* (ж. «="> ^ КЯ) (cMe C72j ^.

Расширение исчисления G считаем моделируемым, если оно является логикой такой шкалы.

Исследование свойств сохраняющихся изоморфизмом }> (будем их называть фукториальными свойствами), приводит к следующим заключениям: расширение l исчисления G является табличным (предтабличным или финитно аппроксимируемым) тогда и только тогда, когда таково расширение ,(теорема 3.3) — моделируемо тогда и только тогда, когда моделируемо (теорема 3.4) — в L допустимо ослабление тогда и только тогда, когда оно допустимо в j*L. (теорема 3.5). Отсюда получаются, например, следующие следствия: существует ровно счетное множество предтабличных расширений исчисления существует не моделируемое расширение исчисления G, существует континуум расширений исчисления I4, в которых допустимо правило ослабления (т.е. совокупность расширений исчисления из С9] континуальна) — причем среди последних имеется наибольшее непротиворечивое расширение — логика Сер = р>)? которая является логикой шкалы где ^^ {Oj^Z,. } f, а ^ означает отношение «больше или равно» на 'V ,.

Чтобы лучше разрбраться во всей совокупности суперинтуиционистских логик, А. В. Кузнецовым в С7] была намечена некоторая их классификация, впоследствие уточненная в Г8]. В отличие от классификации Хосои [57] типа разбиения, Кузнецов выделил классы суперинтуиционистских логик, линейно упорядоченные по включению. Хотя полученная иерархия классов и не является систематической (т.е. без единого определения классов), она все же обращает внимание на важное свойство логик, выделенных в отдельный класс. Важной задачей, вытекающей из такой классификации, является вопрос о совпадении или отличии выделенных классов логик. Ряд таких открытых вопросов был поставлен в C8L Напомним [8, 10], что суперинтуиционистская логика называется м о д ел и р у е м о й, если она является логикой некоторого частично упорядоченного множества, понимаемого как шкалапричем условия (13) для формул сигнатуры (I) ограничиваются только пунктами а) — д). Говорим ?8], что суперинтуиционистская логика, а п-проксимируется псевдобулевыми алгебрами с условием обрыва убывающих цепей, если данная логика предетавима в виде теоретико-множественного пересечения некоторой совокупности логик таких алгебр, или иначе, если для всякой формулы языка 911, не принадлежащей данной логике, найдется псевдобулева алгебра с условием обрыва убывающих цепей, на которой зта формула опровержима, а формулы логики верны. На один из вопросов из [8] дается ответ: класс моделируемых логик строго включает в себя класс логик, аппроксимируемых алгебрами с условием обрыва убывающих цепей (следствие 4.2.8).

Сделаем ряд замечаний относительно нумерации утверждений. Все главы делятся на параграфы. Теоремы имеют двойную нумерацию. Например, теорема 1.3 означает третью теорему первой главы. Остальные утверждения (леммы, замечания и следствия) имеют сквозную нумерацию внутри отдельного параграфа. Так, например, номер 3. I. 2 при таком утверждении означает, что оно находится в первом параграфе третьей главы и второе по счету среди всех утверждений такого рода.

Материалы диссертации докладывались на семинаре по математической логике ЛОМН АН СССР (1975 г.), на семинаре по математической логике ВИНИТИ (1976 г.), на УП Всесоюзной конференции по логике и методологии науки (Киев, 1976 г.), на 1У Всесоюзной конференции по математической логике (Кишинев, 1976 г.), на семинарах «Алгебраические системы» и «Алгебра и логика» Института математики СО АН СССР (1980 г.), на семинаре по математической логике МТУ (1984 г.), на семинарах по математической логике Института математики с ВЦ АН МССР (1975 — 1983 гг.). Результаты опубликованы в работах [13,14], {23 — 27].

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

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

2. Биркгоф Г. Теория решеток. М.: «Наука», 1984.

3. Гейтинг А. Интдиционизм. М., «Мир», 1965.

4. Гретцер Г. Общая теория решеток. М.: «Мир», 1982.

5. Клини С. К.

Введение

в метаматематику. М., ИА, 1957.

6. Крипке С. А. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний. В кн.:Фейс Р. Модальная логика. М.: «Наука», 1974, 254−303.

7. Кузнецов А. В. О некоторых вопросах классификации суперин-туционистских логик. В сб.: Третья. Всесоюзная конф. по матем. логике (тезисы). Новосибирск, 1974, II9-I22.

8. Кузнецов А. В. О суперинтуиционистских логиках. Мат. исследования, 1975, 10, еып. 2, 150−158.

9. Кузнецов А. В. Доказуемостно-интуиционистская логика. В сб.: Модальные и интенсиональные логики (тезисы координац. совещ.). М.: ИФ АН СССР, 1978, 75−79.

10. Кузнецрв А. В. О средствах для обнаружения невыводимости или невыразимости. В сб.: Логический вывод. М.: «Наука», 1979, 5−33.

11. Кузнецов А, В. Об алгебрах открытых множеств. В сб.: Тираспольский симпозиум по общей топологии и ее приложениям. Кишинев: «Штиинца», 1979, с. 72−75.

12. Кузнецов А. В., Герчиу В. Я. О суперинтуиционистских логиках и финитной аппроксимируемости.-ДАН СССР, 1970,195,№ 5, 1029−1032.

13. Кузнецов А. В., Муравицкий А. Ю. Логика доказуемости.1У Всесоюзная конф. по матем. логике (тезисы). Кишинев: «Штиинца», 1976, 73.

14. Кузнецов А. В., Муравицкий А. Ю. Доказуемость как модальность. В сб.: Актуальные проблемы логики и методологии науки. Киев, Наукова думка, 1980, 193−230.

15. Кузнецов А. В., Муравицкий А. Ю. Магариевы алгебры. В сб: 14-я Всесоюзная алгебраическая конференция (тезисы). Новосибирск, 1977, 105−106.

16. Курош А. Г. Лекции по общей алгебре. М., «Наука», 1973.

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

18. Медведев Ю. Т. Финитные задачи. ДАН СССР, 1962, 142, № 5, I0I5-I0I8.

19. Мендельсон Э.

Введение

в математическую логику. М.: «Наука», 1976.

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

21. Максимова Л. Л. Модальные логики конечных слоев. Алгебра и логика, 1975, 14, Ш 3, 304−314.

22. Максимова Л. Л., Рыбаков В. В. О решетке нормальных модальных логик. Алгебра и логика, 1974, 13, № 2, 188−216.

23. Муравицкий А. Ю. Сильная эквивалентность на интуиционистской модели Крипке и ассерторически равнообъемные логики.-Алгебра и логика, 1981, т. 20, № 2, 165−189.

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

25. Муравицкий А. Ю. Класс £Д магариевых алгебр, В сб.:ХУ1 Всесоюзная алгебраич. конф., Ленинград, 1981.

26. Муравицкий А. Ю. О расширениях логики доказуемости. -Матем. заметки, 1983.

27. Муравицкий А. Ю. О расширениях логики. В сб.: Летняя шкала по математической логике и ее приложениям. София, 1983, 9−12.

28. Новиков Г1.С. Конструктивная математическая логика с точки зрения классической. М.: «Наука», 1977.

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

30. Сикорский Р. Булевы алгебры. М.: «Мир», 1969.

31. Скорняков Л. А. Элементы теории структур. М.: «Наука», 1982.

32. Соболев С. К. О конечномерных суперинтуиционистских логиках. Известия АН СССР, серия матем., 1977, 41,№ 5, 963−986.

33. Тростников В. Н. Конструктивные процессы в математике. М.: «Наука», 1975.

34. Шехтман В. Б. О неполных логиках высказываний. ДАН СССР, 1977, 235, й 3, 542−545.

35. Шехтман В. Б. Топологические модели пропозициональных логик. Семиотика и информатика, 1980, вып. 15, 74−98.

36. Эклоф П. Теория ультрапроизведений для алгебраистов. В сб.: Справочная книга по математической логике. Часть I: Теория моделей. М.: «Наука», 1982, 109−140.

37. Эсакиа Л. Л. О некоторых новых результатах теории модальных и суперинтуиционистских систем. В сб.: Теория логического вывода (тезисы). М., 1974, 173−183.

38. Эсакиа Л. Л. О многообразиях алгебр Гржегорчика. В сб.:Исследования по неклассическим логикам и теории множеств. М.: «Натка», 1979, 257−287.

39. Янков В. А. Построение последовательности сильно независимых с^щеринтуиционистских пропозициональных исчислений. ДАН СССР, 1968, 181, № I, 33−34.

40. Bernardi О. The fixed-point theorem for diagonalizable algebras. Studia Logica, 1975, 34, 239−251.

41. Bernardi C. On the equational class of diagonalizable algebras. Studia Logica, 1975, 34, No.4, 321−331.

42. Dummett M.A., Lemmon E.J. Modal logics between S4 and S5. -Zeitschr. mathem. Logik und Grundl. Mathem., 1959, 5, 250 264.

43. Fine K. Logics containing K4. Part I. J. Symb. Logic, 1974,39, No.1, 31−42.

44. Pine K. An incomplete logic containing S4. Theoria, 1974,40, 23−29.

45. Fine К. An ascending chain of S4 logics. Theoria, 1974, 40, ITo.2, 110−116.

46. Fitting M.C. Intuitionistic logic, model theory and forcing. Amsterdam, 1969.

47. GSdel K. Eine Interpretation des intuitionistischen Aussagen-kalktils. In: Ergebnisse eines mathematischen Kolloquiums, 1933, 4, 39−40.

48. Goldblatt R. Arithmetical necessity, probability and intui-tionistic logic. Theoria, 1978, 54, No.1, 38−46.

49. Gr&tzer G. Universal Algebras, New York, 1979.

50. Grzegorczyk A. Some relational systems and the associated topological spaces. Fund. mathem., 1967, 60, 223−231.

51. Harrop R. On the existence of finite models and decision procedures for propositional calculi. Proc. Camb. Phil. Soc., 1958, 54, 1−13.

52. Hilbert D., Bernays. Grundlagen der Mathematifc, vol.2, Berlin, 1939.

53. Hosoi T. On intermediate logics I. J. Fac. Sci. Univ. Tokyo, Sec.1, 1967, 14, 293−312.

54. Hosoi Т., Ono H. Intermediate Propositional bogies (A Survey). J. Tsuda College, 1973, 559. de Jongh D.H.J., Troelstra A.S. On the connection of partially ordered sets with some pseudo-boolean algebras. -Indag. Mathem., 1966, 28, 317−329.

55. Kolmogoroff A. Zur Deutung der intuitionistischen LogicMath. Z., 1932, 35.

56. Lemmon E.J. Some results on finite axiomatizability in modal logic. Notre Dame J. Form. Logic, 1965″ 6, No.4, 301 308.

57. L6b M.H. Solution of problem of Leon Henkin. J. Symb. Logic, 1955, 20, No.2, 115−118.

58. Macintyre A., Simmons H. Gttdel’s diagonalization technique and. related properties of theories Colloquium mathematical, 1973, vol.28, fasc.2, 165−180.

59. Magari R. The diagonalizable algebras. Boll, unione mat. ital, 1975, 12, suppl. fasc. 3, 117−125.65″ Makinson D. Some embedding theorems for modal logic. -Notre Dame J. Form. Logic, 1971″ 12, Ho.2, 252−254.

60. Mc. Kinsey J.C.C., Tarski A. Some theorems about the sentential calculi of Lewis and Heyting. J. symb. Logic, 1948, 13, 1−15.

61. Ono H. Kripke models and intermediate logics.*" Publ. RIMS, Kyoto Univ., 1970, 6, 461−476.

62. Prior A.XT. Past, present, future. Oxford, 1967.

63. Rasiowa H. An algebraic approach to non-classical logics. Warszawa, 1974.

64. Rose G.F. Propositional calculus and realizability. -Trans. Amer. Math. Soc., 1953, 75, 1−19.

65. Segerberg K. An Essay in Classical Modal Logic. Filosofiska studier, Uppsala, 1971″.

66. Solovay R.M. Provability interpretations of modal logic. -Israel J. Mathem., 1976, vol. 25, 287−304.