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

РГб од

2 9 МАЙ 1995

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

Хомич Валентин Иванович

ПРОБЛЕМА ОТДЕЛИМОСТИ В ПРОПОЗИЦИОНАЛЬНЫХ ИСЧИСЛЕНИЯХ

05.13.17 - теоретические основы информатики

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора физико-математических, наук

Москва - 1995

Работа выполнена в Вычислительном центре Российской Академии наук

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

профессор Абрамов С.А., доктор физико-математических наук, доцент Максимова Л.Л., доктор физико-математических наук, старший научный сотрудник Марченков G.G.

Ведущая организация: Красноярский Государственный университет

Защита состоится " ß S " UM?l4iv 1995 года в1££^асов на заседании диссертационного совета Д002.32.06 при Вычислительном центре РАН по адресу:

117967, Москва, ГСП-1, ул. Вавилова 40, конференц-зал

С диссертацией можно ознакомиться в библиотеке МИ РАН

Автореферат разослан " ,/fy/Q X, 1995 года

Ученый секретарь

диссертационного совета Д002.32.06 кандидат физико-математических наук

0/Ül§>OfjJ Тартан G.M.

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

Логические исчисления, преимущественно с интуиционистской основой, используются и в задачах декларативного синтеза программ. В синтезирующих системах искомый алгоритм извлекается из вывода в выбранном исчислении спецификации решаемой задачи из базы знаний рассматриваемой системы [1]. Возможность такого подхода обеспечивается наличием логических исчислений , имеющих конструктивную семантику типа реализуемости 132,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]. На каждой псевдобулевой алгебре можно вычислить значение данной пропозициональной формулы для данных значений ее переменных , причем логические знаки интерпретируются соответствующими операциями этой алгебры. Если на рассматриваемой алгебре при любых значениях переменных какой-либо формулы ее значение является выделенным элементом этой алгебры , то она называется верной ( общезначимой ) на ней. Множество пропозициональных формул, верных на какой-нибудь псевдобулевой алгебре в или выводимых в каком-либо исчислении Н+эе , является суперинтуиционистской пропозициональной логикой, которую будем обозначать через z(B) или с(зе). Чтобы подчеркнуть способ ее задания , эту логику часто называют логикой , поровденной алгеброй в или формулами из х. Логика, порожденная некоторой конечной псевдобулевой алгеброй , называется табличной.

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

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

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

Суперинтуиционистское пропозициональное исчисление называется отделимым , если оно удовлетворяет следующим двум условиям:

1) кавдая из его аксиом содержит не более двух логических знаков, один из которых - импликация;

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

Естественным образом это понятие'распространяется и на суперинтуиционистские пропозициональные логики. Рассматриваемая логика - отделима , если существует ее отделимая аксиоматизация , т.е. отделимое исчисление , в котором выводимы все ее формулы и только они.

Понятие отделимости исчисления тесно связано с понятием консервативности расширения формальной системы , встречающимся в

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

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

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

Цель работы. Основные цели предлагаемого исследования состоят в разработке некоторого алгебраического аппарата и в применении его для получения критериев отделимости исчислений из С и решениия проблемы ( проблемы 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]. Для удобства изложения этих результатов он ввел [22] понятие ^-полноты суперинтуиционистского пропозиционального исчисления, где к - набор логических пропозициональных знаков , содержащий =>. Исчисление Н+зе называется ^-полным, если для каждой ^-формулы ( т.е. формулы, не содержащей логических знаков , отличных от знаков набора ^ ) , выводимой в Н+х , существует ее вывод в Н+зе , состоящий только из ^и{э}-формул. Это понятие неявным образом содержится в [19], является частью понятия отделимости исчисления и фигурирует практически во всех работах , посвященных отделимости суперинтуиционистских пропозициональных исчислений и логик.

В 1968 Мак-Кей [33] доказал неотделимость логики = , где q - пропозициональная переменная, тем са-

мым впервые построил пример неотделимой логики. Неотделимость состоит в невозможности задать ее исчислением, удовлетворяющим условию 1) из определения отделимости. Чтобы констатировать наличие или отсутствие этого факта он ввел понятия нормального исчисления и нормализуемой логики. Исчисление называется нормальным, если оно удовлетворяет условию 1) из определения отделимости , т.е. каждая из его аксиом содержит не более двух логических знаков , один из которых импликация. Логика называется нормализуемой , если существует нормальное исчисление , в котором выводимы все ее формулы и только они.

В работе СЗЗ] было начато , в [29] продолжено и в [41,42,48] закончено изучение проблемы отделимости логик, порожденных формулами в одной переменной. В результате чего для конечного числа логик была доказана их. отделимость, а остальные оказались ненорма-лизуемыми и, следовательно, неотделимыми. Ненормализуемые логики были обнаружены и среди табличных [29,41,42] , т.е. логик , порок-денных конечными псевдобулевыми алгебрами. К обсуждаемым вше работам следует добавить еще и опубликованные в 70-ые годы работы

[26,28,401 , в которых доказана отделимость суперинтуиционистских пропозициональных логик из нескольких достаточно широких классов. Среди обсуждаемых результатов автор диссертации обнаружил [44] и ошибочные [33,26].

Отделимость логик «(Лп) Хосои получил [22] как следствие из доказанного им в [22] другого результата , дающего достаточное условие для отделимости исчислений Н+9, где 2) - конечное множество ^-формул. Это условие немного изменено в [24] и окончательно формулируется так. Исчисление Н+25 отделимо , если оно удовлетворяет двум условиям: 1) исчисление Н+э ^-полное; 2) существуют построенные из переменных ч и » ^-формулы (^.....С^ такие, что ^-формулы а1з(...э(Оп3(Ч^))...) и ^те)^ выводимы в Н+э, т.е. в Н+э дизъюнкция выражается через импликацию. Высказав предположение , что условие 2) в этом утверждении может быть избыточным, Хосои ставит вопрос: будет ли 1) необходимым и достаточным условием для отделимости исчисления Н+э ? Мак-Кей [33] построил отделимое исчисление , в котором дополнительные аксиомы - э-формулы , но условие 2) не выполнено. Утвердительный ответ на поставленный Хосои вопрос дан автором в [38,39] ( теорема 2.13 главы II диссертации ). Опустить и условие 1) , т.е. утверждать , что для любого конечного множества ^-формул зе исчисление Н+эе отделимо , нельзя, так как среди них существуют исчисления , не являющиеся э-полными [34,41 ].

В работах [38,39] автором было введено свойство пропозициональных формул ©. Формула 0 обладает свойством <з, если для каждой переменной д, входящей в 0, формула 0= (Р^ ^ ^ ) выводима в Н, где 1; - пропозициональная переменная, отличная от ч и не входящая в 0, а и Р^А ~ результаты подстановок соответственно г и q&t вместо д в 0 . Там же [38,39] с помощью этого свойства автором было получено'условие , достаточное для отделимости исчислений, т.е. было доказано, что если э-формулы из эе обладают свойством то исчисление Н+эе отделимо ( теорема 2.15 главы II диссертации ); однако обратное ему утверздение неверно [441. Для многих формул сравнительно легко удается доказать , что они обладают свойством © и тем самым установить отделимость исчислений , дополнительными аксиомами которых будут эти формулы [38,39,41,42,8].

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

нообъмного с ним и отделимого исчисления. Искомое построение автор предложил проводить в два этапа.

На первом этапе для рассматриваемого исчисления сначала строим самые сильные по выводимости в Н ^-формулы , выводимые в самом исчислении , но не выводимые в нем без дополнительных аксиом , содержащих отрицание, а затем добавляем их к списку аксиом изучаемого исчисления , получая тем самым новое исчисление , равнообъемное исходному. Чтобы контролировать процесс построения таких формул, констатировать их отсутствие и зафиксировать этот этап,для каждого набора логических пропозициональных знаков не содержащего отрицания , автор ввел свойство исчислений [ 44]. Так как оно представляет и самостоятельный интерес , то для полноты и удобства изложения материала в диссертации мы определили его для любого набора V.

Будем говорить , что исчисление Н+эе обладает свойством Ф^ , если каждая выводимая в Н+эе ^-формула выводима и в исчислении н+*=у4 , где эе^ - подмножество всех =у&-формул множества х.

На втором этапе по исчислению , полученному на первом этапе, строим равнообъемное с ним исчисление с полными фрагментами, заменяя в исходном дополнительные аксиомы новыми аксиомами. С целью, аналогичной той, которая определила введение на первом этапе свойства ц>1> , на втором этапе для каждого набора логических пропозициональных знаков V, содержащего => , автор ввел свойство исчислений сгу [44] , составившее вместе со свойством основу критериев ^-полноты и отделимости исчислений из К. Для удобства обращения с ним в диссертации оно фигурирует в измененном виде.Будем говорить, что исчисление Н+х из К обладает свойством (ж>) , если каждая ^-формула из 5(а?) ^-выводима в Н+х ( т.е. существует ее вывод в Н+эе , состоящий только из ^-формул ) , где 2> (зе) - конечное множество =п-формул , определенным способом построенное по множеству =п-фюрмул эе . Ценным является финитность свойства сг^ , состоящая в том, что наличие его у исчисления из К определяется к-выводимостыо в нем конечного -числа формул . По своим возможностям в доказательстве отделимости исчислений Н+эе из К свойство является в некотором смысле ослаблением свойства @ [38,39] , а именно наличие свойства ® у формул из ж не будет условием , необходимым для того, чтобы исчисление Н+эе обладало свойствами [44]; однако оно будет достаточным. Иначе говоря, если формулы из х обладают свойством ©,

то исчисление Н+зе будет обладать свойством при любом ^ , содержащем => [441 ( следствие 2.8 главы II диссертации ).

Отделимость нормальных исчислений согласно ее определению равносильна их ^-полноте при любом наборе Так как исчисления из класса К являются нормальными , то сначала автором были получены критерии ^-полноты исчислений из £ [44]. В результате чего все наборы ^ разделились на четыре группы: для и из первой группы исчисления из К. являются ^-полными; для и из второй группы ^-полнота исчисления из С эквивалентна наличию у него свойства для ^ из третьей группы - наличию у него свойства ег^; для ^ из четвертой группы - наличию у него свойств и ( леммы 2.13, 2.14, 2.22 и 2.24 главы II диссертации ). С помощью этих результатов автором получен критерий отделимости исчислений из класса К [44], согласно которому отделимость такого исчисления равносильна наличию у него свойств , сг и ( теорема 2.18 главы II диссертации ). Для подкласса исчислений х:1=СН+эе |эе - множество ^-формул) класса £ эти результаты значительно упрощаются [44]. Все наборы V делятся только на две группы , одну из которых составляет первая и вторая , а другую - третья и четвертая. В формулировке критерия отделимости исчислений из Х^ фигурирует только свойство , а именно отделимость исчисления из равносильна наличию у него свойства ( теорема 2.19 главы II диссертации ).

Согласно этому критерию изучение отделимости исчислений из К, можно заменить изучением более простых свойств и а^ , что используется при решении проблемы 2 и позволяет сделать значительный шаг на пути решения проблемы 1 согласно намеченному плану , т.е. свести ее решение к двум более частным проблемам , соответствующим упомянутым выше этапам. Первая из них - эта проблема ( проблема 1.1 ) построения по исчислению из К равнообъемного с ним и обладающего свойствами исчисления из К, а вторая проблема ( проблема 1.2 ) касается свойства и формулируется аналогично проблеме 1.1. Хотя эти проблемы сформулированы как составляющие решения проблемы 1, но они представляют и самостоятельный интерес. По ним автором получены следующие результаты.

Положительно решена [50,54] проблема 1.1 для подклассов ис-исчислений х;1+2={н+зеисн1)} (1=0,1 ) класса К. , где зе - конечное множество э-формул, й0=(-1д=>1;):з( и 1^ = (-1-^=1;)=( (

=1;)э1;) ( д и Ь - пропозициональные переменные , а формулы Н0 и И.

дедуктивно равны в Н соответственно формулам -iqv-nq и -nqv(-nq=q)). Иначе говоря , доказано , что по любому исчислению из можно

построить равнообъемное с ним исчисление из £1+2 , обладающее свойствами ( теорема 2.24 главы II диссертации ).

По проблеме 1.2 получен более сильный результат, чем ее положительное решение [481: доказано, что по любому исчислению из К. можно построить равнообъемное с ним исчисление из К. , обладающее свойствами сохраняя при этом свойства ( теорема 2.20

главы II диссертации ). Одним из основных достоинств этого результата является возможность сохранять свойства при перестраивании рассматриваемых исчислений , что позволяет беспрепятственно использовать его для решения проблемы 1. С помощью этого результата и сформулированного выше критерия она условно решена [46,481, а именно доказано, что по любому исчислению из К , обладающему свойством vd7 , можно построить равнообъемное с ним и отделимое исчисление ( теорема 2.25 главы II диссертации ).

Этот результат сводит решение проблемы 1 к проблеме 1.1. Более того , из него следует положительное решение проблемы 1 для исчислений из , С, и £3 [46,48,50,54] , так как для исчислений из свойство !р=7 выполнено тривиальным образом, а для исчислений из С, и ~ в СИЛУ положительного решения проблемы 1.1 ( теоремы 2.26 и 2.27 главы II диссертации ).

Из последних результатов вытекает отделимость многих суперинтуиционистских пропозициональных логик. Логика а О) , порожденная конечным подмножеством э множества фомул (Х|Х дедуктивно равна в Н Х^.-.&Хд , где X^=R1, или X1=RQ, или Х^ - ^-формула }, может быть задана исчислением из , или К^, иш и поэтому отделима ( теорема 2.28 главы II диссертации ). Если логика нормализуема и множество ее позитивных формул совпадает с множеством позитивных формул интуиционстской пропозициональной логики , то оно может быть задана исчислением из К, обладающим свойством ¡р=у ,"и следовательно , отделима ( следствие 2.16 главы II диссертации ). Этот результат является исправлением леммы 5.2 работы [28]. Также отметим, что следствия, вытекающие из теоремы 2.25 диссертации , перекрывают практически все полученные другими специалистами результаты по проблеме отделимости суперинтуиционистских пропозициональных исчислений и логик.

Как было отмечено выше , в диссертации рассматриватся еще и

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

лений из К. Для свойства при не содержащем V, существование такого алгоритма следует из отделимости интуиционистской пропозициональной логики [37,19] и теоремы Попеля-Диего ИЗ,61. Автору удалось доказать существование алгоритмов , проверяющих наличие свойства р^ при ^ , не содержащем п , у исчислений из £2 , £3 и С4=Ш+эе|* - множество -формул, не являющихся э-формулами) [45, 54,441 ( теорема 2.29 главы II диссертации ). В результате им положительно решена проблема 2 для классов исчислений ( 1=1,2,3, 4 ) [43-45,54] ( теорема 2.30 главы II диссертации ).

Для доказательства уже перечисленных результатов по проблемам 1 и 2 используется возможность разложения пропозициональных формул на характеристические пропозициональные формулы , что позволяет сузить изучаемый класс исчислений £ , рассматривая только те, у которых дополнительные аксиомы - характеристические формулы , при этом сохраняя общность получаемых результатов.

Понятие характеристической формулы было введено в работе [51 для конечной геделевой псевдобулевой алгебры , т.е. алгебры, у выделенного элемента которой имеется единственный непосредственный предшественник. В работе [6] оно было распространено на конечные геделевы ^-алгебры , в которых определена операция пересечения, а в работе [48] - на любые конечные геделевы ^-алгебры. - Понятие ^-алгебры , введеное в [19] для изучения фрагментов исчисления Н, явилось обобщением таких уже известных под другими названиями понятий , как импликативная полуструктура, импликативная структура и псевдобулева алгебра, история которых изложена в [12,35]. По сути дела , ^-алгебра - это множество, на котором заданы операции псевдобулевой алгебры, определяемые набором логических пропозициональных знаков ь> и включающие операцию относительного псевдодополнения. При к, содержащем все четыре знака, ^-алгебра будет псевдобулевой алгеброй. Для удобства изложения материала операции ^-алгебр будем обозначать так же , как и интерпретируемые ими логические пропозициональные связки. Знаки =>, &, у и л будут обозначать соответственно операции относительного псевдодополнения ,'пересечения, объединения и псевдодополнения. Это не приведет к путанице , так

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

Пусть v - какой-нибудь набор логических пропозициональных знаков,содержащий =>, а в - какая-либо конечная геделева ¡-—алгебра. Каждому элементу Z множества 9 поставим в соответствие пропозициональную переменную q^, причем различным элементам 6 сопоставляются различные переменные. Если чей , то положим <u(e,-i)={-iq^qn^|Ce9)U Uiq^oiq^l^e}. Положим -u^oMiq^oq^oq^ll.TjeeJUfq^o ^(q^oq^) | С,т)ев> и ¡&(e,v)={q1}UQyi_,'U(8,D), где о - символ из iA{-i), а 1 - выделенный элемент в . По в построим характеристическую формулу Хд , положив 3^=Qn=> (... = (Q1 ^q^)...) , где Q1.....C^ - все

элементы множества ¡s(Q,f) , а ш - единственный непосредственный предшественник выделенного элемента 6.

Для изложения результатов , связанных с разложением пропозициональных формул на характеристические формулы , введем следующие обозначения. Выражение Р1,....Pnf-^Q будет означать, что ^-формула Q ^-выводима в Н из v-формул Р1р...,Рп с помощью правила модус поненс и правила подстановки , а выражение Р1,...,PnfyQ - что Р!.....РпГ0 и Qf-1^

Для каждого набора v , содержащего = , заданное на множестве всех ^-формул отношение P^Q является рефлексивным и транзитивным , но неантисимметричным ( т.е. не согласованным с графическим равенством формул ) отношением f35 3 , которое часто называют отношением частичного квазипорядка. Если &<=i> , то можно сделать [61 дистрибутивной структурой [7,12,351. Понятие неразложимого в пересечение элемента структуры следующим образом распространяется и на множество . Будем говорить, что ч-фррмула Р не разложима в , если из соотношений Q,S«=3U и Q.SI^P следует, что QfyP или SfvP. Естественным образом ^-формулу Q назовем разложимой в на ^-формулы Р1,...,Р11 , если Р1.....

Характеристические формулы для конечных ^-алгебр и только они являются неразложимыми в э ^-формулами [6,48]. Точнее говоря, любая не выводимая в Н ^-формула Р не разложима в тогда и только тогда, когда Р-Ц-^Х^ для некоторой конечной геделевой v-алгебры Ф. Более того, Xgfvx£ в том и только том случае, когда ^-алгебры в и Ф изоморфны [6,48]. При изучении разложимости v-формул в возникают вопросы о возможности и однозначности их разложения на характеристические ( неразложимые ) формулы и о связи разлагаемой фор-

мулы с множеством "—алгебр, задающим такое ее разложение. Частично ответы на эти вопросы автором получены в работах [48,54]. Во-первых, доказано, что если у«-, то для любой не выводимой в Н ^-фор-мулы 0 существуют неизоморфные друг с другом конечные геделевы у-алгебры Ф-,...,® такие, что Хщ ( теорема 2.7 гла-

вы II диссертации ). Во-вторых , оказалось , что такое разложение однозначно с точностью до дедуктивного равенства ^-формул в Н , а множество ^-алгебр, задающее его, состоит из тех и только тех конечных геделевых "—алгебр , на которых 0 предельно опровержима ( теоремы 2.8, 2.9 и 2.10 главы II диссертации ) . Ценным является и то , что процесс построения по "--формуле 0 ее разложения

Х^ ,и I—алгебр Ф1(...,Ф , задающих это разложение, можно

н п 11

осуществить алгоритмически.

Согласно определению характеристической формулы в ней зашифрована структура представляемой ею у-алгебры. Более того, выводимость в Н у-формулы х£ из "--формулы Хд (т.е. Хд^Х^ ) равносильна изоморфной вложимости I—алгебры 9 в некоторый гомоморфный образ "—алгебры Ф [6,48]. Этот результат вместе с возможностью разлагать в некоторые ^-формулы на характеристические формулы позволяют сводить решения многих вопросов , касающихся выводимости формул в Н , к вопросам , связанным с вложимостью I—алгебр друг в друга, что используется при решении проблем 1 и 2. Поэтому естественным образом возникает необходимость изучения "—алгебр и в особенности изоморфной вложимости их друг в друга.

При различных "- классы конечных "—алгебр, в которых определена операция пересечения, следующим образом соотносятся друг с другом. На каждой конечной "--алгебре можно задать недостающие операции , сделав ее м-алгеброй , где ^ - набор логических пропозициональных знаков, включающий и, а каждая такая ¿—алгебра по определению является и "--алгеброй. Тем самым , изучая какой-нибудь из этих классов , например, класс конечных э&-алгебр ( импликативных полуструктур ), мы в той или иной мере изучаем и все остальные.

Достаточно очевидно , что доказывать изоморфную вложимость "—алгебр друг в друга , исходя непосредстенно из ее определения, дело малоперспективное. Для этой цели желательно использовать представления "—алгебр через объекты более простой структуры. В работах [47-49,51-56] автором предложено и детально разработано представление конечных "—алгебр, в которых определена операция пе-

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

Понятие неразложимого в пересечение элемента в структурах [V] в работе (63 было распространено на импликативные полуструктуры, а в 151] - на любые ^-алгебры. Элемент £ ^-алгебры 6 назовем неразложимым элементом 9 , если из соотношений Т1,ф<=8 , £=>тН , £=><р=1 и тр(срэ£)=1, где 1 - выделенный элемент 9, следует, что £=т) или £=Ф-В каждой ^-алгебре 9 множество 1(8) всех ее неразложимых элементов замкнуто относительно операции относительного псевдодополнения и тем самым является ее ^-подалгеброй , удовлетворяющей следующему условию: для любых £ и т^ из-1(9) в 1(9) верно хотя бы одно из равенств или ?=пт=1 [47,48,51] ( лемма 1.2 главы I диссертации ). Для любой ^-алгебры Ф это условие эквивалентно такому условию: I(Ф)=Ф ( следствие 1.2 главы I'диссертации ). Оператор I множество я1 конечных =&-алгеСр отображает в множество з ={3|Е -конечная =-алгебра и 1(2)=2) , сохраняя при этом свойство геделе-вости и отношения гомоморфности и изоморфности [47,48] ( теоремы 1.1 и 1.2 главы I диссертации ). Более того, для кавдой ^-алгебры Ф из з1 в я1 существует единственная с точностью до изоморфизма =&-алгебра в такая , что э-алгебры 1(9) и Ф изоморфны [47,48,56] ( теорема 1.4 главы I диссертации ). Поэтому I является взаимно однозначным отображением из я1 на з1. Устанавливается связь оператора I с прямым произведением ^-алгебр [55] ( теорема 1.3 главы I диссертации ) и сравниваются два метода построения псевдобулевых алгебр по частично упорядоченным множествам [56], один из которых, предложенный автором в работе [56] , основан на операторе 1~1 , а другой, применяемый в работе [3] , использует топологические понятия ( теорема 1.13 главы I диссертации ).

Для выяснения изоморфной вложимости к-алгебр друг в друга в работах [48,55] автором предложены критерии, использующие оператор

I. Конечная ^-алгебра Ф вложима в конечную у-алгебру 6, на которой определена операция пересечения и операции, заданные на Ф, тогда и только тогда, когда существует вложение э-алгебры 1(Ф) в е, удовлетворяющее некоторым условиям ( теорема 1.5 главы I диссертации ). Их характер поровдает четыре случая и в каздом из них получаем критерий вложимости для соответствующих ^-алгебр. Например, конечная =>&-алгебра 3 вложима в конечную =&-алгебру Ф в том и только том случае , когда =>-алгебра 1(5) вложима в Ф ( следствие 1.15 главы I диссертации ). Поэтому из вложимости э-алгебры 1(3) в э-алгебру 1(Ф) следует влокимость конечной =>8с-алгебры 3 в конечную э&-алгебру Ф ( следствие 1.20 главы I диссертации ). Однако обратное утверждение неверно [48]. Вместе с тем , для каздой конечной э&-алгебры 3 существует конечное множество =-алгебр из з1, содержащее э-алгебру КЗ), такое, что =>&-алгебра 3 вложима в конечную э&-алгебру Ф тогда и только тогда , когда некоторая з-алгебра из этого множества вложима в =>-алгебру 1(ф) [47] ( теорема 1.7 главы I диссертации ). Такой же результат имеет место и для конечных геделевых =>&-алгебр [481 ( теорема 1.8 главы I диссертации ).

Доказательства последних двух результатов являются громоздкими и технически трудными , так как в них реализуется значительная часть предлагаемого автором метода доказательства отделимости исчислений. Именно они непосредственно используются при решении проблемы 1.2 и дают возможность перестроить исчисление из С так, чтобы оно обладало свойством <£_, . Но, чтобы перестроенное исчисление обладало еще и свойством ее , нужно получить аналогичные результаты и для конечных =п&-алгебр. С этой целью вводится определенный на множестве эп-алгебр оператор N. ставящий в соответствие каждой такой =п-алгебре е ее минимальную эч-подалгебру, содержащую 1(6) [48]. На множестве конечных эп-алгебр он сохраняет свойство геделевости и отношения гомоморфности и изоморфности , но не является взаимно однозначным, так как неизоморфным эт-алгебрам могут соответствовать изоморфные [48]. Он будет таковым, если сузить область его определения, рассматривая только те конечные =п-алгеб-ры, на которых определена операция пересечения , т.е. ^&-алгебры [48,49] ( теоремы 1.9 и 1.10 главы I диссертации ).

Таким образом , оператор N взаимно однозначно отображает множество зт^ конечных =п&-алгебр на множество З11={3|3 - конечная =п-алгеСра и Щ2)=3> , сохраняя при этом свойство геделевости и

отношения гомоморфности и изоморфности. На основе его формулируются критерии вложимости =п&-алгебр друг в друга. Конечная =п&-ал-гебра Ф вложима в конечную =-1&-алгеСру 0 в том и только том случае, когда =п-алгебра И(Ф) вложима в в [48,49] ( лемма 1.36 главы I диссертации ). Поэтому из вложимости эп-алгебры N(5) в =н-алгеб-ру N(9) следует вложимость конечной =п&-алгебры Ф в конечную эп&-алгебру в [48] ( следствие 1.29 главы I диссертации ). Однако обратное утверждение неверно [48]. Вместе с тем, для каждой конечной э!&-алгебры Ф существует конечное множество =п-алгебр из эг1, содержащее =п-алгебру ЩФ), такое , что эл&-алгебра Ф вложима в конечную =п&-алгебру 8 тогда и только тогда , когда некоторая =п-алгеСра из этого множества вложима в =п-алгебру N(6) [49] ( теорема 1.11 главы I диссертации ). Такой же результат имеет место и для конечных геделевых =п&-алгебр [48]' ( теорема 1.12 главы I диссертации ). Как было отмечено выше, последние два результата тоже используются при решении проблемы 1.2.

В работе [48] автором установлена связь оператора N с оператором I. Оказывается , что для любой конечной эп&-алгебры в справедливы равенства N(N(6) )=Щ6) и 1(Г1(6))=1(6) ( следствие 1.24 главы I диссертации ). Результаты применения к каким-нибудь двум конечным =п-алгебрам операторов I и N одновременно связаны отношениями гомоморфности и изоморфности независимо от того , удовлетворяют ли им исходные зч-алгебры ( леммы 1.32 и 1.33 главы I диссертации ). Отметим , что такая согласованность будет , т.е. сами алгебры и результаты применения к ним операторов I и N одновременно связаны этими отношениями, если рассматривать конечные =-1&-ал-, гебры.

Как было отмечено выше, каждую конечную ^-алгебру, в которой задана операция пересечения, можно сделать псевдобулевой алгеброй, определив на ней недостающие операции. Осуществить такое же преобразование над любой конечной ^-алгеброй, вообще говоря, невозможно. Однако она вложима в некоторую конечную псевдобулеву алгебру [56] ( теорема 1.6 главы I диссертации ). Таким оброзом, множество конечных ^-алгебр состоит только из ^-подалгебр конечных псевдобулевых алгебр.

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

идейной основе различны . Для проблемы отделимости этих логик и исчислений почти все методы исследований используют идею приведения выводов к нормальной форме в исчислениях секвенций Генцена путем устранения в них сечения или идею изоморфной вложимости ^-алгебр в псевдобулевы алгебры. Приемы реализации этих идей в виде методов сильно зависят от рассматриваемого исчисления и поэтому эти методы не могут быть достаточно общими.

В диссертации исследования основываются на разложении в Н пропозициональных формул на характеристические пропозициональные формулы, на моделировании по выводимости в Н к-алгебр и на представлении конечных ^-алгебр через э-алгебры. Характерной чертой этого представления является то, что как представляемые ^-алгебры, так и представляющие их э-алгебры суть объекты одной и той же природы. Более того, представляющая ^-алгебра изоморфно вложима в представляемую ею ¡^-алгебру. Именно эти обстоятельства делают его главной составляющей предложенного автором метода решения проблемы отделимости исчислений из 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 наименований.

СОДЕРЖАНИЕ РАБОТЫ.

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

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

В §1 дается определение ^-алгебры, вводится оператор I, реализующий идею этого представления , и устанавливаются простейшие свойства оператора I. В §2 изучаются простейшие свойства ^-алгебр, а в §3 рассматриваются два частных случая последовательного соеда-

нения ^-алгебр.

В теоремах 1.1 и 1.2 §4 доказывается, что на множестве конечных э&-алгебр оператор I сохраняет отношения гомоморфности и изо-морфности , а в теореме 1.3 §4 выясняется его связь с операцией прямого произведения ь—алгебр.

В §5 доказывается ( теорема 1.4 ) возможность обращения оператора I при отображении им множества я1 конечных =>&-алгебр в множество з1 конечных э-алгебр ( импликатур ), удовлетворяющих некоторому условию , а именно для каждой =>-алгебры Ф из з1 строится единственная с точностью до изоморфизма =>&-алге0ра Ф из л1 такая, что =>-алгебры Фи 1(Ф) изоморфны. Теоремы 1.1 , 1.2 и 1.4 показывают , что оператор I является взаимно однозначным отображением из я1 на з1 , сохраняющим свойство ^-алгебр быть геделевыми.

В §6 изучается проблема изоморфной вложимости ¡---алгебр друг в друга. Для конечных 1>-алгебр в теореме 1.5. дается критерий вложи-мости , использующий оператор I . Конечная м-алгебра Ф вложима в конечную ^-алгебру в, на которой определена операция пересечения и операции , заданные на Ф , тогда и только тогда , когда существует вложение ^-алгебры 1(Ф) в в , удовлетворяющее некоторым условиям. Их характер порождает четыре случая и в каждом из них получаем критерий вложимости для соответствующих ^-алгебр. Из этой теоремы вытекают критерии вложимости для конечных =&-алгебр , =н&-алгебр, зу&-алгебр и псевдобулевых алгебр ( следствия 1.15, 1.16, 1.17 и 1.18 ).

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

Согласно следствию 1.15 для вложимости конечной =&-алгебры Ф в конечную =>&-алгебру Ф достаточно вложимости э-алгебры 1(Ф) в =>-алгебру 1(Ф) . Однако обратное ему утверждение неверно . Вместе с тем , в теореме 1.7 доказывается , что для каждой конечной з&-алгебры Ф можно построить конечное множество з]-^ з-алгебр из з1 , содержащее э-алгебру 1(Ф) , так , что конечная =&-алгебра Ф вложима в конечную =&-алгебру Ф тогда и только тогда, когда некоторая э-алгебра из вложима в э-алгебру 1(Ф) . Такой же

результат доказывается ( теорема 1.8 ) и для конечных геделевых =>&-алгебр , а именно для каждой конечной геделевой з&-алгебры Ф строится конечное множество геделевых =-алгебр из з^, со-

держащее =-алгебру 1(Ф) , так , что конечная геделева =>&-алгебра Ф вложима в конечную =&-алгебру Ф тогда и только тогда , когда некоторая =-алгебра из з^^ вложима в =-алгебру 1(Ф).

В §7 изучаются эп-алгебры. На множестве =п-алгебр определяется оператор N , ставящий в соответствие каждой такой =п-алгебре в ее минимальную по вложению эл-подалгебру , содержащую 1(0). Выясняется связь оператора N с оператором I и отношениями гомо-морфности и изоморфности . В теоремах 1.9 и 1.10 доказывается, что на множестве конечных =п&-алгебр оператор I сохраняет отношения гомоморфности и изоморфности . Эти результаты показывают, что оператор N является взаимно однозначным отображением множества конечных эп&-алгебр на множество эт1, сохраняющим свойство ^-алгебр быть геделевыми.

С помощью установленных свойств оператора N для конечных =п&-алгебр получены критерии вложимости , основные из которых содержатся в теоремах 1.11 и 1.12 , являющихся аналогами теорем 1.7 и 1.9 . В теореме 1.11 доказывается , что для каждой конечной =п&-алгебры Ф можно построить конечное множество =п-алгебр

из эт1 , содержащее эн-алгебру Л(ф), так, что конечная =п&-алгебра Ф вложима в конечную =п&-алгебру ф тогда и только тогда , когда некоторая =-|-алгебра из вложима в =п-алгебру И(Ф) . В

теореме 1.12 этот результат переносится на конечные геделевы о1&-алгебры, а именно для каждой конечной геделевой =-1&-алгебры Ф строится конечное множество геделевых =-1-алгебр из зИ ,

содержащее л-алгвбру N(9), так, что конечная геделева эп&-алгебра Ф вложима в конечную :п&-алгебру Ф тогда и только тогда , когда некоторая эп-алгебра из ^(ф) вложима в =н~алгебру ЩФ).

В теореме 1.13 §8 решается следующий вопрос: вложима ли конечная ^-алгебра в в конечную к-алгебру Ф , если б вложима в некоторый гомоморфный образ Ф?

В последнем §9 первой главы определяется оператор Вг , устанавливаются некоторые его свойства и сравниваются ( теорема 1.14 ) два основанные соответственно на операторах I-1 и Вг метода построения псевдобулевых алгебр по конечным частично упорядоченным множествам.

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

В §3 рассматриваются вопросы о возможности и однозначности

• разложения в ^-формул на характеристические ( неразложимые )

формулы и о связи разлагаемой ^-формулы с множеством у-алгебр,

задающим ее разложение. В теореме 2.7 доказывается , что если

то для любой не выводимой в Н ^-формулы 0 существуют неизоморфные

друг с другом конечные геделевы алгебры ^.....Фд такие , что

Х^ ,...,Х,т| ■ В теоремах 2.8 , 2.9 и 2.10 устанавливается , что 1 ^п

это разложение 0 однозначно с точностью до дедуктивного равенства

^—формул в Н, а множество ^-алгебр, задающее его, состоит из тех и

только тех конечных геделевых ■—алгебр , на которых 0 предельно

опровержима. Выясняется, что процесс построения по формуле 0 ее

разложения ,...,Хщ и у-алгебр Ф,.....Фп , задающих это разло-

1 п

жение, можно осуществить алгоритмически.

В теоремах 2.11 и 2.12 из §4 доказывается возможность моделирования по выводимости в Н оп8с-алгебр Л2+Л2 ' ГД9 л2 ~ ДВУХЭЛ0_ ментная псевдобулева алгебра , задающая классическую пропозициональную логику , л" - результат декартовой степени Л2 , а Л2+Л2 -результат последовательного соединения Л2 и Л2 .

В §5 вводятся свойство пропозициональных формул « и свойства исчислений и ж,, даются критерии I—полноты и отделимости исчислений из класса К и решается проблема 1.2 , т.е. проблема построения по исчислению из К равнообъемного с ним и обладающего свойствами исчисления из £ . В теоремах 2.13-2.17 содержатся критерии и достаточные условия отделимости исчислений из класса Основной критерий дает теорема 2.18, согласно которому отделимость исчисления из £ равносильна наличию у него свойств <гэ , и ¡рэу. Для исчислений из подкласса Х^ класса К. этот результат значительно упрощается ( теорема 2.19 ), а именно отделимость исчисления из К.^ равносильна наличию у него свойства ®э .

В теореме 2.20 содержится положительное решение проблемы 1.2:

доказывается, что по любому исчислению из К. можно построить равно-объемное с ним исчисление из К , обладающее свойствами (з®),

сохраняя при этом свойство Чр^ для любого набора и .

В §6 изучается свойство исчислений из К. при и , не содержащем т. Для этих исчислений даются критерии свойства р^. Основным результатом этого параграфа является решение проблемы 1.1 ( т.е. проблемы построения по исчислению из К равнообъемного с ним и обладающего свойствами ри исчисления из К ) для подклассов исчислений и класса Доказывается ( теорема 2.24 ) , что по любому исчислению из ( 1=2,3 ) можно построить равнообъемное с ним исчисление из , обладающее свойствами р^ (пы) .

В §7 условно решается проблема 1 ( т.е. проблема построения по исчислению из К равнообъемного с ним и отделимого исчисления ), а именно доказывается ( теорема 2.25 ) , что по любому исчислению из К , обладающему свойством , можно построить равнообъемное с ним и отделимое исчисление . Для исчислений из подклассов К^, К^ и Ед класса К она решается полностью ( теоремы 2.26 и 2.27 ): по любому исчислению из К^ (1=1,2,3) строится равнообъемное с ним и отделимое исчисление.

С помощью теорем 2.25 , 2.26 и 2.27 устанавливается отделимость логик для достаточно широкого их класса . В теореме 2.28 доказывается , что для любого конечного подмножества э множества формул ЩХ-р^.. .&Хц, где Х^Ид, или Х1=Б1, или Х1 - ^-формула) логика а О) является отделимой , а в следствии 2.16 - что если суперинтуиционистская пропозициональная логика нормализуема и все ее формулы выводимы в Н, то она отделима.

В последнем §8 второй главы рассматривается проблема 2 , т.е. проблема построения алгоритма , распознающего отделимые исчисления среди исчислений класса К . С этой целью для каждого набора V , не содержащего ч , в теореме 2.29 доказывается существование алгоритма, проверяющего наличие свойства ¡р^ у исчислений из (1=2,3,4). Кроме того, устанавливается существование и алгоритмов , проверяющих наличие свойств и у исчислений из К. с помощью этих фактов решается проблема 2 для подклассов исчислений (1=1,2, 3,4) класса К, а именно доказывается ( теорема 2.30 ) существование алгоритма , распознающего отделимые исчисления среди исчислений из

В заключении сделан краткий обзор полученных в диссертации

результатов.

ЗАКЛЮЧЕНИЕ.

В диссертации получены следующие основные результаты.

1. Разработан некоторый метод представления конечных ^-алгебр и установлены различные его свойства.

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

3. Доказана моделируемость по выводимости в Н =и&-алгебр Л2+Л2-

4. Получены критерии отделимости исчислений из К.

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

6. Получено положительное решение проблемы отделимости для исчислений из Х^ ( 1=1,2,3 ).

7. Доказана отделимость суперинтуиционистских пропозициональных логик из достаточно широкого их класса.

8. Установлено существование алгоритма, распознающего отделимые исчисления среди исчислений из ( 1=1,2,3,4 ).

ЛИТЕРАТУРА

1. Искусственный интеллект. Книга 2. Модели и метода. ( под ред. Д.А. Поспелова ) М.:Радио и Связь 1990.

2. Марков A.A. О конструктивной математике//Труды Математического института им. В.А. Стеклова. 1962. T.LXVII. С.8-14.

3. Медведев Ю.Т. Об интерпретации логических формул посредством финитных задач//Доклады АН СССР. 1966. Т.169.Л1. С.20-23.

4. Циткин А.И. К вопросу об ошибке в известной работе М.Вайсбер-га//Исследования по неклассическим логикам и теории множеств. М.-.Наука, 1979. С.240-256.

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

6. Янков В.А. Конъюнктивно неразложимые формулы в пропозициональных исчислешшУ/Известия АН СССР. Серия матем. 1969. T.33,Ji1.

С.18-38.

7. Birkhoff G. Lattice theory. P.R. Island, 1967. Рус. перевод: Биркгоф Г. Теория решеток. М.:Наука, 1984.

8. Borülc B.R. A note on some Intermediate proposltlonal calcu-11//J. ОГ Symbolic Logic. 1984. V.49,J«2. P.329-333.

9. Brouwer L.E.J. Intultlonlsm and formalism//Bull. Amer. Math. Soc. 1913. V.20. P.81-96.

10. Church A. Introduction to mathematical logic,vol.I. Princeton, 1956. Рус. перевод: Черч А. Введение в математическую логику, т.1. М.:ИЛ, 1960.

11. Curry Н. A note on the reduction oi Gentzen's calculus LJ// Bull. Amer. Math. Soc. 1939. V.45.M. P.288-293.

12. Curry H.B. Foundations of mathematical logic. New York-San Francisco-Toronto-London, 1963. Рус. перевод: Карри X.B. Основания математической логики. М.:Мир, 1969.

13. Diego А. Sur les algebres de Hilbert. Paris. 1966.

14. Frege G. Begrlifsschrlit, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle. 1879.

15. Gentzen G. Untersuchungen über das logische Schllessen//Mathe-matlsche Zeitschrift. 1934-35. V.39. P.176-210, 405-431. Рус. перевод: Генцен Г. Исследования логических выводов. -В книге: Математическая теория логического вывода. М.:Наука, 1967, С.9-76.

16. Heytlng А. Die formalen Regeln der lntuitlonistischen Logik// Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse. 1930. S.42-56.

17. Heytlng A. Intultlonlsm, an Introduction, Studies in Logic and Foundations of Mathematics. Amsterdam, 1956. Рус. перевод: Гейтинг А. Интуиционизм. М.:Мир,'1965.■

18. Hilbert D. und Bernays Р. Grundlagen der Mathmatlk 1,11. Berlln-Heldelberg-New York:Springer. 1968,1970. Рус. переводы: Гильберт Д., Бернайс П. Основания математики 1,11. М.:Наука

• 1979,1982.

19. Horn A. The separation theorem of intuitionist proposltlonal calculus//J. of Symbolic Logic. 1962. V.27.J64. P.391-399.

20. Hosol T. The separation theorem on the classical system// J. Fac. Scl., Univ. Tokyo, Sec.I. 1966. Y.12. P.223-230.

21. Hosol T. Algebraic proof of the separation theorem on

classical prepositional calculus//Proc. Japan Acad. 1966. V.42,Ji2. P.67-69.

22. Hosol T. On the separation theorem of Intermediate prepositional calcull//Proc. Japan Acad. 1966. V.42.J66. P.535-538.

23. Hosol T. Algebraic proof of the separation theorem on Dummett's LC//Proc. Japan Acad. 1966. V.42.JS7. P.693-695.

24. Hosol T. The separable axlomatlzatlon of the Intermediate pro-positional systems Sn of Gadel/VProc. Japan Acad. 1966. V.42, Ю. P.1001-1006.

25. Hosol T. A criterion for the separable axlomatlzatlon of Gedel's Sn//Proc. Japan Acad. 1967. V.43,Ji5. P.365-368.

26. Hosol T. and Ono H. Axlomatlzatlon of models for Intermediate logics constructed with Boolean models by piling up//Publ. Res. Inst. Math. Sci. 1972. V.8,Ji1. P.1-11.

27. Hosol T. and Ono H. Intermediate prepositional logics ( a survey )//J. Tsuda College. 1973. №5. P.67-82.

28. Hosol T. On Intermediate logics III//J. Tsuda College. 1974. J66. P.23-38.

29. Hosol T. Non-separable Intermediate prepositional logics// J. Tsuda College. 1976. J(8. P.13-18.

30. Kabzlnskl J.K. The Wajsberg's results connected with separability of the lntultlonlstlc prepositional loglc//Bull. Sect, bogle. 1973. V.2,Jfe. P.131-133.

31. Kabzlnskl J.K. and Porebska M. Proof of the separability of the lntultlonlstlc prepositional logic by Wajsberg method// Reports on Math. Logic. 1975. Ji.4. P.31-38.

32. Kleene S.C. Introduction to metamathematlcs. New York-Toronto, 1952. Рус. перевод: Клини O.K. Введение в метаматематику. М.:Ш1, 1957.

33. McKay C.G. The non-separablllty of a certain finite extension of Heytlng's prepositional logic/ZProc. Nederl. Acad. Wetensch. Ser. A. 1968. V.71 ,J63. P.312-315.

34. Prior A.N. Two addition to positive lmplication//J. of Symbolic Logic. 1964. V.29,Jf1. P.31-32.

35. Raslowa H. and Slkorskl R. The mathematics of metamathematlcs. Warshawa, 1963. Рус. перевод: Расева E., Сикорский P. Математика метаматематики. М.:Наука, 1972.

36. Rose G.F. Prepositional calculus and realizability//Trans.

Amer. Math. Soc. 1953. V.75.JS1. P.1-19.

37. Wajsberg M. Untersuchungen über den Aussagenkalkul von A.Heyting//Wiadomosci matematyczne. 1938. V.46. P.45-101.

Работы автора по теме диссертации.

38. Хомич В.И. Теорема отделимости для суперинтуиционистских исчислений высказываний//Доклады АН СССР. 1976. Т.229.J66.

С.1327-1329.

39. Хомич В.И. Теорема отделимости для суперинтуиционистских исчислений высказываний//Четвертая Всесоюзная конференция по математической логике: Тезисы докладов . Кишинев: Штиинца, 1976. С.153.

40. Хомич В.И. Теорема отделимости для одной предтабличной суперинтуиционистской пропозициональной логшш//Мсследования по теории алгорифмов и математической логике. М.: ВЦ АН СССР, 1976. Т.2. С.140-153.

41. Хомич В.И. Отделимость суперинтуиционистских пропозициональных логик//Исследования по теории алгорифмов и математической логике. М. .-Наука, 1979. С.98-115.

42. Homle W. On the problem of separability of a superintuitionis-tic proposltlonal calculus//Sixth International congress oi logic , methodology and philosophy of science. Abstract's. Hannover, 1979. P.38-42.

43. Хомич В.И. Разрешимость проблемы отделимости для некоторых классов суперинтуиционистских пропозициональных исчислений// Пятая Всесоюзная конференция по математической логике: Тезисы докладов. Новосибирск: ИМ СО АН СССР, 1979. С.158-159.

44. Хомич В.И. О проблеме отделимости для суперинтуиционистских пропозициональных логик//Доклады АН СССР. 1980. Т.254, JM.

С.820-823.

45. Хомич В.И. О разрешимых случаях некоторых свойств суперинтуиционистских пропозициональных исчислений//Шестая Всесоюзная конференция по математической логике: Тезисы докладов.Тбилиси: Тбилис. гос. ун-т, 1982. С.199.

46. Хомич В.И. Об отделимости суперинтуиционистских пропозициональных исчислений с импликативными дополнительными аксиома-ми//Седьмая Всесоюзная конференция по математической логике: Тезисы докладов. Новосибирск: ИМ СО АН СССР, 1984. С.190.

47. Хомич В.И. О вложении импликатур в импликативные полуструкту-

ры//Восемнадцатая Всесоюзная алгебраическая конференция: Тезисы сообщений, часть вторая. Кишинев: Штиинца, 1985. С.255.

48. Хомич В.И. Об отделимых суперинтуиционистских пропозициональных исчислениях и о конъюнктивно неразложимых элементах в им-пликативных полуструктурах//2е1гзсЬг11г fur mathematlsche Logik und Grundlagen der Mathematlk. 1986. Bd.32,Ji2. S.149-180.

49. Homii V.I. On some properties of generalizations of pseudo-Boolean algebras//Elghth International congress of logic, methodology and philosophy of science. Abstract's. V.1. Moscow, 1987. P.95-97.

50. Хомич В.И. О полноте позитивных фрагментов суперинтуиционистских пропозициональных исчислений//Девятая Всесоюзная конференция по математической логике: Тезисы докладов . Ленинград: Наука, 1988. С.169.

51. Хомич В.И. О вложении импликатур//Вопросы математической логики и теории алгоритмов. М.: ВЦ АН СССР, 1988. С.17-33.

52. Хомич В.И. Логики , основанные на частично упорядоченных множествах/ /Первая Всероссийская школа по основаниям математики и теории функций: Тезисы докладов. Саратов: Саратов, гос. пед. ин-т, 1989. С.92.

53. Хомич В.И. Представление псевдобулевых алгебр и логика финитных задач//Десятая Всесоюзная конференция по математической логике: Тезисы докладов. Алма-Ата: ИММ АН Каз.ССР, 1990.С.159.

54. Хомич В.И. О свойствах суперинтуиционистских пропозициональных исчислений//Сибирский математический журнал. 1990. Т.31 ,J66. С.158-175.

55. Хомич В.И. О суперинтуиционистских пропозициональных логиках, связанных с частично упорядоченными множествами//Известия • АН СССР. Серия матем. 1991. T.55,Ji2. С.384-406.

56. Хомич В.И. О представлении конечных псевдобулевых алгебр и об одном его применении//Математические заметки. 1992. T.52,Jt2. С.127-137.