Phenomenological Extension of the Formal Proof Theory.pdf Введение В статье рассматривается становление современной теории доказательств с точки зрения феноменологии. Мотивом послужил тот факт, что именно теория доказательств обнажает череду следующих друг за другом логических и математических рефлексий. Эти рефлексии обусловлены естественным желанием посмотреть на себя со стороны сначала в одеянии «метаматематики», а затем в медитациях второго порядка о «математике метаматематики», когда изучаются формализованные языки при помощи универсальных алгебр или теории решеток. Феноменология не претендует на принципиальное решение логических проблем и математических задач, но она в состоянии содействовать научному успеху как в приложениях, так и в теоретических обобщениях. Более того, тесное взаимодействие символической логики, математической рефлексии и феноменологического анализа может оказаться весьма полезным для решения актуальных проблем оснований математики. Этому способствует то обстоятельство, что теория доказательств является точкой соприкосновения интересов математики, логики и феноменологии, объединяющей рефлексию, функциональное мышление и пространственные отображения. Данный тезис о возможности расширения формальной теории доказательств представляет собой формулировку теоремы, а все последующее изложение есть попытка ее доказательства в оправе феноменологических дескрипций. Идея заключается в том, чтобы достичь продуктивного синтеза математики, логики и феноменологии, опираясь на классическое наследие Фреге, Гильберта и Гуссерля. Основной вопрос, который затрагивает феноменология в рамках теории доказательств, есть ее специфический интерес: можно ли дать детализированное описание того, что мы реально делаем, проводя доказательства? Критика современных подходов и возможный синтез Философию математики принято считать исключительным достоянием «аналитической школы», некоторые догматы которой созвучны феноменоло- Ю.Г. Седов 42 гическим идеям. Профессиональные контакты Эдмунда Гуссерля с этим направлением достаточно тесные и конструктивные: Карл Вейерштрасс, Георг Кантор, Г оттлоб Фреге, Лейтзен Брауэр, кружок Давида Г ильберта, Бертран Рассел, Рудольф Карнап. Например, общей темой для Гуссерля и Фреге стал вопрос о различении смысла и значения, причем Фреге связывал свои размышления по данной проблеме с математическими доказательствами, полагая, что для некоторых доказательств имеет значение определенная знаковая конфигурация. Среди тех, кто озабочен проблемами взаимосвязи формализованных теорий и феноменологии сознания, нет единства, нет общей позиции, а есть только стремление действовать по принципу divide et impera. Но такая позиция поверхностна, за обсуждением вполне естественных различий во взглядах оппонентов теряется сама проблема. Подобную картину можно было наблюдать в недавних дискуссиях по поводу сближения математики, логики и феноменологии. Разумеется, возник вопрос о феноменологических основаниях математики. Но он затерялся в бесплодных противопоставлениях «Фреге или Гуссерль», хотя здравый смысл в данном случае говорит о конъюнкции. Содержание феноменологической идеи полностью вытесняется из рассмотрения в результате новой оппозиции, теперь между Брауэром и Гуссерлем. Многолетние исследования привели к выводу о тенденции гуссер-левской мысли к точке зрения Гильберта [1. P. 66]. С легкостью можно предсказать следующую «фундаментальную» тему о различиях между Гильбертом и Гуссерлем. Однако затронутые темы второстепенны, ибо математика не ограничивается Гильбертом, а философия - Гуссерлем. Продуктивный синтез возможен в условиях поиска общих точек соприкосновения. Феноменологию не следует рассматривать в качестве альтернативной версии теории доказательств. Она служит лишь частью более широкого системного подхода. И нет особой нужды противопоставлять феноменологию иным теоретическим конструкциям, ограничиваясь поиском различий, которые при желании всегда можно обнаружить во взглядах даже у представителей одной научной школы. Важными являются не мелкие различия между Гуссерлем, Фреге и Гильбертом по поводу аксиоматизации, а наметившиеся общие тенденции понимания сущности теории доказательств, характер которой объясняется включением понятия «интенсиональность». Необходимость такого включения была также осознана в конструктивной логике и математике, в сочинениях Брауэра и его последователей. Ярким примером может служить статья Аренда Г ейтинга, посвященная основаниям математики [2. Р. 107]. Здесь он представил интуиционистскую точку зрения и сделал попытку объяснить понятия пропозиции и доказательства в терминах, весьма близких языку феноменологии Гуссерля. Терминологические совпадения можно обнаружить во многих случаях. Например, исходное определение математики включает в себя указание на естественную функцию интеллекта и на живую активность мышления (lebendige Aktivitat des Denkens). В другом случае возможность познания (Erkenntnis) проявляет себя только в процессе самого познавания (Erkennen selbst), в процессе доказывания. Предложенные Гейтингом идеи привлекли внимание молодого Курта Гёделя, который в своем обзоре [3] откликнулся на вышеуказанную статью. В последующем Гёдель неоднократно обращался к идеям феноменологиче- Феноменологическое расширение формальной теории доказательств 43 ской философии Гуссерля и вплоть до конца своей активной деятельности серьезно изучал его сочинения. Если мы ищем точки соприкосновения логики, математики и феноменологии, не ограничиваясь поверхностными различиями, то было бы естественным решить вопрос: как понимать обращение Гёделя к философии Гуссерля, чего он хотел достичь, используя феноменологические методы в логических и математических исследованиях? Библиографические ссылки по данной теме можно найти в книге [4. P. 7]. В ней делается вывод о том, что для Гёделя феноменология представляла не законченную доктрину, а целую исследовательскую программу, которую можно модифицировать в свете дальнейшей рефлексии и опыта. О возможности феноменологического расширения формальной теории доказательств Обнаружение теоретико-множественных парадоксов и сомнения по поводу использования абстракций высокого уровня привели к формулировке «финитной» программы с целью осуществления последовательной аксиоматизации фундаментальных разделов математики при помощи самых надежных методов, имеющих характер элементарного комбинирования. Благодаря Г ильберту возросло значение аксиоматической теории в математике. Аксиоматическая теория доказательств несет на себе печать экзистенциального подхода, характеризуемого финитной установкой, свободной от антиномий и парадоксов, не приемлющей абстракцию актуальной бесконечности и ограничивающей применение логического закона tertium non datur. Одним из важнейших аспектов указанной программы является теория строгих «концептуально структурированных доказательств» [5. P. 7]. Главной идеей финитной программы оснований математики была разработка тщательно продуманной системы правил вывода, легко обозримой и обеспечивающей непротиворечивые результаты научных исследований. Обстоятельное рассмотрение начал арифметики, геометрии и алгебры предпринято с целью показать действие финитной установки, которая характеризуется принципиальной представимостью объектов и выполнимостью всех логических операций. Финитная теория доказательств имеет свои естественные пределы. Например, аналитические методы теории функций, дифференциальной геометрии, теории множеств и топологии нарушают границы финитной установки. Существуют также «нефинитные» подходы, связанные с применением неполных индуктивных определений. Использование бесконечной области индивидов сталкивается с необходимостью формализации выводов для доказательства непротиворечивости всего построения, приводя к формулировке проблем оснований математики. Понятие «основания математики» приемлемо здесь в расширенном смысле, включающем логические компоненты математических построений и осознание того, что наряду с привычными формальными структурами доказательств должна рассматриваться специфика самого процесса доказывания. По мнению Фреге, без такого рода средств было бы вообще невозможно строгое обоснование математики. Если используемые понятия не имеют исчерпывающего определения, они являются недопустимыми, мнимыми представлениями, дающими только частичное, неполное удовлетворение. Приме- Ю.Г. Седов 44 рами неудовлетворительных словообразований в математике могут служить такие понятия, как число, степень, величина, близость, часть, целое, и многие другие. Неудовлетворительным словообразованием является также отношение равенства (Gleichheitsbeziehung). В математической практике доказывания принято рассматривать равенство в качестве тождества, что теоретически не всегда оправдано. Проиллюстрируем данный тезис на двух простых примерах [6. Р. 75, 148-149]. Пример 1. Уравнение 4х - 3 = 3 имеет бесконечное количество корней, но для понимания сути дела достаточно двух: 6/4 и 3/2. Хотя они равны, никто не осмелится утверждать, что эти два корня совпадают по значению. Определение равенства в виде тождества иногда приводит к столкновению явно высказываемой теории с молчаливо практикуемыми методами доказательства и поспешными обобщениями. В подобных случаях значение доказываемых положений в математике должно быть подкреплено применением логических законов, обеспечивающим строгое разграничение понятий и дающим полные их дефиниции. Пример 2. Рассмотрим отношение равенства при совпадении функций. Допустим, что функция f(£) для того же самого аргумента имеет всегда то же самое значение, что и функция g(£). Это равенство можно записать следующим образом: f = g. Однако недопустимость такого всеобщего отношения обнаруживается при переходе к особенному случаю, поскольку оказывается несостоятельным отождествление формулы - 1 для функции f(E) с положением (£ - 1)(^ + 1) для функции g(£). Отсюда вытекает, что нельзя просто написать f = g, требуются дополнительные размышления о смысле и значении равенства, о фундаментальных законах логики, а также ясное осознание (mit vollem Bewusstsein) производимых арифметических действий. Данный подход к формализации представляется универсальным: он объединяет математические рефлексии, логические законы и строгий анализ структуры мысли. На том основании, что расширяющиеся математические функции могут интерпретироваться как продолжения, а логические функции как произвольные изменения, появилась задача провести строгую формализацию рассуждений в теории доказательств. Такая формализация связана с методом «арифметизации метаматематики», разработанным Гёделем [7]. Расширению финитной теории доказательств, в первую очередь, способствовало осознание того, что любой «не слишком узкий» формализм оказывается незавершенным. Именно здесь наметился выход за рамки финитной установки, обусловленный тем, что в доказательствах встречаются допущения, в которых говорится об истинности всеобщих предложений, когда некая формула оказывается истинной всегда при замене ее свободных переменных цифрами. Задача построения непротиворечивой формальной аксиоматики сущностным образом связана с вопросом о разрешимости. В узком смысле слова под разрешимостью понимается совокупность методов установления общезначимости и выполнимости формул. В случае конечного числа индивидов общезначимость и выполнимость представляют собой простой комбинаторный факт, который легко проверяется перебором всех возможных элементов исследуемой области. В случае бесконечной индивидной области последовательный перебор всех значений невозможен. И тогда очень важно выбрать подходящий предикат, например: «х больше у» или «у следует за х», отноше- Феноменологическое расширение формальной теории доказательств 45 ние близости между произвольными переменными, отношение целого к части и т.п. Вводимая нами идеализация должна быть непротиворечивой. Бесконечную индивидную область нельзя наглядно представить, но можно выявить косвенным образом через отношение между ее элементами, что выполнимо посредством направленной последовательности формул или простейшего алгоритма. Развитие понятия «алгоритм исчисления» произошло благодаря идее смоделировать интеллектуальную деятельность человека, например, последовательные действия логика, доказывающего теорему. В следующем определении я использую аналогию с «символьным пространством» Эмиля Поста, в котором может быть достигнуто решение определенной проблемы [8. P. 103]. Этот концепт применим к финитной теории доказательств. Я также следую здесь известному тезису Алана Тьюринга, который касается поведения вычислителя (behaviour of the computer) и состояния его ума (state of mind) в любой момент проведения операции [9. P. 250]. Пространство доказательств - это специфическая форма мышления, в которой реализуются доказательственные конструкции. Развитие теории доказательств свидетельствует о том, что данное пространство способно к сжатию и расширению, к поочередному усилению то содержательной, то формальной установки сознания. Современная теория доказательств выявила сугубо механический характер процедур рассуждения, оформившись в виде программы, предназначенной для моделирования работы человеческого мышления, после чего началась усиленная разработка машинно-ориентированных методов доказательства, связанных с пространственной интенцией. В силу этих и других обстоятельств теория доказательств трансформировалась в logic of proof, в логику доказуемости, которая предлагает подход к решению задач представления знаний, анализа систем формализации и проверки доказательств. Однако имеются все основания полагать, что финитные рассуждения могут быть расширены с помощью феноменологического подхода. Финитная программа оснований математики послужила исходной точкой последующих логических исследований. Логики поставили под вопрос априорный характер математики. В одной из своих поздних работ Пауль Бернайс признал, что логика и математика a priori не предопределены, но они вырастают на почве интеллектуального опыта. В качестве иллюстрации он использует генезис геометрических концептуальных формулировок в абстрактном мышлении. Бернайс даже апеллирует к аналитике сознания, когда предлагает рассматривать математику в качестве «теоретической феноменологии формальных структур» [10. P. 81-82]. Предметом феноменологии он считал объективность, отличную от реальных предметов природы. Кроме того, Гуссерль в третьем логическом исследовании (§ 24), подводя итоги учения о целом и части, однозначно заявляет о возможности перехода феноменологии к математически точным теориям [11]. Все дескриптивные феноменологические разъяснения указанной темы в принципе сводимы к простейшим формам, т.е. формализуемы. Для феноменологии здесь наиболее интересен переход к категориальному мышлению, которое оперирует частями совокупности определенного вида, в том числе математического. И что характерно, во всех подобных случаях категориальное мышление предпочи- Ю.Г. Седов 46 тает обходиться без понятия целого и намеренно упрощает ситуацию, ограничиваясь привычным сосуществованием частей. Разумеется, такая позиция удобна, но она оставляет в стороне некоторые существенные детали. А именно, любая классификация и любое ранжирование предлагают вниманию исследователя или пользователя некую целостность, состоящую из строго определенных частей, а вовсе не набор произвольно соединенных элементов. Позднее Гуссерль модифицировал свой подход, сфокусировав внимание на интуитивном содержании пространственного упорядочивания концептов [12. Р. 40]. Формальная теория доказательств и феноменология: Гёдель и Гуссерль Философские основания теории доказательств связаны с эпистемологическим анализом. После теорем о неполноте стало весьма затруднительно утверждать, что всякое суждение может быть либо доказано, либо опровергнуто. Это было настоящим вызовом, брошенным финитной программе оснований математики и соответствующей теории доказательств. В любой непротиворечивой системе можно сформулировать такие утверждения, которые на основании принятых аксиом нельзя будет ни доказать, ни опровергнуть, а внутри непротиворечивой системы невозможно дать доказательство ее собственной непротиворечивости. Однако не осталось без внимания то обстоятельство, что в отличие от первой теоремы - достаточно понятной вторая теорема остается весьма проблематичной и не укладывается в привычный математический контекст. Вторая теорема в большей мере соотнесена с модально-логическими свойствами формулы, выражающей доказуемость. Тут затрагиваются вопросы, выходящие за рамки математики, но ею инициируемые и связанные с пониманием природы ума, искусственного интеллекта и человеческого мышления. Согласно Гёделю, любые математические теории страдают неполнотой, хотя могут быть расширены за счет процедур, которые включали бы в себя абстрактные термы на основе их значений. Другими словами, нужны такие процедуры, в которые были бы включены некоторые элементы значения, что позволило бы решать проблемы, не поддающиеся машинной обработке. Гёдель не исключал возможности открытия подобного рода процедур. Они просто требуют более совершенного понимания работы ума, каковое может быть достигнуто, в частности, с помощью феноменологического метода. «По крайней мере, в трех пунктах мысль Гёделя обнаруживает черты логики Гуссерля: различие между двумя ориентациями в виде теории значений и теории объектов; рационалистический идеал, которым руководствуются математики; роль рефлексивного метода в математических науках» [13. P. 335-336]. Кроме того, Гёдель обращался к изучению сочинений Гуссерля в период между изданиями первой и второй версии статьи, посвященной континуум-гипотезе [14. P. 21]. Тщательное изучение Гёделем феноменологической философии было вызвано не предположением о независимости существования математических объектов, но скорее пониманием принципиальной важности интуитивного схватывания концептов. В феноменологии существенная роль отводится интуиции. Эйдетический метод «видения сущности» (Wesensschau) исполняет вполне определенную Феноменологическое расширение формальной теории доказательств 47 функцию в формальной логике, где мы обращаемся только к пропозициям, оставляя в стороне любые высказывания о свойствах объектов. Доказательство выстраивается на уровне аподиктической очевидности. В целом такое доказательство выглядит как рассуждение на основе заранее сформулированных аксиом и логических правил. На первый взгляд, здесь, казалось бы, нет места эйдетическим вариациям, но в действительности это наблюдается, например, когда исследователь присоединяет к системе аксиом дополнительные предположения, которые впоследствии оказываются нетривиальными и существенными для доказательства.

Скачать электронную версию публикации