Теорія доказів

Теорія доказів — розділ сучасної математичної логіки, що вивчає властивості і перетворення формальних доказів, тобто формальних об'єктів, синтаксична правильність яких гарантує семантичну. Це визначення уніфікує безліч різнорідних понять формального доказу, існуючих у математичній логіці: послідовності формул, графи, діаграми і т. д.

Опис

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

Поява та розвиток

Теорія доказів спочатку з'явилася у зв'язку з програмою Гільберта(див. Формалізм), із завданням обґрунтування того, що кожне формальне виведене твердження, що змістовно інтерпретується (реального), дає змістовно правильний результат, що включає у разі потреби і відповідна побудова.

Одним із кроків у напрямку до цієї мети здавався доказ несуперечності формальних теорій. Цей засіб непомітно підмінив собою мету і тому першим результатом теорії доказів, що став відомим, була теорема Геделя про неповноту і її слідуванн, а саме про недоказовність несуперечності.

Теорема Новікова

Важливим позитивним результатом є теорема П. С. Новікова: твердження про існування результату алгоритмічної побудови, доведене в класичній арифметиці, дає вірне слідство, і у тому числі (грубу) оцінку числа необхідних кроків побудови. Ця теорема стала основою цілого класу результатів сучасної теорії доказів, що обґрунтовують збіг класичної істинності і конструктивної обґрунтованості для багатьох видів тверджень(останнім часом такі результати все частіше доводяться методами моделей теорії).

Робота Генцена

Наступним кроком в розвитку теорії доказів, що надовго зумовив її магістральний напрям, стало формулювання Г. Генценом числення секвенцій і природного виведення і доказ їм теореми нормалізації для класичного і інтуїціоністського числення секвенцій. Змістовно теорема нормалізації означає можливість перебудувати будь-яке формальне виведення в нормалізоване виведення без лем.

Формулювання Правіца

Було ясно, що поняття нормалізованого виведення застосовне і до природного виведення, але точне формулювання дав тільки Д. Правіц(1965). Хоча формальне визначення Правіца є складним, змістовний сенс його цілком прозорий. Логічних правил для кожної зв'язки зазвичай два: правило її введення, що показує, як доводити твердження цього виду, і правило видалення, що показує, як їх застосовувати. Наприклад, для імплікації в класичній і у багатьох інших логіках правила мають вигляд: Припустимо А

В, виходячи з А А = ^ У 'А, А => В В

У другому з цих правил формула А=>У використовується саме як імплікація, формула ж А не аналізується і може бути будь-якою. Для того, щоб підкреслити цей факт, Α=^ΰ називається головною посилкою правила видалення імплікації.

У виведенні є обхідний шлях, якщо результат правила введення використовується як головна посилка у відповідному правилі видалення, а така пара правил називається вершиною обхідного шляху. Якщо у виведенні немає вершин обхідних шляхів, то він називається прямим або нормалізованим.

Теорема нормалізації

Теорема нормалізації свідчить, що будь-яке виведення можна перебудувати в нормалізоване. Тривалий час різні форми нормалізації були провідною темою досліджень в теорії доказів. Розширювався клас числень і теорій, для яких встановлювалася нормалізація виведень. Зараз вона обґрунтована для теорії типів і для множини некласичних логік.

Встановлювалися й оцінки співвідношення довжини нормалізованого і початкового виведення. Тут була підтверджена правота Гільберта про необхідність ідеальних об'єктів для реальних результатів. Зокрема, В. А. Оревков побудував приклад послідовності формул, таких, що доказ η-ї формули з обхідними шляхами відбувається приблизно за 13 кроків, а нормалізоване виведення або виведення методом резолюцій повинен робити не менше 22 кроків. У непрямому доказі (η + 1) -ї формули використовується проміжний результат, що містить удвічі більше зв'язок, ніж в доказі /1-ї. У численні висловлювань оцінка збільшення довжини виведення трохи «оптимістичніша» — вона експоненціальна. У свою чергу вивчення властивостей самих перетворень, використовуваних при нормалізації виведень, зокрема показало, що запропонована Правіцом система операцій усунення вершин обхідних шляхів має властивість повної недетермінованості : незалежно від порядку застосування операцій за кінцеве число кроків виходить нормалізоване виведення. Але саме результуюче виведення істотно залежить від порядку застосування кроків.

Зв'язок з інформатикою

Останнім часом на стиках між теорією доказів і інформатикою з'явилися нові класи результатів. По-перше, з'ясувалося, що структури доказів і структури витягуваних з них побудов, записаних алгоритмічною мовою досить високого рівня(що допускає роботу зі значеннями вищих типів; так що Pascal і С цим вимогам не задовільняють), тісно пов'язані. Побудова мономорфно вкладається в доказ, а частина доказу, що виходить відкиданням кроків і формул, потрібних лише для обґрунтування результату, ізоморфна програмі.

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

Див. також

• Доказові обчислення

Література

• Теорія доказів : навч. посіб. для студентів галузі знань «Право» спец. «Правознавство» / В. С. Канцір, М. М. Олашин, Б. П. Ратушна, Ю. О. Фігель; Укоопспілка, Львів. комерц. акад. — Львів : Вид-во Львів. комерц. акад., 2015. — 295 c. — Бібліогр.: с. 290—293.
• Теорія доказів: підручник / К. В. Антонов, О. В. Сачко, В. М. Тертишник, В. Г. Уваров / За заг. ред. В. М. Тертишника. — Київ: Алерта, 2015. — 294 с.