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

• Ходикова, Нина Анатольевна
• кандидат философских наук
• 2004

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

Введение.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Введение диссертации (часть автореферата) на тему «Логико-методологическое исследование происхождения теории поиска вывода»

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

Наука как вид профессиональной деятельности существует сравнительно недавно, всего около четырех столетий. Но важность этого вида деятельности для общества была осознана почти одновременно с его появлением, и вслед за наукой возникла история науки как особая дисциплина, занимающаяся описанием научных достижений, открытий, поисков и даже ошибок. Долгое время историко-научные исследования представляли собой по преимуществу биографии великих ученых с подробным описанием их достижений и ошибок. Основой изложения служила хронология, и молчаливо предполагалось, что такой порядок компоновки материала сам по себе обеспечивает отображение внутренней логики развития научной мысли. Таким образом, история науки представлялась как история идей. С другой стороны, до 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 века, может успешно применяться к описанию и объяснению возникновения теорий в логике. Разработке этого перспективного вопроса автор планирует посвятить свои дальнейшие исследования.

Список литературы диссертационного исследования кандидат философских наук Ходикова, Нина Анатольевна, 2004 год

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.