Каковы философские последствия использования компьютеров в науке и математике?

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

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

С тех пор было указано, что «абсолютная уверенность» никогда не была абсолютной, и проблемы с общественным признанием доказательств возникли не из-за компьютеров. Например, доказательство теоремы четырех красок Кемпе 1879 года принималось как таковое в течение 11 лет, пока Хивуд не нашел в нем изъян. Ожесточенные дебаты о роли строгости и экспериментов/моделирования начались, когда Джаффе и Куинн в 1993 г. предложили реализовать идею Тимочко путем разграничения «теоретической» (по образцу теоретической физики) и «строгой» математики институционально, в публикациях и т. д. См. обсуждение и ссылки в разделе Что делает что-то математика?Идея институционализации не прижилась (некоторые видели в предложении Джаффе-Куинна попытку обесценить «теоретическую математику»), но четкое разграничение предположительного/эвристического материала остается неформальной нормой. Также ожидается, что любое существенное использование компьютерных инструментов, даже в расчетах, не говоря уже о доказательствах, будет явно упомянуто и описано достаточно, чтобы его можно было воспроизвести (что аналогично отчету об экспериментах в науке).

Но заламывание рук по поводу «абсолютной» строгости — не единственная забота. Хэмминг , чья математика была ориентирована на информатику, хорошо известен тем, что заметил, что « печатание не заменит мышление » и « цель вычислений — понимание, а не числа ». Можно относиться к этому прагматично, а можно относиться более фундаментально. Даже с практической точки зрения моделирование движений ураганов, скажем, может дать нам предсказания, но не почему .они такие и такие. Когда модели расходятся во мнениях, мы остаемся в неведении, потому что отсутствует ключевой элемент понимания. А в кантианской/интуиционистской концепции математики и математической достоверности пропасть между доказательствами, сделанными человеком и компьютером, больше, чем вопрос степени. То, что дедукция представляет собой доказательство, пока каждый ее шаг соответствует «правилам», является формалистской идеей. Но не все ученые или математики формалисты. Для некоторых существует тот неуловимый аспект интуитивного понимания, без которого доказательство в лучшем случае является слепым расчетом с прикрепленным клеймом неполноценности. «Понимание» просто не происходит вне понимающего, и доказательство не есть доказательство, пока оно не понято. Подобные чувства затрагивают рецепцию квантовой механики, жалобы на «не редкость.

В «Заметках об основаниях математики » еще до появления компьютеров Витгенштейн определил общий феномен, который подпитывает такие опасения. Чтобы сделать компьютер способным помочь в доказательстве, требуется множество лингвистических преобразований. Обычно мы предполагаем «прозрачность языка» и рассматриваем их как преобразование «одних и тех же» вычислений в разные формализмы, но предполагаемые «преобразования» могут изменить концепцию того, что делается. « Опасная, обманчивая вещь » в нем состоит в том, что « он делает определение понятия — образование понятия — похожим на факт природы »:

« Математическое доказательство должно быть наглядным... Доказательство должно быть конфигурацией, точное воспроизведение которой может быть достоверно... То, что нас убеждает, — это и есть доказательство: конфигурация, которая нас не убеждает, не есть доказательство, даже когда она может быть показано для иллюстрации доказанного предложения Это означает: не должно быть необходимости проводить физическое исследование конфигурации доказательства, чтобы показать нам то, что было доказано.

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

[...] Я хотел бы сказать, что это не логика, которая заставляет меня принять предложение ... когда в первых двух парах скобок миллион переменных и два миллиона в третьей. Я хочу сказать: логика не заставила бы меня принять в данном случае вообще какое-либо положение. Что-то другое заставляет меня принять такое положение как логичное... Я хочу сказать: логикой Principia Mathematica можно было бы обосновать арифметику, в которой 1000 + 1 = 1000; и все, что для этого нужно, — это усомниться в разумной правильности вычислений. Но если мы не сомневаемся в этом, то дело не в нашей убежденности в истинности логики. "

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

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