Введение к работе
Актуальность темы исследования. Работы Герхарда Генцена "Исследования логических выводов" (1934), ''Непротиворечивость чистой теории чисел" (1936) и "Новое изложение доказательства непротиворечивости для чистой теории чисел" (1939) во многом определили состояние современной логики. Они имели фундаментальное значение для теории доказательств, внесшей существенный вклад в развитие математики, особенно в исследования по ее основаниям.Их влияние на различнее раздели современной математики продолжает возрастать. Не меньшее значение имеют гендеповские методы и для развития исследований по программе "искусственного интеллекта, прежде всего в такой ее области как теория и практика автоматического доказательства теорем. В настоящее время наблюдается усг. ливающееся влияние генценовских методов в такой новой v бкетро прогрессирующей области исследований как теоретическое программирование и различные его практические приложения.
Влияние развитой Г.Генценом теории естественного вывода выходит за пределы математической логики и оказыгает существенное воздействие на исследования ло легическсму анализу естественного языка, методологик науки и на йиглитическ}ю с|илосо^ию.
Хотя проз.л ) почти шестьдесят лет со времени опубликования классических трудов Генцена и список работ, посвященных иодннтим в них проблемам, исчисляется у«е не одной сотней названий, однако до сих пор нет исследований, содермуіх хотя бы краткий л5зор истории развития генценовских методов. Необходимость в такого рода исследованиях диктуется не только историкл-научными интересами, зни акт.альны также с точки зрения перспектив дальнейшего развития самих генценовских методов, поскольку нет работ, лосея-ііієнньіх анализу всех суцественных модификаций, приращений, усилений и упрощений, которые эти методи претерпели за указанный период. Напротив, наблюдается даже тенденция к утрате накопленного здесь опьта
Степень разработанности темы. Имеется превосходные работы по отдельные разделам темы настоящей диссертации. В "Журнале символической логики" проводится систематическая библиографическая раб/га по математической логике, правда, доведенная только до 19/5 года. Имеется фундаментальные исследования по натуральным, секвенциальном и табличньм методам, Клини U.K.( 1УЬ2, Vili),
_ ц _
'Карри X. (1948), (1963), Бета Э. (1955), Шютте К.( 1956,19/7), Правица Д. (1965,1971), Земана №. (1973), Смирнова В.А. (1972), Івкеути (1953).
Из работ, посвкщеннчх историческому обзору отдельных тем, отметим статью Минца Г.Е. о развитии теории доказательств в СССР (1988), Краизеля Г. - об исследованиях по теории доказательств (1981), Сереорянникова О.Ф. (1987), Правица Д. (1971), Сурми С. (1981), Радкио А. (1985), Йоргенсена И- (1938). Применению секвенциальных и табличных методов в модальной логике о середины 50-х - по начало 80-х годов посвящена диссертация Быстрова П.И. (1981). Попов В. И. (1979) дает обзор генценовских методов для релевантных систем.
-Важную рольдля.развития тема диссертации имели работы, свя-
занные со сравнительным анализом генценовских методов. Об отноше
нии натуральных и секвенциальных исчислений - это работы самого ГенценаГ. (1934,1939), Клини С.К. (1952, 1973), Карри Х.(1948, 1963), Правица'Д. (1965), Земана №. (1973). Смирнова В.А.(1972) Шанина Н.А. (1965), Сурмы С. (1981), Серебрянникова О.Ф. (1970), Роесера №. (1948), Минца Г.Е. (1988).
Сравнительный анализ различных секвенциальных исчислений, осуществлен Генценом (1934,1939), Клини С.К. (1952,1973), Карри X. (1963), Шольцем X. (1961), Хазенйегером Г. (1952, 1961), Шютте К. (1977), Сурыой С. (1981), Серебрянниковым О.Ф. (19/0,1979, 1967), Смирновым В.А. (1972,1979). .'.
Важными для понимания процеоса развития генценовских методов и применения их для исследования логических систем являетоя вопрос о разных способах доказательства Основной теоремы. Сравнительному анализу этих'способоЕ посвящены статьи или отдельные главы в работах таких авторов как Клини O.K. (, 1952,1973), КарриХ. (.1963), Смирнов В.А. ЧУ72), Серебрянников 0.«. (,1У79), Быстров . 1.1987, 1989),-Смаллчан Р. (1*68), Колмогоров А.Н. (.1982), Драгалин А.Г. (.1979, 1982), ічосоеский Н.К.(198Г), Кетонен 0. (ЇУЧЧ), Хазенйегер Г. (,Ь61), Уусталу Т. и Пентус М. (Д*89), Зе-ман №лЪП), Ладриер ».(,bbl), Шютте к.(.1У77) и Такеути Т.1978. Однако, разработке тепы Тенценовскив методы в логике" в том объеме и о той систематичностью, о которой шла речь вине, еще не реализована.
цели и задачи исследования. Цель диссертационной работы в том, чтебы дать связный исторический анвлиз развития -гєншиюві:-них методов и рассмотреть всь суіуествекние модификации и усиле-
ния, которые они претерпели до наших дней. В соответствии с этой целью ставятся следующие задачи:
рассмотреть исторические, философские и логические предпосылки возникновения натуральних и секвенциальных исчислений;
собрать и систематизировать все известные на сегодня варианты секвенциальных и табличных исчислений;
дать сравнительный анализ вышеуказанных методов и их модификаций;
произвести сравнительный анализ методов доказательства Основной теоремы;
рассмотреть те трудности, которые возникают при доказательстве Основной теоремы для модальных, релевантных и паранепротиворе-чивых логик.
Методологической основой диссертации являются раооты отечественных и зарубежных логиков, философов и историков науки. При решении частных задач, применялись методы исторической рекнстру-кции лингвистического анализа, аппарат математической логики.
Научная новизна диссертации состоит з следующем:
воссоздана целостная история развития генценовских методов; удалось включить в общую картину, ранее не рассматриваемые в этой связи, работи и целые направления исследований;
проанализирован различные тактики поиска еыводэ и различия между секвенциальными исчислениями рассмотрены в связи с особенностями этих тактик, предметом специального рассмотрения стали различные методы доказательства обратимости правил вывода;
проанализированы исторические приоритеты совершенствования генценовских методов;
найдено ревиние проблемы доказательства Основной теоремы прямым методом Серебрянникова 0.. для систен без структурных правил.
Теоретическое и практическое значение диссертационного исследования заключается, по мнения автора, в следующем: во-первых, работа способствует более ясному пониманию особенностей истории современной логики, в одной из ее наиболее важных областей - теории доказательств; 'во-вторых, детально знакомит с малоизвестными, но важными работами отечественных и зарубежных авторов; з-третьих, материалы данной диссертации можно использовать в учебных курсах "История современной логики" и "Теория естественного вывода".
- б -
Основные положения диссертации просіли апробацию в докладах на научной конференции "Современная чогика: проблемы теории, истории и применения в науке" /Ленинград, май, 1990 г./, на теоретическом семинаре испирантов кафедры логики ЯГУ /декабрь, 1989 г./
Структура работы. Диссертация состоит из введения, трех глав, заключения и библиографии.
