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

  • Год: 2004
  • Автор научной работы: Ходикова, Нина Анатольевна
  • Ученая cтепень: кандидата философских наук
  • Место защиты диссертации: Калининград
  • Код cпециальности ВАК: 09.00.07
450 руб.
Диссертация по философии на тему 'Логико-методологическое исследование происхождения теории поиска вывода'

Полный текст автореферата диссертации по теме "Логико-методологическое исследование происхождения теории поиска вывода"

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

Ходикова Нина Анатольевна

Логико-методологическое исследование происхождения теории поиска вывода

09.00.07-логика

Автореферат диссертации на соискание ученой степени кандидата философских наук

Калининград - 2004

Работа выполнена в Калининградском государственном университете.

Научный руководитель: Официальные оппоненты:

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

доктор философских наук, профессор Брюшинкин Владимир Никифорович

доктор философских наук, профессор Маркин Владимир Ильич

кандидат философских наук, доцент Мухачев Виктор Павлович

Институт математики Сибирского отделения РАН

Защита состоится «07 _» декабря 2004 г. в 15.00 на заседании диссертационного совета К.212.084.09 по защите диссертаций на соискание ученой степени кандидата философских наук в Калининградском государственном университете по адресу: г.Калининград, ул. Чернышевского, 56, ауд. 130.

С диссертацией можно ознакомиться в библиотеке Калининградского государственного университета (236040, г. Калининград, ул.Университетская, 2).

Автореферат разослан ноября 2004 г.

Ученый секретарь диссертационного совета

Н.В.Андрейчук

Общая характеристика работы

Актуальность исследования

Наука как вид профессиональной деятельности

существует

сравнительно недавно, всего около четырех столетий. Но важность этого вида деятельности для общества была осознана почти одновременно с его появлением, и вслед за наукой возникла история науки как особая дисциплина, занимающаяся описанием научных достижений, открытий, поисков и даже ошибок. Долгое время историко-научные исследования представляли собой по преимуществу биографии великих ученых с подробным описанием их достижений и ошибок. Основой изложения служила хронология, и молчаливо предполагалось, что такой порядок компоновки материала сам по себе обеспечивает отображение внутренней логики развития научной мысли. Таким образом, история науки представлялась как история идей. С другой стороны, до 50-х годов XX века в исследованиях по методологии науки преобладали проблемы, связанные с анализом понятийного аппарата науки, схем обоснования знания, структуры теорий, логики индуктивного и дедуктивного вывода, эмпирического содержания теоретического знания. Проблема изучения законов изменения теорий, природы научных революций, особенностей развития научного знания впервые отчетливо выдвигается на первый план в работах К.Поппера. В дальнейшем его идеи рациональной реконструкции развития научных теорий были развиты и в некотором смысле пересмотрены в методологических концепциях Т. Куна, К.Лакатоса, П.Фейерабенда, Дж.Агасси.

Известный советский методолог науки Б.С. Грязное на основании критического анализа постпозитивистских методологических концепций разработал оригинальную модель происхождения научных теорий. Ключевым понятием этой модели является понятие «поризм». На естественнонаучном (и, частично, математическом) материале Грязное показал, что непредвиденное следствие, полученное в ходе решения задачи в рамках имеющейся теории, при выполнении определенных условий может привести к появлению новой теории. Истолкование ядра новой теории как логического, но, тем не менее, неожиданного, непредвиденного, следствия предыдущей теории, открывает путь к построению рациональной реконструкции происхождения новой научной теории.

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

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

В данном исследовании рассматривается вопрос о происхождении одной из сравнительно молодых логических теорий (появившейся в 70-х г.г. XX века) - теории поиска вывода. Идейный создатель теории поиска вывода С.Ю.Маслов определял ее как область математической логики, занимающуюся «выявлением по исчислению и объекту в языке исчисления структуры возможных выводов этого объекта»2. Другими словами, теория поиска вывода исследует возможные способы решения задач в различных исчислениях. Теория поиска вывода является пограничной дисциплиной комплекса computer science - она стоит на стыке логики, психологии и эвристики. Поэтому помимо активного практического применения, она находит интересные теоретические приложения в философии3 и психологии творчества4. Применение поризматической модели развития научного знания к возникновению теории поиска вывода позволит более полно осмыслить особенности основных идей и методов этой теории, очертить круг решаемых в ней задач. Вместе с тем, успешное решение задачи представления возникновения одной логической теории на основе другой (теории поиска вывода на основе гильбертовской теории доказательств) порождает новый взгляд на историю логики вообще - как на историю смены и преемственности теорий. Степень разработанности темы

Основные положения теории поиска вывода были сформулированы СЮ. Масловым в его работах 70-х годов XX века5. Отдельные аспекты

Kneale, William, Kneale, Marta. The Development of Logic / William Kneale, Marta Kneale. - Oxford: At the Clarendon Press, 1964. P. V. - 761 p. - Bibliography; p. 743-751.

1 Маслов, С.Ю. Теория дедуктивных систем и ее применения / Сергей Юрьевич Маслов. - М.: Радио и связь, 1986.-С.93.

3 Брюшинкин, В.Н. Логика, мышление, информация / Владимир Никифорович Брюшинкин. - JI.: Изд-во Ленинградского ун-та, 1988. - 152 с. - ISBN 5-288-00158-8.

4 Маслов, CJO. Теория дедуктивных систем и ее применения. М.: Радио и связь, 1986; Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества // Семиотика и информатика,- М.,1979. Вып. 13. С. 17-46.

5 Маслов, С.Ю. Теория дедуктивных систем и ее применения. М.: Радио и связь, 1986, Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества // Семиотика и информатика,- М.,1979. Вып. 13. С. 17-14.

теории поиска вывода и ее приложений разрабатывались В.Н. Брюшинкиным6 и С.Л. Катречко7.

Вопросы о возникновении научного знания, о преемственности и смене научных теорий являются ключевыми в философии науки постпозитивизма. Идеи фальсификационизма, предложенные К.Поппером8 развиты в таких методологических схемах, как теория «исследовательских программ» И.Лакатоса9, теория «нормальной» и «кризисной» науки Т.Куна10 и теория несоизмеримости П.Фейерабенда11. В советской и российской методологии вопросам развития научного знания также уделяется достаточно большое внимание. В частности, Е.К.Войшвилло рассматривает процессы, приводящие к смене научных теорий и те отношения, которые возникают между старой и новой теорией в свете принципа соответствия.12 Критический анализ постпозитивистских концепций и изложение некоторых аспектов проблемы смены и преемственности научных теорий содержится также в работах В.Н. Садовского13, В.А. Смирнова , А.Л. Никифорова15, Ю.А. Петрова16. Значительный и оригинальный вклад в исследование сущности научной теории, ее предметной области и объекта, в закономерности функционирования теории как сложной системы внесли работы

' Брюшинкин, В.Н. Логика, мышление, информация. - Л.: Изд-во Ленинградского ун-та, 1988; Брюшинкин, В.Н. О возникновении теорий в логике: теория поиска вывода как поризм // Современная логика: Проблемы теории, истории и применения в науке: Сб. науч. тр. / Под. ред. АЛ Слинина.- Л.: Изд-во Ленинградского ун-та, 1990. С.17-18; Брюшинкин В.Н. О методологическом значении различения понятий "вывод" и "поиск вывода" / Философские науки, 1984. № 4. С. 49-54.

7 Катречко, CJL Логический анализ интеллектуальных систем с метапроцедурами: Дис.... канд. филос. наук. • М„ 1992.

' Popper, Karl R. The Logic of Scientific Discovery. London and New Yoik: TJ. Press (Padstow) Ltd, 1995. -479 P. - ISBN 0-415-07892-x.

9 Лакатос, Имре. Фальсификация и методология научно-исследовательских программ / Имре Лакатос; пер. с англ. с прим. и пред. В.Поруса; худ. В. Михельсон. Московский философский фовд. - М.; Медиум, 1995.-236е.- ISBN5-85691-040-0.

10 Кун, Т. Структура научных революций / Т. Кущ пер. с англ. И.З. Налетова. - М.: Прогресс, 1975. - 288 с.-Указ.:с. 283-287.

" Фейерабенд, П. Избранные труды по методологии науки / Пол Фейерабенд; пер. с англ. и нем. А Л.Никифорова; общ. ред. и вст. ст. И.С. Нарского. М.: Прогресс, 1986. - 543 е., ил. - Библиогр.: с.524-537.

12 Войшвилло, Е.К. Принцип соответствия как форма развития знаний и понятие относительной истины. Критика концепции несоизмеримости сменяющих друг друга теорий // Логика и В.Е.К.: Сб. науч.тр / Под ред. В.И. Маркина и др. - М.: Современные тетради, 2003. - 256 с. С.11-22.

Садовский, В.Н. Карл Поппер и Россия / Садовский Вадим Николаевич. - М.: Эдиториал УРСС, 2002. - 280 с. - Библиогр.: с. 247- 259. - ISBN 5-8360-0324-6.

14 Смирнов, В.А. Логические методы анализа научного знания / Владимир Александрович Смирнов; М.: Наука, 1987. - 255 с. - (Институт философии АН СССР). - Библиогр.: с. 248-254.

15 Никифоров, A Л. От формальной логики к истории науки: критический анализ буржуазной методологии науки / Александр Леонидович Никифоров. Институт философии АН СССР. - М.: Наука, 1983.-177 с.

14 Петров, Ю.А. Проблема соизмеримости теорий// Филос. Науки, 1986. №4. - С. 61-70.

Б.С.Грязнова . Следствием общих методологических установок Грязнова стала его оригинальная поризматическая модель происхождения научных теорий. Применимость этой модели к возникновению одних естественнонаучных теорий на базе других демонстрируется в работах Грязнова на убедительных примерах. Однако о возможности применения своей модели к математическому знанию Грязнов замечает вскользь, упоминая непредвиденное, но вполне закономерное появление в математике отрицательных и комплексных чисел. Что касается логических теорий, то применимость своей модели к их возникновению Грязнов не рассматривал вовсе. Вообще, вопрос о смене теорий в логике с общих методологических позиций в истории логики практически не рассматривался. Исключение составляет подход Е.К. Войшвилло к происхождению релевантной логики из классической логики (высказываний или предикатов) за счет уточнения понятия логического следования для формул языка классической логики. Идея о возможности применения поризматической модели Грязнова к возникновению теорий в логике, в частности, к возникновению теории поиска вывода из гильбертовской теории доказательств, была впервые изложена в работах В.Н. Брюшинкина. Цели и задачи исследования

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

Для достижения этой цели ставятся и решаются следующие задачи:

• Реконструировать и уточнить систему методологических взглядов лежащих в основе предложенной Б.С. Грязновым поризматической теории происхождения научной теории и показать ее применимость в области дедуктивных наук, в частности, в математике;

• Осуществить методологический анализ гильбертовской теории доказательств, выделить предметную область и объект этой теории;

• Провести историко-логическую реконструкцию возникновения свойства подформульности в ходе решения задачи доказательства непротиворечивости арифметики в рамках гильбертовской

17

Грязнов, B.C. Логика. Рациональность. Творчество / Борис Семенович Грязное; отв. ред. И.С. Тимофеев; сост. К.В. Малиновская, Н.И. Кузнецова, Е.Г1. Никитин. - М.: Наука, 1982. - 235 с.

18 Брюшинкин, В.Н. О возникновении теорий в логике: теория поиска вывода как поризм // Современная логика: Проблемы теории, истории и применения в науке: Сб. науч. тр. / Под. ред. А Я Слинина. - Л.: Изд-во Ленинградского ун-та, 1990. С.17-18.

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

• Проанализировать первые теоретические попытки использования систем, обладающих свойством подформульности для определения процедур поиска вывода (Э. Бет, Я. Хинтикка);

• Рассмотреть первые попытки построения процедур автоматического доказательства теорем: программа «Логик-теоретик», не использующая свойства подформульности, и программа Хао Вана, основанная на свойстве подформульности. Провести сравнительный анализ эффективности этих программ;

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

• Выявить на основе работ СЮ. Маслова основные особенности метода резолюций и обратного метода: аналитичность, метапеременность, локальность;

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

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

Научная новизна полученных результатов

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

• реконструирована и уточнена система методологических взглядов лежащих в основе предложенной Б. С. Грязновым поризматической теории происхождения научной теории и показана ее применимость в области дедуктивных наук, в частности, в математике, обоснован тезис о том, что на место эмпирической интерпретации,

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

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

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

• разработан новый подход к интерпретации свойства подформульности как поризма состоящий в различении двух составляющих: 1) внутренней теоретической интерпретации поризма, 2) внешней «квазиэмпирической» интерпретации поризма как новой области задач, которая включает поризм в новую систему понятий, следствием чего является появление нового теоретического объекта и возникновение новой теории;

• проанализированы первые теоретические попытки использования систем, обладающих свойством подформульности для определения процедур поиска вывода (Э. Бет, Я. Хинтикка); показано, что «чисто теоретическая» интерпретация этих процедур не приводит к возникновению новой теории;

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

• установлено, что аналитическая интерпретация доказательства (рассмотрение «снизу вверх»), в конечном счете, порождает новый теоретический объект - дерево поиска вывода,

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

Теоретическая и методологическая основа исследования

Методологической основой исследования является аппарат современной логики, теории познания, методологии науки, эвристики. Решающее влияние на идею и результаты исследования оказали методологические и логические исследования Б.С. Грязнова и В.Н. Брюшинкина, а также разработка теории поиска вывода, предпринятая в трудах С.Ю.Маслова. Теоретической основой исследования являются труды по основаниям математики Д.Хильберта, И.Бернайса; логико-математические работы Ж.Эрбрана, Г.Генцена, С.К.Клини, Я.Хинтикки, Э.Бета, Р.Смальяна, Д.Правица, С.Кангера, Д.Пойа, О.Ф.Серебрянникова, В.А Смирнова, Е.Д. Смирновой, Е.К.Войшвилло, С.С.Гончарова, Ю.Л.Ершова, К.Ф.Самохвалова. Важную роль в диссертационном исследовании сыграли логико-философское исследование теории поиска вывода, проведенное С.Л. Катречко, историко-логические исследования Н.И. Стяжкина, У. и М. Нил; исследования по современной реконструкции аристотелевской силлогистики и других теорий, сыгравших важную роль в истории логики, В.А. Бочарова и В.И. Маркина. Труды Л.А. Микешиной по философии познания оказали решающее влияние на осмысление понятий «интерпретация» и «рациональность». Автор опирался также на работы специалистов в области программирования и «искусственного интеллекта»: Н.Нильсона, Хао Вана, А.Ньюэлла, Дж.Шоу, Г.Саймона, Дж.Робинсона.

Практическая значимость исследования.

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

Результаты исследования могут быть использованы для разработки курса «Истории логики», «Философские проблемы математики»,

спецкурсов «Логические проблемы искусственного интеллекта» и «Теория поиска вывода». Апробация диссертации

Диссертация обсуждена на заседании кафедры философии и логики исторического факультета КГУ и рекомендована к защите. Основные положения диссертации изложены в ряде публикаций общим объемом 1,7 п.л. (см. список), представлены на УШ Международных Кантовских чтениях (Светлогорск, 1999), обсуждались на постоянном научном семинаре кафедры философии и логики, использовались для разработки курсов символической логики и математики для студентов философского отделения исторического факультета КГУ.

Структура диссертации. Диссертационное исследование изложено на 167 страницах и состоит из введения, четырех глав, заключения и списка литературы (106 названий).

Общее содержание диссертационной работы

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

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

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

19

истории науки .

Однако определенные возможности для рассмотрения «теоретической» истории логики появились в металогических исследованиях XX века в связи с появлением гильбертовской теории доказательств. Эта теория демонстрирует определенное сходство со стандартным понятием научной теории, как она используется в методологии науки. Это дает нам возможность применить к ней аппарат, выработанный в методологических учениях XX века. Вместе с тем в 70-х годах XX века в логике возникла теория поиска вывода, основные положения которой сформулированы в работах СЮ. Маслова. Проблематика этой новой теории связана с гильбертовской теорией доказательств, что позволяет нам поставить вопрос о соотношении этих теорий и их преемственности. В качестве модели, в рамках которой будет рассматриваться происхождение теории поиска вывода из гильбертовской теории доказательств, выбрана концепция рациональной реконструкции возникновения научных теорий, предложенная известным советским философом и методологом Б.С. Грязновым. Целью второго параграфа «Б.С. Грязнов о рациональной реконструкции развития науки» является рассмотрение понятия рациональности знания и ответ на вопрос - как возможна рациональная реконструкция развития научного знания. В качестве тех требований, которым должно удовлетворять рационально организованное знание, Б.С. Грязнов выделяет гомогенность, замкнутость и наличие причинно-следственной структуры20. Он выделяет в структуре научного знания язык науки и его интерпретацию, а взаимодействие между ними рассматривает как некоторое согласование. В силу определенной самостоятельности функционирования и развития языка и интерпретации, может оказаться, что процессы в сфере языка (происходящие строго по законам данной области) со временем приводят к результатам, не согласующимся с областью интерпретации. Необходимость изменения интерпретации таким образом, чтобы вновь возникшие языковые конструкции получили смысл, может приводить к возникновению новых научных теорий. Третий параграф «Модель происхождения научной теории Грязнова и ее значение для логики и математики» посвящен анализу модели происхождения научных теорий, предложенной Б.С.

19 См. Лакатос, И. Фальсификация и методология научно-исследовательских программ / Пер. с англ. и пред. В.Поруса. - М.: Медиум, 1995; Поппер, К.Р. Логика и рост научного знания: избр. раб. / Карл Раймунд Поппер; пер. с англ., сост., общ. ред. и вступ. ст. В. Садовского. - М.: Прогресс, 1983. - 60S с; Кун, Т.С. Структура научных революций. - М.: Прогресс, 1975.

20 Грязнов, Б.С. Логика. Рациональность. Творчество. - М.: Наука, 1982. - С.103.

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

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

Важным этапом отражаемого этой схемой процесса является устранение рассогласования между языком и интерпретацией. В качестве примера реализации описанной поризматической схемы возникновения новой теории реконструируется возникновение понятия комплексного числа, и появление в дальнейшем теории комплексных чисел. Во второй главе «Логическая теория доказательств: непротиворечивость и подформульность» выполнен первый этап реконструкции возникновения теории поиска вывода. В первом параграфе «Гильбертовская теория доказательств и непротиворечивость» рассматриваются главные этапы развития гильбертовской теории доказательств, рассматриваемой в рамках поризматической модели в качестве исходной теории, осуществляется ее методологический анализ. После обнаружения парадоксов теории множеств были предложены различные варианты их устранения, и тем самым, способы обоснования математики, необходимость которого ясно продемонстрировали антиномии. Одной из основных проблем обоснования математики является доказательство непротиворечивости различных математических систем. Традиционный метод проведения таких доказательств состоит в указании модели рассматриваемой теории, взятой из некоторой теории, непротиворечивость которой не вызывает сомнений. Однако, для теории множеств невозможно построение метатеории, обладающей большей надежностью, чем она сама. Гильберт предложил новый метод обоснования теории множеств, получивший название формалистической программы. Он предложил показать, что применяемые в математике методы доказательства достаточно сильны для того, чтобы получить всю классическую математику, в том числе всю канторовскую теорию множеств, исходя из подходящим образом выбранных аксиом, но не настолько сильны, чтобы вывести из аксиом противоречие. Рассуждения, посредством которых должна быть доказано

это утверждение должны быть настолько элементарными, чтобы в их справедливости невозможно было усомниться (такие рассуждения Гильберт назвал финитными). Метатеория, в рамках которой предполагалось исследовать методы математических доказательств, была названа Гильбертом метаматематикой или теорией доказательств. Особый интерес представляет методологический анализ этой своеобразной «металогической» теории. Для теории доказательств предметной областью исследования являются реальные доказательства, изобретаемые в содержательных математических теориях. Вместе с тем гильбертовская теория доказательств создает новый объект - формальное доказательство в некотором логико-математическом исчислении. Формальное доказательство в таком случае представляет собой результат абстракции от реальных математических доказательств свойства формальной выводимости теоремы из аксиом теории, представленное в виде синтаксической последовательности формул языка данного исчисления, каждая из которых является либо аксиомой исчисления, либо выводима из предыдущих по явно сформулированным в исчислении правилам вывода. Однако доказательство в логико-математическом исчислении является формальным синтаксическим объектом, а теория доказательств или метаматематика является содержательной теорией о формальных системах. Это означает, что для того, чтобы формальное доказательство стало абстрактным объектом, представляющим объект некоторой теории, оно должно быть интерпретировано, то есть ему должен быть приписан смысл, определяющий место этого объекта в теории. Для Гильберта смысл формальному доказательству придавался его связью с аксиоматическим методом. Аксиоматическое построение теории означает определенную интерпретацию доказательства как движения по нисходящему ряду, от основания к следствию, «сверху вниз», или если вспомнить античную интерпретацию математических доказательств, данную в александрийской математической школе, синтетическое построение доказательства. Во времена создания гильбертовской теории доказательств аксиоматическое построение было единственным известным способом задания логико-математических теорий. Поэтому рассмотрение формального объекта «доказательство» вместе с синтетическим способом его построения «сверху вниз» традиционно воспринималось как нечто само собой разумеющееся. На этом основании можно заключить, что объектом гильбертовской теории доказательств является понятие формального доказательства, которому придана «синтетическая» или «нисходящая» интерпретация.

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

Г-+®,Р ДА-»А

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

рассматриваемой модели, это обстоятельство вводит новую аналитическую интерпретацию основного объекта гильбертовской теории доказательств - формального доказательства. Поскольку объект гильбертовской теории доказательств представляет собой понятие формального доказательства вместе с его синтетической интерпретацией «сверху вниз», возможность новой аналитической интерпретации создает возможность нового теоретического объекта. Поскольку же синтетическая и аналитическая интерпретации противоположны, то новый теоретический объект означает рассогласование с первоначальной интерпретацией объекта теории доказательств и требует развития нового взгляда на доказательства в секвенциальных исчислениях как на объекты, обладающие важными «аналитическими» свойствами. Построение доказательства, обладающего свойством подформульности, «снизу вверх» реализует некоторую элементарную стратегию поиска доказательства, в которой структура доказываемой секвенции и выделение в ней главного знака почти однозначно21 определяют следующий шаг построения доказательства. Тем самым построение доказательства исходной секвенции «снизу вверх» включает в себя формализацию некоторой стратегии обнаружения доказательства, а значит, порождает возможность нового теоретического объекта - поиска вывода. Третий параграф «Использование свойства подформульности в теоретической логике: таблицы Бета и модельные множества Хинтикки» содержит анализ условий, необходимых для определения процедур поиска вывода на основе свойства подформульности. Выполнение принципа подформульности позволяет доказывать секвенции, применяя фигуры заключения «снизу вверх». Однако сам Генцен не формулирует идею организации поиска доказательства, основанного на принципе подформульности. В свете поризматической модели происхождения теории этот факт объясняется тем обстоятельством, что он решал задачу (доказательство непротиворечивости), поставленную еще в исходной теории -гильбертовской теории доказательств. Задача доказательства непротиворечивости относится к метауровню формальной системы и решается при помощи обоснования утверждения об исчислении в целом. Для определения процедур поиска вывода на основе свойства подформульности нужно было сформулировать новую цель исследовательской деятельности — построение доказательства в самом исчислении. Хотя эта цель уже неявно содержалась в аналитической

21 За исключением применения так называемых минус-правил: правил введения квантора общности в антецедент и введения квантора существования в сукцедент секвенции.

интерпретации формального доказательства, ее надо было явно сформулировать для того, чтобы на основании свойства подформульности определить процедуры поиска вывода22. Такого рода интерпретация исчислений секвенциального типа появилась не у Генцена, а позднее - в середине 50-х годов - в работах голландского логика Э. Бета и финского логика Я. Хинтикки. Метод семантических таблиц Э.Бета и аппарат модельных множеств Я. Хинтикки реализуют свойство подформульности в системах без сечения для построения доказательства «снизу вверх». Таким образом, можно говорить о том, что пройден первый этап интерпретации свойства подформульности как поризма - внутренняя теоретическая интерпретация. Однако цели, которые ставили и Бет, и Хинтикка в целом не выходят за рамки теории доказательств. Не случайно и семантические таблицы и модельные множества были использованы их авторами для доказательства метатеорем исчисления предикатов таких, как, например, полнота этого исчисления. Иначе говоря, новые методы были применены для решения задач, поставленных еще в теории доказательств, и тем самым не привели к осознанию поиска вывода как нового теоретического объекта, отличного от формального доказательства в некотором исчислении.

Для превращения непредвиденного следствия в новую теорию, необходимо включение поризма в новую систему задач и понятий. Такого рода включение достигается при помощи интерпретации поризма на новой предметной области или области задач. Такой областью стало автоматическое доказательство теорем на ЭВМ.

Третья глава «Автоматическое доказательство логико-математических теорем и формализация эвристик» посвящена реконструкции истории автоматического доказательства теорем и анализу этой области задач как внешней «квазиэмпирической» области интерпретации свойства подформульности, которая обеспечивает его включение в новую систему понятий, что, в конечном счете, и приводит к возникновению новой теории - теории поиска вывода. Первые работы по автоматическому доказательству теорем появились в середине 50-х гг. Можно выделить два основных подхода к решению задачи автоматического доказательства теорем: первый предполагает работу в аксиоматических исчислениях с использованием некоторых специальных методов (эвристик); второй использует свойство подформульности в секвенциальных исчислениях без сечений. В первом направлении работали А.Ньюэлл, Дж.Шоу и Г.Саймон, а также Гелернтер и Рочестер. Анализу этого направления

п О характере поиска вывода как вида деятельности и его отличии от доказательства см. Брюшинкин, В.Н. О методологическом значении различения понятий "вывод" и "поиск вывода". // Философские науки, 1984, № 4. - С. 49-54.

посвящен первый параграф «Ранняя история автоматического доказательства: программа «Логик-теоретик»». Во втором параграфе «Применение секвенциальных исчислений: процедура Хао Вана» на примере программ, написанных Хао Ваном, анализируется подход к автоматическому доказательству теорем, связанный с реализацией свойства подформульности. Уже первые результаты исследований показали, что возможность эффективно доказывать теоремы логики высказываний и логики предикатов может дать лишь использование систем, свободных от сечений. Поскольку для исчисления предикатов не существует процедуры разрешения, то из этой области нельзя полностью исключить потенциально бесконечный перебор подстановок. Одним из путей преодоления этих трудностей может быть использование метода метапеременных, идея и пример применения которого приводится в третьем параграфе «Идея метапеременности в процедуре Кангера». Формулировка и применение такой плодотворной для организации поиска вывода идеи, как введение метапеременных, оказалось возможным возможно только при рассмотрении поиска вывода снизу вверх, основанном на свойстве подформульности. В четвертом параграфе «Методы автоматического доказательства, основанные на теореме Эрбрана» рассматриваются метод автоматического доказательства, предложенный Гилмором и его модификация, выполненная Девисом и Патнемом. Теорема Эрбрана позволяет «сводить процесс поиска вывода произвольной формулы А классического исчисления предикатов (без равенства) к процессу поиска формулы, выводимой средствами классического исчисления высказываний, среди членов некоторой последовательности бескванторных формул, структура которых тесно связана со структурой формулы А».233 Появление генцено-эрбрановских методов знаменует важный этап развития автоматического доказательства теорем. Решительное продвижение на пути к созданию предметной области теории поиска вывода и выделению специфических понятий и методов теории поиска вывода было достигнуто в связи с формулировкой универсальных методов поиска вывода - метода резолюций Дж. Робинсона и обратного метода С Ю. Маслова. Анализу этих методов посвящен пятый параграф «Универсальные методы поиска доказательства: метод резолюций и обратный метод». Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество дизъюнктов S пустой дизъюнкт D. Если содержит, то S невыполнимо. Шаги доказательства

23 Минц, Г.Е. Теорема Эрбрана / Г.Е. Минц II Математическая теория логического вывода: сб. перев. / Под ред. A.B. Идельсона и Г.Е. Минца. - М.: Наука, Глав. ред. физико - математической литературы, 1967. С. 311.

невыполнимости множества 8 могут быть представлены в виде растущего вверх дерева вывода, в котором каждому начальному узлу приписывается дизъюнкт из 8, а каждому следующему - резольвента дизъюнктов, приписанных к его непосредственным предшественникам. Если корневому узлу дерева вывода приписан дизъюнкт К, то это дерево есть дерево вывода дизъюнкта R. Метод резолюций, так же как и обратный метод является локальным методом с метапеременностъю. Идеи метапеременности и локальности обработки информации позволяют повысить «эвристичность» генценовского исчисления, то есть сделать поиск вывода, основанный на свойстве подформульности, более эффективным. Необходимость использования метода метапеременных обусловлена наличием в исчислении правил типа сечения (с-правил), то есть таких правил у которых при фиксированном

возможно бесконечное число различных наборов посылок Если

допустить некоторое изменение языка и вида выводимых в исчислении объектов, окажется возможным такое устранение с-правил, что качество результирующего вывода не пострадает. Такое изменение исчисления связано с использованием метода метапеременных. Метод метапеременных состоит в явном введении собственных переменных справил в язык исчисления. Значения таких переменных при контрприменении правил не уточняются сразу, при этом постепенно строится «снизу вверх» заготовка вывода. Для нее время от времени проверяется, можно ли подобрать значения метапеременных, превращающие ее в настоящий вывод. Идея использования метапеременных для построения «снизу вверх» не вывода, а его заготовки оказалась весьма эффективной, хотя и потребовала дополнительно привлечения принципа локальной обработки информации. Этот принцип состоит в том, что правила вывода в исчислении должны быть «локальными», то есть их применение требует обработки лишь части информации о построенном к данному моменту дереве поиска вывода. Видимо, наиболее перспективными являются такие методы поиска вывода, которые сочетают локальный принцип обработки информации и основную идею метода метапеременных: не большую уточненность значений термов, чем это необходимо в данный момент. К таким методам относятся метод резолюций и обратный метод. Как показано С.Ю.Масловым, обратный метод можно распространить на произвольные секвенциальные исчисления без правил сечения (то есть обладающие свойством

подформульности).

Четвертая глава «Теория поиска вывода и ее происхождение из теории доказательств» посвящена реконструкции возникновения теории поиска вывода в рамках поризматической модели. В первом параграфе «Логические алгоритмы и эвристики: подход О.Ф. Серебрянникова» рассмотрен теоретический подход к способам формализации эвристик в исчислениях секвенциального типа, предложенный

О.Ф.Серебрянниковым24. На основании анализа эвристических свойств аксиоматических, натуральных и секвенциальных исчислений можно сделать вывод о том, что, определяя возможность построения алгоритма поиска вывода, основанного на применении правил вывода «снизу вверх», свойство подформульности вместе с тем является фактически формализацией определенного эвристического принципа в самом логическом исчислении. Второй параграф «Теория поиска вывода: подход СЮ. Маслова» содержит анализ обобщения основных идей универсальных методов поиска вывода - аналитичности, локальности и метапеременности - на аппарат канонических исчислений Поста. Если некоторая система может быть смоделирована посредством исчисления общего типа, то процессы, происходящие в ней, можно представить как процессы поиска вывода. В этом случае аппаратом получения результата является теория поиска вывода. Поиску вывода препятствует наличие в исчислениях правил типа сечения или с-правил. Устранение с-правил из нелогических исчислений с целью обеспечения подформульности является необходимым условием для решения тех задач, которые ставятся перед теорией поиска вывода. Обе основные идеи обратного метода для исчисления С - метапеременность и принцип локальной обработки информации применимы и к исчислениям, не являющимся логико-математическими. В третьем параграфе «Приложения теории поиска вывода в психологии и философии логики» рассматриваются возможные направления теоретического применения идей и методов теории поиска вывода. Имеется аналогия между методами теории поиска вывода и способами, вырабатываемыми человеком при решении конкретных творческих задач и классов таких задач. Автоматизация элементов интеллектуальной деятельности является одним из основных направлений развития теории поиска вывода. Совокупность всех идей и методов теории поиска вывода может рассматриваться как своеобразная модель человеческого интеллекта, отражающая некоторые его важные свойства. Так, можно говорить о возможности моделирования в терминах теории

24 Серебрянников, О.Ф. Эвристические принципы и логические исчисления / Олег Федорович Серебрянников; отв. ред. Б.В. Бирюков. - М.: Наука, 1970. - 282 с. - Библиогр.: с.280-282.

поиска вывода некоторых известных результатов по функциональной асимметрии полушарий человеческого мозга.25 Идеи теории поиска вывода позволяют также находить новые решения ряда проблем философии логики. Теория поиска вывода с ее идеями и методами дала тот аппарат, который позволил сформулировать и обосновать новую концепцию в философии логики - концепцию метапсихологизма . В четвертом параграфе «Рациональная реконструкция происхождения теории поиска вывода в свете поризматической модели возникновения научных теорий» уточняется и детализируется на основании рассмотренного историко-логического материала поризматическая модель Б.С.Грязнова, особенно та часть этой модели, где идет речь об интерпретации поризма. Специфика интерпретации поризма в логико-математических теориях состоит в том, что логико-математические науки, в отличие от эмпирических наук, не предполагают эмпирической проверки теорий и связанной с ней эмпирической интерпретации. Проанализированный в данной диссертации процесс возникновения теории поиска вывода показывает, что на место такой эмпирической интерпретации в логико-математических науках заступает интерпретация на новой области задач или объектов. Итак, для возникновения теории поиска вывода, было необходимо выполнение двух условий: обнаружение свойства подформулъности и наличие новой области задач (автоматическое доказательство теорем), которая обеспечила «квазиэмпирическую» интерпретацию нового теоретического объекта, выявление его свойств и распространение этих свойств на более широкий класс дедуктивных систем, что и привело к возникновению теории поиска вывода.

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

Основное содержание диссертации изложено в следующих работах автора:

1. Значение теории поиска вывода для философии и психологии творчества // Материалы VIII Международных Кантовских чтений, посвященных 275-летию И.Канта. Калининград: Калининградский ун-т, 1999. С. 33-34. -Библиогр.: с. 34. 0,1 п.л.

2. Истоки возникновения теории поиска вывода: доказательство непротиворечивости арифметики // Критическое мышление, логика,

и См.: Маслов, С.Ю, Теория дедуктивных систем и ее применения. - М: Радио и связь, 1986 С.И6. 26 См.: Брюшинкин, В Н. Логика, мышление, информация. - Л.: Изд-во Ленинградского ун-та, 1988. С.39-66.

аргументация. Калининград: Изд-во КГУ, 2003. С. 147-156. -Библиогр.: с. 156.0,6 п.л.

3. Значение поризматической модели развития научных теорий для рациональной реконструкции происхождения теории поиска вывода // Модели мира. Исследования по логике, аргументации и истории философии: Сборник научных статей. / Под общ. ред. В.Н. Брюшинкина. - Калининград: Изд-во КГУ, 2004. С. 20-37. -Библиогр.: С. 37.1 п.л.

Ходикова Нина Анатольевна

Логико-методологическое исследование происхождения теории поиска вывода

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата философских наук

Подписано в печать 3.11.2004 г. Бумага для множительных аппаратов. Формат 60x90 1/16. Ризограф. Гарнитура «Таймс». Усл. печ. л. 1,3. Уч. изд. л. 1,3. Тираж 100 экз. Заказ 235

Издательство Калининградского государственного университета 236041, г. Калининград, ул. А. Невского, 14

«24276

279

 

Оглавление научной работы автор диссертации — кандидата философских наук Ходикова, Нина Анатольевна

Введение.

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

§ 1. История логики и рациональная реконструкция развития науки.

§ 2. Б.С. Грязнов о рациональной реконструкции развития науки.

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

Глава 2. Гильбертовская теория доказательств: непротиворечивость и подформульность.

§ 1. Гильбертовская теория доказательств и непротиворечивость.

§ 2. Генценовское доказательство непротиворечивости: подформульность как поризм.

§ 3. Использование свойства подформульности в теоретической логике: таблицы Бета и модельные множества Хинтикки.

Глава 3. Автоматическое доказательство логико-математических теорем и формализация эвристик.

§ 1. Ранняя история автоматического доказательства: программа «Логик-теоретик».

§ 2. Применение секвенциальных исчислений: процедура Хао Вана.

§ 3. Идея метапеременности в процедуре Кангера.

§ 4. Методы автоматического доказательства, основанные на теореме Эрбрана.

§ 5. Универсальные методы поиска доказательства: метод резолюций и обратный метод.

Глава 4. Теория поиска вывода и ее происхождение из теории доказательств.

§ 1. Логические алгоритмы и эвристики: подход О.Ф. Серебрянникова.

§ 2. Теория поиска вывода: подход С.Ю. Маслова.

 

Введение диссертации2004 год, автореферат по философии, Ходикова, Нина Анатольевна

Актуальность исследования.

Наука как вид профессиональной деятельности существует сравнительно недавно, всего около четырех столетий. Но важность этого вида деятельности для общества была осознана почти одновременно с его появлением, и вслед за наукой возникла история науки как особая дисциплина, занимающаяся описанием научных достижений, открытий, поисков и даже ошибок. Долгое время историко-научные исследования представляли собой по преимуществу биографии великих ученых с подробным описанием их достижений и ошибок. Основой изложения служила хронология, и молчаливо предполагалось, что такой порядок компоновки материала сам по себе обеспечивает отображение внутренней логики развития научной мысли. Таким образом, история науки представлялась как история идей. С другой стороны, до 50-х годов XX века в исследованиях по методологии науки преобладали проблемы, связанные с анализом понятийного аппарата науки, схем обоснования знания, структуры теорий, логики индуктивного и дедуктивного вывода, эмпирического содержания теоретического знания. Проблема изучения законов изменения теорий, природы научных революций, особенностей развития научного знания впервые отчетливо выдвигается на первый план в работах К.Поппера. В дальнейшем его идеи рациональной реконструкции развития научных теорий были развиты и в некотором смысле пересмотрены в методологических концепциях Т.Куна, И.Лакатоса, П.Фейерабенда, Дж.Агасси.

Известный советский методолог науки Б.С. Грязнов на основании критического анализа постпозитивистских методологических концепций разработал оригинальную модель происхождения научных теорий. Ключевым понятием этой модели является понятие «поризма». На естественнонаучном (и, частично, математическом) материале Грязнов показал, что непредвиденное следствие, полученное в ходе решения задачи в рамках имеющейся теории, при выполнении определенных условий может привести к появлению новой теории. Истолкование ядра новой теории как логического, но, тем не менее, неожиданного, непредвиденного, следствия предыдущей теории, открывает путь к построению рациональной реконструкции происхождения новой научной теории.

Если говорить об истории логики, то в отличие от стандартных механизмов реконструкции развития научного знания, разработанных в методологии науки XX века, в истории логики до сих пор не идет речь о логических теориях, их преемственности и смене. Развитие логики обычно представляется либо как хронологическая последовательность работ различных логиков, либо - в лучшем случае - как развитие некоторых идей или представлений о правильности рассуждений и способов их формализации1. В связи с этим актуальной является проблема такого представления истории логики, которое соответствовало бы общенаучным методологическим концепциям, выработанным в XX веке. В данном исследовании рассматривается вопрос о происхождении одной из сравнительно молодых логических теорий (появившейся в 70-х г.г. XX века) - теории поиска вывода. Идейный создатель теории поиска вывода С.Ю.Маслов определял ее как область математической логики, занимающуюся «выявлением по исчислению и объекту в языке исчисления л структуры возможных выводов этого объекта» . Другими словами, теория поиска вывода исследует возможные способы решения задач в различных исчислениях. Теория поиска вывода является пограничной дисциплиной комплекса computer science - она стоит на стыке логики, психологии и эвристики. Поэтому помимо активного практического применения, она находит интересные теоретические приложения в философии3 и психологии

1 Kneale W, Kneale М, The Development of Logic. - Oxford, 1964. P. V.

2МасловС.Ю. Теория дедуктивных систем и ее применения - М.: Радио и связь, 1986. С,93.

3 Брюшинкин В Н. Логика, мышление, информация. - Л.: Изд-во Ленинградского ун-та, 1988. творчества4. Применение поризматической модели развития научного знания к возникновению теории поиска вывода позволит более полно осмыслить особенности основных идей и методов этой теории, очертить круг решаемых в ней задач. Вместе с тем, успешное решение задачи представления возникновения одной логической теории на основе другой (теории поиска вывода на основе гильбертовской теории доказательств) порождает новый взгляд на историю логики вообще - как на историю смены и преемственности теорий. Степень разработанности темы.

Основные положения теории поиска вывода были сформулированы С.Ю. Масловым в его работах 70-х годов XX века5. Отдельные аспекты теории поиска вывода и ее приложений разрабатывались В.Н. 7

Брюшинкиным и C.JI. Катречко .

Вопросы о возникновении научного знания, о преемственности и смене научных теорий являются ключевыми в философии науки о постпозитивизма. Идеи фальсификационизма, предложенные К.Поппером развиты в таких методологических схемах, как теория «исследовательских программ» И.Лакатоса9, теория «нормальной» и «кризисной» науки Т.Куна10

4 Маслов С.Ю. Теория дедуктивных систем и ее применения. М.: Радио и связь, 1986; Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества// Семиотика и информатика.- М.,1979. Вып. 13. С. 17-46.

5 Маслов С.Ю. Теория дедуктивных систем и ее применения. - М.: Радио и связь, 1986; Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества // Семиотика и информатика - М ,1979. Вып.13. С. 17-46.

6 Брюшинкин В Н. Логика, мышление, информация. - Л.: Изд-во Ленинградского ун-та, 1988; Брюшинкин В Н. О возникновении теорий в логике: теория поиска вывода как поризм // Современная логика: Проблемы теории, истории и применения в науке: Сб. науч. тр. / Под ред. А.Я Слинина.- Л : Изд-во Ленинградского унта, 1990. С.17-18; Брюшинкин ВН. О методологическом значении различения понятий "вывод" и "поиск вывода" / Философские науки, 1984. № 4. С. 49-54.

7 Катречко СЛ. Логический анализ интеллектуальных систем с метапроцедурами: Дис. . канд. филос. наук.- М., 1992.

8 Popper Karl R. The Logic of Scientific Discovery. London- New York: Routledge, 1995.

9 Лакатос И. Фальсификация и методология научно-исследовательских программ / Пер. с англ. и пред В Поруса.- М: Медиум, 1995. и теория несоизмеримости П.Фейерабенда11. В советской и российской методологии вопросам развития научного знания также уделяется достаточно большое внимание. В частности, Е.К.Войшвилло рассматривает процессы, приводящие к смене научных теорий и те отношения, которые возникают между старой и новой теорией в свете принципа соответствия.12 Критический анализ постпозитивистских концепций и изложение некоторых аспектов проблемы смены и преемственности научных теорий содержится также в работах В.Н. Садовского13, В.А. Смирнова14, A.J1. Никифорова15, Ю.А. Петрова16. Значительный и оригинальный вклад в исследование сущности научной теории, ее предметной области и объекта, в закономерности функционирования теории как сложной системы внесли работы

1 "7

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

10 К>н Т.С. Структура научных революций. - М.: Прогресс, 1975.

11 Фейерабенд П. Избранные труды по методологам науки / Пер. с англ. и нем. А.Л.Никифорова; под ред. И С.Нарского - М.: Прогресс, 1986. u Войшвилло Е.К, Принцип соответствия как форма развития знаний и понятие относительной истины. Критика концепции несоизмеримости сменяющих друг друга теорий // Логика и В Е К.: Сб науч.тр / Под ред И.В.Маркина и др. - М.: Современные тетради, 2003. - 256 с. С.11-22. u Садовский В.Н. Карл Поппер и Россия. - М.: Эдиториал УРСС, 2002.

14 Смирнов В А. Логические методы анализа научного знания. - М.: Наука, 1987.

15 Никифоров А.Л. От формальной логики к истории науки: критический анализ буржуазной методологии науки - М.: Наука, 1983.

16 Петров Ю.А. Проблема соизмеримости теорий // Филос. Науки, 1986. №4.

17 Грязнов Б С. Логика. Рациональность. Творчество. - М.: Наука, 1982. вовсе. Вообще, вопрос о смене теорий в логике с общих методологических позиций в истории логики практически не рассматривался. Исключение составляет подход Е.К.Войшвилло к происхождению релевантной логики из классической логики (высказываний или предикатов) за счет уточнения понятия логического следования для формул языка классической логики.18 Идея о возможности применения поризматической модели Грязнова к возникновению теорий в логике, в частности, к возникновению теории поиска вывода из гильбертовской теории доказательств, была впервые изложена в работах В.Н. Брюшинкина.19 Цели и задачи исследования.

Целью работы является обоснование возможности применения общенаучных методологических концепций рациональной реконструкции развития научного знания к описанию возникновения новых теорий в логике на примере объяснения возникновения теории поиска вывода в рамках поризматической модели Б.С.Грязнова. Для достижения этой цели ставятся и решаются следующие задачи:

• Реконструировать и уточнить систему методологических взглядов лежащих в основе поризматической теории происхождения научной теории и показать ее применимость в области дедуктивных наук, в частности, в математике;

• Осуществить методологический анализ гильбертовской теории доказательств, выделить предметную область и объект этой теории;

18 Войшвилло Е.К. Релевантная логика как этап развития символической логики. Ее философско-методологическое значение // В. сб.: Гуманитарная наука в России: соросовские лауреаты.- М., 1996. С. 1429.

19

Брюшинкин В.Н. О возникновении теорий в логике: теория поиска вывода как поризм // Современная логика: Проблемы теории, истории и применения в науке; Сб. науч. тр. / Под ред. А.Я Слинина. - Л.: Изд-во Лен-го ун-та, 1990. С. 17-18.

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

• Проанализировать первые теоретические попытки использования систем, обладающих свойством подформульности для определения процедур поиска вывода (Э. Бет, Я. Хинтикка);

• Рассмотреть первые попытки построения процедур автоматического доказательства теорем: программа «Логик-теоретик», не использующая свойства подформульности, и программа Хао Вана, основанная на свойстве подформульности. Провести сравнительный анализ эффективности этих программ;

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

• Выявить на основе работ С.Ю. Маслова основные особенности метода резолюций и обратного метода: аналитичность, метапеременность, локальность;

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

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

Методологической основой исследования является аппарат современной логики, теории познания, методологии науки, эвристики. Решающее влияние на идею и результаты исследования оказали методологические и логические исследования Б.С. Грязнова и В.Н. Брюшинкина, а также разработка теории поиска вывода, предпринятая в трудах С.Ю.Маслова. Теоретической основой исследования являются труды по основаниям математики Д.Гильберта, П.Бернайса; логико-математические работы Ж.Эрбрана, Г.Генцена, С.К.Клини, Я.Хинтикки, Э.Бета, Р.Смальяна, Д.Правица, С.Кангера, Д.Пойа, О.Ф.Серебрянникова, В.А. Смирнова, Е.Д. Смирновой, Е.К.Войшвилло, С.С.Гончарова, Ю.Л.Ершова, К.Ф.Самохвалова. Важную роль в диссертационном исследовании сыграли логико-философское исследование теории поиска вывода, проведенное C.JI. Катречко, историко-логические исследования Н.И. Стяжкина, У. и М. Нил; исследования по современной реконструкции аристотелевской силлогистики и других теорий, сыгравших важную роль в истории логики, В.А. Бочарова и В.И. Маркина. Труды JI.A. Микешиной по философии познания оказали решающее влияние на осмысление понятий «интерпретация» и «рациональность». Автор опирался также на работы специалистов в области программирования и «искусственного интеллекта»: Н.Нильсона, Хао Вана, А.Ньюэлла, Дж.Шоу, Г.Саймона, Дж.Робинсона.

Научная новизна исследования.

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

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

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

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

• разработан новый подход к интерпретации свойства подформульности как поризма состоящий в различении двух составляющих: 1) внутренней теоретической интерпретации поризма, 2) внешней «квазиэмпирической» интерпретации поризма как новой области задач, которая включает поризм в новую систему понятий, следствием чего является появление нового теоретического объекта и возникновение новой теории;

• проанализированы первые теоретические попытки использования систем, обладающих свойством подформульности для определения процедур поиска вывода (Э. Бет, Я. Хинтикка); показано, что «чисто теоретическая» интерпретация этих процедур не приводит к возникновению новой теории;

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

• установлено, что аналитическая интерпретация доказательства (рассмотрение «снизу вверх»), в конечном счете, порождает новый теоретический объект - дерево поиска вывода,

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

Практическая значимость исследования.

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

Результаты исследования могут быть использованы для разработки курса «Истории логики», «Философские проблемы математики», спецкурсов «Логические проблехмы искусственного интеллекта» и «Теория поиска вывода».

Апробация диссертации.

Диссертация обсуждена на заседании кафедры философии и логики исторического факультета КГУ и рекомендована к защите. Основные положения диссертации изложены в ряде публикаций, обсуждались на постоянном научном семинаре кафедры философии и логики, использовались для разработки курсов символической логики и математики для студентов философского отделения исторического факультета КГУ. Структура работы.

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

 

Заключение научной работыдиссертация на тему "Логико-методологическое исследование происхождения теории поиска вывода"

Заключение.

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

• Реконструирована и уточнена система методологических взглядов лежащих в основе поризматической теории происхождения научной теории и показана ее применимость в области дедуктивных наук, в частности, в математике;

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

• Осуществлен методологический анализ гильбертовской теории доказательств, выделены предметная область и объект этой теории;

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

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

Для решения этой задачи было рассмотрено решение Генценом задачи доказательства непротиворечивости арифметики в рамках гильбертовской теории доказательств -построение им натуральных, а затем секвенциальных исчислений, доказательство основной теоремы об устранимости сечения. В качестве доказательства поризматической природы обнаружения свойства подформульности доказательств и связанной с ним «аналитической» интерпретации доказательств используется тот факт, что сам Генцен использовал свойство подформульности «синтетических» доказательств лишь для доказательства метатеорем теории доказательств (таких, как теорема о непротиворечивости арифметики). При этом он не ставил вопрос о применении свойства подформульности для аналитического построения доказательства и организации некоторых систематических процедур этого построения.

Проанализированы первые теоретические попытки использования систем, обладающих свойством подформульности для определения процедур поиска вывода (Э. Бет, Я. Хинтикка);

Анализ работ Э.Бета и Я. Хинтикки показал, что они использовали свойство подформульности в системах без сечения для построения доказательства «снизу вверх». Однако новые методы построения доказательств, основанные на свойстве подформульности, были применены ими для решения задач, поставленных еще в теории доказательств (например, доказательство полноты логических систем) и потому не привели к осознанию поиска вывода как нового теоретического объекта, отличного от формального доказательства в некотором исчислении. Таким образом, оказалось, что для возникновения новой теории необходимо появление новой области задач, на которой новый теоретический объект находит применение и окончательно осознается как самостоятельный объект исследования.

Рассмотрены первые попытки построения процедур автоматического доказательства теорем: программа «Логик-теоретик», не использующая свойства подформульности, и программа Хао Вана, основанная на свойстве подформульности. Проведен сравнительный анализ эффективности этих программ;

При решении этой задачи было выяснено, во-первых, что автоматическое доказательство теорем играет роль новой «квазиэмпирической» области интерпретации для свойства подформульности, без которой, согласно принятой в исследовании поризматической модели, невозможно появление новой теории. С другой стороны, на примере сравнения программы «Логик-теоретик» и программы Хао Вана было показано, что метод Хао Вана, реализующий свойство подформульности в секвенциальном исчислении значительно эффективнее метода, осуществляющего поиск доказательства в аксиоматическом исчислении с использованием неких эвристик. Этот анализ позволил сделать промежуточный вывод: эффективное автоматическое доказательство теорем невозможно без постановки задачи формализации эвристических принципов в самом логическом исчислении.

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

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

• Проведена историко-логическая реконструкция возникновения теории поиска вывода в работах С.Ю. Маслова как результата обобщения свойств аналитичности, метапеременности и локальности на аппарат исчислений общего типа.

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

В процессе исследования получены следующие новые результаты: впервые детально реконструирована поризматическая модель Б.С.Грязнова и предложена ее общая схема; на основании анализа историко-логического материала развит и систематизирован взгляд В.Н. Брюшинкина на свойство подформульности как на поризм, возникший в теории доказательств при решении задачи доказательства непротиворечивости формальной арифметики, и ставший ядром новой теории - теории поиска вывода; установлено, что применение поризматической модели к реконструкции развития логико-математических теорий требует определенной доработки самой модели, которая и была произведена. В частности, в исследовании впервые поставлена проблема специфики соотношения поризма и интерпретации в логико-математических теориях. В ходе ее решения выдвинут и обоснован тезис о том, что на место эмпирической интерпретации поризма, имеющей место для естественнонаучных теорий, в логико-математических науках заступает «квазиэмпирическая» интерпретация на новой области задач или объектов, позволяющая включить его в новую систему понятий. В ходе исследования установлено, что интерпретация свойства подформульности как поризма может быть представлена как последовательность двух этапов:

1. Внутренняя теоретическая интерпретация поризма. Согласно разработанной в исследовании концепции, объектом гильбертовской теории доказательств изначально является формальный объект «доказательство» вместе с присущей ему «синтетической» интерпретацией, характерной для аксиоматических исчислений гильбертовского типа. С другой стороны, показано, что обнаружение Генценом свойства подформульности у доказательств в секвенциальных исчислениях без сечений (рассматриваемое как поризм) привело к новому - «аналитическому» - взгляду на доказательство, который создает возможность нового теоретического объекта. Поскольку же синтетическая и аналитическая интерпретации противоположны, то новый теоретический объект означает рассогласование с первоначальной интерпретацией объекта теории доказательств и требует развития нового взгляда на доказательства в секвенциальных исчислениях как на объекты, обладающие важными «аналитическими» свойствами.

2. Внешняя «квазиэмпирическая» интерпретация поризма.

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

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

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

 

Список научной литературыХодикова, Нина Анатольевна, диссертация по теме "Логика"

1. Андронов, И.К. Математика действительных и комплексных чисел / И.К. Андронов; под ред. Н.М. Матвеева. М.: Просвещение, 1975.- 153 с.

2. Балтага, В.К. Комплексные числа / В.К. Балтага // Отв. ред. М.И. Кадец. Харьков, изд-во Харьковского ун-та, 1959.- 105 с.

3. Бет, Э.В. Метод семантических таблиц / Э.В. Бет // Математическая теория логического вывода: Сб. перев. / Под ред. А.В. Идельсона и Г.Е. Минца. М.: Наука, Глав. ред. физико -математической литературы, 1967. С. 191-200. - Библиогр.: с. 199.

4. Бочаров, В.А. Аристотель и традиционная логика. Анализ силлогистических теорий / Вячеслав Александрович Бочаров М.: Изд-во Московского ун-та, 1984. - 136 с. - Библиогр.: с. 129-132.

5. Брюшинкин, В.Н. Логика, мышление, информация / Владимир Никифорович Брюшинкин. JL: Изд-во Ленинградского унта, 1988. - 152 с. - ISBN 5-288-00158-8.

6. Брюшинкин, В.Н. Логическое моделирование процессов мышления: автореф. дис. . д-ра филос. наук / Брюшинкин Владимир Никифорович. М., 1990. - 40 с.

7. Брюшинкин В.Н. О методологическом значении различения понятий "вывод" и "поиск вывода" / В.Н. Брюшинкин // Философские науки 1984. - № 4. - С. 49-54.

8. Брюшинкин, В.Н. Кант и силлогистика. Некоторые размышления по поводу «Ложного мудрствования в четырех фигурах силлогизма» / В.Н. Брюшинкин // Кантовский сборник, Вып. И. -Калининград, 1986. - С.29-39.

9. Войшвилло, Е.К. Символическая логика: классическая и релевантная. Философско-методологические аспекты: учеб. пособие / Войшвилло Е.К.; рец. Я.А. Слинин, Е.А. Сидоренко. М.: Высшая школа, 1989. - 150 с. - Библиогр.: с. 147 - 148. - ISBN 5-06-001417-7.

10. Вычислительные машины и мышление: сб. науч. тр. / Под ред. Э.Фейгенбаума и Дж. Фельдмана; пер. с англ. под ред. Э.М. Браверманна, А.В. Напалкова и Ю.В. Орфеева. М.: Мир, 1967. - 552 с. - (Редакция литературы по новой технике).

11. Генцен, Г. Непротиворечивость чистой теории чисел // Математическая теория логического вывода: сб. перев. / Под ред. А.В. Идельсона и Г.Е. Минца. М.: Наука, 1967. С. 77-153.

12. Генцен, Г. Исследования логических выводов / Герхард Генцен // Математическая теория логического вывода: Сб. перев. / Под ред. А.В. Идельсона и Г.Е. Минца. М.: Наука, Глав. ред. физико -математической литературы, 1967. С. 9-75.

13. Генцен, Г. Новое изложение доказательстваIнепротиворечивости для чистой теории чисел / Герхард Генцен // Математическая теория логического вывода: Сб. перев. / Под ред. А.В.

14. Идельсона и Г.Е. Минца. М.: Наука, Глав. ред. физико -математической литературы, 1967. С. 154-191.

15. Гильберт, Д. Основания геометрии / Д. Гильберт // Пер. с 7-го нем. издания И.С. Градштейна; под ред. и со вступ. ст. П.К. Рашевского. M.-JI.: ОГИЗ Государственное Технико-теоретическое изд-во, 1948.-491 с.

16. Гильберт, Д. Аксиоматическое мышление / Д. Гильберт; пер. с англ. А.Г. Барабашева // Методологический анализ оснований математики / Ф. Китчер, В.Я. Перминов, Б.И. Федоров и др. М.: Наука, 1988. - С. 97-104. - ISBN 5-02-008094-2. - С. 97-104.

17. Гильберт, Д., Бернайс, П. Основания математики. Логические исчисления и формализация арифметики / Давид Гильберт, Пауль Бернайс; пер. с нем. Н.М. Нагорного; под ред. С.И. Адяна. М.: Наука, Главная ред. физико-математической литературы, 1979.-560 с.

18. Гильберт, Д., Бернайс, П. Основания математики. Теория доказательств / Давид Гильберт, Пауль Бернайс; пер. с нем. Н.М. Нагорного; под ред. С.И. Адяна. М.: Наука, Главная ред. физико-математической литературы, 1982. - 652 с.

19. Грязнов, Б.С. Логика. Рациональность. Творчество / Борис Семенович Грязнов; отв. ред. И.С. Тимофеев; сост. К.В. Малиновская, Н.И. Кузнецова, Е.П. Никитин. М.: Наука, 1982. - 255 с.

20. Интерпретация как историко-научная и методологическая проблема: сб. науч. тр. / Под ред. В.П. Горана. АН СССР СО: Институтистории, филологии и философии. Новосибирск: Наука, 1986. - 206 с.

21. История логики / Под ред. В.Ф. Беркова и Я.С. Яскевич. Минск: Новое знание, 2001. 169 С.

22. История математики с древнейших времен до начала 19 столетия: В 3 т. // Т 1. С древнейших времен до начала нового времени; авт. И.Г. Башмакова и др. .; под ред. А.П. Юшкевича. М.: Наука, 1970. - 351 с. - Библиогр.: с. 327-342.

23. Кант, И. Критика чистого разума / Иммануил Кант; пер. с нем. Н.О.Лосского с вар. пер. на рус. и евр. яз.; ред., сост. и вступ. ст. В.А. Жучкова; примеч., слов. Терминов В.А. Жучкова, В.В. Васильева. Институт философии РАН. М. Наука, 1998. - 655 с.

24. Карнап, Р. Значение и необходимость. Исследование по семантике и модальной логике / Рудольф Карнап; пер. Н.В.Воробьева; общ. ред. Д.А. Бочвара; пред. С.А. Яновской. М. Изд-во иностранной литературы, 1959 г. - 382 с. - Библиогр.: с. 357-360.

25. Катречко, С.Л. Логический анализ интеллектуальных систем с метапроцедурами: автореф. дис. . канд. филос. наук / Катречко Сергей Леонидович. М., 1992. - 24 с.

26. Клини, С.К. Математическая логика / С.К. Клини; пер. с англ. Ю.А.Гастева; под ред. Г.Е.Минца. М.: Мир, 1973. - 480 с. -Библиогр.: с. 451-465.

27. Ковальски, Р., Семантические деревья в автоматическом поиске доказательств / Р. Ковальски, П.ДЖ. Хайс // Кибернетический сборник: сб. науч. тр. Новая серия; вып. 9./ Под ред. А.А.Ляпунова и О.Б.Лупанова. М: Мир, 1972. - С. 66-83. - Библиогр.: с. 83.

28. Крайзель, Г. Исследования по теории доказательств: сб. ст. / Г. Крайзель // Пер. с англ. Ю.А. Гастева и Г.Е. Минца; под ред. С.Ю.Маслова. М.: Мир, 1981. - 289 с. - Библиогр.: 285-287.

29. Кун, Т. Структура научных революций / Т. Кун; пер. с англ. И.З. Налетова. М.: Прогресс, 1975. - 288 с. - Указ.: с. 283-287.

30. Курант, Р., Гильберт, Д. Методы математической физики: в 2 т. / Р. Курант, Д. Гильберт; пер. со второго нем. изд. 3. Либина, Б. Лившица, Ю. Рабиновича. М.-Л.: Госуд-е изд-во технико-теоретической литературы, 1951. Т. 1. - 476 с.

31. Лакатос, И. Доказательства и опровержения. Как доказываются теоремы / И. Лакатос // Пер. с англ. И.Н. Веселовского; отв. ред. И.Б. Погребысский. М.: Наука, 1967. - 152 с. - Библиогр.: с. 146-151.

32. Лакатос, Имре. Фальсификация и методология научно-исследовательских программ / Имре Лакатос; пер. с англ. с прим. и пред. В.Поруса; худ. Е. Михельсон. Московский философский фонд. -М.: Медиум, 1995. 236 с. - ISBN 5-85691-040-0.

33. Ларин, В.Н., Ежела, В.В. К столетию открытия кванта действия // Вестник РФФИ Электронный ресурс. № 3, 2003. Режим доступа: http://www.rfbr.ru/default.asp7section id=162. - Загл. с экрана.

34. Логический вывод: сб. науч. тр. / Под ред. В.А. Смирнова и др.; Институт философии АН СССР. М.: Наука, 1979. - 310 с.

35. Маковельский, А.О. История логики / Александр Осипович Маковельский. М.: Наука, 1967.

36. Малаховский, B.C. Избранные главы истории математики: учеб. изд. / Владислав Степанович Малаховский. Калининград: ФГУИПП «Янтарный сказ», 2002. - 304 е.: порт. - ISBN 5-7406-0544-х.- Библиогр.: с. 285-288.

37. Маркин, В.И. Интенсиональная семантика традиционной силлогистики / В.И. Маркин // Логические исследования. М.: Наука, 2001. Вып. 8.-С. 82-91.

38. Маркин, В.И. Силлогистические теории в современной логике / Маркин Владимир Ильич. М.: Изд-во МГУ, 1991. — 96 с. -Библиогр.: с. 93-94. - ISBN 5-211-01967-9.

39. Маслов, С.Ю. Теория дедуктивных систем и ее применения / Сергей Юрьевич Маслов. М.: Радио и связь, 1986. - 136 е., ил. -(Кибернетика).

40. Маслов, С.Ю. Теория поиска вывода и вопросы психологии творчества / С.Ю. Маслов // Семиотика и информатика. М., 1979. Вып. 13. - С. 17-46.

41. Методологический анализ оснований математики / Ф. Китчер, В.Я. Перминов, Б.И. Федоров и др. М.: Наука, 1988. - 175 е.- ISBN 5-02-008094-2.

42. Микешина, Л.А. Философия познания. Полемические главы / Микешина Людмила Александровна. М.: Прогресс-Традиция, 2002.- 624 с. ISBN 5-89826-108-7. - Библигр.: с. 588-612.

43. Минц, Г.Е. Теорема Эрбрана / Г.Е. Минц // Математическая теория логического вывода: сб. перев. / Под ред. А.В. Идельсона и Г.Е. Минца. М.: Наука, Глав. ред. физико - математической литературы, 1967. С. 311-350.-Библиогр.: с. 349-350.

44. Непейвода, Н.Н. Прикладная логика: учеб. пос. / Непейвода Николай Николаевич; 2-е изд., испр. и доп. Новосибирск: Изд-во Новосибирского ун-та, 2000. - 521 с. - ISBN 5-7615-0490-1. -Библиогр.: с. 479-481.

45. Никифоров, А.Л. От формальной логики к истории науки: критический анализ буржуазной методологии науки / Александр

46. Леонидович Никифоров. Институт философии АН СССР. М.: Наука, 1983.- 177 с.

47. Нильсон, Н. Принципы искусственного интеллекта / Ниле Нильсон; пер. с англ. P.M. Абдусаматова, Ю.И. Крюкова; под ред. В.Л. Сефанюка. М.: Радио и связь, 1985. - 376 е., ил. - Библиогр.: с. 338371. - (Редакция переводной литературы).

48. Очерки по истории математики: учеб. пособ. / Авт. И.Г. Башмакова и др.; под ред. Б.В.Гнеденко. М.: Изд-во Московского ун-та, 1997. - 496 е., ил. - ISBN 5-211-03401-5.

49. Петров, Ю.А. Методологические вопросы анализа научного знания / Петров Юрий Александрович. М.: Высшая школа, 1977. -224 с. - Библиогр.: с. 220-221.

50. Петров Ю.А. Проблема соизмеримости теорий // Филос. науки. М.: Высшая школа: научные доклады высшей школы, 1986. №4.-С. 61-70.

51. Петров, Ю.А., Никифоров, А.Л. Логика и методология научного познания / Юрий Александрович Петров, Александр Леонидович Никифоров. М.: Изд-во Московского ун-та, 1982. - 249 с. - Библиогр.: с. 244 - 247.

52. Пойа, Д. Математическое открытие. Решение задач: основные понятия, изучение и преподавание / Джордж Пойа; пер. с англ. В.С.Бермана; под ред. И.М.Яглома. М. Наука, 1970. - 452 е., ил. - Библиогр.: с. 445-447.

53. Пономарев, В.Ф. Математическая логика: учеб. пособие / Вениамин Федорович Пономарев // Часть 1. Логика высказываний, логика предикатов. Калининград: КГТУ, 2001.- 130 с. - Библиогр.: с. 124.

54. Попов, П.С. Стяжкин, Н.И. Развитие логических идей от античности до эпохи возрождения / Павел Сергеевич Попов, Николай Иванович Стяжкин. М.: Изд-во МГУ, 1974. - 222 с. - Библиогр.: с. 209- 221.

55. Попович, М.В. Очерк развития логических идей в культурно-историческом контексте / Мирослав Владимирович Попович. Киев: Наукова думка, Редакция философской и правовой литературы, 1979. -243 с.

56. Поппер, К.Р. Логика и рост научного знания: избр. раб. / Карл Раймунд Поппер; пер. с англ., сост., общ. ред. и вступ. ст. В. Садовского. М.: Прогресс, 1983. - 605 с.

57. Правиц, Д. Достижения и проблемы в развитии процедур механического доказательства / Д. Правиц // Кибернетический сборник: сб. науч. тр. Новая серия; вып. 9./ Под ред. А.А.Ляпунова и О.Б.Лупанова. М: Мир, 1972. - С. 52-66. - Библиогр.: с. 65-66.

58. Рассел, Б. История западной философии и ее связи с политическими и социальными условиями от античности до наших дней / Б. Рассел ; пер. с англ. В.В. Целищева; 3-е изд., стер. М.: Акад. проект, 2000. - 767 с. - ISBN 5-8291-0087-8.

59. Рузавин, Г.И. Философские проблемы оснований математики / Георгий Иванович Рузавин. М.: Наука, 1983. - 230 с.

60. Садовский, В.Н. Карл Поппер и Россия / Садовский Вадим Николаевич. М.: Эдиториал УРСС, 2002. - 280 с. - Библиогр.: с. 247259. - ISBN 5-8360-0324-6.

61. Серебрянников, О.Ф. Эвристики, алгоритмы и правила логики / О.Ф. Серебрянников // Проблемы законов науки и логики научного познания: сб. науч. тр. / Под ред. ИЛ.Чупахина, В.П.Рожина. JL: Изд-во Ленинградского ун-та , 1980. С. 132-138.

62. Серебрянников, О.Ф. Эвристические принципы и логические исчисления / Олег Федорович Серебрянников; отв. ред. Б.В. Бирюков.- М.: Наука, 1970. 282 с. - Библиогр.: с.280-282.

63. Смальян, Р. Теория формальных систем / Раймонд М. Смальян; пер. с англ. Н.К. Косовского; под ред. Н.А. Шанина. М.: Наука, Главная ред. физико-математической литературы, 1981. - 207 с.- Библиогр.: с. 202-204.

64. Смирнов, В.А. Логические методы анализа научного знания / Владимир Александрович Смирнов; М.: Наука, 1987. 255 с. -(Институт философии АН СССР). - Библиогр.: с. 248-254.

65. Смирнова, Е.Д. Логическая семантика и философские основания логики / Елена Дмитриевна Смирнова. М.: Изд-во Московского ун-та, 1986.

66. Смирнова, Е.Д. Логика и философия / Е.Д. Смирнова; ред. кол. А.А. Воронин, А.П. Огурцов, В.А. Смирнов.- М.: «Российская политическая энциклопедия» (РОССПЭН), 1996. 304 с. - ISBN 586004-039-3.

67. Современная философия науки: знание, рациональность, ценности в трудах мыслителей Запада: Учеб. хрест. / 2-е изд., перераб.и доп. М.: Издательская корпорация «Логос», 1996. - 400 с. - ISBN 588439-061-0.

68. Столл Роберт Р. Множества. Логика. Аксиоматические теории / Роберт Р. Стол; пер. с англ. Ю.А. Гастева и И.Х. Шмаина; под ред. Ю.А. Шихановича. М.: Просвещение, 1968. - 321 с.

69. Стройк, Д.Я. Краткий очерк истории математики / Дирк Ян Стройк; пер. с нем. и доп. И.Б. Погребысского. М.: Наука, 1984. 282 с.

70. Стяжкин, Н.И. Формирование математической логики / Стяжкин Николай Иванович; отв. ред. А.Л. Субботин. М.: Наука, 1967.- 508 с. - Библиогр.: с. 456-505.

71. Субботин, А.Л. Традиционная и современная формальная логика / Александр Леонидович Субботин. Институт философии АН СССР. М.: Наука, 1969. - 160 с. - Библиогр.: с. 157-159.

72. Такеути, Гаиси. Теория доказательств / Гаиси Такеути; пер. с англ. С.К. Соболева, под ред. С.И. Адяна. М.: Мир, 1978. - 412 с. -(Редакция литературы по математическим наукам).

73. Фейерабенд, П. Избранные труды по методологии науки / Пол Фейерабенд; пер. с англ. и нем. А.Л.Никифорова; общ. ред. и вст. ст. И.С. Нарского. М.: Прогресс, 1986. 543 е., ил. - Библиогр.: с. 524537.

74. Френкель, А., Бар-Хиллел, И. Основания теории множеств / Абрахам Френкель, Иегоша Бар-Хиллел; пер. с англ. Ю.А. Гастева;под. ред. А.С. Есенина Вольпина. - М.: Мир, 1966. - 555 с. -Библиогр.: с. 422-537.

75. Хао, Ван. На пути к механической математике / Ван Хао // Кибернетический сборник: сб. науч. тр. / Под ред. А.А.Ляпунова, О.Б.Лупанова и Н.Н. Рикко. М.: Изд-во иностранной литературы, 1962. Вып. 5. С.114-165.-Библиогр.: с. 164-165.

76. Хинтикка, Я. Логико-эпистемологические исследования: сб. науч. ст. / Я. Хинтикка; пер. с англ. В.Н. Брюшинкина, Э.Л. Наппельбаума, А.Л. Никифорова. М.: Прогресс, 1980. - 445 с. -Библиогр.: с. 430-437. - (Редакция литературы по философии и педагогике).

77. Цейтен, Г.Г. История математики в древности и в средние века / Г.Г. Цейтен; пер. П. Юшкевича с фр. издания, испр. автором; предисл. М. Выготского. М.-Л.: Государственное технико-теоретическое изд-во, 1932. - 230 с.

78. Энглер, Э. Метаматематика элементарной математики / Энглер Э.; пер. с нем. Г.Е. Минца. Под ред. А.О. Слисенко. М.: Мир, 1987.- 128 с.

79. Юдин, Б.Г. Методологический анализ как направление изучения науки / Борис Григорьевич Юдин; М.: Наука, Институт истории естествознания и техники АН СССР, 1986. 260 с. -Библиогр.: с. 252-259.

80. Яглом, И.М. Комплексные числа и их применение в геометрии / Исаак Моисеевич Яглом. М.: Госуд. изд-во физико-математической литературы, 1963. - 192 е., ил.

81. Handbook of Logic in Artificial Intelligence and Logic Programming. VI. Logical Foundations / Edited by Dov M. Gabbay, C.J. Hogger, J.A. Robinson. Oxford: Clarendon Press, 1993. 182 P. - ISBN 0-19-853745-x.

82. Handbook of Logic in Artificial Intelligence and Logic Programming. V2. Deduction Methodologies / Edited by Dov M. Gabbay, C.J. Hogger, J.A. Robinson. Oxford: Clarendon Press, 1993. 215 P. -ISBN 0-19-853745-x.

83. Handbook of Logic in Artificial Intelligence and Logic Programming. V3. Nonmonotonic Reasoning and Uncertain Reasoning / Edited by Dov M.Gabbay, C.J.Hogger, J.A.Robinson. Oxford: Clarendon Press, 1994. 198 P. - ISBN 0-19-853747-6.

84. Hintikka, J., Remes, U. The Method of Analysis. Its geometrical origin and its general significance / J. Hintikka, U.Remes. Dordrecht: D. Reidel, 1974. - 352 P. - ISBN 90-277-0532-1.

85. Kneale, William, Kneale, Marta. The Development of Logic / William Kneale, Marta Kneale. Oxford: At the Clarendon Press, 1964. P. V. - 761 p. - Bibliography: p. 743-751.

86. Popper, Karl R. The Logic of Scientific Discovery. London and New York: T.J. Press (Padstow) Ltd, 1995. 479 P. - ISBN 0-415-07892-x.

87. Quine, W.V. Philosophy of Logic / Willard Van Orman Quine/ London: Harvard University Press, Cambridge, Massachusetts and1.ndon, England,1994. 109 P. - ISBN 0-674-66563-5.

88. Robinson, J.A. Logic: Form and Function. The Mechanization of Deductive Reasoning / J. A. Robinson. Edinburg: Edinburg University Press, 1979. - 312 P. - ISBN 0-85224-305-7.

89. Russell, Bertrand. Mathematical logic as based on the theory of types // Russell, Bertrand. Logic and Knowledge. Essays 1901-1950. Edited by Robert Charles Marsh. London: Routledge, 1989. P. 59-102.-ISBN 0-415-09074-1.