В поисках теории поиска вывода

ЭПИСТЕМОЛОГИЯ & ФИЛОСОФИЯ НАУКИ • 2013 • Т. XXXVII • № 3

В

ПОИСКАХ ТЕОРИИ ПОИСКА ВЫВОДА

Е.Г. ДРАГАЛИНА-ЧЕРНАЯ

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

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

X

0)

2 й О

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

Современная металогика, использующая технику переводов и погружающих операций, существенно продвинулась в исследовании взаимоотношений логических теорий, основанных на различных категориальных и онтологических допущениях. Однако адекватная для решения многих металогических задач идеализирующая трактовка теории как множества предложений, замкнутых относительно логического следования, может затруднить постановку вопроса о генетической преемственности теорий, способах возникновения одной логической теории на основании другой, более ранней. Особым эвристическим потенциалом для теоретической реконструкции истории логики как истории смены логических теорий обладает теория доказательств. Ключом к такой ™ реконструкции оказывается обна-^^ ружение методологического аналога понятия интерпретации, играющего центральную роль как в Ф гильбертовской теории доказательств, так и в теории поиска выЙ вода. Такой аналог усматривается i^j авторами монографии в предло-—™ женной Грязновым поризматиче-

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

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

В ПОИСКАХ ТЕОРИИ ПОИСКА ВЫВОДА

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

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

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

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

Особое место в монографическом исследовании Брюшинкина и Ходиковой занимает анализ прило-

X

0)

2 Й о

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

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

Ф дирующее теорию поиска вывода

2 различение понятий вывода и поЮ иска вывода устраняет видимость

О

а

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

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

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