Теорія доведення
Теорія доведення (доказів)— розділ математичної логіки, який представляє докази у вигляді формальних математичних об'єктів, здійснюючи їх аналіз за допомогою математичних методів. Докази, як правило, представлені у вигляді індуктивно визначеної структур даних, таких як списки і дерева, створених відповідно до аксіом і правил виводу формальних систем. Таким чином, теорія доказів є синтаксичною, на відміну від семантичної теорії моделей.
Хоча формалізація логіки набагато виросла в роботах таких діячів, як Готлоб Фреге, Джузеппе Пеано, Бертран Расселл, і Ріхард Дедекінд, історія сучасної теорії доведень часто розглядається як створена Давидом Гільбертом, який ініціював те, що називається Програма Гільберта в основах математики. Оригінальна робота Курта Геделя про теорію доведень була вперше висунута, і відразу же спростована. Вся ця робота була проведена за допомогою доказових обчислень і отримала назву система Гільберта.
Теорія доведення спочатку з'явилася у зв'язку з програмою Гільберта (див. Формалізм), із завданням обґрунтування того, що кожен формальний висновок змістовно інтерпретуючого (реального) твердження дає змістовно правильний результат, що включає в разі потреби і відповідну будову.
Одним із кроків у напрямку до даної мети здавалося доведення несуперечності формальних теорій. Цей засіб непомітно підмінив собою мету, і тому першим результатом теорії доведень була теорема Геделя про неповноту і її наслідок — про недовідність несуперечності.
Важливим позитивним результатом є теорема П. С. Новікова: твердження про існування результату алгоритмічної побудови, доведене в класичній арифметиці, дає вірне слідство, і у тому числі (грубу) оцінку числа необхідних кроків побудови. Ця теорема стала основою цілого класу результатів сучасної теорії доказів, що обґрунтовують збіг класичної істинності і конструктивної обґрунтованості для багатьох видів тверджень(останнім часом такі результати все частіше доводяться методами моделей теорії).
Наступним кроком в розвитку теорії доказів, що надовго зумовив її магістральний напрям, стало формулювання Г. Генценом числення секвенцій і природного виведення і доказ їм теореми нормалізації для класичного і інтуїціоністського числення секвенцій. Змістовно теорема нормалізації означає можливість перебудувати будь-яке формальне виведення в нормалізоване виведення без лем.
Було ясно, що поняття нормалізованого виведення застосовне і до природного виведення, але точне формулювання дав тільки Д. Правіц(1965). Хоча формальне визначення Правіца є складним, змістовний сенс його цілком прозорий. Логічних правил для кожної зв'язки зазвичай два: правило її введення, що показує, як доводити твердження цього виду, і правило видалення, що показує, як їх застосовувати. Наприклад, для імплікації в класичній і у багатьох інших логіках правила мають вигляд: Припустимо А
В, виходячи з А А = ^ У 'А, А => В В
У другому з цих правил формула А=>У використовується саме як імплікація, формула ж А не аналізується і може бути будь-якою. Для того, щоб підкреслити цей факт, Α=^ΰ називається головною посилкою правила видалення імплікації.
У виведенні є обхідний шлях, якщо результат правила введення використовується як головна посилка у відповідному правилі видалення, а така пара правил називається вершиною обхідного шляху. Якщо у виведенні немає вершин обхідних шляхів, то він називається прямим або нормалізованим.
Теорема нормалізації свідчить, що будь-яке виведення можна перебудувати в нормалізоване. Тривалий час різні форми нормалізації були провідною темою досліджень в теорії доказів. Розширювався клас числень і теорій, для яких встановлювалася нормалізація виведень. Зараз вона обґрунтована для теорії типів і для множини некласичних логік.
Встановлювалися й оцінки співвідношення довжини нормалізованого і початкового виведення. Тут була підтверджена правота Гільберта про необхідність ідеальних об'єктів для реальних результатів. Зокрема, В. А. Оревков побудував приклад послідовності формул, таких, що доказ η-ї формули з обхідними шляхами відбувається приблизно за 13 кроків, а нормалізоване виведення або виведення методом резолюцій повинен робити не менше 22 кроків. У непрямому доказі (η + 1) -ї формули використовується проміжний результат, що містить удвічі більше зв'язок, ніж в доказі /1-ї. У численні висловлювань оцінка збільшення довжини виведення трохи «оптимістичніша» — вона експоненціальна. У свою чергу вивчення властивостей самих перетворень, використовуваних при нормалізації виведень, зокрема показало, що запропонована Правіцом система операцій усунення вершин обхідних шляхів має властивість повної недетермінованості : незалежно від порядку застосування операцій за кінцеве число кроків виходить нормалізоване виведення. Але саме результуюче виведення істотно залежить від порядку застосування кроків.
Коли говорять про формальне доведення, перш за все описують формальну модель — набір (або множину) аксіом, записаних за допомогою формальної мови, і правил виводу. Формальним виводом називається скінчена впорядкована множина рядків, написаних на формальній мові, таких, що кожен з них або є аксіомою, або отриманий з попередніх рядків застосуванням одного з правил виводу. Формальним доказом твердження називається формальний вивід, останнім рядком якого є дане твердження. Твердження, що має формальний доказ, називається теоремою, а множина всіх теорем в даній формальній моделі (що розглядається разом з алфавітом формальної мови, множиною аксіом і правил виводу) називається формальною теорією.
Теорія називається повною, якщо для будь-якого твердження доведено або воно, або його заперечення, і несуперечливою, якщо в ній не існує тверджень, які можна довести разом з їхніми запереченнями. Більшість математичних теорій, як показує перша теорема Геделя про неповноту, є неповними, тобто в них існують твердження, про істинність яких нічого сказати не можна. Найпоширенішим набором аксіом у наш час є аксіоматика Цермело — Френкеля з аксіомою вибору (хоча деякі математики виступають проти використання останньої). Теорія на основі цієї системи аксіом не повна (наприклад, континуум-гіпотеза не може бути ані доведена, ані спростована в ній). Не зважаючи на повсюдне використання цієї теорії в математиці, її несуперечність не може бути доведена методами її самої. Проте, переважна більшість математиків вірять в її несуперечність, вважаючи, що інакше суперечності вже давно були б виявлені.
При прямому доведенні висновок встановлюється через логічну комбінацію аксіом, визначень і раніше доведених теорем. Для прикладу розглянемо доведення, що сума двох парних цілих чисел також є парною:
- кожне з двох парних чисел x та y ми можемо за визначенням записати у вигляді x = 2a та y = 2b, де a і b — деякі цілі числа, бо x та y діляться на 2. Але тоді сума x + y = 2a + 2b = 2(a + b) також ділиться на 2, так що вона є парною за визначенням.
Цей доказ використовує визначення парних цілих чисел, і також дистрибутивний закон додавання.
Припустимо, що потрібно встановити справедливість нескінченної послідовності тверджень, занумерованих натуральними числами: . Припустимо, що
- Встановлене, що P1 вірно. (Це твердження називається базою індукції.)
- Для будь-якого n доведено, що якщо вірно Pn, то вірно Pn + 1. (Це твердження називається індукційним переходом.)
Тоді всі твердження нашої послідовності вірні.
Метод перестановки встановлює істинність твердження Якщо А, то Б доведенням еквівалентного твердження Якщо не Б, то не А.
Цей метод доведення відомий також як приведення до абсурду (лат. reductio ad absurdum). Доказ твердження A проводиться таким чином. Спочатку приймають припущення, що твердження A невірно, а потім доводять, що за такого припущення було б вірне деяке твердження B, яке заздалегідь невірне. Отримана суперечність показує, що початкове припущення було невірним, і тому вірне твердження ¬¬A, яке за законом подвійного заперечення рівносильно твердженню A.
Конструктивне доведення або доведення наданням прикладу — це конструювання конкретного прикладу з властивостями, для того щоб довести, що існують приклади з цими властивостями. Наприклад, Жозеф Ліувілль, для того щоб довести існування трансцендентних чисел, явно сконструював таке число.
При доведенні методом витягів висновок про істинність твердження досягається розділенням твердження на скінчену кількість випадків і доведенням кожного такого випадку окремо. Кількість таких випадків може бути дуже великою. Наприклад, перший доказ проблеми чотирьох фарб складався з розгляду 1936 випадків. Більшість цих випадків розглядала комп'ютерна програма, а не людина. Сучасніші коротші докази теореми про чотири фарби все одно вимагають розгляду понад 600 випадків.
Ймовірнісним доказом називають метод, коли існування прикладу доводиться засобами теорії ймовірності. Тільки не треба плутати цей метод з аргументом, що теорема «ймовірно» істинна. Такого типу аргументи називаються «правдоподібністю» і не можуть вважатися доказом. Ймовірнісний доказ, поруч із конструктивним методом, є одним з багатьох шляхів доведення теореми існування.
Суть комбінаторного доказу полягає у встановлені еквівалентності різних виразів, так що вони представляють той самий об'єкт, але в різний спосіб. Звичайно, для того щоб показати, що дві інтерпретації дають той самий об'єкт, використовується бієкція.
Неконструктивне доведення встановлює, що певний математичний об'єкт повинен існувати (тобто певний X, що задовольняє f(X)), без пояснення, як цей об'єкт може бути встановлений. Часто це робиться зведенням до суперечності твердження, що такого об'єкта не існує. На противагу цьому, конструктивне доведення встановлює існування об'єкта представленням способу визначення об'єкта.
Відомим прикладом неконструктивного доведення є доказ існування двох ірраціональних чисел a і b, таких що ab є числом раціональним.
- Або є раціональним числом і ми маємо приклад (де ),
- або ж показує, що ми маємо та .
Існує клас математичних тверджень, для яких не існує ані доказу, ані спростування (тобто доведення зворотного твердження) в рамках аксіоматики Цермело — Френкеля, стандартної основи теорії множин. Як приклад можна навести континуум-гіпотезу. Якщо погодитися з непротивоічністю аксіом Френкеля — Цермело, існування таких прикладів нам гарантує перша теорема неповноти Геделя. Чи можна довести певне твердження чи його спростування, не завжди очевидно і може вимагати надзвичайної техніки для встановлення цього факту.
Елементарним доведенням називають докази, що не потребують складного аналізу.
В деяких випадках теореми, як наприклад теорема про асимптотичний розподіл простих чисел, вимагала застосування «вищої» математики. Але з часом були отримані нові докази з використанням елементарної техніки.
- Гільберт Д., Бернайс П. — Основи математики.
- Кліні С. К. Введення в метаматематику. М, 1957.
- Такеуті Г. Теорія доказів. М., 1978.
- Асмус В. Ф. Учение логики о доказательстве и опровержении. — М., 1954.
- Горский Д. П., Ивин А. А., Никифоров А. А. Краткий словарь по логике. — М., 1991.
- Ерышев А. А., Лукашевич Н. П., Сластенко Е. Ф. Логика. — К.: МАУП, 2000.
- Иванов Е. А. Логика. — М., 2001.
- Івін О. А. Логіка. — К.,1996.
- Кириллов В. И., Старченко А. А. Логика. — М., 1995.
- Литвак М. Е. Как узнать и изменить свою судьбу. — Ростов-на Дону: Феникс, 2002.
- Рузавин Н. В. Логика и аргументация. — М., 1997.
- Эйсман А. А. Логика доказывания. — М., 1997.