Введение

Тип математического доказательства

Доказательство исчерпанием, также известное как доказательство по случаям, доказательство посредством анализа случаев, полная индукция или метод перебора, является методом математического доказательства, в котором утверждение, подлежащее доказательству, разбивается на конечное число случаев или наборов эквивалентных случаев, и для каждого типа случая проверяется, выполняется ли рассматриваемое утверждение. Это метод прямого доказательства. Доказательство исчерпанием обычно состоит из двух этапов:

Доказательство того, что набор случаев является исчерпывающим, то есть каждый экземпляр утверждения, подлежащего доказательству, соответствует условиям (как минимум) одного из случаев. Доказательство каждого из случаев. Широкое распространение цифровых компьютеров значительно упростило использование метода исчерпания (например, первое компьютерное доказательство теоремы о четырёх красках в 1976 году), хотя подобные подходы могут подвергаться критике с точки зрения математической элегантности. Экспертные системы могут использоваться для получения ответов на многие задаваемые им вопросы. В теории метод исчерпания может применяться всякий раз, когда число случаев конечно. Однако, поскольку большинство математических множеств бесконечны, этот метод редко используется для получения общих математических результатов. В изоморфизме Карри — Ховарда доказательство исчерпанием и анализ случаев связаны с сопоставлением с образцом в стиле ML.

Элегантность

Математики предпочитают избегать доказательств перебором большого количества случаев, которые считаются неэлегантными. Примером того, почему такие доказательства могут быть неэлегантными, служит следующее рассуждение, показывающее, что все современные летние Олимпийские игры проводятся в годы, кратные 4:

Доказательство: Первые современные летние Олимпийские игры состоялись в 1896 году, а затем каждые 4 года (не учитывая исключения, такие как отмены из-за Первой и Второй мировых войн, а также перенос Олимпийских игр в Токио в 2020 году на 2021 год из-за пандемии COVID-19). Поскольку 1896 = 474 × 4 делится на 4, следующие Олимпийские игры пройдут в году 474 × 4 + 4 = (474 + 1) × 4, который также кратен четырем, и так далее (это доказательство методом математической индукции). Следовательно, утверждение доказано. Это же утверждение можно доказать перебором, перечислив все годы, в которые проводились летние Олимпийские игры, и убедившись, что каждый из них делится на четыре. Поскольку к 2016 году состоялось 28 летних Олимпийских игр, это доказательство перебором, включающее 28 случаев. Помимо меньшей элегантности, доказательство перебором также потребует добавления нового случая каждый раз, когда будут проводиться новые летние Олимпийские игры. Это следует противопоставить доказательству методом математической индукции, которое доказывает утверждение на неопределённое будущее.

Количество дел

Не существует верхнего предела для количества случаев, допустимых в доказательстве от противного перебором. Иногда достаточно двух или трех случаев, а иногда их могут быть тысячи или даже миллионы. Например, строгое решение шахматной эндшпильной задачи может потребовать рассмотрения очень большого числа возможных позиций в дереве игры этой задачи. Первое доказательство теоремы о четырех красках было доказательством от противного перебором, состоящим из 1834 случаев. Это доказательство вызвало споры, поскольку большинство случаев были проверены компьютерной программой, а не вручную. Самое короткое известное на сегодняшний день доказательство теоремы о четырех красках все еще содержит более 600 случаев. В целом, вероятность ошибки во всем доказательстве возрастает с увеличением числа случаев. Доказательство с большим количеством случаев создает впечатление, что теорема верна лишь случайно, а не благодаря какому-либо лежащему в основе принципу или закономерности. Другие типы доказательств, такие как доказательство по индукции (математической индукции), считаются более изящными. Однако существуют важные теоремы, для которых не было найдено других методов доказательства, такие как:
Доказательство отсутствия конечной проективной плоскости порядка 10. Классификация конечных простых групп. Гипотеза Кеплера. Задача булевых пифагоровых троек.