Доказательство против понимания в математическом доказательстве | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2020. № 54. DOI: 10.17223/1998863X/54/3

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

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

Proof Versus Understanding in Mathematical Proof.pdf Противопоставление математической концепции и эпистемологической категории не приводит к ясной постановке проблемы. Фактически обсуждение начинается с обсуждения вопросов, которые напрямую имеют отношение к некоторым особенностям математической практики. Одним из самых интересных таких вопросов является вопрос, зачем математики передоказывают теоремы [1]. Самый простой ответ - чтобы лучше их понять. Так возникает вопрос о соотношении доказательства и понимания. Здесь возникает ряд проблем, типичных для философии математики. Во-первых, если сама по себе теорема является осмысленным истинным утверждением только в том случае, если у нее есть доказательство, теорема в каком-то смысле отождествляется с ним. Если же представлено новое доказательство, остается ли первоначальная теорема той же самой или при этом возникает новая теорема? Во-вторых, в чем состоят новые более высокие эпистемические требования при передоказательстве теоремы? То есть в чем состоит большая «понятность» теоремы: это может быть более полное постижение сути теоремы, или же это может быть улучшение самого доказательства? Уже эти вопросы поднимают массу проблем, которые откровенно присутствуют в математической практике, но не артикулированы в достаточной степени для более или менее строгого обсуждения. Тем не менее в последнее время оба сообщества - работающие математики и философы математики - проявляют к этой проблематике значительный интерес [2]. Более точная постановка проблемы состоит в обсуждении противоречий между современной концепцией доказательства и неформальным постижением содержания математического утверждения. Я. Хакинг настойчиво говорит о двух видах доказательств, которые напрямую увязывают эти две вещи. Концепция непосредственного постижения математического утверждения приписывается им Р. Декарту, и в качестве примера (который используется не только им) приводится описание эпизода из Менона Платона с удвоением площади квадрата. Другая концепция приписывается Лейбницу, у которого доказательство есть вычисление. Крайнее выражение этой тенденции представлено программой В. Воеводского, согласно которой любое математическое доказательство должно сопровождаться компьютерной его проверкой [3. C. 61-62]. Эти две концепции доказательства апеллируют к разным сторонам процесса математического дискурса. Концепция строгого доказательства обязана понятию логического следования А. Тарского. Стандартным изложением этого понятия стала книга П. Суппеса, согласно которой математическое доказательство есть последовательность предложений, начинающихся с аксиом, каждое из которых есть логическое следствие предыдущих предложений. Это представление обеспечивает «полностью точную теорию вывода, адекватную для всех стандартных примеров дедуктивного вывода в математике» [4. P. xii]. В общем, такая же цель, среди прочих, фигурировала при построении системы Principia Mathematica Уайтхеда и Рассела, поскольку система была призвана кодифицировать математическое мышление. Согласно этому идеалу строгое доказательство разбивает реальный «ход мысли» математика на небольшие шаги, каждый из которых санкционирован правилами вывода формальной системы. На практике математик опускает тривиальные логические выводы, делает неявные предположения, которые должны быть выявлены и восстановлены в формальном доказательстве. И опять-таки реальная математическая практика полностью избегает реализации такого идеала, подразумевая при этом, что идеал верен «в принципе». Таким образом, в реальном математическом доказательстве кроется две ипостаси: с одной стороны, «содержательное» доказательство, оперирующее с концепциями, определениями, неформальными вербальными оборотами, и с другой стороны, «формальная», знаки которой лишены всякого содержательного значения. Обе ипостаси связаны понятием интерпретации, придания намеренного значения знакам формального доказательства. Но на практике каждая из них существует как-бы по отдельности, выполняя свое предназначение. Одна призвана передать мысль, содержание концепций, а другая -блюсти строгость этой передачи, дабы не допустить ее искажения и уж тем более потери истинности утверждений. Такой дуализм математического дискурса требует более точного представления о том, что же при этом происходит. Как соотнести содержательную сторону концепций математики с формальным изложением доказательства? Должны быть какие-то объяснения одного в терминах другого, в противном случае мы имеем две параллельные структуры мышления, одна из которых близка реальному процессу человеческого рассуждения, а вторая -механическому, машинному представлению мыслительного процесса. Так что же делает математик, доказывая теорему, - дает простор ассоциативному мышлению или имитирует компьютер (который, по своему замыслу, сам должен имитировать мышление)? Хотя работающий математик практически никогда не воспроизводит доказательство в строго формальном виде, он уверен, как отмечалось выше, что это можно сделать «в принципе». Данная возможность «в принципе» реализуется в виде описания того, как это можно было бы сделать. Здесь мы имеем ситуацию, аналогичную ситуации соотношения языка и метаязыка, т.е. соотношения двух уровней дискурса. Неформальный текст высокого уровня указывает на существование текста низкого уровня; первый вид дискурса есть описание второго - формального доказательства. Такая концепция является довольно распространенной [5]. Однако она становится проблематичной, если принимаются во внимание два типа доказательства: доказательство как размышление (Декарт) и доказательство как вычисление (Лейбниц). Одно может быть сделано описательно, другое - в виде инструкции; одно может быть сделано в рамках принятых нотационных преобразований, другое - в словесной форме [6]. Что такое в данном случае словесная форма? Это принятые в дискурсе дескриптивные фразы, за которыми лежит принадлежность к определенной «языковой игре», в смысле Витгенштейна. Эти фразы несут смысл, доступный игрокам, и их буквальное толкование отнюдь не исчерпывает их значения. Более того, каждая из таких фраз означает практически указание, как должно идти доказательство. Их примерами являются фразы типа: «отсюда, по принципу вполне-упорядочения...», «по определению простого числа...», «первый закон может быть доказан индукцией по n...» и т.д., которые можно найти во множестве действительных доказательств. Правила подобных языковых игр сложны, и сама проблема передачи значения с помощью этих правил является сложной философской проблемой, косвенно связанной с так называемой проблемой следованию правилу [7]. В любом случае формальное доказательство само по себе не дает понимания, поскольку знаки в последовательности формул при логическом выводе не имеют значения. Конечно же, имеется подразумеваемая или намеренная интерпретация этих знаков, но она присоединяется к знакам «извне», к уже существующей формальной системе, которая обладает своего рода автономией. Поэтому можно предположить, что математическое понимание зиждется не в практике математического доказательства, но в каком-то другом аспекте математической практики. Это является кардинальной проблемой философии математики. Что же представляет собой математическое доказательство -формально-логическую структуру или же какого-то рода дополнительные соображения (среди которых могут быть и соображения о намеренной интерпретации). Эти соображения могут быть названы концептуальным окружением формального доказательства. Действительно, доказательством вполне можно считать формальную структуру, потому что именно она является свидетельством правильности доказательства. Но это свидетельство само по себе есть продукт определенного понимания, что формализация является надежным средством подтверждения истинности, что практическая невыполнимость полной формализации любого доказательства компенсируется пониманием того, что формализация в принципе возможна и т.д. Другими словами, если считать формальное доказательство настоящим доказательством, то оно должно сопровождаться пониманием всех этих оговорок. Это означает, что фактически апелляция к формальному доказательству сопряжена с необходимостью обращения к содержательным аспектам математического мышления. Такой половинчатой позиции придерживается К. Мандерс, признающий формальное доказательство настоящим доказательством, но одновременно выводящий понимание доказательства за пределы формальной структуры [8]. Нужно понимать, что различение в доказательстве двух ипостасей -формализма и понимания - может быть выражено с точки зрения философии в очень расплывчатых терминах. Только что приведенная точка зрения намекает, что помимо формализма, который и есть, по сути, само доказательство, существует и другой фактор: формальное доказательство является правильной кодификацией математического понимания, и стало быть, в качестве «фона» присутствует это самое понимание, занимая подчиненное положение. Другой подход к данной проблеме состоит в различении природы формализации и понимания. Формализация является синтаксической, в то время как понимание - семантический феномен. При этом предполагается, что, во-первых, семантика несводима к синтаксису, и, во-вторых, суть доказательства как раз зиждется на семантике, определенном кластере концепций. Реальное математическое мышление состоит в ассимиляции и понимании значений этих концепций [9]. Однако нельзя сказать, как и в предыдущем случае, что есть ясность в такого рода объяснениях. Скорее, речь идет о нащупывании философских оснований очень тонкого различения, а сама эта задача является типичной философской, когда нет четко поставленного вопроса. Помимо этого, сюда вплетаются вопросы сопоставления возможности человеческого мышления и машинного мышления, поскольку понимание относится к первому, а формализация - ко второму. А эти вопросы связаны, в свою очередь, с более общими вопросами алгоритмизации мышления [10]. Рассмотренные варианты соотношения формального доказательства и математического мышления могут быть выстроены в четкую альтернативу: либо математическое доказательство отлично от его формального представления, либо математическое доказательство является формальным. В первом случае речь идет о концепции понимания доказательства, а во втором - о правильности доказательства, понимание которого нам недоступно. В некотором смысле это настоящий парадокс: если наша логика является подходящим инструментом дедуктивного мышления, то как могут нормы, управляющие математическим дискурсом, на самом деле расходиться с нормами знакомых логических выводов? Другими словами, почему концептуальная ясность математики существенно отлична от формальной ясности? В математике мы заинтересованы в непротиворечивости или даже в истинности утверждений. Именно достижению этих целей служит концепция формального доказательства; управляемые логическими константами, а значит, формальные доказательства должны быть машинно-проверяемы. Но тогда откуда берется «несводимое математическое содержание», о котором говорит Рав? Именно ему отводится важная роль в понимании математического дискурса: У. Терстон утверждает, что надежность математического дискурса происходит не от математически проверяемых формальных аргументов; она происходит от математического и тщательного обдумывания математических идей [11]. Представленную выше коллизию можно отобразить на старую дихотомию, а именно дихотомию формы и содержания. Собственно математический дискурс, или же математическое размышление, происходит на содержательном уровне. Переходы между идеями должна обеспечить логика, и во имя ясности и отсутствия противоречий логические шаги должны быть механическими, т.е. лишенными значения. Тогда дилемма заключается в том, как задать синтаксическую логику без потери значения кодифицируемых идей. Преимущество философии, как уже упоминалось выше, состоит в постановке вопросов, на которые нет ответов. Таким вопросом в данном случае будет вопрос: можно ли сделать так, чтобы семантическое содержание математики представлялось в логической форме? При кажущейся противоречивости такой постановки вопроса он вполне осмыслен. Почти сразу можно указать несколько попыток снабдить синтаксис семантикой. Наиболее распространенным является метод моделей А. Тарского. Задаваемая им структура логики включает логические константы, машинерию квантификации (включая понятие переменной для индивидов), а также нелогические константы, которые не указывают на конкретные сущности, но могу применяться к разным структурам. В данном случае семантическая компонента обеспечивается интерпретацией нелогических констант и кванторов. Формальное строгое доказательство не опирается на такую интерпретацию, т.е. невосприимчиво к экстралогическим значениям. Но подразумеваемая аппаратом квантификации область значений (универсум рассмотрения) является «мостиком» к семантике. Другими словами, чистая логика, по Тарскому, апеллирует неявно к структурам, к моделям. Природа этой апелляции представляет в исследуемой проблеме ключевой интерес [12]. Именно то обстоятельство, что нелогические константы имеют множество потенциальных интерпретаций, требует от математического дискурса максимальной строгости. Интерпретации используют терминологию, которая не является строго изолированной от остального математического дискурса, за счет чего доказательство может оказаться дефектным: «...немногие, по-видимому, в равной степени осознают ловушки, которые мы ставим перед собой, когда используем общие слова для обозначения математических понятий. Ибо такие слова имеют много ассоциированных значений, не имеющих отношения к задаче строго дедуктивной науки, и эти ассоциированные значения влияют на нас в ущерб строгости» [13. P. 142] Избежать этой опасности (но одновременно и источника семантических интерпретаций) можно только допущением в математический дискурс примитивных терминов, строгое определение которых обеспечит единственность интерпретации. Но уже сам список примитивных терминов в достаточной степени очертит круг семантических концепций, с которыми имеет дело конкретный математический дискурс. Однако в процессе определения примитивных терминов делаются разъяснения (установление связи с другими терминами и пр.), которые обеспечивают то самое понимание на семантическом уровне, которое мы ищем в синтаксических структурах. Другими словами, наличие в формальном синтаксисе в стиле Тарского области интерпретации является фоновым семантическим фактором. Другим семантическим фактором будет употребление знаков, скажем, нелогических констант. Как утверждает Д. Макбет, понятие строгого формального доказательства должно пониматься, так сказать, осмысленно: «Все, что требует строгость, - это чтобы в системе не делалось никаких шагов, кроме тех, которые разрешены аксиомами, определениями и данными правилами вывода, которые служат для обеспечения того, чтобы все предположения были сделаны явными. Хотя и верно, что возможность следовать правилам механически, как если бы нелогические примитивные знаки не имели никакого значения, может служить проверкой адекватности системы аксиом и определений, из этого просто не следует, что знаки следует воспринимать как пустые от всякого смысла и значения» [14. P. 37]. Далее Макбет ссылается на Фреге, и эта ссылка не является «проходной»: «.. .можно, конечно, употреблять числовые знаки механически, как можно говорить подобно попугаю... [Но] это возможно только после того, как посредством действительного мышления математический знаковый язык разовьется так, что он, как говорят, мысли за нас» (цит. по: [15. С. 18]). И далее Макбет продолжает цитирование Фреге, говоря, что «использование символов не должно приравниваться к бездумной, механической процедуре... Можно мыслить и символами» [16. P. 33]. Если Фреге прав, математики разрабатывают системы письменных знаков не для того, чтобы обойтись без всякого содержания, а для того, чтобы выразить содержание таким образом, чтобы на основе этого содержания можно было строить строгие рассуждения. Только что высказанное мнение Макбета о том, что нотация Фреге, первоначально кажущаяся очень трудно воспринимаемой, содержит на самом деле важные соображения о вхождении семантического содержания в синтаксические структуры, начинает обсуждаться более активно. Это означает, что истоки семантики могут зиждиться в нотационных особенностях. Довольно любопытно, что проблемы соотношения семантики и синтаксиса в математическом дискурсе давно являлись предметом рассмотрения ранних аналитических философов, о чем говорит пример Фреге. И не только его. Недавно переоткрытая так называемая Подстановочная теория Рассела основана на понятии структурированной переменной, которая, будучи чисто синтаксическим элементом языка, тем не менее, содержит в себе семантические структуры [17]. Видимо, для установления проблематики соотношения понимания и доказательства в математическом дискурсе, помимо анализа собственно математического мышления, требуется обращение к логическим основаниям, еще более ранним, чем концепция логического следования Тар-ского. В заключение мы хотим вернуться к идее о том, что математический дискурс осмыслен, несмотря на формальное его представление, являясь некоторой языковой игрой, где основное положение занимает понятие правила. Апелляция к понятию логической формы математического вывода фактически, согласно этой идее, равносильна применению чего-то более общего, схемы или правила, которое применяется не только в данном случае, но и в других, релевантных ему. Обращение к витгенштейновской идее с первого взгляда позволяет ликвидировать противопоставление логической формы понятию семантического содержания, содержания, существенного для понимания и истины. С точки зрения Макбета, как логический вывод, так и «содержательный вывод» является примером правила, которое применяется и в других случаях: «Например, умозаключение (материальное) от „Феликс-кошка" к „Феликс-млекопитающее". Этот вывод хорош, если он хорош, потому что из того, что нечто является кошкой, можно вообще сделать вывод, что это млекопитающее; вывод хорош (если он хорош), потому что выводы вида „r-кошка; следовательно, х-млекопитающее" хороши. Вывод хорош не в силу того, что он касается Феликса. Хотя кто-то и делает какие-то выводы о Феликсе, обоснованность этого вывода объясняется не ссылкой на Феликса, а апелляцией к правилу, что-то вроде того, что быть кошкой означает быть млекопитающим» [14. Р. 39]. Выше приведен весьма неполный набросок путей преодоления конфликта между пониманием доказательства и его формальным представлением. Он дает представление о спектре возможностей в этом направлении. И все же остается ощущение, что центральный вопрос все больше обходит стороной математическую практику, склоняя его исходную формулировку либо в сторону логики или философии Витгенштейна, либо в сторону наивных предположений, что синтаксис сам по себе не является жизнеспособной идеей. Работающий математик согласится с тем, что хотя любое умозаключение и справедливо в силу своей формы, действительное математическое рассуждение есть рассуждение из содержания понятий, из математических идей. Это содержание формируется в системе (по выражению Д. Гильберта) «хорошо подобранных определений». Определения выступают в обсуждаемом нами вопросе в двоякой роли: с одной стороны, это сокращения, с другой стороны, они представляют собой математическое содержание. Вполне разумно рассматривать их как искомый пункт контакта между формой и содержанием, между формальным доказательством и математическим пониманием. Действительно, «математики часто считают нахождение правильного / подходящего / корректного / естественного определения в качестве цели исследования, а успех-нахождение „правильного" определения - значительным прогрессом в знаниях» [18. P. 256]. Уже сам перечень «добродетелей» определения говорит о том, что в них концентрируется понимание математического дискурса, поскольку сам эффект передоказывания теорем, с обсуждения которого мы начали статью, состоит в тривиализации сложного результата с помощью «хорошо подобранных определений». Результат такой тривиализации может считаться прогрессом в «понимании». Этого не могло бы случиться, будь определение простым нотационным сокращением. Это означает, что рассмотрение роли определений в экспликации концепции понимания математического дискурса является еще одним путем исследования этого феномена. Наконец, пожалуй, самым трудным вопросом является то, в какой степени содержание математического дискурса зависит от нотационных факторов. Нотация принятой математической логики намеренно лишена содержания. Но может быть, другие нотационные системы более близки к тому, чтобы в них формулировать содержательные вещи. Такие нотационные варианты нужно искать в «нестандартных» представлениях математического доказательства. В качестве примера этого подхода можно говорить о роли диаграмм, двухмерных формул Begriffsschrift Фреге, алгебраических уравнений. Макбет заверяет нас, что Фреге преуспел в такого рода предприятии: «Фреге явно и сознательно разработал свою странную двумерную нотацию, чтобы выразить математическое содержание таким образом, который позволял бы строгое рассуждение на основе этого содержания. И в части III своей логики 1879 г. он доказывает теорему на основе явных определений, которая призвана точно проиллюстрировать, как строго дедуктивное доказательство в его языке может быть амплиативным, то есть представлять собой реальное расширение нашего знания. Если Фреге прав, то его язык - это именно то, что нам нужно показать, а не просто способ описать как содержание математических понятий, так и цепочки рассуждений, которые ведут нас от определений понятий к теоремам, раскрывающим логические отношения между этими определенными понятиями. Конечно, мы не сможем даже начать понимать, как это могло быть так, пока мы продолжаем читать его нотацию как просто вариант нашей собственной» [14. P. 50-51]. Правда, освоение фрегевской нотации представляет не меньшие трудности для понимания математического дискурса. Но может быть, дело в том, что и это является особой языковой игрой. Витгенштейн часто прибегал при обсуждении этого понятия к шахматам. Тогда все согласятся с тем, что шахматы требуют практики и умения, дабы видеть смысл в позициях и таким образом понимать всю игру. И опять-таки, проблема понимания такой знаковой системы как математическое доказательство должна решаться обращением к понятию языковой игры. В какой степени данный подход окажется плодотворным, а не просто поверхностной аналогией, зависит от множества факторов, требующих дополнительного исследования.

Ключевые слова

понимания, доказательство, семантика, синтаксис, нотация, интерпретация, understanding, proof, semantics, syntax, notation, interpretation

Авторы

ФИООрганизацияДополнительноE-mail
Целищев Виталий ВалентиновичИнститут философии и права Сибирского отделения Российской академии наукдоктор философских наук, профессор, научный руководительleitval@gmail.com
Хлебалин Александр ВалерьевичИнститут философии и права Сибирского отделения Российской академии науккандидат философских наук, заместитель директора по научной работеsasha_khl@mail.ru
Всего: 2

Ссылки

Dawson J. W. Why Prove It Again. New York : Springer, 2015.
Avigad J. Understanding Proofs // The Philosophy of Mathematical Practice / ed. P. Mancosu. Oxford : Oxford University Press, 2008. P. 316-353.
Хакинг Я. Почему вообще существует философия математики? М. : Канон+, 2020.
Suppes Р. Introduction to Logic. New York : Van Nostrand Reinhold, 1957.
Avigad J. Mathematical Method and Proof // Synthese. 2006. Vol. 153. P. 105-159.
Azzouni J. Tracking Reason: Proof, Consequence, and Truth. Oxford : Oxford University Press, 2006.
Ладов В.А. Иллюзия значения: проблема следования правилу в аналитической философии. Томск : Изд-во Том. гос. ун-та, 2008.
Manders K. Logic and Conceptual Relationship in Mathematics // Logic Colloquium'85. North-Holland : Elsevier Science, 1987. P. 193-211.
Rav Y. Why Do We Prove Theorems? // Philosophia Mathematica. 1999. Vol. 7. P. 5-41.
Целищев В.В. Алгоритмизация мышления: геделевский аргумент. Новосибирск : Параллель. 2005.
Thurston W. On Proof and Progress in Mathematics // 18 Unconventional Essays on the Nature of Mathematics / ed. R. Hersh. New York : Springer, 2006. P. 37-55.
Pattersen D. Alfred Tarski: Philosophy of language and logic. Palgrave, 2012.
Nagel E. The Formation of Modern Conceptions of Formal Logic in the Development of Geometry // Teleology Revisited and Other Essays in the Philosophy and History of Science. New York : Columbia University Press, 1979. P. 130м152.
Macbeth D. Proof and Understanding in Mathematical Practice // Philosophia Scientiae. 2012. Vol. 16 (1). P. 29-54.
Фреге Г. Основоположения арифметики / пер. В.А. Суровцева. Томск : Водолей, 2000.
Frege G. Philosophical and Mathematical Correspondence / G. Gabriel et al. (eds.). Chicago : University of Chicago Press, 1980.
Halimi D. Structured Variables // Philosophia Mathematica. 2013. Vol. 21, № 2. P. 220-246.
Tappenden J. Mathematical Concepts and Definitions // The Philosophy of Mathematical Practice / ed. Mancosu P. Oxford : Oxford University Press, 2008.
 Доказательство против понимания в математическом доказательстве | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2020. № 54. DOI: 10.17223/1998863X/54/3

Доказательство против понимания в математическом доказательстве | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2020. № 54. DOI: 10.17223/1998863X/54/3