Не поддающиеся проверке доказательства

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

Аргумент Тимочко

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

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

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

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

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

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

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

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

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

Контраргументы заявлениям Тимочко о неподконтрольности

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

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

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

Меры противодействия невозможности наблюдения

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

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