Введение

Метод доказательства в математике
В математике конструктивное доказательство — это метод доказательства, который демонстрирует существование математического объекта, создавая его или предоставляя метод для его создания. Это противопоставляется неконструктивному доказательству (также известному как доказательство существования или теорема о чистом существовании), которое доказывает существование определённого типа объекта, не приводя примера. Чтобы избежать путаницы с более строгим понятием, которое следует далее, такое конструктивное доказательство иногда называют эффективным доказательством. Конструктивное доказательство может также относиться к более строгой концепции доказательства, которое является допустимым в конструктивной математике. Конструктивизм — это математическая философия, которая отвергает все методы доказательства, предполагающие существование объектов, которые не построены явно. Это, в частности, исключает использование закона исключённого третьего, аксиомы бесконечности и аксиомы выбора, и придает иной смысл некоторым терминам (например, термин "или" имеет более сильное значение в конструктивной математике, чем в классической). Некоторые неконструктивные доказательства показывают, что если определённое утверждение ложно, возникает противоречие; следовательно, утверждение должно быть истинным (доказательство от противного). Однако принцип взрыва (ex falso quodlibet) был принят в некоторых вариантах конструктивной математики, включая интуиционизм. Конструктивные доказательства можно рассматривать как определение сертифицированных математических алгоритмов: эта идея исследуется в интерпретации конструктивной логики Брауэра — Хейтинга — Колмогорова, соответствии Карри — Ховарда между доказательствами и программами, а также в таких логических системах, как интуиционистская теория типов Пера Мартина Лёфа и исчисление конструкций Тьерри Коквана и Жерара Хюэ.

Брауверовские контрпримеры

В конструктивной математике утверждение может быть опровергнуто приведением контрпримера, как и в классической математике. Однако возможно также привести броуэровский контрпример, чтобы показать, что утверждение неконструктивно. Такой контрпример демонстрирует, что утверждение влечет за собой некоторый принцип, который, как известно, является неконструктивным. Если конструктивно можно доказать, что утверждение влечет за собой принцип, который не может быть конструктивно доказан, то само утверждение не может быть конструктивно доказано. Например, можно показать, что определенное утверждение влечет за собой закон исключённого третьего. Примером броуэровского контрпримера этого типа является теорема Диаконеску, которая показывает, что полная аксиома выбора неконструктивна в системах конструктивной теории множеств, поскольку аксиома выбора влечет за собой закон исключённого третьего в таких системах. Область конструктивной обратной математики развивает эту идею дальше, классифицируя различные принципы с точки зрения «степени их неконструктивности», показывая, что они эквивалентны различным фрагментам закона исключённого третьего. Брауэр также приводил «слабые» контрпримеры. Однако такие контрпримеры не опровергают утверждение; они лишь показывают, что в настоящее время не известно конструктивного доказательства этого утверждения. Один слабый контрпример начинается с нерешённой математической проблемы, такой как гипотеза Гольдбаха, которая спрашивает, является ли каждое чётное натуральное число, большее 4, суммой двух простых чисел. Определим последовательность a(n) рациональных чисел следующим образом: для каждого n значение a(n) может быть определено полным перебором, и, следовательно, a является чётко определённой последовательностью, конструктивно. Более того, поскольку a — последовательность Коши с фиксированной скоростью сходимости, a сходится к некоторому действительному числу α, согласно общепринятому подходу к действительным числам в конструктивной математике. Несколько фактов о действительном числе α могут быть конструктивно доказаны. Однако, исходя из иного значения слов в конструктивной математике, если существует конструктивное доказательство того, что «α = 0 или α ≠ 0», то это означало бы, что существует конструктивное доказательство гипотезы Гольдбаха (в первом случае) или конструктивное доказательство ложности гипотезы Гольдбаха (во втором случае). Поскольку такого доказательства не существует, приведённое утверждение также не должно иметь известного конструктивного доказательства. Однако вполне возможно, что гипотеза Гольдбаха может иметь конструктивное доказательство (поскольку в настоящее время мы не знаем, существует ли оно), в этом случае приведённое утверждение также будет иметь конструктивное доказательство, хотя и неизвестное в настоящее время. Основное практическое применение слабых контрпримеров — определение «сложности» проблемы. Например, только что приведённый контрпример показывает, что приведённое утверждение «по крайней мере столь же трудно доказать», как и гипотезу Гольдбаха. Слабые контрпримеры такого рода часто связаны с ограниченным принципом всезнания.