автореферат диссертации по философии, специальность ВАК РФ 09.00.07
диссертация на тему: Генценовские методы в логике

Полный текст автореферата диссертации по теме "Генценовские методы в логике"

РГи 0.1

'-} п • ГОС/ЛАРСТШНШЙ САНКТ-ПЕТЕРБУРГСКИЙ ШВЕРСИТЕТ

с. и

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

МУХЛЧЁВ Виктор Павлович

ГЕНЦ&ЮВСКИЕ МЕТОД! В ЛОГИКЕ Специальность 09.00.07.- логика

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

САНКТ-ПЕТЕРБУРГ 1993

. Работа выполнена на кафедре логики философского факультета Санкт-Петербургского университета

Научные руководители: _

доктор философских наук, профессор] СЕРЕБРЙННИКОВТЩ; доктор философских наук,'профессор БРОДСКИЙ И.Н.

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

доктор философских наук, профессор СМИРНОВ В.А. кандидат философских наук, доцент ФАТИЕВ Н.И.

Ведущая организация:

Санкт-Петербургский государственный педагогический университет.

Защита состоится " 1993 г. в часов

на заседании специализированного совета Д.063.37.01. по прису-вденив ученой степени доктора философских наук в Санкт-Петербургском государственном университете по адресу: 199034, Санкт-Петербург, Менделеевская линия,д.5, ауд._

С диссертацией можно ознакомиться в научной библиотеке Государственного Санкт-Петербургского университета.

Автореферат разослан '/8 " ¿¿¿>сР I 1993 г.

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

Л.М. Райкова.

ОЩЛЯ ХАРАКТЕРИСТИКА РАБ01Ы.

Актуальность темы исследования. Работы Герхврда Генцена "Исследования логических выводов" (1934), ''Непротиворечивость чистой теории чисел" (1936) и "Новое изложение доказательства непротиворечивости для чистой теории чисел" (1939) во многом определили состоянии современной логики. Они имели фундаментальное значение для теории доказательств, внесшей существенный вклад в развитие математики, особенно в исследования по ее основаниям.Их влияние на различнее раздели современной математики продолжает возрастать. Не меньшее значение имеют генценовские методы и для развития исследований по программе "искусственного интеллекта? прежде всего в такой ее области как теория и практика автоматического доказательства теорем. В настоящее время наблюдается уск ливаюцееоя влияние генценовских методов в такой новой у бкетро прогрессирующей области исследований как теоретическое программирование и различные его практические приложения.

Влияние развитой Г.Генценом теории естественного вывода выходит за пределы математической логики и оказыгвет существенное воздействие на исследования ло лсгическсму анализу естественного язкка, метододогик науки и на аналитическую [¡и.чосо$ив.

Хотя проз.л ) почти шестьдесят лет со времени опубликования классических трудов Генцена и список работ, посвященных поднятым в них проблемам, исчисляется уже не одной сотней названий, однако до сих пор нет исследований, содержащих хотя бы краткий л5зор истории развития гениеноЕСКих методов. Необходимость в такого рода исследованиях диктуется не только историкл-научными интересами, зни акт.альны также с точки зрения перспектив дальнейшего развития самих генценовских методов, поскольку нет работ, лосея-щенных анелизу всех существенных модификаций, приращений, усилений и упрощений, кл-орые эти методн претерпели за указанный период. Напротив, наблюдается даже тенденция к утрате накопленного здесь опьта

Степень разработанности темы. Имеется превосходные работы по отдельны-! разделам темы настоящей диссертации. В "Журнале символической логики" проводится систематическая библиографическая раб /га по математической логике, правда, доведенная только до 19/5 года. Имеется ■{.ундпментальнь'е исследования по натуральным, секвенциальном и табличньм методам, Клини 1УЬ2,1У Ч),

Карри X. (1948), (1963), Бета Э. (1955), Шютте К.( 1956,19/7), Правица Д. (1965,19/1), Земана Дк. (1973), Смирнова В.А. (19/2), 1вкеути (1953).

Из работ, посвкщеннчх историческому обзору отдельных тем, отметим статью Минца Г.Е. о развитии теории доказательств в СССР (1938), Краюеля Г. - об исследованиях по теории доказательств ( 1981), Сереорянникова О.Ф. (1987), Правмца Д. ( 1971) , Сурмы С. (1981), Радкио А. (1985), Йоргенсене И- (1938). Применению секвенциальных и табличных методов в модальной логике о середины 50-х - г.о начало 80-х годов посвящена дисоергация Быстрова П.И. (1981). Попов В. M. (19/9) дает обзор генценовских методов для релевантных систем.

-Важную рольдля.развития тема диссертации имели работы, свя-

■ занные со сравнительным анализом генценовских методов. Об отноше-------

нии натуральных и секвенциальных исчислений - это работы самого ГенценаГ. (1934,1939), Клини C.K. (1952, 1973), Карри Х.(1948, 1963), Правица'Д. (1965), Земана M. (1973), Смирнова В.А.(1972) Шанина H.A. (1965), Сурмы С. (1981), Серебрянникова О.Ф.'(1970), Россерс Дк. (1948), Минца Г.Е. (1988).

Сревнительный анализ различных секвенциальных исчислений, осуществлен Генценом (1934,1939), Клини C.K. (1952,1973), Карри X. (1963), Июльцем X. (1961), Хазенйегером Г. (1952, 1961), Шют-те К. (1977), Сурыой С. (1981), Серебрянниковым О.Ф. (19/0,19/9, 1987), Смирновым В.А. (1972,1979). .*.

Важными для понимания процеоса развития генценовских методов и применения их для исследования логических систем являетоя вопрос о разных способах доказательства Основной теоремы. Сравнительному анализу этих 'способоЕ посвящены статьи или отдельные главы в работах таких авторов как Клини С.К. (. 1952,1973), КарриХ. (.1963), Смирнов В.А. ЧУ/2), Серебрянников 0.«. (.1У79), Быстрой li.ll. 1.1987, 1989),' Смаллчан Р. (1*68), Колмогоров А.Н. (.1982), Драгалин А.Г. (.1979, 1982), лосоеский Н.К.(1981). Кетонен 0. (1УЧЧ), Хазенйегер Г. <.Ь61), Уусталу Т. и Пентус М. (Д*89), Зе-ман Д»лЬ73;, Ладриер д.(.ЬЫ), Нютте П.(.1У77) и Такеути Г.1978.

Однако, разработке тепы Тенценовскив методы в логике" в том объеме и о той си схематичностью, о которой шла речь вше, еще не реализовано.

цели и задачи исследовании. Цель диссертационной работы в том, чтвбы дать связный историч'ескии анвлиэ разеити« геншиюис-ких методой и рассмотреть BCfe fiyiy®CTBeKHue модификации и усиле-

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

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

- собрать и систематизировать все известные на сегодня варианты секвеьциальных и табличных исчислений;

- дать сравнительный анализ вьшеуказанных методов и их модификаций;

- произвести сравнительный анализ методов доказательства Основной теоремы;

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

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

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

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

- проанализированы исторические приоритеты совершенствования генценовских методов;

- найдено ревлме проблемы доказательства Основной теоремы прямым методом Серебрянникова 0.9. для систем без структурных правил.

Теоретическое и практическое значение диссертационного исследования заключается, по мнения автора, в следующем: во-первых, работа способствует более ясному пониманию особенностей истории современной, логики, в одной из ее наиболее важных областей - теории доказательств; 'во-вторых, детально знакомит с малоизвестными, но важными роботами отечественных и зарубежных авторов; в-третьих, материалы данной диссертации можно использовать в учебных курсах "История современной логики" и "Теория естественного вывода".

Основные положения диссертации проили апробацию в докладах на научной конференции "Современная чогика: проблемы теории, истории и применения в науке" Дзнинград, май, 1990 г./, на теоретическом семинаре аспирантов кафедры логики ЛГУ /декабрь, 1989 г./

Структура работы. Диссертация состоит из введения, трех глав, заключения и библиографии.

Общий объем диссертации 213 страниц, из них основного текста 198 страниц. Библиография содерлит 149 наименований.

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

Во взедении обоснована актуальность темы, дана оценка ее разработанности, сформулированы цели и задачи исследования, указаны методологические и теоретические основы диссертации. Лриведены краткие библиографические сведения о Герхарде Генцене. "

В первой главе "Открытие Генцзна и исследование секвенциальных исчислений в 1930 - ВД-е годы" рассматриваются исторические и логические предпосылки появления методов Генцена. Дается описание натуральных и секвенциальных исчислений, излагается Основная теорема и осуществляется переход к первой модификации секвенциальных исчислении, предложенной'финским логиком Кетоненом 0. (1944). Рассматриваются различные применения Основной теоремы.

В первом параграфе "Система обозначения. Натуральные исчисления" формулируется язык, на котором излагаются все исчисления, рассматриваемые в диссертации; но так как сохранить единую систему обозначений в отдельных случаях не удается, то соответствующие изменения в языке всегда специально оговаривавтся. Устанавливается, что ряд основных понятий и обозначений вводимых Генценом, заимствован у Герца. Это касается самого понятия секвенции и структурных правил вывода: сечения и утончения. Последние правила рассматриваются Генценом в его Солее ранних работах как основные правила вывода, и если утончение заимствуется у Герца без изменений, то сечение является модификацией правила сложного силлогизма Герца, следует отметить, что эти заимствования носят скорее внешний характер, поскольку основная идея идея Генцена иная, чем у Герца и связана с его доказательством непротиворечивости арйфмети ки. После известных результатов Геделя (1931) стало ясно, что доказательство непротиворечивости достаточно богетых формальных си-стек сталкивается с рядом глубоких проблем и формализация логики, ' ^уцествпенная $реге, Расселом и Гильбертом требуег существенных

изменений. Генцен выдвигает гипотезу о том, что поиск доказательства непротиворечивости надо проводить не в сфере определения объектов типа числа или множества, а ъ с^ере логического вывода, поскольку именно здесь обнаруживаются те способы заключения, которые приводят к антиномиям. Следовательно, если мы хотим доквзн вать непротиворечивость, то объектами исследования необходимо сделать сами доказательства так, как они обычно используются в математике. Известные к тому времени формализмы были по своей структуре весьма далеки от естественных способов заключения, поэтому для Гендена первым шагом в решении поставленной задачи было построение такого исчисления, которое бы соответствовало естественным рассуздениям. Исчисления такого типа Генцен назвал натуральными исчислениями. Сам Генцен характеризует их следующим образом: "Вамейшее отличиз ДО - еыводов от выводов в системах Рассела, Гил.ьберта, Гейтинга следующее: в последних истинные фор мулы выводятся из некоторого нножестаа "логических основных формул" посредством применения не многих прагил вывода; натуральные же выводы исходят вообще нз из логических аксиом, а из допущений, из которых делаются логические заключения. А затем посредством некоторых дальнейших заключений результат делается уне независим ым от допущений. Среди этих исчислений Генцзн отмечает также следующие: "Выводы истинных формул в этом исчислении всегда короче, чем в логистических исчислениях. Уто существенно евлзяно с тем, что в логистических выбодвх одна и тфе формула в большинстве случаев появляется несколько раз (как часть других формул), тогда как вЛЛ< - выводах это имеет место гораздо реже, ... в этом исчислении имеется заслуживающая внимания систематизация фигур заключения. С каждым из логических знаков... связана одна ?игура "введения" и одна фигура "удаления" его как внешнего знаке формулы. ... Введения представляют собой, так сказать, "определения" соответствующих знаков, а удаления являются в конце концов лишь следствиями этих определений, что можно выразить так: при удалении некоторого знака формула, которой это касается, и • знак, о котором идет речь, могут "использоваться лишь в том значении, которое они получают при введении данного знака."

Г. Генцен "Исследования логических выводов" /В кн. Математическая теория логического вывода. М. 1967 г. с. 18./ 2 Там же. с. ¿3.

Говоря об отличии натуральных исчислений от исчислений гиль-бертовского типа, мы не случайно привели цитату из. работы Генцена, Де^о в том, что достаточно продолжительное время различие между этими системами связывалось с тем, что в исчислениях гильбертов-ского типа имеются аксиомы, в системах же натурального вывода аксиом нет. Однако, как показал Смирнов в.А. в работе "Формальный вывод и логические исчисления-4 (, 1У72), системы натурального вывода отличаются от систем гильбертовского типа прежде всего понятием вывода; если для систем гильбертовского типа формальный вывод имеет вид дерева или последовательности формул, то для натуральных исчислений вывод имеет вид леса деревьев или леса последовательностей. Для натурального вывода обязательно не отсутствие аксиом (схем аксиом), а наличие по крайней мере одного правила непрямого (косвенного) вывода.

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

Во втором параграфе "^'счисления и1.К (логистические интуиционистское и классическое). Огчовная теорема." рассматриваются секвенциальные исчисления. Секвенциальные исчисления представляют собой исчисления способов заключения, которые не содержат, в противоположность исчислению АЛ), никаких допущений, но сохраняют присущее натуральным исчислениям деление способов заключений на'введения и удаления логических знаков. Также в отих исчислениях имеются структурные фигуры заключения, которые относятся уже не к логическим знакам, а к структуре секвенций. Правило сечения относится к структурным правилам, оно имеет вид:

£> <0. А Г, А - ©, А

где©- формула сечения, не входящая в заключение.

Классическое и интуиционистское исчисления секвенций отличается тем, что в сукцедентах секвенций классического исчисления допускается наличие нескольких формул, тогда как в интуиционистском исчислении возникают секвенции с не Солее, чем одной формулой в сукцеденте. По существу же дорма этих исчислений определена с учетом доказываемой Генценом "основной теоремы". Смысл ее состоит в том, что каждый вывод в секвенциальном исчислении, содержаний применение правила сечения, можно преибразовать в вывод, не содержащий се"ений, причем результирующая формула этого вывода остается без изменения, а в сам вывод будут входить только те, понятия, которые участвуют в построении конечного результата. Возможность такого преобразования .чьтекает из формулировок фигур заключения. Согласно Генцеяу, введение логического знака в сукце-дент секвенции является определением этого знака, а удалением логического знака является введение его в антецедент. Отсюда следует, что появление формально равных формул в посылках правила сечения, указывает на то, что мк одновременно вводим логический знак и удаляем его, а это,в свою очередь, является симптомом того, что доказательство данной формулы ведется окольным путем, с использованием излишних шагов. Сечение, следовательно, выполняет функцию устранений следствий неправильно выбранного пути доказательства. Основная теорема обосновывает такую процедуру перестрой ки вывода, которая позволяет устранять из вывода все окольные пути. Практически данная процедера сводится к доказательству устранимости правила сечения, которое предварительно обещается Генцз-ном в правиле"с»:ешение". Доказательство ведется по двум параметрам: по степени вывода и рангу вывода, то есть по количеству логических знаков формулы смешения и количеству секвенций содержащих формулу смешения. Устранение сечения достигается рядом последовательных структурных преобразований, постепенно понижающих степень и ранг вывода, вплоть до устранения лишних ветвей. Основная теорема достаточно подробно изложена в диссертации.

В трет рем параграфе "Исследование по теме исчисления предикатов" О.Кетонена." подробно рассматривается первое после 1'енцена исследование секвенциальных исчислений. Хотя в логической литературе на эту работу делаются ссылки, но они касаются только некоторых структурных изменений, внесенных Кетоненом в однопосылочныз правила для дизъюнкции и конъюнкции и также для правила введения импликации в сукцедент. Сама же работа посвящена применению ген-

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

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

Во второй главе "Развитие генценовских методов в 1550 - 60-е годы" рассматривается ряд существенных модификаций секвенциальных исчислений, принадлежащих как зарубежным, так и советским авторам. Их работы показали особую значимость генценовских методов для теорш поиска вывода и ее использования в программе исследовании по искусственному интеллекту: соответствующие модификации этих исчислений могут выступать в роли алгоритмов поиска Ьывода.

выясняется, что древовидная форма.вывода - не единственный спо соб представления генценовских исчислений: поиск доказательства молено вести методом построения семантических таблиц. В главе рассматривается также,метод модельных множеств, предложенный финским логиком Хинтиккой, который в идейном отношении совпадает с методом семантических таблиц Ьета, но основан на д^гой технике.

В первом параграфе "Перестановочность применений правил. Исчисления без структурных правил. Семантические таблицы." рассматривается семейство' исчислений, предложенных Клини и обладающих рядом впиьх свой«в. Бо-первых, Клини доказывает общую теорему о пе;естановчности применении правил при построении вывода. Это означает,'что мы в достаточно широких пределах можем переставлять фигури заключения в дереве вывода, увеличивая тем самым эффективность поиска вывода, при этом можно перестраивать вывод так, что например все утончения будут производиться в исходных секвгнциях, а сокращения е заключительной секвенции. Секвенциальные исчисления моишо задавать без включения в них структурных

правил для этого достаточно в посылках фигур заключ ния сохранять главную формулу данной фигуры заключения. В отом случае доказательство удобно- строить снизу вверх. Уто позволяет иметь в вершинах ветвей вывоца полный список подформул результирующей формулы. Но если ми не заинтересованы в выписывании всех подформул, то можно модифицировать оти исчисления так, чтобы сохранять в посылках лишь интересующие нас главные формулы, например, можно строить . исчислиния.в которых главная формула будет повторяться в посылках лишь для двух кванторных правил: введения существования в сукце-дент и всеобщности в антецедент. Каждой из этих тактик соответствует одно из ниже перечисленных исчислений:бЭ,6.3в,С^4, G'iS, построенных Клини. Так как структурные правила в этих исчислениях являются допустимыми правилами, то восполняя пробел в логической литературе мы даем доказательство допустимости правила сечения для . Heme доказательство выполнено методом прямого устранен ния сечения, предложенного Серебрянниковым О.Ф. Вышеупомянутый метод устранения сечения впервые примеиил Карри и он отличается от генценовского метода тем, что в нем устраняется не смешение, а сечение. Доказательство делится на три этапа. На первом этапе строится вывод одной посылки сечения, на втором этапе-другой поен лки,пр1чем ранг сечения не должен быть равен нулю. Если все прави ла, с помощью которых можно Еывести элиминируемую формулу - обратимы, то рассуждения обоих этапов можно заменить леммой об обратимости правил рассматриваемого секвенциального исчисления. Эти два этапа исчерпывающим образом заканчивают рассмотрение главней индукции - индукции по построению формулы сечекия. Они подготавливают. шег индукции, приводя обе посылки в специальный вид: выводы посилок заканчивается введением элиминируемом формулы с помощью логического правила. Далее следует третий этап, на котором в предположении, что посилок выводы имеют нужный вид и чю теорема Берна для любой подформулы формулы сечения, доказывается, что теорема верна и для данной формулы. Доказательство это злемзнтар-' но и ¡ведется по числу используемых логических знаков.

Уже упоминалось, чю для выводимых формул секвенциальные исчисления дают эффективную процедуру построения вывода. Однако у секвенциальных исчислений с сбрачнмыми правилами ость с>цеотьен-ны1 недостаток, который, витекает кьк раз из наиболее сильного свинства этих систем - свойства ьодформульност. Дало в том, что ее::и формула появляется о дсказа'Юльсгвв не lineup к езченин, и

она .уже не исчезает и должна многократно переписываться на каждом этапе доказательства или как подформула или как параметрическ кая формула. К ели после появления данной формулы последует сто шагов, то формула будет повторно выписана все сто раз. Метод Бета позволяет избавиться от такой рутинной работы. Этот метод строится на основе семантической интерпретации формул в виде таблиц. Суть процедуры состоит в том, что исследуемое утверждение (формулу) стремятся доказать косвенным образом, то есть данную формулу, стремяться не доказать (исходя из некоторого списка аксиом или до лущений), а опровергнуть, подыскивая подходящее распределение истинностных значений для ее подформул. Если нам удается найти контрпример, опровергающий данную формулу, то она ложна, если такого примера найти не удается, то после разбора всех случаев, процедура заканчивается, подтверждая ис.инность данной формулы. Заметим, что для семантических таблиц выполняется принцип подфор-мульности, поскольку при построении таблицы исходная формула разбивается на свои подформулы, к эти подформулы, однажды уже испытанные в качестве контрпримера, в ходе дальнейшего исследования уже нё используются. Метод семантических таблиц Бета так же как и секвенциальные исчисления можно использовать в качестве разрешающей процедуры.

Во втором параграфе "Модельные множества Хинтикки. Симметричные правила Хазенйегера. Метод метапеременных Кангера." рассматривается подробно метод модельных множеств Хинтикки. tro метод сходен с методом семантических таблиц Бета, но оформляется на языке теории множеств. Хинтикка так же как и Бет трактует доказательство общезначимости некоторой формулы как попытку найти опровержение для отрицания этой формулы. Ьсли 'она осуществлена, то формула доказуема. Аналогом построения модельных множеств могут быть системы Клину без структурных прввил. Далее рассматриваются системы Хазенйегера. В одной из этих систем отказываются от древовидного вывода в связи с необходимостью приспособить эти исчисления для. машинного поиска доказательств, /ругая система интересна сведением всех фигур заключения к некоторому стандартному виду: все фигуры (кроме отрицания) имеют вид двухпосьлочных правил. Кроме того пригодятся фигуры заключения с обратимыми правилами. В заведение параграфа рассматривается метод метапеременных Кангера, который повышает эффективность поиска подстановок при применениях кванторных правил в логике предикатов.

В трегьем параграфе "Исследования по теории поиска вывода в шестидесятые годи" рассматриваютей работк советских лигиков: Матулиса B.C., Плюшкявичуса P.A., Рогавы Н.Г., Шанина H.A., Мас-лова С.Ю. , Оревкова Е.П., Минца Г.Е/, посвященные дальнейшему развитию генценовских методов, приспособлению этих методов для малинного поиска вывода. 1ак Матулис B.C. (1962) дает варианта классического исчисления предикатов с единственным деревом вывода (идея этих исчислений принадлежит Ван Хао). Исчисления этого типа сходны и исчислениями Клини, но лучше приспособлены для поиска вывода секвенций. Особенностью их является то, что в каждом из прагил вывода,, секвенции, являющиеся посылками правила, однозначно строятся по секвенции, являющейся заключением правша.

Рассматриваются аналогичные системам Кангера и Матулиса 'секвенциальные варианты для аксиоматических теорий, определяемых конечным списком или перечиилимьм множеством специфических аксиом и имеющих и качестве лшического аппарата средства классическо го исчисления предикатов с постоянными(функциональными знаками и равенством, которые вводит. Рогава Н.Г. (1967). Плюшкявичус f.А. (1968) строит вариант конструктивного исчисления предикатов без структурных правил вывода. Его исчисление улучшает свойства исчис ления Клини в частности он не использует понятие сходной секвенции, главные формулы дублируются в посылках там, где это необходимо, а ограничении на квангорние правила более сильные, чем у Клини. Заметным явлением в теории поиска вывода была работа -"Алгорифмы машинного поиска логического вывода в исчислении высказывании" (19.65), написанная Паниным H.A., Давыдовым Г.В., Масловым С.Ю., Минцем Г.Е., Оревковым В.П.и Слисенко А.О.. Главная цель, к которои они стремились, состояла в том, чтобы разработать алгорифм, строящий возможно более естественные логические выводы на основе генценовских методов. Предложенный ими метод позволил преобразовать генценовский вариант секвенциальных исчислении, содержащий |Люгосукцедентные- секвенции в некоторый удобный вариант этого исчисления с односукцедентныии правилами, а затем последний бил сведен к натуральному исчислению с помощью введения ряда правил натурального вывода, удобному для автоматиг ческогс поиска доказательства.

Распрстранекие основной теореми Генцена на исчиление предикат ов с paienc'ifioM и Функционалист знаками псущестгил ¿ифшиц В.А, (1968). Основная идея состояла в том, чтобы все применения првзкд

с равенством были вше применении всех других правил, остальное доказательство совпадает с генценовским (1934).

Маслов С.Ю. (1967) предложил секвенциальный вариант конструктивного исчисления предикатов с функциональными знаками и равенством, не содержаний структурных правил. Оревков В. Г/, и Слисенко 1 0. (1965) построили машинный алгорифм установления выводимости на основе обратного метода.

В четЕегтом параграфе "Аналитические таблицы и блок таблицы . Смаллиана" рассматривания варианты табличных исчислений Бета и методов Уинтикки. ьсли аналитические таблицы хорошо известны в нашей литературе блогодаря учебнику логики Костюка В.Н. (1981),то о блок таблицах едви ли где-либо упоминается. О) них в общих чертах можно сказать лить то, что они совпадают с исчислениями Клини <53, но процесс построения выьода идет в противоположном направлении, то есть доказываемся 'формула является вершиной таблицы. От таблиц Бета их отличает то, что в этих таблицах точками дерева являются конечные множества формул, а не единичные формулы, и то, что каждый шаг в построении птих таблиц зависит исключительно от тех точек, которые на данный момент являются последними. Блок таблица называется закрытой, если каждая заключительная точка содер жит некоторый элемент и его отрицание (у Смаллиана - спряжение). Аналитические таблицы преобразуются в блок таблицы следующим образом: каждую точку закрытой аналитической таблицы заменяем на множество, содержащее эту точку и все точки, расположешие вмве нее в данной ветви, в результате получаем закрытую блок таблицу.

В третьей главе "1970 - Ь0-е годы. Новые модификации основной теоремы. Применения генценовских методов в неклассических логиках" рассматриваются доказательства основной теоремы, предложенные Смирновым В.А. (19/2), Драгалиным А.Г. (197У) и Серебрянниковым 0.$. (1УН7). Применению генценовских методов в модальной, паранепротиворечивой и релевантной логиках посвящены второй и третий параграфы данной главы.

В первом параграфе "-Обобщенное смешение. Прямые методы устранения сечения. 06]йтимость правил. Метод индексации." рассмотри ваются дальнейшие усиления и развитие генценовских методов.Методы устранения сечения в целом можно разделить на прямые и косвенные.

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

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

Дрьгалин ззедет доказательство Основной теоремы как доказательство о допустимости структурных правил. Серебрянников е своем доказательстве не использует параметр по числу сечений"в исходном выводе, а в качестве основной индукции применяет индукцию по числу вхождения фигур заключения в исходный вывод. Величина рента сечения определяется числом параметрических предков формулы сечения. Метод Серебрянникова не требует никаких дополнительных' условий относительно состояния исходного вывода, обратимости правил или элементарности аксиом, поэтому устранение сечения становится вполне естественной процедурой для широкого класса секвенциальных исчислений.

Далее рассматривается доказательство обратимости правил секвенциальных исчислений, принадлежащее КосоЕскому Н.К. (1981). Это доказательство распадается на два этапа: сначала доказывается допустимость структурных правил Еывода, а затем по методу обратной индукции обосновывается обратимость правил.

Завершает параграф изложение метода индексации предложенного Бродским И. Н.( 1988).

Во втором параграфе "Применение генценовских методов в исследованиях модальных систем" дан обзор наиболее существенных модификаций секвенциальных исчислений,с помощьв которые была доказана Основная теорема для всех модальных-систем. В особенности5 мы останавливаемся на решении этой П)облемы для систем 54.2 и вГ , 6 именно на методах предложенных Минцем Г.К. (19А), Сато И.(1980) и Серебрянникова О.Ф. (1987). Минц и Сато решили эту проблему лиаь частично,' поскольку введение ими прввмлв для оператора необходимости сохраняли печение в скрытой форме. Полное решение принадлежит Серебрянникову, который предложил новый хетод, связанней с использованием глобальных правил для модальных операторов.

Далее рассматривается сравнительный анализ твйличнчх к. индег. сньх систем, проделанный Быстровым П.И. Завешает параграф варя- , ант систе«н85" , построенный Уусталу Г. и Пентусом И. ^1989),

представляющий собой симбиоз -табличного и секвенциального исчис--лений..

Б третьем параграфе "Применение генценовских методов в иссле доЕаниях релевантных и паранепротиворечивых систем" рассматриваются системы секвенциальных исчислений приспособленных для реле вантных логик. А также исчисления Смирнова В.А. и Попова В.И. для паранепротиворечивых логик.

Ьсли для классических, интуиционистских и модельных логик удалось доказать теорему об устранении сечения, то для релевант- . них систём в общем случае она не проходит. Сложность решения этой проблемы, по- видимому, связана с определенной неестественностью самих релевантных систем. Правда для некоторых из них элиминационная теорема доказывается, в частности ото сделано для систем предложенных Серейршникэвьин 0.ё. (,1970), Смирновым В.А. (.1979), Быстровым П.И.(1987)-, Минцем Г.Е.(1972).

Далее рассматриваются секвенциальные исчисления В.А. Смирнова для паранепротиворечивых систем, являющихся раскиренчем систем Черыака и Гудмена, в которых паранепротиворечивыми логиками' называются системы, двойственные интуиционистским.

Попов В. М. (1989) предложил метод построения таких секвенциальных систем для пара ^противоречивых логик, который основан на идее вгедения не только отдельных логических констант, но и целых их комплексов.

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

Основные положения диссертации отражены в следующих публикациях: • '

I. К эволюции генценовских методов в логике (1930 - 50-е гг.) //Современная логика: Проблемы теории, истории и применения в на^ уке. Тезисы докладов научной конференции. чЛ. с.69 - 70." I. 1990. г.//

•2. Развитие генценовских методов в 1960 - 80 гг. -1.1990. Дел. в КНИОН АН СССР »44263 от 18.12. 1990 г.