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

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

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

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

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

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

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

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

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

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

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