Не поддающиеся проверке доказательства
В философии математики — не поддающееся контролю доказательство это математическое доказательство , которое считается невозможным для человека-математика и поэтому имеет спорную достоверность . Этот термин был придуман Томасом Тимочко в 1979 году для критики Кеннета Аппеля и Вольфганга Хакена теоремы компьютерного доказательства о четырех цветах и с тех пор применяется к другим аргументам, в основном к аргументам с чрезмерным разделением регистров и / или с отправкой частей. с помощью труднопроверяемой компьютерной программы. Обзорность остается важным фактором в вычислительной математике .
Аргумент Тимочко
[ редактировать ]Тимочко утверждал, что три критерия определяют, является ли аргумент математическим доказательством:
- Убедительность , которая относится к способности доказательства убедить рационального доказывающего в своем выводе;
- Обзорность , которая относится к доступности доказательства для проверки членами человеческого математического сообщества; и
- Формализуемость , которая относится к обращению доказательства только к логическим отношениям между понятиями для обоснования своего аргумента. [1]
По мнению Тимочко, доказательство Аппеля-Хакена не соответствует критерию обзорности.путем, утверждал он, экспериментом дедукции : замены
… если мы примем [Теорему о четырёх цветах] как теорему, мы обязуемся изменить смысл «теоремы» или, что более важно, изменить смысл лежащей в ее основе концепции «доказательства».
…[использование компьютеров в математике, как в [Теореме четырёх цветов], вводит в математику эмпирические эксперименты. Независимо от того, решим ли мы считать [теорему о четырёх цветах] доказанной, мы должны признать, что текущее доказательство не является традиционным доказательством, не является априорным выводом утверждения из посылок. Это традиционное доказательство с лакуной или пробелом, который заполняется результатами хорошо продуманного эксперимента.- Томас Тимочко, «Проблема четырех цветов и ее философское значение». [1]
Без возможности обзора доказательство может служить своей первой цели — убедить читателя в своем результате, но при этом не справиться со своей второй целью — просветить читателя относительно того, почему этот результат верен — оно может играть роль наблюдения, а не аргумента. [2] [3]
Это различие важно, поскольку оно означает, что доказательства, не поддающиеся контролю, подвергают математику гораздо более высокому риску ошибок. В частности, в случае, когда невозможность наблюдения обусловлена использованием компьютерной программы (которая может содержать ошибки ), особенно когда эта программа не опубликована, в результате может пострадать убедительность. [3] Как писал Тимочко:
Предположим, какой-нибудь суперкомпьютер был запущен для проверки непротиворечивости арифметики Пеано и выдал доказательство несогласованности , доказательство, которое было настолько длинным и сложным, что ни один математик не мог понять его за пределами самых общих терминов. Можем ли мы иметь достаточную веру в компьютеры, чтобы принять этот результат, или мы скажем, что эмпирических доказательств их надежности недостаточно?
- Томас Тимочко, «Проблема четырех цветов и ее философское значение». [1]
Контраргументы заявлениям Тимочко о неподконтрольности
[ редактировать ]Однако точка зрения Тимочко оспаривается аргументами о том, что доказательства, которые трудно исследовать, не обязательно так же недействительны, как доказательства, которые невозможно исследовать.
Пол Теллер утверждал, что возможность исследования зависит от степени и зависит от читателя, а не от того, что доказательство имеет или не имеет. Поскольку доказательства не отвергаются, когда у студентов возникают проблемы с их пониманием, утверждает Теллер, также не следует отвергать доказательства (хотя они могут подвергаться критике) просто потому, что профессиональным математикам трудно следовать этому аргументу. [4] [3] (Теллер не согласился с оценкой Тимочко о том, что «[Теорема о четырех цветах] не проверялась математиками шаг за шагом, как проверялись все другие доказательства. Действительно, ее нельзя проверить таким способом».)
Аналогичный аргумент заключается в том, что разделение падежей является общепринятым методом доказательства, а доказательство Аппеля-Хакена является лишь крайним примером разделения падежей. [2]
Меры противодействия невозможности наблюдения
[ редактировать ]С другой стороны, точка зрения Тимочко о том, что доказательства должны быть по крайней мере возможными для проверки и что ошибки в доказательствах, которые трудно исследовать, с меньшей вероятностью попадут в поле зрения, обычно не оспаривается; вместо этого были предложены методы улучшения возможности исследования, особенно компьютерных доказательств. Среди ранних предложений было распараллеливание: задача проверки могла быть разделена между многими читателями, каждый из которых мог просмотреть часть доказательства. [5] Но современная практика, прославленная Флайспеком , заключается в том, чтобы представить сомнительные части доказательства в ограниченном формализме, а затем проверить их с помощью средства проверки доказательств , которое само доступно для просмотра. Действительно, доказательство Аппеля–Хакена таким образом проверено. [6]
Тем не менее, автоматизированная проверка еще не получила широкого распространения. [7]
Ссылки
[ редактировать ]- ^ Jump up to: а б с Тимочко, Томас (февраль 1979 г.). «Проблема четырех цветов и ее философское значение». Журнал философии . 76 (2): 57–83. дои : 10.2307/2025976 . JSTOR 2025976 .
- ^ Jump up to: а б Бонни Голд и Роджер Саймонс. Доказательство и другие дилеммы: математика и философия.
- ^ Jump up to: а б с Джандоменико Сика. Очерки оснований математики и логики. Том 1.
- ^ Пол Теллер. «Компьютерное доказательство». Журнал философии. 1980.
- ^ Нил Теннант. «Укрощение истины». 1997.
- ^ Джули Ремейер. «Как (действительно) доверять математическому доказательству». Новости науки. https://www.sciencenews.org/article/how-really-trust-mathematical-proof . Проверено 14 ноября 2008 г.
- ^ Фрик Видейк, Новый взгляд на манифест QED , 2007 г.