Доказательство против понимания в математическом доказательстве
В.В. Целищев, А.В. Хлебалин
Противопоставление математической концепции и эпистемологической категории не приводит к ясной постановке проблемы. Фактически обсуждение начинается с обсуждения вопросов, которые напрямую имеют отношение к некоторым особенностям математической практики. Одним из самых интересных таких вопросов является вопрос, зачем математики передоказывают теоремы [1]. Самый простой ответ - чтобы лучше их понять. Так возникает вопрос о соотношении доказательства и понимания.
Здесь возникает ряд проблем, типичных для философии математики. Во- первых, если сама по себе теорема является осмысленным истинным утверждением только в том случае, если у нее есть доказательство, теорема в каком-то смысле отождествляется с ним. Если же представлено новое доказательство, остается ли первоначальная теорема той же самой или при этом возникает новая теорема? Во-вторых, в чем состоят новые более высокие эпистемические требования при передоказательстве теоремы? То есть в чем состоит большая «понятность» теоремы: это может быть более полное постижение сути теоремы, или же это может быть улучшение самого доказательства? Уже эти вопросы поднимают массу проблем, которые откровенно присутствуют в математической практике, но не артикулированы в достаточной степени для более или менее строгого обсуждения. Тем не менее в последнее время оба сообщества - работающие математики и философы математики - проявляют к этой проблематике значительный интерес [2]. доказательство математический теорема дедуктивный
Более точная постановка проблемы состоит в обсуждении противоречий между современной концепцией доказательства и неформальным постижением содержания математического утверждения. Я. Хакинг настойчиво говорит о двух видах доказательств, которые напрямую увязывают эти две вещи. Концепция непосредственного постижения математического утверждения приписывается им Р. Декарту, и в качестве примера (который используется не только им) приводится описание эпизода из Менона Платона с удвоением площади квадрата. Другая концепция приписывается Лейбницу, у которого доказательство есть вычисление. Крайнее выражение этой тенденции представлено программой В. Воеводского, согласно которой любое математическое доказательство должно сопровождаться компьютерной его проверкой [3. C. 61-62]. Эти две концепции доказательства апеллируют к разным сторонам процесса математического дискурса.
Концепция строгого доказательства обязана понятию логического следования А. Тарского. Стандартным изложением этого понятия стала книга П. Суппеса, согласно которой математическое доказательство есть последовательность предложений, начинающихся с аксиом, каждое из которых есть логическое следствие предыдущих предложений. Это представление обеспечивает «полностью точную теорию вывода, адекватную для всех стандартных примеров дедуктивного вывода в математике» [4. P. xii]. В общем, такая же цель, среди прочих, фигурировала при построении системы Principia Mathematica Уайтхеда и Рассела, поскольку система была призвана кодифицировать математическое мышление.
Согласно этому идеалу строгое доказательство разбивает реальный «ход мысли» математика на небольшие шаги, каждый из которых санкционирован правилами вывода формальной системы. На практике математик опускает тривиальные логические выводы, делает неявные предположения, которые должны быть выявлены и восстановлены в формальном доказательстве. И опять-таки реальная математическая практика полностью избегает реализации такого идеала, подразумевая при этом, что идеал верен «в принципе». Таким образом, в реальном математическом доказательстве кроется две ипостаси: с одной стороны, «содержательное» доказательство, оперирующее с концепциями, определениями, неформальными вербальными оборотами, и с другой стороны, «формальная», знаки которой лишены всякого содержательного значения. Обе ипостаси связаны понятием интерпретации, придания намеренного значения знакам формального доказательства. Но на практике каждая из них существует как-бы по отдельности, выполняя свое предназначение. Одна призвана передать мысль, содержание концепций, а другая - блюсти строгость этой передачи, дабы не допустить ее искажения и уж тем более потери истинности утверждений.
Такой дуализм математического дискурса требует более точного представления о том, что же при этом происходит. Как соотнести содержательную сторону концепций математики с формальным изложением доказательства? Должны быть какие-то объяснения одного в терминах другого, в противном случае мы имеем две параллельные структуры мышления, одна из которых близка реальному процессу человеческого рассуждения, а вторая - механическому, машинному представлению мыслительного процесса. Так что же делает математик, доказывая теорему, - дает простор ассоциативному мышлению или имитирует компьютер (который, по своему замыслу, сам должен имитировать мышление)?
Хотя работающий математик практически никогда не воспроизводит доказательство в строго формальном виде, он уверен, как отмечалось выше, что это можно сделать «в принципе». Данная возможность «в принципе» реализуется в виде описания того, как это можно было бы сделать. Здесь мы имеем ситуацию, аналогичную ситуации соотношения языка и метаязыка, т.е. соотношения двух уровней дискурса. Неформальный текст высокого уровня указывает на существование текста низкого уровня; первый вид дискурса есть описание второго - формального доказательства. Такая концепция является довольно распространенной [5]. Однако она становится проблематичной, если принимаются во внимание два типа доказательства: доказательство как размышление (Декарт) и доказательство как вычисление (Лейбниц). Одно может быть сделано описательно, другое - в виде инструкции; одно может быть сделано в рамках принятых нотационных преобразований, другое - в словесной форме [6].
Что такое в данном случае словесная форма? Это принятые в дискурсе дескриптивные фразы, за которыми лежит принадлежность к определенной «языковой игре», в смысле Витгенштейна. Эти фразы несут смысл, доступный игрокам, и их буквальное толкование отнюдь не исчерпывает их значения. Более того, каждая из таких фраз означает практически указание, как должно идти доказательство. Их примерами являются фразы типа: «отсюда, по принципу вполне-упорядочения...», «по определению простого числа...», «первый закон может быть доказан индукцией по п...» и т.д., которые можно найти во множестве действительных доказательств. Правила подобных языковых игр сложны, и сама проблема передачи значения с помощью этих правил является сложной философской проблемой, косвенно связанной с так называемой проблемой следованию правилу [7].
В любом случае формальное доказательство само по себе не дает понимания, поскольку знаки в последовательности формул при логическом выводе не имеют значения. Конечно же, имеется подразумеваемая или намеренная интерпретация этих знаков, но она присоединяется к знакам «извне», к уже существующей формальной системе, которая обладает своего рода автономией. Поэтому можно предположить, что математическое понимание зиждется не в практике математического доказательства, но в каком-то другом аспекте математической практики. Это является кардинальной проблемой философии математики. Что же представляет собой математическое доказательство - формально-логическую структуру или же какого-то рода дополнительные соображения (среди которых могут быть и соображения о намеренной интерпретации). Эти соображения могут быть названы концептуальным окружением формального доказательства.
Действительно, доказательством вполне можно считать формальную структуру, потому что именно она является свидетельством правильности доказательства. Но это свидетельство само по себе есть продукт определенного понимания, что формализация является надежным средством подтверждения истинности, что практическая невыполнимость полной формализации любого доказательства компенсируется пониманием того, что формализация в принципе возможна и т.д. Другими словами, если считать формальное доказательство настоящим доказательством, то оно должно сопровождаться пониманием всех этих оговорок. Это означает, что фактически апелляция к формальному доказательству сопряжена с необходимостью обращения к содержательным аспектам математического мышления. Такой половинчатой позиции придерживается К. Мандерс, признающий формальное доказательство настоящим доказательством, но одновременно выводящий понимание доказательства за пределы формальной структуры [8].
Нужно понимать, что различение в доказательстве двух ипостасей - формализма и понимания - может быть выражено с точки зрения философии в очень расплывчатых терминах. Только что приведенная точка зрения намекает, что помимо формализма, который и есть, по сути, само доказательство, существует и другой фактор: формальное доказательство является правильной кодификацией математического понимания, и стало быть, в качестве «фона» присутствует это самое понимание, занимая подчиненное положение.
Другой подход к данной проблеме состоит в различении природы формализации и понимания. Формализация является синтаксической, в то время как понимание - семантический феномен. При этом предполагается, что, во- первых, семантика несводима к синтаксису, и, во-вторых, суть доказательства как раз зиждется на семантике, определенном кластере концепций. Реальное математическое мышление состоит в ассимиляции и понимании значений этих концепций [9]. Однако нельзя сказать, как и в предыдущем случае, что есть ясность в такого рода объяснениях. Скорее, речь идет о нащупывании философских оснований очень тонкого различения, а сама эта задача является типичной философской, когда нет четко поставленного вопроса. Помимо этого, сюда вплетаются вопросы сопоставления возможности человеческого мышления и машинного мышления, поскольку понимание относится к первому, а формализация - ко второму. А эти вопросы связаны, в свою очередь, с более общими вопросами алгоритмизации мышления [10].
Рассмотренные варианты соотношения формального доказательства и математического мышления могут быть выстроены в четкую альтернативу: либо математическое доказательство отлично от его формального представления, либо математическое доказательство является формальным. В первом случае речь идет о концепции понимания доказательства, а во втором - о правильности доказательства, понимание которого нам недоступно. В некотором смысле это настоящий парадокс: если наша логика является подходящим инструментом дедуктивного мышления, то как могут нормы, управляющие математическим дискурсом, на самом деле расходиться с нормами знакомых логических выводов? Другими словами, почему концептуальная ясность математики существенно отлична от формальной ясности?
В математике мы заинтересованы в непротиворечивости или даже в истинности утверждений. Именно достижению этих целей служит концепция формального доказательства; управляемые логическими константами, а значит, формальные доказательства должны быть машинно-проверяемы. Но тогда откуда берется «несводимое математическое содержание», о котором говорит Рав? Именно ему отводится важная роль в понимании математического дискурса: У. Терстон утверждает, что надежность математического дискурса происходит не от математически проверяемых формальных аргументов; она происходит от математического и тщательного обдумывания математических идей [11].
Представленную выше коллизию можно отобразить на старую дихотомию, а именно дихотомию формы и содержания. Собственно математический дискурс, или же математическое размышление, происходит на содержательном уровне. Переходы между идеями должна обеспечить логика, и во имя ясности и отсутствия противоречий логические шаги должны быть механическими, т.е. лишенными значения. Тогда дилемма заключается в том, как задать синтаксическую логику без потери значения кодифицируемых идей. Преимущество философии, как уже упоминалось выше, состоит в постановке вопросов, на которые нет ответов. Таким вопросом в данном случае будет вопрос: можно ли сделать так, чтобы семантическое содержание математики представлялось в логической форме?
При кажущейся противоречивости такой постановки вопроса он вполне осмыслен. Почти сразу можно указать несколько попыток снабдить синтаксис семантикой. Наиболее распространенным является метод моделей А. Тарского. Задаваемая им структура логики включает логические константы, машинерию квантификации (включая понятие переменной для индивидов), а также нелогические константы, которые не указывают на конкретные сущности, но могу применяться к разным структурам. В данном случае семантическая компонента обеспечивается интерпретацией нелогических констант и кванторов. Формальное строгое доказательство не опирается на такую интерпретацию, т.е. невосприимчиво к экстралогическим значениям. Но подразумеваемая аппаратом квантификации область значений (универсум рассмотрения) является «мостиком» к семантике. Другими словами, чистая логика, по Тарскому, апеллирует неявно к структурам, к моделям. Природа этой апелляции представляет в исследуемой проблеме ключевой интерес [12]. Именно то обстоятельство, что нелогические константы имеют множество потенциальных интерпретаций, требует от математического дискурса максимальной строгости. Интерпретации используют терминологию, которая не является строго изолированной от остального математического дискурса, за счет чего доказательство может оказаться дефектным: «...немногие, по- видимому, в равной степени осознают ловушки, которые мы ставим перед собой, когда используем общие слова для обозначения математических понятий. Ибо такие слова имеют много ассоциированных значений, не имеющих отношения к задаче строго дедуктивной науки, и эти ассоциированные значения влияют на нас в ущерб строгости» [13. P. 142]