Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Аргумент Тимочко [ править ]

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

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

По мнению Tymoczko, в доказательстве Appel-Хакен провалило критерий Обозреваемости мимо, он утверждал, подставляя эксперимент для удержания :

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

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

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

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

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

-  Томас Тимочко, «Задача о четырех цветах и ​​ее математическое значение» [1]

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

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

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

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

Контрмеры против невозможности наблюдения [ править ]

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

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

Ссылки [ править ]

  1. ^ a b c Тимочко, Томас (февраль 1979 г.). «Проблема четырех цветов и ее философское значение». Журнал философии . 76 (2): 57–83. DOI : 10.2307 / 2025976 . JSTOR  2025976 .
  2. ^ а б Бонни Голд и Роджер Саймонс. Доказательство и другие дилеммы: математика и философия.
  3. ^ a b c Джандоменико Сика. Очерки основ математики и логики. Том 1.
  4. ^ Пол Теллер. «Компьютерное доказательство». Журнал философии. 1980 г.
  5. ^ Нил Теннант. «Укрощение истины». 1997 г.
  6. ^ Julie Rehmeyer. «Как (действительно) доверять математическому доказательству». ScienceNews. https://www.sciencenews.org/article/how-really-trust-mat Mathematical-proof . Проверено 14 ноября 2008.
  7. ^ Фрик Wiedijk, КЭД Манифест Revisited , 2007