Математическое доказательство
Математическое доказательство | |
---|---|
Предыдущее по порядку | гипотеза |
Изучается в | теория доказательств |
Цель проекта или миссии | теорема |
Медиафайлы на Викискладе |
Математическое доказательство — рассуждение с целью обоснования истинности какого-либо утверждения (
На протяжении всей истории математики представление о способах и допустимых методах доказательства существенно менялось, в основном, в сторону большей формализации и бо́льших ограничений. Ключевой вехой в вопросе формализации доказательства стало создание математической логики в XIX веке и формализация её средствами основных техник доказательства. В XX веке построена теория доказательств — теория, изучающая доказательство как математический объект . С появлением во второй половине XX века компьютеров особое значение получило применение методов математического доказательства для проверки и синтеза программ , и даже было установлено структурное соответствие между компьютерными программами и математическими доказательствами (соответствие Карри — Ховарда ), на основе которого созданы средства автоматического доказательства .
Основные приёмы, используемые при построении доказательств: прямое доказательствоматематическая индукция и её обобщения , доказательство от противного , контрапозиция , построение , перебор , установление биекции , двойной счёт ; в приложениях в качестве математических доказательств привлекаются также методы, не дающие формального доказательства, но обеспечивающие практическую применимость результата — вероятностные, статистические, приближённые. В зависимости от раздела математики, используемого формализма или математической школы не все методы могут приниматься безоговорочно, в частности, конструктивное доказательство предполагает серьёзные ограничения.
,Значение доказательства в математике
В отличие от других наук, в математике недопустимы эмпирические доказательства: все утверждения доказываются исключительно логическими способами. В математике важную роль играют математическая интуиция и аналогии между разными объектами и теоремами; тем не менее, все эти средства используются учёными только при поиске доказательств, сами доказательства не могут основываться на таких средствах. Доказательства, написанные на естественных языках, могут быть не очень подробными в расчёте на то, что подготовленный читатель сам сможет восстановить детали. Строгость доказательства гарантируется тем, что его можно представить в виде записи на формальном языке (это и происходит при компьютерной проверке доказательств).
Этот раздел исправив и дополнив его. |
Статус утверждений
Доказанные утверждения в математике называют теоремами (в математических текстах обычно подразумевается, что доказательство кем-либо найдено; исключения из этого обычая в основном составляют работы по логике, в которых исследуется само понятие доказательства); если ни утверждение, ни его отрицание ещё не доказаны, то такое утверждение называют гипотезой. Иногда в процессе доказательства теоремы выделяются доказательства менее сложных утверждений, называемых леммами.
Некоторые математические утверждения традиционно известны под названиями, не соответствующими их фактическому статусу. Так,
Ошибочным доказательством называется текст, содержащий логические ошибки, то есть такой, по которому нельзя восстановить формальное доказательство. В истории математики были случаи, когда выдающиеся учёные публиковали неверные «доказательства», однако обычно их коллеги или они сами довольно быстро находили ошибки (одна из наиболее часто неправильно доказывавшихся теорем — Великая теорема Ферма. До сих пор встречаются люди, не знающие о том, что она доказана, и предлагающие новые неверные «доказательства»[3][4]). Ошибочным может быть только признание доказательством «доказательства» на естественном или формальном языке; формальное доказательство ошибочным не может быть по определению.
История
Античность
В странах
Первые доказательства использовали простейшие логические построения. В частности
Известно, что доказательство несоизмеримости стороны и диагонали квадрата, которое является основой понятия
Важным моментом на пути к будущей формализации математических доказательств стало создание Аристотелем логики, в которой он попытался систематизировать и кодифицировать все правила рассуждений, используемые для доказательств, описал основные возникающие сложности и двусмысленности. Аристотель предполагал доказательства важной составляющей науки, считая, что доказательство «выявляет сущность вещей»[11]. Но непосредственного влияния на древнегреческую математику аристотелева логика не оказала, и вопросам формальной логики в доказательствах внимания не уделяли[12].
Средневековье и Новое время
С развитием математики в
К Новому времени благодаря успехам применения математики в естественных науках математические утверждения и доказательства считались надёжными, как только дано точное и формальное определение исходных понятий, и математика в целом считалась образцом строгости и доказательности для всех прочих дисциплин. В частности, Лейбниц считает аксиомы и правила вывода незыблемыми и стремится построить формальную систему логики, чтобы «доказать всё доказуемое»[15]. Однако, даже в XVIII веке понятие доказательства было всё ещё слишком неформализованным и умозрительным, свидетельством тому может быть факт того, что Эйлер считал обосновываемыми одновременно следующие утверждения:
- и ,
а также:
- ,
понимая, естественно, бессмысленность этих утверждений, но считая их «доказуемость» парадоксами[16].
В XIX веке всё чаще возникают идеи необходимости постулирования некоторых интуитивно очевидных правил, которые формальным способом доказать невозможно. Ещё одним толчком к пониманию относительности доказательств в зависимости от постулируемых принципов после многих веков неуспешных попыток доказать
Формализация логики и программа Гильберта
Этот раздел статьи ещё не написан. |
Интуиционизм
Этот раздел статьи ещё не написан. |
Теоремы о неполноте
Этот раздел статьи ещё не написан. |
Конструктивизм
Этот раздел статьи ещё не написан. |
Формальное доказательство
Когда говорят о формальном доказательстве, прежде всего описывают формальную модель —
Теория называется полной, если для любого утверждения доказуемо оно или его отрицание, и
Теория доказательств
Формальными доказательствами занимается специальная ветвь математики — теория доказательств. Сами формальные доказательства математики почти никогда не используют, поскольку для человеческого восприятия они очень сложны и часто занимают очень много места.
Этот раздел исправив и дополнив его. |
В информатике
В информатике математические доказательства используются для верификации и анализа правильности алгоритмов и программ (см. логика в информатике) в рамках технологий доказательного программирования.
Этот раздел исправив и дополнив его. |
Методы формального доказательства
Прямое доказательство
Прямое доказательство[англ.] предусматривает применение только непосредственного дедуктивного вывода из считающихся верными утверждений (аксиом, ранее доказанных лемм и теорем), без использования суждений с отрицанием каких-либо утверждений[18]. Например, для прямого доказательства считаются приемлемым следующие фигуры (в нотации натурального вывода:
- , , (modus ponens).
Также методом прямого доказательства считается и подстановка: если утверждение верно для любых значений входящих в него свободных переменных, то подстановка каких-либо конкретных значений вместо какого-нибудь подмножества из них во всех вхождениях (частный случай формулы) даёт верное утверждение, в нотации натурального вывода (неформальная запись, упрощено до одной переменной):
В некоторых случаях непрямые доказательства, использующие рассуждения с отрицанием, особенно, относительно конечных объектов, могут быть простым образом сведены к прямым без ущерба общности, но относительно утверждений о бесконечных совокупностях это далеко не всегда так, и с ростом ценности конструктивных доказательств в математике XX века считается важным найти прямое доказательство для утверждений, считавшихся доказанными, но непрямыми методами.
В теории доказательств разработано формальное определение прямого доказательства[19].
Индукция
Индуктивный метод, позволяющий перейти от частных утверждений ко всеобщим, наиболее интересен в применении к бесконечным совокупностям объектов, но его формулировки и применимость существенно отличаются в зависимости от сферы применения.
Простейший индуктивный метод[20] — математическая индукция, умозаключение относительно натурального ряда, идея которого в утверждении некоторого закона для всех натуральных чисел, исходя из фактов его выполнения для единицы и следования истинности для каждого последующего числа, в нотации натурального вывода:
- .
Метод математической индукции естественным образом может быть применён для любых счётных совокупностей объектов, считается надёжным и легитимным как в классических, так и в интуиционистских и конструктивных системах доказательств. Метод аксиоматизируется в системе аксиом арифметики Пеано.
Более сложный вопрос состоит в возможности распространения индуктивного метода на
Существует конструктивный метод структурной индукции, позволяющий применять индукцию по отношению к вполне упорядоченным совокупностям объектов, но при условии их рекурсивного определения.
От противного
Доказательство от противного использует логический приём доведения до абсурда и строится по следующей схеме: чтобы доказать утверждение предполагается, что оно неверно, а затем по дедуктивной цепочке приходят к заведомо ложному утверждению, например, , из чего согласно закону двойного отрицания делается вывод об истинности , в нотации натурального вывода:
- .
В интуиционистских и конструктивных системах доказательство от противного не используется, так как не принимается закон двойного отрицания.
Контрапозиция
Контрапозиционное доказательство[англ.] использует закон контрапозиции и состоит в следующем: для доказательства факта, что из утверждения следует требуется показать, что из отрицания следует отрицание , в символике натурального вывода:
- .
Контрапозиционное доказательство сводится к методу от противного проверяется его отрицание , а так как имеет место посылка , выявляется противоречие.
: для доказательстваВ качестве примера контрапозиционного доказательства приводится[22] установление факта, что если
В системах, не принимающих закон двойного отрицания, контрапозиционное доказательство не применяется.
Построение
Для утверждений типа теорем существования, в которых формулируется в качестве результата наличие какого-либо объекта, например, существование числа, удовлетворяющего каким-либо условиям, наиболее характерный тип доказательства — непосредственное нахождение искомого объекта с использованием методов соответствующей формальной системы или с использованием контекста соответствующего раздела. Многие классические теоремы существования доказаны от противного: приведением к абсурду предположения о несуществовании объекта с заданными свойствами, но такие доказательства считаются неконструктивными, и, соответственно, в интуиционистской и конструктивной математике для такого рода утверждений используются только доказательства построением.
Исчерпывание вариантов
В некоторых случаях для доказательства утверждения перебираются все возможные варианты совокупности, относительно которой сформулировано утверждение (полный перебор) или все возможные варианты разбиваются на конечное число классов, представляющих частные случаи, и относительно каждого из которых доказательство проводится отдельно[23]. Как правило, доказательство методом исчерпывания вариантов[англ.], состоит из двух этапов:
- установления всех возможных частных случаев, и доказательства, что других частных случаев нет,
- доказательство каждого частного случая.
Количество вариантов может быть достаточно велико, например, для доказательства
Биекция
Доказательство методом
Простейшие примеры биективных доказательств — доказательства комбинаторных утверждений о числе сочетаний или количестве элементов множеств, более сложные примеры — установление изоморфизмов, гомеоморфизмов, диффеоморфизмов, биморфизмов, за счёт чего на изучаемый объект или совокупность переносятся свойства уже известного объекта , инвариантные по отношению к тому или специальному виду биекции.
Двойной счёт
Этот раздел статьи ещё не написан. |
Геометрическое доказательство
Этот раздел статьи ещё не написан. |
Прикладные методы
Приближённые методы
Этот раздел статьи ещё не написан. |
Вероятностные методы
Этот раздел статьи ещё не написан. |
Статистические методы
Этот раздел статьи ещё не написан. |
Терминология
Этот раздел статьи ещё не написан. |
Символы
Этот раздел исправив и дополнив его. |
Традиционно окончание доказательства обозначалось сокращением «Q.E.D.», от латинского выражения лат. Quod Erat Demonstrandum («Что и требовалось доказать»). В современных трудах для обозначения окончания доказательства чаще используется знак □ или ■, ‣, //, а также русская аббревиатура ч. т. д.
Примечания
- ↑ Bill Casselman. One of the Oldest Extant Diagrams from Euclid . University of British Columbia. Дата обращения: 26 сентября 2008. Архивировано 4 июня 2012 года.
- Сов. энциклопедия », 1988. — С. 211.
- ↑ Гастев Ю., Смолянский М. Несколько слов о Великой теореме Ферма // Квант. — 1972. — Т. 8. — С. 23—25. Архивировано 28 ноября 2007 года.
- ↑ Цымбалов А. С. Теорема Ферма . Доклад на конференцию. Современная гуманитарная академия. Дата обращения: 14 мая 2011. Архивировано из оригинала 30 марта 2009 года.}
- ↑ Кранц, 2011, The Babylonians had certain diagrams that indicate why the Pythagorean theorem is true, and tablets have been found to validate this fact, p. 44.
- ↑ История математики, том I, 1970, с. 65—66.
- ↑ Бурбаки, 1963, с. 11.
- ↑ История математики, том I, 1970, с. 73.
- ↑ Кранц, 2011, <…> Eudoxus who began the grand tradition of organizing mathematics into theorems <…> What Eudoxus gained in the rigor and precision of his mathematical formulations, he lost because he did not prove anything, p. 44—45.
- ↑ История математики, том I, 1970, с. 95.
- ↑ История математики, том I, 1970, с. 59—61.
- ↑ Бурбаки, 1963, Труды Аристотеля и его преемников, по-видимому, не оказали заметного влияния на математику. Греческие математики в своих исследованиях шли по пути, предложенному пифагорейцами и их последователями в IV в. (Теодором, Теэтетом, Евдоксом), и мало интересовались формальной логикой при изложении своих результатов, с. 12—14.
- ↑ Rabinovich, N. L. Rabbi Levi ben Gershom and the origins of mathematical induction // Archive for History of Exact Sciences. — 1970. — Вып. 6. — С. 237—248.
- ↑ Бурбаки, 1963, с. 27.
- ↑ Бурбаки, 1963, с. 22.
- ↑ Кранц, 2011, 3.1. Euler and the Profundity of Intuition, p. 74—75.
- ↑ Бурбаки, 1963, с. 25—26.
- ↑ Хаммак, 2009, Chapter 4. Direct proof, с. 95—109.
- ↑ Справочная книга по математической логике, том IV, 1983, Глава 3. Стетмен Р. Теорема Эрбрана и генценовское понятие прямого доказательства, с. 84—99.
- ↑ Хаммак, 2009, Chapter 10. Mathematical Induction, с. 152—154.
- ↑ Математическое доказательство — статья из Математической энциклопедии. Драгалин А. Г.
- ↑ Хаммак, 2009, Chapter 7. Proving Non-Conditional Statements, с. 129—138.
- ↑ Львовский С. М., Тоом А. Л. Разберем все варианты // Квант. — 1988. — № 1. — С. 42—47. Архивировано 19 июля 2020 года.
- ↑ Самохин А. В. Проблема четырех красок: неоконченная история доказательства // Соросовский образовательный журнал. — 2000. — № 7. — С. 91—96. (недоступная ссылка)
- ↑ Stanley R. Bijective proof problems (англ.) (18 августа 2009). Дата обращения: 12 мая 2013. Архивировано 13 мая 2013 года.
Литература
- С древнейших времён до начала Нового времени // История математики / Под редакцией Юшкевича А. П., в трёх томах. — М.: Наука, 1970. — Т. I.
- Справочная книга по математической логике. IV. Теория доказательств и конструктивная математика = Handbook of Mathematical Logic / Барвайс Дж.. — М.: Наука, 1983. — 392 с.
- Бурбаки Н. Основания математики. Логика. Теория множеств // Очерки по истории математики / И. Г. Башмакова(перевод с французского). — М.: Издательство иностранной литературы, 1963. — С. 37—53. — 292 с. — (Элементы математики).
- Доказательство / Ю. А. Гастев // Большая советская энциклопедия : [в 30 т.] / гл. ред. А. М. Прохоров. — 3-е изд. — М. : Советская энциклопедия, 1969—1978.
- Даан-Дальмедико А., Пейффер Ж. Пути и лабиринты. Очерки по истории математики = Routes et dédales / Перевод с французского А. А. Брядинской под редакцией И. Г. Башмаковой. — М.: Мир, 1986. — С. 394—402. — 432 с. — (Современная математика. Популярная серия). — 50 000 экз.
- 12 января 2014 года.
- Franklin J., Daoud A. Proof in the Mathematics. — Sydney: Quakers Hill Press, 2001. — 98 p. — ISBN 1876192003.
- Hammak R. Book of Proof (англ.) (2009). Дата обращения: 11 мая 2013. Архивировано 13 мая 2013 года.
- Krantz S. G.[англ.]. The Proof is in the Pudding. A Look at the Changing Nature of Mathematical Proof. — N. Y.: Springer, 2011. — 281 p. — ISBN 978-0387489087.
Ссылки
- Ю. Л. Ершов «Доказательность в математике», программа А. Гордона от 16 июня 2003 года