Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
Это относится к математике в той же мере, что и к физике, лингвистике или биологии. Эволюция признанных критериев дока-
53
зательности — почти не исследованная тема в истории науки. Однако со времени Евклида неизменной остается идеальная структура математической демонстрации «неочевидной истины»: переход к ней от «очевидных» или установленных ранее посылок посредством серии явно выписанных «очевидно законных» элементарных умозаключений.
Таким образом, дедукция как общенаучный метод является методом математики par excellence. («Математическая индукция» явно восходит к этой же идее. Принцип индукции Пеано постулирует разрешение писать только первый и общий шаги доказательства и, таким образом, является по существу первым метаматематическим принципом. Это затемняется традиционным отнесением аксиомы Пеано к числу специальных (п. 4.7д), но так или иначе она принадлежит к фундаментальным архетипам математического мышления.)
Чем длиннее дедуктивное рассуждение, тем жестче требования к эксплицитности и нормализованноети его элементарных компонент. В конечном счете количество исходных данных в формальной математике так мало, что несоблюдение правил гигиены в длинных выводах ведет к распаду системы, если ее не корректировать извне. При индукции, напротив, сравнительно короткие выводы покоятся на обширном исходном материале: дарвиновскую концепцию эволюции объясняют школьникам, но жизни едва хватило бы, чтобы оценить убедительность ее доказательств. Аналогичное положение дел наблюдается в сравнительном языкознании при реконструкции праязыковых фактов. Поэтому здесь «правила вывода» не могут быть столь жестки, несмотря на картину младограмматиков.
2. Изложенные выше суждения согласуются с тем, что понятие формального вывода в языках 3?, является хорошим приближением к представлению об идеальном математическом доказательстве. Поэтому поучительнее рассмотреть различия между выводами и нашими повседневными аргументами.
а) Надежность принципов. Не только математика, заложенная в специальные аксиомы L^Set и LiAr, но даже логика языков 3?\ не является общепризнанной. В частности, после Брауэра оспаривается закон исключительного третьего. С этих крайне критических позиций наши «доказательства» в лучшем случае безупречно выводят бессмыслицу из лжи.
Быть совершенно глухим к этой критике математик не может себе позволить; вдумываясь в нее, следует по крайней мере осознать, что существуют объективно различные «степени доказательности» доказательств.
б) Уровни доказательности. Каждое предложенное доказательство апробируется на приемлемость математиками, иногда нескольких поколений. При этом подлежит уточнению и само до-
54
казательство, и его результат. Чаще всего доказательство является более или менее краткой схемой формального вывода в подходящем языке. Однако, как уже было отмечено, иногда утверждение р устанавливается посредством доказательства того, что доказательство Р существует. Эта иерархия доказательств существования доказательств в принципе может быть как угодно высокой. Мы снимаем ее с помощью высших логических или теоретикомножественных принципов, с которыми, однако, можно и не соглашаться. Работы по конструктивной математике пестрят утверждениями типа: «не может не существовать алгоритма, вычисляющего х» там, где классический математик сказал бы просто «х существует» или в крайнем случае «х существует и эффективно вычислим».
в) Ошибки. Особенности человеческой психики делают формальные выводы практически не поддающимися проверке, даже если согласиться, что в принципе это идеальный вид доказательства. Два обстоятельства действуют в одну сторону с губительным эффектом: формальные выводы гораздо длиннее текстов на арго; скорость их сознательного чтения человеком гораздо ниже.
Нередки доказательства одной теоремы на пяти, пятнадцати и даже пятидесяти страницах. Доказательства двух гипотез Бернсайда из теории конечных групп занимают около пятисот страниц каждое. Длина -соответствующих формальных выводов не поддается воображению.
Поэтому отсутствие ошибок в математической работе, (если они не обнаружены), как и в других естественных науках, часто устанавливается по косвенным данным: имеет значение соответствие с общими ожиданиями, использование аналогичных аргументов в других работах, разглядывание «под микроскопом» отдельных участков доказательства, даже репутация автора; словом, воспроизводимость в широком смысле -слова. «Непонятные» доказательства могут сыграть очень полезную роль, стимулируя поиски более доступных рассуждений.
В последние десятилетия появилось очень мощное средство для проведения длинных формальных выводов: речь идет об ЭВМ. На поверхностный взгляд это может резко изменить статус формального вывода и сделать достижимым лейб-ницев идеал механической проверки истинности. На самом деле положение дел гораздо менее тривиально.
Приведем сначала два авторитетных мнения на этот -счет, принадлежащие К. Л. Зигелю и X. П. Ф. Суиннертону-Дайеру [32, 33]. Оба высказывались по поводу машинной обработки конкретных теоретико-числовых задач.
