Введение к работе
Актуальность темы исследования . Для решения различного рода задач теоретической информатики используются результаты и методы из многих областей математики и в особенности из математической логики. В настоящее время многие исследования по математической логике считаются в той или иной мере исследованиями и по теоретической информатике. На базе некоторых ее разделов образовались целые направления в информатике , а ее основные понятия стали основными понятиями и теоретической информатики . Среди них - понятие логического исчисления и понятие вывода в данном логическом исчислении. Они используются при построении многих систем представления знаний , что связано с написанием программ и выбором моделей предметной области , называемых базами знаний [1] . Сейчас различают несколько их типов , к одному из них относятся логические модели [1], в основе которых лежит логическое исчисление - система, определяемая аксиомами и правилами вывода . При таком подходе формулы используемого исчисления интерпретируются суждениями из рассматриваемой области знаний , а правила вывода путем их последовательных применений позволяют получать из исходных ( аксиом ) новые знания. Логические исчисления, преимущественно с интуиционистской основой, используются и в задачах декларативного синтеза программ. В синтезирующих системах искомый алгоритм извлекается из вывода в выбранном исчислении спецификации решаемой задачи из базы знаний рассматриваемой системы [1]. Возможность такого подхода обеспечивается наличием логических исчислений , имеющих конструктивную семантику типа реализуемости Г32.36] и допускающих эффективный поиск вывода.
В основе логического программирования лежит идея вывода в логическом исчислении. Программа в нем по сути дела есть набор правил вывода , а ее выполнение - процесс построения вывода в классическом исчислении предикатов [32,18]. Поставленная задача записывается в виде формулы ( цели ) этого исчисления , а ее решение с помощью подходящей программы осуществляется путем поиска вывода в нем формулы ( цели ).
Понятие логического исчисления возникло не сразу, а постепенно формировалось в математике , стимулируя развитие математической логики , что привело к выделению ее в самостоятельный раздел. По сути дела, в нем соединены аксиоматико-дедуктивный метод в математике , приписываемый Пифагору и дошедший до нас благодоря Эвклиду,
и метод формального рассмотрения логики, принадлежащий, по-видимому, Аристотелю.
Первым шагом в процессе построения современных логических исчислений следует считать осуществленную Фреге в 1879 году формулировку классического пропозиционального исчисления [14,18,32,10]. Значительным вкладом в его развитие Оыло и выполненное в неявной форме Расселом в 1908 году и явной Гильбертом и Аккерманом в 1928 году оформление в виде исчисления логики классической математики ( по существу логики Аристотеля ), получившего в дальнейшем название классического исчисления предикатов [18,32,10]. Большое влия-яние на ускорение этого процесса оказал и формализм Гильберта [18, 32), предложенный им для доказательства непротиворечивости различных разделов математики. Необходимость такого доказательства была обусловлена наличием парадоксов в основаниях математики. Существенным шагом в нем явилось и выполненная Гейтинтом в 1930 году формализация [16] логики интуиционистской математики Брауэра [9, 17,32] , известная теперь как интуиционистское исчисление предикатов [32]. Оно вместе с классическим исчислением предикатов составили основу математической логики и подверглись разностороннему и тщательному изучению. Это Оыло вызвано не только удобствами рассматривать упомянутые выше логики в виде исчислений, но и той значительной ролью , которую они играли в математических исследованиях. Их ценность стала еще более ясной после появления конструктивного направления в математике [2] , предложенного Марковым на базе теории алгоритмов , так как логики интуиционистской и конструктивной математик совпали. Самостоятельный интерес был проявлен к пропозициональному фрагменту интуиционистского исчисления предикатов, получившему название интуиционистского пропозиционального исчисления [32] и соответствующему одноименным фрагментам логик интуиционистской и конструктивной математик. Всестороннее изучение этого исчисления и его расширений - суперинтуиционистских пропозициональных исчислений - привело к образованию самостоятельного раздела математической логики, называемого суперинтуиционистскими пропозициональными логиками.
Интуиционистское пропозициональное исчисление, задуманное как формализация интуиционистского математического обращения с высказываниями, в процесе изучения меняло свою форму задания и в настоящее время имеется несколько различных способов его построения. В
диссертации будет задействован только однин из них , использующий аксиомы и два правила вывода: подстановка и модус поненс ( modus ponens ) [32]. Построенное таким способом интуиционистское пропозициональное исчисление в дальнейшем будем обозначать через Н , а суперинтуиционистское пропозициональное исчисление , получающееся из интуиционистского путем добавления к нему конечного множества аксиом эе , называемых его дополнительными аксиомами, - через Н+ж. Среди них оказалось и классическое пропозициональное исчисление, для построения которого достаточно одной дополнительной аксиомы, выражающей, например, закон исключенного третьего или снятия двойного отрицания. В процессе изучения этих исчислений менялось первоначальное соотношение между логикой и исчислением и теперь суперинтуиционистской пропозициональной логикой называют множество пропозициональных формул , содержащее все аксиомы Н и замкнутое относительно правила подстановки и правила модус поненс.
Для задания этих логик чаще всего используются исчисления и псевдобулевы алгебры [35]. На каждой псевдобулевой алгебре можно вычислить значение данной пропозициональной формулы для данных значений ее переменных , причем логические знаки интерпретируются соответствующими операциями этой алгебры. Если на рассматриваемой алгебре при любых значениях переменных какой-либо формулы ее значение является выделенным элементом этой алгебры , то она называется верной ( общезначимой ) на ней. Множество пропозициональных формул, верных на какой-нибудь псевдобулевой алгебре в или выводимых в каком-либо исчислении Н+эе , является суперинтуиционистской пропозициональной логикой, которую будем обозначать через а(8) или с(зе). Чтобы подчеркнуть способ ее задания , эту логику часто называют логикой , порожденной алгеброй в или формулами из х. Логика, порожденная некоторой конечной псевдобулевой алгеброй , называется табличной.
В настоящее время суперинтуиционистские пропозициональные исчисления находят важные применения и в теоретической информатке. Например, они используются в задачах декларативного синтеза программ и автоматического доказательства теорем. Многие проблемы как теоретического так и прикладного характера сводятся к поиску вывода в рассматриваемых исчислениях. Часто искать вывод данной формулы приходится не во всем исчислении , а в некотором его фрагменте, заранее зная о ее выводимости в самом исчислении. Существование
формул, невыводимых в изучаемом фрагменте исчисления, но выводимых в самом исчислении , делает этот поиск иногда безуспешным. Чтобы всегда надеятся на успех , нужно для каждого фрагмента рассматриваемого исчисления убедиться в отсутствии таких формул, что по сути дела есть отделимость этого исчисления. Желательно иметь и алгоритмы, распознающие только что обозначенное свойство исчислений.
Понятие отделимости исчисления сформировалось в математической логике и играет важную роль в изучении свойств суперинтуицио-нистских пропозициональных исчислений. Его появление обусловлено возникшей к тому времени в математической логике необходимостью в нем , имевшей идейную основу. Ее суть состоит в том, что в математике при доказательстве теорем часто интересуются теми логическими средствами, с помощью которых они получены. Для удобства изучения этих средств желательно формализовать их так , чтобы они фигурировали явным образом, а не выраженными через другие средства, т.е. в отделенном друг от друга виде. Эта идея была реализована при построении и сравнении различных аксиоматик интуиционистского пропозиционального исчисления. Его аксиомы, выражающие интуиционистскую суть логических пропозициональных связок , были построены отдельно для каждой связки , содержали ее саму и импликацию и позволяли устраивать выводы в нем так , что формулы рассматриваемого вывода содержат лишь импликацию и логические связки, входящие в выводимую формулу. Чтобы фиксировать эту ситуацию, и было введено понятие отделимого исчисления.
Суперинтуиционистское пропозициональное исчисление называется отделимым , если оно удовлетворяет следующим двум условиям:
-
каждая из его аксиом содержит не более двух логических знаков, один из которых - импликация;
-
для любой выводимой в этом исчислении формулы Q существует ее вывод в нем, формулы которого не содержат логических знаков, отличных от импликации и знаков формулы Q.
Естественным образом это понятие'распространяется и на суперинтуиционистские пропозициональные логики. Рассматриваемая логика - отделима , если существует ее отделимая аксиоматизация , т.е. отделимое исчисление , в котором выводимы все ее формулы и только они.
Понятие отделимости исчисления тесно связано с понятием консервативности расширения формальной системы , встречающимся в
исследованиях по математической логике и теоретической информатике , а наличие отделимости у какого-нибудь исчисления позволяет изучать его фрагменты без потери их формул , выводимых в самом исчислении.
Таким образом, при изучении суперинтуиционистских пропозициональных исчислений и логик одно из центральных мест занимает проблема отделимости этих исчислений , т.е. проблема построения по рассматриваемому исчислению отделимого исчисления , равнообъмного исходному , т.е. имеющего то же самое множество выводимых формул что и исходное.
Многие суперинтуиционистские пропозициональные логики ( например, логики , порожденные формулами , не содержащими дизъюнкции или допускающими ее элиминирование ) могут быть заданы исчислениями, дополнительные аксиомы которых не содержат логических знаков, отличных от импликации и отрицания. Поэтому решение вопроса об отделимости этих логик сводится к проблеме отделимости таких исчислений, с ней тесно связаны и некоторые проблемы , сформулированные Хоси и Оно в работе [27J. В дальнейшем класс этих исчислений будем обозначать через К..
Цель работы. Основные цели предлагаемого исследования состоят в разработке некоторого алгебраического аппарата и в применении его для получения критериев отделимости исчислений из С и решениия проблемы ( проблемы 1 ) построения по исчислению из К равнообъмного с ним и отделимого исчисления и проблемы ( проблемы 2 ) построения алгоритма , распознающего отделимые исчисления среди исчислений класса К.
Научная новизна . Неявным образом идея отделимости и доказа-тельство отделимости интуиционистской пропозициональной логики содержится в теореме Генцена о нормальной форме выводов в исчислениях [15] , опубликованной в 1934-35 годах . Понятие отделимости исчисления ввел Вайсберг и в явной форме доказал отделимость некоторой аксиоматизации интуиционистской пропозициональной логики [37] в 1938 году, однако его доказательство содержало пробел [10, стр.399] , который впоследствии устраняли Кабзинский и Поребска [30,31] , а также Циткин [4]. В 1939 году такой же результат получил Карри [11] как следствие теоремы Генцена , а в 1952 году -Клини [32,стр.406] тем же что и Карри методом , ссылаясь, на работу [11] . Там же [32] содержится и доказательство отделимости класси-
ческой пропозициональной логики . В 1962 году Хорн [19] доказал отделимость интуиционистской пропозициональной логики алгебраическим методом.
Продолжением этих исследований были опубликованные в 1966-67 годах работы Хосои , в которых доказана отделимость классической пропозициональной логики [20,21] алгебраическим методом и логик «(/О , порожденных конечными и счетной линейно упорядоченными псевдобулевыми алгебрами Лд (п=2,...,ю) [22-25]. Для удобства изложения этих результатов он ввел [221 понятие ^-полноты суперинтуиционистского пропозиционального исчисления, где v - набор логических пропозициональных знаков , содержащий =. Исчисление Н+зе называется ^-полным, если для каждой ^-формулы ( т.е. формулы, не содержащей логических знаков , отличных от знаков набора ^ ) , выводимой в Н+х , существует ее вывод в Н+зе , состоящий только из ^и{э}-формул. Это понятие неявным образом содержится в [19], является частью понятия отделимости исчисления и фигурирует практически во всех работах , посвященных отделимости суперинтуиционистских пропозициональных исчислений и логик.
В 1968 Мак-Кей [33] доказал неотделимость логики R( ((-nq=q)= = (qviq))3(-nqv-iq}) , где q - пропозициональная переменная, тем самым впервые построил пример неотделимой логики. Неотделимость состоит в невозможности задать ее исчислением, удовлетворяющим условию 1) из определения отделимости. Чтобы констатировать наличие или отсутствие этого факта он ввел понятия нормального исчисления и нормализуемой логики. Исчисление называется нормальным, если оно удовлетворяет условию 1) из определения отделимости , т.е. каждая из его аксиом содержит не более двух логических знаков , один из которых импликация. Логика называется нормализуемой , если существует нормальное исчисление , в котором выводимы все ее формулы и только они.
В работе СЗЗ] было начато , в [29] продолжено и в [41,42,48] закончено изучение проблемы отделимости логик, порожденных формулами в одной переменной. В результате чего для конечного числа логик была доказана их отделимость, а остальные оказались ненорма-лизуемыми и, следовательно, неотделимыми. Ненормализуемые логики были обнаружены и среди табличных [29,41,42] , т.е. логик , порожденных конечными псевдобулевыми алгебрами. К обсуждаемым выше работам следует добавить еще и опубликованные в 70-ые годы работы
[26,28,401 , в которых доказана отделимость суперинтуиционистских пропозициональных логик из нескольких достаточно широких классов. Среди обсуждаемых результатов автор диссертации обнаружил [44] и ошибочные [33,26].
Отделимость логик «(Лп) Хосои получил [22] как следствие из доказанного им в [221 другого результата , дающего достаточное условие для отделимости исчислений H+2J, где 2) - конечное множество о-формул. Это условие немного изменено в [24] и окончательно формулируется так. Исчисление H+2J отделимо , если оно удовлетворяет двум условиям: 1) исчисление H+2J ^-полное; 2) существуют построенные из переменных q и w о-формулы (^,...,CL такие, что ^-формулы (^3(.., = (Q^3(qvw))...) и (qvwJ^Q^ (Кісп) выводимы в H+3J, т.е. в Н+э дизъюнкция выражается через импликацию. Высказав предположение, что условие 2) в этом утверждении может быть избыточным, Хосои ставит вопрос: будет ли 1) необходимым и достаточным условием для отделимости исчисления Н+э ? Мак-Кей [33] построил отделимое исчисление , в котором дополнительные аксиомы - э-формулы , но условие 2) не выполнено. Утвердительный ответ на поставленный Хосои вопрос дан автором в [38,39] ( теорема 2.13 главы II диссертации ). Опустить и условие 1) , т.е. утверждать , что для любого конечного множества ^-формул зе исчисление Н+эе отделимо , нельзя, так как среди них существуют исчисления , не являющиеся э-ПОЛНЫМИ [34,41].
В работах [38,39] автором было введено свойство пропозициональных формул е. Формула Q обладает свойством <з, если для каждой переменной q, входящей в Q, формула Q=> (Fiji LQj =FJj& t LQj) выводима в Н, где t - пропозициональная переменная, отличная от q и не входящая в Q, a P^LQj и FJLtiQj - результаты подстановок соответственно t и qfiet вместо q в Q . Там же [38,39] с помощью этого свойства автором было получено'условие , достаточное для отделимости исчислений, т.е. было доказано, что если э-формулы из эе обладают свойством @, то исчисление Н+эе отделимо ( теорема 2.15 главы II диссертации ); однако обратное ему утверждение неверно [441. Для многих формул сравнительно легко удается доказать , что они обладают свойством @ и тем самым установить отделимость исчислений , дополнительными аксиомами которых будут эти формулы [38,39,41,42,8].
Обсуждаемые выше результаты оказались малопригодными для решения проблемы 1, т.е. проблемы построения по исчислению из К рав-
ноооъмного с ним и отделимого исчисления. Искомое построение автор предложил проводить в два этапа.
На первом этапе для рассматриваемого исчисления сначала строим самые сильные по выводимости в Н ^-формулы , выводимые в самом исчислении , но не выводимые в нем без дополнительных аксиом , содержащих отрицание, а затем добавляем их к списку аксиом изучаемого исчисления , получая тем самым новое исчисление , равнообъемное исходному. Чтобы контролировать процесс построения таких формул, констатировать их отсутствие и зафиксировать этот этап,для каждого набора логических пропозициональных знаков ^, не содержащего отрицания , автор ввел свойство исчислений vv [44]. Так как оно представляет и самостоятельный интерес , то для полноты и удобства изложения материала в диссертации мы определили его для любого набора v.
Будем говорить , что исчисление Н+эе обладает свойством vv , если каждая выводимая в Н+эе ^-формула выводима и в исчислении H+3C^v& ' где x=>v& ~ подин031600 всех =>у&-формул множества х.
На втором этапе по исчислению , полученному на первом этапе, строим равнообъемное с ним исчисление с полными фрагментами, заменяя в исходном дополнительные аксиомы новыми аксиомами. С целью, аналогичной той, которая определила введение на первом этапе свойства уи , на втором этапе для каждого набора логических пропозициональных знаков v, содержащего => , автор ввел свойство исчислений сгу [44] , составившее вместе со свойством vv основу критериев v-полноты и отделимости исчислений из К. Для удобства обращения с ним в диссертации оно фигурирует в измененном виде.Будем говорить, что исчисление Н+х из К обладает свойством
то исчисление Н+зе будет обладать свойством
Отделимость нормальных исчислений согласно ее определению равносильна их ^-полноте при любом наборе ^. Так как исчисления из класса К являются нормальными , то сначала автором были получены критерии ^-полноты исчислений из [44]. В результате чего все наборы v разделились на четыре группы: для v из первой группы исчисления из К. являются ^-полными; для \> из второй группы У-ПОЛНО-та исчисления из С эквивалентна наличию у него свойства 4>v; для v из третьей группы - наличию у него свойства <г^; для » из четвертой группы - наличию у него свойств vu и &v ( леммы 2.13, 2.14, 2.22 и 2.24 главы II диссертации ). С помощью этих результатов автором получен критерий отделимости исчислений из класса К [44], согласно которому отделимость такого исчисления равносильна наличию у него свойств &э , сг и >DV ( теорема 2.18 главы II диссертации ). Для подкласса исчислений К^СН+зеї* - множество ^-формул) класса К. эти результаты значительно упрощаются [44]. Все наборы v делятся только на две группы , одну из которых составляет первая и вторая , а другую - третья и четвертая. В формулировке критерия отделимости исчислений из j фигурирует только свойство сс= , а именно отделимость исчисления из К^ равносильна наличии у него свойства ^ ( теорема 2.19 главы II диссертации ).
Согласно этому критерию изучение отделимости исчислений из К, можно заменить изучением более простых свойств 4>v и
Положительно решена [50,54] проблема 1.1 для подклассов ис-исчислений x;1+2={H+3eU{R1>} (1=0,1 ) класса К. , где эе - конечное множество =>-формул, Rg=(-iq=>t)=((mqr>t)=t) и R1 = (inq=t)=(( (nnq=q)= =>t);>t) ( q и t - пропозициональные переменные , а формулы RQ и R1
дедуктивно равны в Н соответственно формулам -iqv-nq и -nqv(-nq=q)) Иначе говоря , доказано , что по любому исчислению из .+2 можно построить равнообъемное с ним исчисление из 1+2 , обладающее свойствами vv (lev) ( теорема 2.24 главы II диссертации ).
По проблеме 1.2 получен более сильный результат, чем ее положительное решение [481: доказано, что по любому исчислению из Е можно построить равнообъемное с ним исчисление из Е , обладающее свойствами &и (=*^), сохраняя при этом свойства ч\, ( теорема 2.20 главы II диссертации ). Одним из основных достоинств этого результата является возможность сохранять свойства yv при перестраивании рассматриваемых исчислений , что позволяет беспрепятственно использовать его для решения проблемы 1. С помощью этого результата и сформулированного выше критерия она условно решена [46,481, а именно доказано, что по любому исчислению из Е , обладающему свойством уэЧ , можно построить равнообъемное с ним и отделимое исчисление ( теорема 2.25 главы II диссертации ).
Этот результат сводит решение проблемы 1 к проблеме 1.1. Более того , из него следует положительное решение проблемы 1 для исчислений из Е, , Eg и Eg [46,48,50,541 , так как для исчислений из С1 свойство 5>з7 выполнено тривиальным образом, а для исчислений из Eg и *-з ~ в силу положительного решения проблемы 1.1 ( теоремы 2.26 и 2.27 главы II диссертации ).
Из последних результатов вытекает отделимость многих суперин-туиционистских пропозициональных логик. Логика а(3)) , порожденная конечным подмножеством э множества фомул (Х|Х дедуктивно равна в Н Х^.-.&Хд , где X1=R1, или X^Rq, или Xj - =>~формула }, может быть задана исчислением из Е1, или Eg, или Eg и поэтому отделима ( теорема 2.28 главы II диссертации ). Если логика нормализуема и множество ее позитивных формул совпадает с множеством позитивных формул интуиционстской пропозициональной логики , то оно может быть задана исчислением из Е, обладающим свойством гр=у ,'и следовательно , отделима ( следствие 2.16 главы II диссертации ). Этот результат является исправлением леммы 5.2 работы [281. Также отметим, что следствия, вытекающие из теоремы 2.25 диссертации , перекрывают практически все полученные другими специалистами результаты по проблеме отделимости суперинтуиционистских пропозициональных исчислений и логик.
Как было отмечено выше , в диссертации рассматриватся еще и
проблема 2 , т.е. проблема построения алгоритма, распознающего отделимые исчисления среди исчислений класса К. Согласно полученному критерию , для ее положительного решения достаточно построить алгоритмы, проверяющие наличие свойств Фэу , «^ и <б= у исчислений из К. Для свойства &и при v, не содержащем v, существование такого алгоритма следует из отделимости интуиционистской пропозициональной логики [37,19] и теоремы Попеля-Диего [13,61. Автору удалось доказать существование алгоритмов , проверяющих наличие свойства vv при ^ , не содержащем -і , у исчислений из 2 , 3 и С4=Ш+эе|х - множество =п-формул, не являющихся э-формулами) [45, 54,441 ( теорема 2.29 главы II диссертации ). В результате им положительно решена проблема 2 для классов исчислений К* ( 1=1,2,3, 4 ) [43-45,54] ( теорема 2.30 главы II диссертации ).
Для доказательства уже перечисленных результатов по проблемам 1 и 2 используется возможность разложения пропозициональных формул на характеристические пропозициональные формулы , что позволяет сузить изучаемый класс исчислений , рассматривая только те, у которых дополнительные аксиомы - характеристические формулы , при этом сохраняя общность получаемых результатов.
Понятие характеристической формулы было введено в работе [51 для конечной геделевой псевдобулевой алгебры , т.е. алгебры, у выделенного элемента которой имеется единственный непосредственный предшественник. В работе [б] оно было распространено на конечные геделевы v-алгебры , в которых определена операция пересечения, а в работе [481 - на любые конечные геделевы ^-алгебры. - Понятие f-алгебры , введеное в [19] для изучения фрагментов исчисления Н, явилось обобщением таких уже известных под другими названиями понятий , как импликативная полуструктура, импликативная структура и псевдобулева алгебра, история которых изложена в [12,35]. По сути дела , ^-алгебра - это множество, на котором заданы операции псевдобулевой алгебры, определяемые набором логических пропозициональных знаков v и включающие операцию относительного псевдодополнения. При к, содержащем все четыре знака, ^-алгебра будет псевдобулевой алгеброй. Для удобства изложения материала операции ^-алгебр будем обозначать так же , как и интерпретируемые ими логические пропозициональные связки. Знаки =>, &, v и л будут обозначать соответственно операции относительного псевдодополнения ."пересечения, объединения и псевдодополнения. Это не приведет к путанице , так
как из контекста будет ясен смысл применения знака . Дадим определение характеристической формулы.
Пусть и - какой-нибудь набор логических пропозициональных
знаков,содержащий =>, а 8 - какая-либо конечная геделева ^-алгебра.
Каждому элементу і множества 9 поставим в соответствие пропозицио
нальную переменную q,, причем различным элементам 6 сопоставляются
различные переменные. Если -леи , то положим
UCq^oiq^^e). Положим «(e.oMfq^oq^qg |g,T)ee}U{qg :>
= (qeoq )|,т)є8} и »(6,K)={q1}Ucyi<4J(e,D)', где о - символ из iA{-i),
а 1 - выделенный элемент 9 . По Є построим характеристическую фор
мулу Хд , положив ^=(^=(...^(Q^qy)...) , где Q1 С^ - все
элементы множества 3(8,^) , а ш - единственный непосредственный предшественник выделенного элемента 8.
Для изложения результатов , связанных с разложением пропози Для каждого набора v , содержащего = , заданное на множестве Характеристические формулы для конечных ^-алгебр и только они являются неразложимыми в "8V ^-формулами [6,48]. Точнее говоря, любая не выводимая в Н ^-формула Р не разложима в # тогда и только тогда, когда Pt"x для некоторой конечной ге де левой v-алгебры Ф. Более того, Xq1vX^ в том и только том случае, когда ^-алгебры 8 и Ф изоморфны [6,48]. При изучении разложимости v-формул в "sv возникают вопросы о возможности и однозначности их разложения на характеристические ( неразложимые ) формулы и о связи разлагаемой фор- мулы с множеством ^-алгебр, задающим такое ее разложение. Частично ответы на эти вопросы автором получены в работах [48,54]. Во-первых, доказано, что если v«v, то для любой не выводимой в Н ^-фор-мулы Q существуют неизоморфные друг с другом конечные геделевы у-алгебры .,...,3) такие, что Хщ ,...,х fl^Q ( теорема 2.7 гла- *1 п вы II диссертации ). Во-вторых , оказалось , что такое разложение однозначно с точностью до дедуктивного равенства ^-формул в Н , а множество ^-алгебр, задающее его, состоит из тех и только тех конечных геделевых ^-алгебр , на которых Q предельно опровержима ( теоремы 2.8, 2.9 и 2.10 главы II диссертации ) . Ценным является и то , что процесс построения по v-формуле Q ее разложения х ,..., и v-алгебр Ф*,...,* , задающих это разложение, можно осуществить алгоритмически. Согласно определению характеристической формулы в ней зашифрована структура представляемой ею ^-алгебры. Более того, выводимость в Н ^-формулы х из v-формулы Хд (т.е. Хд^Х^ ) равносильна изоморфной вложимости v-алгебры в в некоторый гомоморфный образ v-алгебры Ф [6,48]. Этот результат вместе с возможностью разлагать в зу некоторые ^-формулы на характеристические формулы позволяют сводить решения многих вопросов , касающихся выводимости формул в Н , к вопросам , связанным с вложимостью ^-алгебр друг в друга, что используется при решении проблем 1 и 2. Поэтому естественным образом возникает необходимость изучения к-алгебр и в особенности изоморфной вложимости их друг в друга. При различных ^ классы конечных v-алгебр, в которых определена операция пересечения, следующим образом соотносятся друг с другом. На каждой конечной "--алгебре можно задать недостающие операции , сделав ее м-алгеброй , где v - набор логических пропозициональных знаков, включающий и, а каждая такая ^-алгебра по определению является и v-алгеброй. Тем самым , изучая какой-нибудь из этих классов , например, класс конечных э&-алгебр ( импликативных полуструктур ), мы в той или иной мере изучаем и все остальные. Достаточно очевидно , что доказывать изоморфную вложимость ^-алгебр друг в друга , исходя непосредстенно из ее определения, дело малоперспективное. Для этой цели желательно использовать представления и-алгебр через объекты более простой структуры. В работах (47-49,51-561 автором предложено и детально разработано представление конечных ^-алгебр, в которых определена операция пе- ресечения, через ^-алгебры ( импликатуры ) специального вида или частично упорядоченные множества , имеющие наибольший элемент. Его суть заключается в том , что каждая такая ^-алгебра однозначно с точностью до изоморфизма определяется множеством ее неразложимых в пересечение элементов. Это множество является как э-алгеброй, удовлетворяющей некоторому условию , так и частично упорядоченным множеством с наибольшим элементом, которые легко превращаются друг в друга. При таком подходе как представляемые ^-алгебры , так и представляющие их з-алгебры суть объекты одной и той же природы, что облегчает изучение ^-алгебр. Понятие неразложимого в пересечение элемента в структурах [7] в работе (63 было распространено на импликативные полуструктуры, а в [51) - на любые v-алгебры. Элемент ^-алгебры 6 назовем неразложимым элементом 9 , если из соотношений Т1,ф<=8 , =>т)=1 . =(р=1 и тр((р)=1, где 1 - выделенный элемент 9, следует, ЧТО =Т) или С=Ф-В каждой ^-алгебре 8 множество 1(8) всех ее неразложимых элементов замкнуто относительно операции относительного псевдодополнения и тем самым является ее ^-подалгеброй , удовлетворяющей следующему условию: для любых g и т? из-1(9) в 1(9) верно хотя бы одно из равенств =17=77 или g=nrj=l [47,48,51] ( лемма 1.2 главы I диссертации ). Для любой ^-алгебры Ф это условие эквивалентно такому условию: 1(Ф)=Ф ( следствие 1.2 главы I'диссертации ). Оператор I множество я1 конечных =&-алгебр отображает в множество з ={3|S -конечная =>-алгебра и I(2)=S) , сохраняя при этом свойство геделе-вости и отношения гомоморфности и изоморфности [47,48] ( теоремы 1.1 и 1.2 главы I диссертации ). Более того, для каждой ^-алгебры Ф из з1 в я существует единственная с точностью до изоморфизма =&-алгебра в такая , что э-алгебры 1(8) и Ф изоморфны [47,48,56] ( теорема 1.4 главы I диссертации ). Поэтому I является взаимно однозначным отображением из я на з . Устанавливается связь оператора I с прямым произведением ^-алгебр [551 ( теорема 1.3 главы I диссертации ) и сравниваются два метода построения псевдобулевых алгебр по частично упорядоченным множествам [56], один из которых, предложенный автором в работе [561 , основан на операторе I , а другой, применяемый в работе [3] , использует топологические понятия ( теорема 1.13 главы I диссертации ). Для выяснения изоморфной вложимости к-алгебр друг в друга в работах [48,55] автором предложены критерии, использующие оператор I. Конечная ^-алгебра Ф вложима в конечную у-алгебру 6, на которой определена операция пересечения и операции, заданные на Ф, тогда и только тогда, когда существует вложение э-алгебры І(Ш) в е, удовлетворяющее некоторым условиям ( теорема 1.5 главы I диссертации ). Их характер пороадает четыре случая и в каждом из них получаем критерий влозкимости для соответствующих ^-алгебр. Например, конечная =>&-алгебра 3 вложима в конечную =&-алгебру Ф в том и только том случае , когда =>-алгебра 1(5) вложима в Ф ( следствие 1.15 главы I диссертации ). Поэтому из вложимости э-алгебры 1(3) в э-алгебру 1(Ф) следует влокимость конечной =>8с-алгеСры S в конечную э&-алгебру Ф ( следствие 1.20 главы I диссертации ). Однако обратное утверждение неверно [48]. Вместе с тем , для каждой конечной э&-алгебры 3 существует конечное множество =-алгвбр из з , содержащее э-алгеОру 1(3), такое, что =>&-алгебра 3 вложима в конечную =&-алгебру Ф тогда и только тогда , когда некоторая з-алгебра из этого множества вложима в =>-алгебру 1(ф) [47] ( теорема 1.7 главы I диссертации ). Такой же результат имеет место и для конечных геделевых =>&-алгебр [481 ( теорема 1.8 главы I диссертации ). Доказательства последних двух результатов являются громоздкими и технически трудными , так как в них реализуется значительная часть предлагаемого автором метода доказательства отделимости исчислений. Именно они непосредственно используются при решении проблемы 1.2 и дают возможность перестроить исчисление из С так, чтобы оно обладало свойством <_, . Но, чтобы перестроенное исчисление обладало еще и свойством Таким образом , оператор N взаимно однозначно отображает множество sr^ конечных =п&-алгебр на множество 3i1={S|S - конечная =п-алгеСра и N(S)=3> , сохраняя при этом свойство геделевости и отношения гомоморфное и изоморфности. На основе его формулируются критерии вложимости =п&-алгебр друг в друга. Конечная =п&-ал-гебра Ф вложима в конечную =-і&-алгебру Є в том и только том случае, когда з-1-алгеОра N(3>) вложима в в [48,49] ( лемма 1.36 главы I диссертации ). Поэтому из вложимости эп-алгебры N(ffi) в =н-алгеб-ру N(9) следует вложимость конечной =п&-алгеСры Ф в конечную эп&-алгебру в [48] ( следствие 1.29 главы I диссертации ). Однако обратное утверждение неверно [48]. Вместе с тем, для каждой конечной э!&-алгебры Ф существует конечное множество =п-алгебр из эг , содержащее э-1-алгебру N(ffi), такое , что з-і&-алгебра Ф вложима в конечную =п&-алгебру 8 тогда и только тогда , когда некоторая =п-алгебра из этого множества вложима в =п-алгебру N(6) [49] ( теорема 1.11 главы I диссертации ). Такой же результат имеет место и для конечных геделевых =п&-алгебр [48] ( теорема 1.12 главы I диссертации ). Как было отмечено выше, последние два результата тоже используются при решении проблемы 1.2. В работе [48] автором установлена связь оператора N с оператором I. Оказывается , что для любой конечной эп&-алгебры в справедливы равенства N(N(6))=N(6) и I(N(6))=I(6) ( следствие 1.24 главы I диссертации ). Результаты применения к каким-нибудь двум конечным =п-алгебрам операторов I и N одновременно связаны отношениями гомоморфности и изоморфности независимо от того , удовлетворяют ли им исходные зп-алгебры ( леммы 1.32 и 1.33 главы I диссертации ). Отметим , что такая согласованность будет , т.е. сами алгебры и результаты применения к ним операторов I и N одновременно связаны этими отношениями, если рассматривать конечные =-і&-ал-, гебры. Как было отмечено выше, каждую конечную ^-алгебру, в которой задана операция пересечения, можно сделать псевдобулевой алгеброй, определив на ней недостающие операции. Осуществить такое же преобразование над любой конечной ^-алгеброй, вообще говоря, невозможно. Однако она вложима в некоторую конечную псевдобулеву алгебру [561 ( теорема 1.6 главы I диссертации ). Таким оброзом, множество конечных ^-алгебр состоит только из v-подалгебр конечных псевдобулевых алгебр. Методы исследований . Методы изучения суперинтуиционистских пропозициональных логик и исчислений условно можно разбить на дедуктивные и алгебраические . Многие как те так и другие по своей идейной основе различны . Для проблемы отделимости этих логик и исчислений почти все метода исследований используют идею приведения виводов к нормальной форме в исчислениях секвенций Генцена путем устранения в них сечения или идею изоморфной вложимости ^-алгебр в псевдобулевы алгебры. Приемы реализации этих идей в виде методов сильно зависят от рассматриваемого исчисления и поэтому эти методы не могут быть достаточно общими. В диссертации исследования основываются на разложении в Н пропозициональных формул на характеристические пропозициональные формулы, на моделировании по выводимости в Н к-алгебр и на представлении конечных ^-алгебр через э-алгебры. Характерной чертой этого представления является то, что как представляемые у-алгебры, так и представляющие их э-алгебры суть объекты одной и той же природы. Более того, представляющая ^-алгебра изоморфно вложима в представляемую ею ^-алгебру. Именно эти обстоятельства делают его главной составляющей предложенного автором метода решения проблемы отделимости исчислений из 1С. Согласно ему построение по исчислению из К отделимого и равнообъемного исходному исчисления проводится по такой схеме. Сначала по рассматриваемому исчислению путем разложения его дополнительных аксиом на характеристические пропозициональные формулы получаем равнообъемное данному исчисление из К, сохраняя при этом нужные нам свойства исчислений. Затем, используя представление конечных ^-алгебр , в два этапа строим отделимое и равнообъемное исходному исчисление. На этих этапах применяем еще и моделирование по выводимости в Н ^-алгебр, а также некоторые другие приемы, характерные для таких исследований. Отметим, что результаты, полученные с помощью этого метода, перекрывают практически все полученные другими методами результаты по проблеме отделимости суперинтуиционистских пропозициональных исчислений и логик. Это дает основание считать его самым общим по своим возможностям среди методов , применяемых при изучении только что упомянутой проблемы. Теоретическая и практическая ценность. Результаты диссертации являются новыми и вносят значительный вклад в исследования по математической логике и теоретической информатике . Ее результаты по проблеме отделимости суперинтуиционистских пропозициональных исчислений и логик перекрывают практически все полученные другими специалистами результаты по этой проблеме . Они могут быть исполь- зованы при дальнейших исследованиях в этих областях. Все выносимые на защиту результаты получены автором лично. Апробация . Результаты диссертации излагались на 6 и 8 Ме'жду-народных конгрессах по логике , методологии и философии науки (Ганновер, 1979.и Москва, 1987) , на IV, V, VI, VII, IX и X Всесоюзных конференциях по математической логике (Кишинев, 1976, Новосибирск, 1979 , Тбилиси, 1982 , Новосибирск, 1984 , Ленинград, 1988 и Алма-Ата, 1990) , на 18 Всесоюзной алгебраической конференции (Кишинев, 1985) , на I Всероссийской школе по основаниям математики и теории функций (Саратов," 1989) , на научно-исследовательском семинаре по математической логике кафедры математической логики МГУ под руководством члена-корреспондента РАН С.И.Адяна и профессора В.А.Успенского (1989,1994) , на семинаре лаборатории математической логики ПОМИ под руководством д.ф.-м.н. Ю.В.Матия-севича (1993) , на семинаре "Основания математики и информатика" ВЦ РАН под руководством к.ф.-м.н. Н.М.Нагорного (1989), а'также на некоторых других конференциях и семинарах. Публикации . Результаты диссертации опубликованы в 19 работах [38-56К Структура и объем работы . Диссертация состоит из введения, двух глав, заключения и списка литературы. Первая глава разбита на 9 параграфов, вторая - на 8 . Объем работы 258 страниц , включая 7 страниц цитированной литературы . В списке литературы 65 наименований.
циональных формул на характеристические формулы , введем следующие
обозначения. Выражение Р1,.,.,Р l-^Q будет означать, что ^-формула
Q ^-выводима в Н из v-формул P1F...,P с помощью правила модус
поненс и правила подстановки , а выражение Р1,... .P^Q - что
Р, РпГ0 и Q№± (fCL
всех ^-формул 3„ отношение P^Q является рефлексивным и транзитив
ным , но неантисимметричным ( т.е. не согласованным с графическим
равенством формул ) отношением 135] , которое часто называют отно
шением частичного квазипорядка. Если &<=i> , то ъи можно сделать [6]
дистрибутивной структурой [7,12,35]. Понятие неразложимого в пере
сечение элемента структуры следующим образом распространяется и на
множество #v . Будем говорить, что ч-фррмула Р не разложима в "Sv ,
если из соотношений Q.Se^y и Q.SI^P следует, что QfyP или SfvP.
Естественным образом ^-формулу Q назовем разложимой в yv на
^-формулы Р1,...,Р11 , если Р1 рп^а"
*1 п "