Не подлежащее обследованию доказательство

В философия математики, доказательство, не подлежащее обследованию - это математическое доказательство, которое считается невозможным для человека-математика проверить и поэтому вызывает споры. срок действия. Термин был введен Томасом Тимочко в 1979 году в ходе критики Кеннета Аппеля и Вольфганга Хакена компьютерного доказательства теорема о четырех цветах, и с тех пор применялась к другим аргументам, в основном к аргументам с чрезмерным разделением регистров и / или с частями, отправляемыми трудно проверяемой компьютерной программой. Возможность обзора остается важным фактором в вычислительной математике.

• 1 Аргумент Тимочко
• 2 Контраргументы против требований Тимочко о невозможности проведения обзора
• 3 Контрмеры против отсутствия возможности обзора
• 4 Ссылки

Тимочко утверждал, что три критерия определяют, является ли аргумент математическим доказательством:

• Убедительность, которая относится к способности доказательства убедить рационального доказывающего его заключения;
• Возможность обзора, который относится к доступности доказательства для проверки членами человеческого математического сообщества; и
• Формализуемость, которая относится к доказательству, апеллирующему только к логическим отношениям между концепциями для обоснования своего аргумента.

По мнению Тимочко, доказательство Аппеля-Хакена не соответствовало критерию обозримости, как он утверждал, заменяя эксперимент для дедукции :

… если мы примем [теорему о четырех цветах] как теорему, мы будем стремиться изменить смысл «теоремы» или, что более конкретно, изменить смысл основной концепции «доказательства».. … [] использование компьютеров в математике, как в [теореме четырех цветов], вводит эмпирические эксперименты в математику. Независимо от того, решим мы или нет считать [теорему четырех цветов] доказанной, мы должны признать, что текущее доказательство не является ни традиционным доказательством, ни априорным выводом утверждения из посылок. Это традиционное доказательство с пробелом или пробелом, которое заполняется результатами хорошо продуманного эксперимента.

— Томас Тимочко, «Проблема четырех цветов и ее философское значение»

Без возможности обзора, Доказательство может служить своей первой цели - убедить читателя в своем результате и все же не справиться со своей второй целью - просветить читателя относительно того, почему этот результат верен - оно может играть роль наблюдения, а не аргумента.

Это различие важно, потому что оно означает, что доказательства, не подлежащие проверке, подвергают математику гораздо более высокому риску ошибок. Убедительность может пострадать, особенно в случае, когда невозможность обзора связана с использованием компьютерной программы (которая может иметь ошибки ), особенно когда эта программа не опубликована. Как писал Тимочко:

Предположим, что какой-то суперкомпьютер был настроен на работу над согласованностью арифметики Пеано, и он сообщил о доказательстве несоответствия, доказательстве, которое было настолько длинным и сложным, что ни один математик не мог понять его, кроме самые общие термины. Можем ли мы иметь достаточно веры в компьютеры, чтобы принять этот результат, или мы сказали бы, что эмпирических доказательств их надежности недостаточно?

— Томас Тимочко, «Четырехцветная проблема и ее математическое значение»

Мнение Тимочко, однако, оспаривается аргументами о том, что доказательства, которые трудно исследовать, не обязательно так же недействительны, как доказательства, которые невозможно исследовать.

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

Аргумент в том же духе состоит в том, что разделение регистра является общепринятым методом доказательства, а доказательство Аппеля – Хакена является лишь крайним примером разделения регистра.

С другой стороны, тезис Тимочко о том, что доказательства должны быть по крайней мере возможными для обзора и что ошибки в доказательствах, которые трудно исследовать, с меньшей вероятностью попадут в поле зрения, обычно не оспаривается; вместо этого были предложены методы улучшения обзора, особенно компьютерных доказательств. Одним из первых предложений было распараллеливание: задачу проверки можно разделить между несколькими читателями, каждый из которых может изучить часть доказательства. Но современная практика, известная благодаря Flyspeck, состоит в том, чтобы представить сомнительные части доказательства в ограниченном формализме, а затем проверить их с помощью программы проверки доказательств, которая сама доступна для просмотра. Таким образом, доказательство Аппеля – Хакена было подтверждено.

Тем не менее, автоматическая проверка еще не получила широкого распространения.