Конструктивне доведення

В математиці конструктивне доведення — це метод доведення, що підтверджує існування математичного об'єкта шляхом надання або створення способу відтворення даного об'єкта. Він протиставляється неконструктивному доведенню (також відомому як теорема доведення існування, або чиста теорема існування), яке доводить існування певного об'єкта без надання прикладів.

Деякі неконструктивні доведення показують, що якщо якась передумова помилкова, то випливає суперечність; отже, передумова повинна бути істинною (доведення від протилежного). Проте в деяких розділах конструктивної математики, в тому числі в інтуїціонізмі, був прийнятий принцип вибуху (лат. ex Falso QuodLibet, «за брехнею нічого не слідує»).

Конструктивізм — це математична філософія, яка відкидає всі, за виключенням конструктивних, доведення в математиці. Це призводить до обмеження дозволених методів доведень (спочатку закон виключеного третього не було заведено застосовувати) і іншого змісту термінології (наприклад, термін «або» має більш обмежений зміст в конструктивній математиці, ніж в класичній).

Конструктивні доведення можна розглядати як визначення перевірених математичних алгоритмів: ця ідея досліджується в інтерпретації конструктивної логіки Брауера-Гейтінга-Колмогорова^[en], у відповідності Каррі-Говарда, а також в таких логічних системах, як інтуїціоністська теорія типів Пера Мартіна-Льофа та числення конструкцій Тьєррі Кокана й Жерара Гуета.

Приклади ред.

Неконструктивні доведення ред.

Докладніше: Неконструктивне доведення

Розглянемо спочатку теорему, згідно з якою множина простих чисел є нескінченною. Доведення Евкліда конструктивне. Але загальний вид спрощеного Евклідового доведення стверджує, що, всупереч твердженням в теоремі, кількість їх обмежена, і в цьому випадку найбільше число позначається n. Тоді розглянемо число (n! + 1) (1 + добуток перших n чисел). Або це число є простим, або сума всіх його простих множників більша, ніж n. Без встановлення конкретного простого числа це доводить, що існує принаймні одне, що більше, ніж n, всупереч початковому постулату.

Розглянемо тепер таку теорему: «Існують два ірраціональні числа a і b, такі, що $a^{b}$ раціональне». Цю теорему можна довести за допомогою як конструктивного доведення, так і неконструктивного.

Таке доведення, сформульований Довом Джарденом в 1953 році, широко використовується як приклад неконструктивного доведення принаймні з 1970 року:^[1]^[2]

CURIOSA 339. Просте доведення, що результат піднесення ірраціонального числа до степеня з ірраціональним показником може бути раціональним числом. ${\sqrt {2}}^{\sqrt {2}}$ є або раціональним, або ірраціональним. Якщо воно раціональне, наше твердження доведено. Якщо воно ірраціональне, $({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2$ доводить наше твердження. Дов Джарден, Єрусалим

Детальніше:

Нагадаємо, що ${\sqrt {2}}$ ірраціональне число, а 2 раціональне. Розглянемо число $q={\sqrt {2}}^{\sqrt {2}}$ . Воно або раціональне, або ірраціональне.
Якщо $q$ раціональне, то теорема вірна, бо $a$ і $b$ обидва дорівнюють ${\sqrt {2}}$ .
Якщо $q$ ірраціональне, то теорема вірна, бо, $a$ дорівнює ${\sqrt {2}}^{\sqrt {2}}$ , а $b$ дорівнює ${\sqrt {2}}$ , оскільки

\left({\sqrt {2}}^{\sqrt {2}}\right)^{\sqrt {2}}={\sqrt {2}}^{({\sqrt {2}}\cdot {\sqrt {2}})}={\sqrt {2}}^{2}=2.

Це доведення є неконструктивним, оскільки воно спирається на твердження «Або q раціональне, або ірраціональне» — приклад до закону виключеного третього, який не діє в конструктивному доведенні. Неконструктивне доведення не наводить приклад a і b; воно просто надає ряд можливостей (у цьому випадку, дві взаємовиключні можливості) і показує, що одна з них — незрозуміло яка — повинна задовольнити потрібний приклад.

(Виявляється, що ${\sqrt {2}}^{\sqrt {2}}$ є ірраціональним через теорему Гельфонда-Шнайдера, але цей факт не має ніякого відношення до правильності неконструктивного доведення.)^{[citation needed]}

Конструктивне доведення ред.

Конструктивне доведення сформульованої вище теореми про ірраціональні степені ірраціональних надає конкретний приклад:

a={\sqrt {2}}\,,\quad b=\log _{2}9\,,\quad a^{b}=3\,.

Квадратний корінь з 2 є ірраціональним, а число 3 — раціональним. $\log _{2}9$ також ірраціональний: якби він дорівнював $m \over n$ , то, за властивістю логарифмів, 9ⁿ дорівнювало б 2^m, але перше є непарним, а останнє парним.

Більш суттєвим прикладом може служити теорема теорема про мінор графу. З теореми випливає, що графік можна намалювати на торі тоді й тільки тоді, коли жоден з його мінорів не належить до деякої скінченної множини «заборонених мінорів». Проте доведення існування цієї скінченної множини не є конструктивним, і заборонені мінори фактично не вказані. Вони дотепер невідомі.

Брауерівські контрприклади ред.

Як в конструктивній, так і в класичній математиці вислів може бути спростований контрприкладом. Проте можна також навести Брауерівський контрприклад, щоб показати, що твердження не є конструктивним. Такого роду контрприклад показує, що твердження допускає наявність неконструктивного принципу. Якщо можна конструктивно довести, що твердження допускає, що якийсь конструктивний принцип можна довести, то саме твердження не може бути конструктивно доведено. Наприклад, можемо взяти конкретний вислів, що допускає закон виключеного третього. Прикладом Брауеріського контрприкладу цього типу є теорема Діаконеску, яка показує, що повна аксіома вибору неконструктивна в системах конструктивної теорії множин, бо аксіома вибору передбачає закон виключеного третього в цих системах. Поле конструктивної реверсивної математики розгортає цю ідею, класифікуючи різні принципи, зважаючи на «ступінь їхньої неконструктивності», та показуючи, що вони еквівалентні різним фрагментам закону виключеного третього.

Брауер також надавав «слабкі» контрприклади. Однак, ці контрприклади не заперечують вислів; вони лише показують, що на цей момент не відомо жодного конструктивного доведення. Один із слабких контрприкладів розпочинається з розгляду невирішеної математичної проблеми, а точніше гіпотези Гольдбаха. Визначимо функцію f натурального числа x наступним чином:

f(x)={\begin{cases}0&{\mbox{if Goldbach's conjecture is false}}\\1&{\mbox{if Goldbach's conjecture is true}}\end{cases}}

Попри те, що визначення лише представлене окремими випадками, воно все одно є допустимим в конструктивній математиці. Кілька фактів про функцію f можна довести конструктивно. Однак, ґрунтуючись на різному значенні слів в конструктивній математиці, якщо існує конструктивне доведення того, що «f(0) = 1 or f(0) ≠ 1», то це буде означати, що існує конструктивне доведення гіпотези Гольдбаха (в першому випадку) або конструктивне доведення того, що гіпотеза Гольдбаха є хибною (в останньому). Оскільки таке доведення ще не відоме, процитований вислів також не повинен мати конструктивного доведення. Проте цілком можливо, що гіпотеза Гольдбаха може мати конструктивне доведення (оскільки ми ще не знаємо, чи воно є), в цьому випадку процитований вислів також матиме конструктивне доведення, хоча й те наразі невідоме. Основне практичне застосування слабких контрприкладів полягає у визначенні «твердості» проблеми. Наприклад, щойно наведений контрприклад показує, що процитований вислів настільки ж важко довести, як і принаймні гіпотезу Гольдбаха. Слабкі контрприклади такого роду часто пов'язані з обмеженим принципом всезнання.

Див. також ред.

Ерретт Бішоп^[en] — автор книги «Основи конструктивного аналізу».
Теорема існування
Неконструктивне доведення
Неконструктивні доведення існування алгоритмів^[en]
Імовірнісний метод

Примітки ред.

↑ J. Roger Hindley, «The Root-2 Proof as an Example of Non-constructivity», unpublished paper, September 2014, full text [Архівовано 23 жовтня 2014 у Wayback Machine.]
↑ Dov Jarden, «A simple proof that a power of an irrational number to an irrational exponent may be rational», Curiosa No. 339 in Scripta Mathematica 19:229 (1953)

[1] J. Roger Hindley, «The Root-2 Proof as an Example of Non-constructivity», unpublished paper, September 2014, full text [Архівовано 23 жовтня 2014 у Wayback Machine.]

[2] Dov Jarden, «A simple proof that a power of an irrational number to an irrational exponent may be rational», Curiosa No. 339 in Scripta Mathematica 19:229 (1953)

[1]

[2]