Русская Википедия:Математическое доказательство

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Файл:Oxyrhynchus papyrus with Euclid's Elements.jpg

Один из древнейших найденных фрагментов «Начал» Евклида, учебника геометрии, бывшего примером техники доказательств в течение тысячелетий

Математическое доказательство — рассуждение с целью обоснования истинности какого-либо утверждения (теоремы), цепочка логических умозаключений, показывающая, что при условии истинности некоторого набора аксиом и правил вывода утверждение верно. В зависимости от контекста, может иметься в виду доказательство в рамках некоторой формальной системы (построенная по специальным правилам последовательность утверждений, записанная на формальном языке) или текст на естественном языке, по которому при необходимости можно восстановить формальное доказательство. Необходимость формального доказательства утверждений — одна из основных характерных черт математики как дедуктивной отрасли знаний, соответственно, понятие доказательства играет центральную роль в предмете математикиШаблон:Переход, а наличие доказательств и их корректность определяют статус любых математических результатовШаблон:Переход.

На протяжении всей истории математикиШаблон:Переход представление о способах и допустимых методах доказательства существенно менялось, в основном, в сторону большей формализации и бо́льших ограничений. Ключевой вехой в вопросе формализации доказательства стало создание математической логикиШаблон:Переход в XIX веке и формализация её средствами основных техник доказательства. В XX веке построена теория доказательств — теория, изучающая доказательство как математический объектШаблон:Переход. С появлением во второй половине XX века компьютеров особое значение получило применение методов математического доказательства для проверки и синтеза программШаблон:Переход, и даже было установлено структурное соответствие между компьютерными программами и математическими доказательствами (соответствие Карри — ХовардаШаблон:Переход), на основе которого созданы средства автоматического доказательстваШаблон:Переход.

Основные приёмы, используемые при построении доказательств: прямое доказательствоШаблон:Переход, математическая индукция и её обобщенияШаблон:Переход, доказательство от противногоШаблон:Переход, контрапозицияШаблон:Переход, построениеШаблон:Переход, переборШаблон:Переход, установление биекцииШаблон:Переход, двойной счётШаблон:Переход; в приложениях в качестве математических доказательств привлекаются также методы, не дающие формального доказательства, но обеспечивающие практическую применимость результатаШаблон:Переход — вероятностные, статистические, приближённые. В зависимости от раздела математики, используемого формализма или математической школы не все методы могут приниматься безоговорочно, в частности, конструктивное доказательствоШаблон:Переход предполагает серьёзные ограничения.

Значение доказательства в математике

В отличие от других наук, в математике недопустимы эмпирические доказательства: все утверждения доказываются исключительно логическими способами. В математике важную роль играют математическая интуиция и аналогии между разными объектами и теоремами; тем не менее, все эти средства используются учёными только при поиске доказательств, сами доказательства не могут основываться на таких средствах. Доказательства, написанные на естественных языках, могут быть не очень подробными в расчёте на то, что подготовленный читатель сам сможет восстановить детали. Строгость доказательства гарантируется тем, что его можно представить в виде записи на формальном языке (это и происходит при компьютерной проверке доказательств). Шаблон:Раздел не завершён

Статус утверждений

Доказанные утверждения в математике называют теоремами (в математических текстах обычно подразумевается, что доказательство кем-либо найдено; исключения из этого обычая в основном составляют работы по логике, в которых исследуется само понятие доказательства); если ни утверждение, ни его отрицание ещё не доказаны, то такое утверждение называют гипотезой. Иногда в процессе доказательства теоремы выделяются доказательства менее сложных утверждений, называемых леммами.

Некоторые математические утверждения традиционно известны под названиями, не соответствующими их фактическому статусу. Так, Великая теорема Ферма никогда не называлась «гипотезой Ферма», даже до её доказательства Эндрю Уайлсом. С другой стороны, гипотеза Пуанкаре продолжает носить такое название и после её доказательства Григорием Перельманом.

Ошибочным доказательством называется текст, содержащий логические ошибки, то есть такой, по которому нельзя восстановить формальное доказательство. В истории математики были случаи, когда выдающиеся учёные публиковали неверные «доказательства», однако обычно их коллеги или они сами довольно быстро находили ошибки (одна из наиболее часто неправильно доказывавшихся теорем — Великая теорема Ферма. До сих пор встречаются люди, не знающие о том, что она доказана, и предлагающие новые неверные «доказательства»). Ошибочным может быть только признание доказательством «доказательства» на естественном или формальном языке; формальное доказательство ошибочным не может быть по определению.

История

Античность

В странах Древнего Востока (Вавилоне, Древнем Египте, Древнем Китае) решение математических задач приводилось, как правило, без обоснования и было догматичным, хотя графическое обоснование теоремы Пифагора можно встретить на вавилонских клинописных табличкахШаблон:Sfn. Понятия доказательства не существовало и в Древней Греции в VIII—VII веках до н. э. Однако уже в VI веке до н. э. в Греции логическое доказательство становится основным методом установления истины. В это время были построены первые математические теории и математические модели мира, которые имели вполне современный вид, то есть строились из конечного числа посылок с помощью логических умозаключений.

Первые доказательства использовали простейшие логические построения. В частности Фалес Милетский, доказавший что диаметр делит круг пополам, углы при основании равнобедренного треугольника равны, две пересекающиеся прямые образуют равные углы, видимо, использовал в своих доказательствах методы перегибания и наложения фигур. По словам греческого философа Прокла (V век н. э.) «Иногда он рассматривал вопрос несколько общо, иногда опираясь на наглядность». Уже при Пифагоре доказательство переходит от конкретных представлений к чисто логическим заключениямШаблон:Sfn. В доказательствах Парменида используется закон исключённого третьего, а его ученик Зенон в апориях пользуется приведением к абсурдуШаблон:Sfn.

Известно, что доказательство несоизмеримости стороны и диагонали квадрата, которое является основой понятия иррациональности, скорее всего принадлежит пифагорейцам, хотя впервые приведено лишь в Началах Евклида (X), происходит от противного и основано на теории делимости чисел на дваШаблон:Sfn. Возможно, что расхождение во взглядах на роль математического доказательства явилось одной из причин конфликта между Евдоксом (считающимся основателем традиции организации математики в виде теорем, но принципиально не прибегавшего к доказательствамШаблон:Sfn) и ПлатономШаблон:Sfn.

Важным моментом на пути к будущей формализации математических доказательств стало создание Аристотелем логики, в которой он попытался систематизировать и кодифицировать все правила рассуждений, используемые для доказательств, описал основные возникающие сложности и двусмысленности. Аристотель предполагал доказательства важной составляющей науки, считая, что доказательство «выявляет сущность вещей»Шаблон:Sfn. Но непосредственного влияния на древнегреческую математику аристотелева логика не оказала, и вопросам формальной логики в доказательствах внимания не уделялиШаблон:Sfn.

Средневековье и Новое время

С развитием математики в Средневековье и воспринятой из схоластики опорой на логику постепенно выстраиваются представления о формальном доказательстве и развиваются его методы. К Герсониду относят обоснование и введение в практику метода математической индукции. С XVI века отмечаются отдельные попытки критического осмысления доказательств древнегреческих математиков, например Пелетье, комментируя «Начала» Евклида, критикует доказательство равенства треугольников перемещениемШаблон:Sfn.

К Новому времени благодаря успехам применения математики в естественных науках математические утверждения и доказательства считались надёжными, как только дано точное и формальное определение исходных понятий, и математика в целом считалась образцом строгости и доказательности для всех прочих дисциплин. В частности, Лейбниц считает аксиомы и правила вывода незыблемыми и стремится построить формальную систему логики, чтобы «доказать всё доказуемое»Шаблон:Sfn. Однако, даже в XVIII веке понятие доказательства было всё ещё слишком неформализованным и умозрительным, свидетельством тому может быть факт того, что Эйлер считал обосновываемыми одновременно следующие утверждения:

<math>\sum_{n=0}^\infty {1 - (n \operatorname{mod} 2) \cdot 2} = 0</math> и <math>\sum_{n=1}^\infty {1 - (n \operatorname{mod} 2) \cdot 2} = 1</math>,

а также:

<math>\sum_{n=0}^\infty {2^n} = -1</math>,

понимая, естественно, бессмысленность этих утверждений, но считая их «доказуемость» парадоксамиШаблон:Sfn.

В XIX веке всё чаще возникают идеи необходимости постулирования некоторых интуитивно очевидных правил, которые формальным способом доказать невозможно. Ещё одним толчком к пониманию относительности доказательств в зависимости от постулируемых принципов после многих веков неуспешных попыток доказать аксиому параллельности Евклида стало создание Лобачевским, Бойяи, Гауссом и Риманом неевклидовых геометрийШаблон:Sfn.

Формальное доказательство

Когда говорят о формальном доказательстве, прежде всего описывают формальную модель — множество аксиом, записанных с помощью формального языка, и правил вывода. Формальным выводом называется конечное упорядоченное множество строк, написанных на формальном языке, таких, что каждая из них либо является аксиомой, либо получена из предыдущих строк применением одного из правил вывода. Формальным доказательством утверждения называется формальный вывод, последней строкой которого является данное утверждение. Утверждение, имеющее формальное доказательство, называется теоремой, а множество всех теорем в данной формальной модели (рассматриваемое вместе с алфавитом формального языка, множествами аксиом и правил вывода) называется формальной теорией.

Теория называется полной, если для любого утверждения доказуемо оно или его отрицание, и непротиворечивой, если в ней не существует утверждений, которые можно доказать вместе с их отрицаниями (или, эквивалентно, если в ней существует хотя бы одно недоказуемое утверждение). Большинство «достаточно богатых» математических теорий, как показывает первая теорема Гёделя о неполноте, являются неполными либо противоречивыми. Самым распространённым набором аксиом в наше время является аксиоматика Цермело — Френкеля с аксиомой выбора (хотя некоторые математики выступают против использования последней). Теория на основе этой системы аксиом не полна (например, континуум-гипотеза не может быть ни доказана, ни опровергнута в ней — в предположении, что эта теория непротиворечива). Несмотря на повсеместное использование этой теории в математике, её непротиворечивость не может быть доказана методами её самой. Тем не менее, подавляющее большинство математиков верит в её непротиворечивость, считая, что в противном случае противоречия уже давно были бы обнаружены.

Теория доказательств

Шаблон:Main Формальными доказательствами занимается специальная ветвь математики — теория доказательств. Сами формальные доказательства математики почти никогда не используют, поскольку для человеческого восприятия они очень сложны и часто занимают очень много места. Шаблон:Раздел не завершён

В информатике

В информатике математические доказательства используются для верификации и анализа правильности алгоритмов и программ (см. логика в информатике) в рамках технологий доказательного программирования. Шаблон:Раздел не завершён

Методы формального доказательства

Прямое доказательство

Шаблон:Нп5 предусматривает применение только непосредственного дедуктивного вывода из считающихся верными утверждений (аксиом, ранее доказанных лемм и теорем), без использования суждений с отрицанием каких-либо утвержденийШаблон:Sfn. Например, для прямого доказательства считаются приемлемым следующие фигуры (в нотации натурального вывода:

<math>\frac{A, B}{A}</math>, <math>\frac{A \Rightarrow B, B \Rightarrow C}{A \Rightarrow C}</math>, <math>\frac{A, A \Rightarrow B}{B}</math> (modus ponens).

Также методом прямого доказательства считается и подстановка: если утверждение <math>A</math> верно для любых значений входящих в него свободных переменных, то подстановка каких-либо конкретных значений вместо какого-нибудь подмножества из них во всех вхождениях (частный случай формулы) даёт верное утверждение, в нотации натурального вывода (неформальная запись, упрощено до одной переменной):

<math>\frac{\forall x \, A(x)}{A[x:=a]}</math>

В некоторых случаях непрямые доказательства, использующие рассуждения с отрицанием, особенно, относительно конечных объектов, могут быть простым образом сведены к прямым без ущерба общности, но относительно утверждений о бесконечных совокупностях это далеко не всегда так, и с ростом ценности конструктивных доказательств в математике XX века считается важным найти прямое доказательство для утверждений, считавшихся доказанными, но непрямыми методами.

В теории доказательств разработано формальное определение прямого доказательстваШаблон:Sfn.

Индукция

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

Простейший индуктивный методШаблон:Sfn — математическая индукция, умозаключение относительно натурального ряда, идея которого в утверждении некоторого закона для всех натуральных чисел, исходя из фактов его выполнения для единицы и следования истинности для каждого последующего числа, в нотации натурального вывода:

<math>\frac{P(1), \forall n\in \mathbb N (P(n) \Rightarrow P(n+1))}{\forall n \in \mathbb N (P(n))}</math>.

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

Более сложный вопрос состоит в возможности распространения индуктивного метода на несчётные совокупности. В рамках наивной теории множеств создан метод трансфинитной индукции, позволяющий распространить индуктивное правило вывода для любых вполне упорядоченных множеств по схеме, сходной с математической индукцией. Найдена возможность применения индуктивноподобного рассуждения для несчётных совокупностей и в интуиционистской логике, известная как Шаблон:Нп5.

Существует конструктивный метод структурной индукции, позволяющий применять индукцию по отношению к вполне упорядоченным совокупностям объектов, но при условии их рекурсивного определения.

От противного

Шаблон:Main Доказательство от противного использует логический приём доведения до абсурда и строится по следующей схеме: чтобы доказать утверждение <math>A</math> предполагается, что оно неверно, а затем по дедуктивной цепочке приходят к заведомо ложному утверждению, например, <math>B \land \neg B</math>, из чего согласно закону двойного отрицания делается вывод об истинности <math>A</math>, в нотации натурального вывода:

<math>\frac{\neg A \Rightarrow (B \land \neg B)}{A}</math>.

В интуиционистских и конструктивных системах доказательство от противного не используется, так как не принимается закон двойного отрицания.

Контрапозиция

Шаблон:Нп5 использует закон контрапозиции и состоит в следующем: для доказательства факта, что из утверждения <math>A</math> следует <math>B</math> требуется показать, что из отрицания <math>B</math> следует отрицание <math>A</math>, в символике натурального вывода:

<math>\frac{\neg B \Rightarrow \neg A}{A \Rightarrow B}</math>.

Контрапозиционное доказательство сводится к методу от противногоШаблон:Переход: для доказательства <math>A \Rightarrow B</math> проверяется его отрицание <math>\neg (A \Rightarrow B) \equiv \ A \land \neg B</math>, а так как имеет место посылка <math>\neg B \Rightarrow \neg A \equiv \neg (A \land \neg B)</math>, выявляется противоречие.

В качестве примера контрапозиционного доказательства приводитсяШаблон:Sfn установление факта, что если <math>n^2</math> нечётно, то <math>n</math> также нечётно (<math>n \in \mathbb N</math>), для этого доказывается контрапозиция, что если <math>n</math> — чётно, то <math>n^2</math> также чётно.

В системах, не принимающих закон двойного отрицания, контрапозиционное доказательство не применяется.

Построение

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

Исчерпывание вариантов

В некоторых случаях для доказательства утверждения перебираются все возможные варианты совокупности, относительно которой сформулировано утверждение (полный перебор) или все возможные варианты разбиваются на конечное число классов, представляющих частные случаи, и относительно каждого из которых доказательство проводится отдельно. Как правило, доказательство Шаблон:Нп5, состоит из двух этапов:

1. установления всех возможных частных случаев, и доказательства, что других частных случаев нет,
2. доказательство каждого частного случая.

Количество вариантов может быть достаточно велико, например, для доказательства гипотезы четырёх красок потребовалось перебрать почти 2 тыс. различных вариантов с помощью компьютера. Появление такого рода доказательств в конце XX века в связи с развитием вычислительной техники, подняли вопрос об их статусе в математической науке из-за возможных проблем с проверяемостью.

Биекция

Доказательство методом Шаблон:Нп5 применяется для установления утверждений о размере или структуре совокупности или сопоставимости совокупности с какой-либо другой совокупностью и состоит в построении взаимно-однозначного соответствия между изучаемым множеством <math>A</math> и множеством с известными свойствами <math>B</math>. Иными словами, доказательство утверждений о некоей совокупности сводится к доказательству построением биекции, возможно, с дополнительными ограничениями, с совокупностью, для которой это утверждение известно.

Простейшие примеры биективных доказательств — доказательства комбинаторных утверждений о числе сочетаний или количестве элементов множеств, более сложные примеры — установление изоморфизмов, гомеоморфизмов, диффеоморфизмов, биморфизмов, за счёт чего на изучаемый объект или совокупность <math>A</math> переносятся свойства уже известного объекта <math>B</math>, инвариантные по отношению к тому или специальному виду биекции.

Геометрическое доказательство

Файл:Pythagorean proof.png

Геометрическое доказательство теоремы Пифагора

Символы

Шаблон:Раздел не завершён Традиционно окончание доказательства обозначалось сокращением «Q.E.D.», от латинского выражения Шаблон:Lang-la («Что и требовалось доказать»). В современных трудах для обозначения окончания доказательства чаще используется знак □ или ■, ‣, //, а также русская аббревиатура ч. т. д.

Литература

• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:БСЭ3
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Cite web
• Шаблон:Книга

Ссылки

• Ю. Л. Ершов «Доказательность в математике», программа А. Гордона от 16 июня 2003 года