Алгоритмічна розв'язність
Алгоритмічна розв'язність — властивість формальної теорії володіти алгоритмом, який визначає за даною формулою, виводиться вона з множини аксіом даної теорії чи ні. Теорія називається розв'язною, якщо такий алгоритм існує, і нерозв'язною, в іншому випадку. Питання про виводимість у формальній теорії є частковим, але разом з тим найважливішим випадком більш загальної проблеми розв'язності.
Історія питання та передумови
Поняття алгоритму та аксіоматичної системи мають давню історію. І те й інше відоме ще з часів античності. Досить згадати постулати геометрії Евкліда і його ж алгоритм знаходження найбільшого спільного дільника. Незважаючи на це, чіткого математичного визначення числення та особливо алгоритму не існувало дуже довгий час. Особливість проблеми, пов'язаної з формальним визначенням нерозв'язності полягала в тому, що для того, щоб показати, що існує певний алгоритм, достатньо його просто знайти і продемонструвати. Якщо ж алгоритм не знаходиться, можливо його не існує і це тоді потрібно строго довести. А для цього потрібно точно знати, що таке алгоритм.
Значного прогресу у формалізації цих понять було досягнуто на початку XX століття Гільбертом і його школою. Тоді, спочатку, сформувалися поняття числення і формального виводу, а потім Гільберт у своїй знаменитій програмі обґрунтування математики поставив мету формалізації всієї математики. Програма передбачала, зокрема, можливість автоматичної перевірки будь-якої математичної формули на предмет істинності. Відштовхуючись від робіт Гільберта, Гедель вперше описав клас так званих рекурсивних функцій, за допомогою якої довів свої теореми про неповноту. Згодом було введено низку інших формалізмів, таких як машина Тюрінга, λ-числення, які виявилися еквівалентними рекурсивним функціям. У даний час кожен з них вважається формальним еквівалентом інтуїтивного поняття обчислюваної функції. Ця еквівалентність постулюється тезою Черча.
Коли поняття числення і алгоритму були уточнені, з'явилась низка результатів про нерозв'язності різних теорій. Одним з перших таких результатів була теорема, доведена Новіковим, про нерозв'язність проблеми слів у групах. Розв'язні ж теорії були відомі задовго до цього.
Інтуїтивно зрозуміло, що чим складніша і виразніша теорія, тим більше шансів, що вона виявиться нерозв'язною. Тому, грубо кажучи, «нерозв'язна теорія» — «складна теорія».
Загальні відомості
Формальне обчислення в загальному випадку має визначати мову, правила побудови термів та формул, аксіоми і правила виводу. Таким чином, для кожної теореми T завжди можна побудувати ланцюжок A1, A2, … , An=T, де кожна формула Ai або є аксіомою, або виводима з попередніх формул за одним з правил виведення. Розв'язність означає, що існує алгоритм, який для кожного правильно побудованого речення T за скінченний час видає однозначну відповідь: так, дане речення виводиме в рамках числення або ні — воно невиводиме.
Очевидно, що суперечлива теорія розв'язна, оскільки будь-яка формула буде виводимою. З іншого боку, якщо числення не має рекурсивно зліченної множини аксіом, як наприклад, логіка другого порядку, воно, очевидно, не може бути розв'язним.
Напіврозв'язність і автоматичне доведення
Розв'язність — дуже сильна властивість, і більшість корисних і використовуваних на практиці теорій нею не володіють. У зв'язку з цим було введено слабше поняття напіврозв'язності. Напіврозв'язність означає наявність алгоритму, який за скінченний час завжди підтвердить, що речення істинне, якщо це дійсно так, але якщо ні — може працювати нескінченно.
Вимога напіврозв'язності еквівалентна можливості ефективно перелічити всі теореми даної теорії. Іншими словами, множина теорем повинна бути рекурсивно-зліченною. Більшість використовуваних на практиці теорій задовольняють цій вимозі.
Велике практичне значення мають ефективні напіврозв'язувальні процедури для логіки першого порядку, оскільки вони дозволяють (напів)автоматично доводити формалізовані твердження дуже широкого класу. Проривом у цій галузі було відкриття Робінсоном у 1965 році методу резолюцій.
Зв'язок розв'язності та повноти
У математичній логіці традиційно використовується два поняття повноти: власне повнота і повнота щодо деякого класу інтерпретацій (або структур). У першому випадку, теорія повна, якщо будь-яке речення в ній є або істинним, або хибним. У другому — якщо будь-яке речення, істинне при всіх інтерпретаціях з даного класу, виводиме.
Обидва ці поняття тісно пов'язані з розв'язністю. Наприклад, якщо множина аксіом повної теорії першого порядку рекурсивно зліченна, то вона розв'язна. Це випливає з відомої теореми Поста, яка стверджує, що якщо множина і її доповнення обидва рекурсивно зліченні, то вони також розв'язні. Інтуїтивно, аргумент, який засвідчує істинність наведеного твердження, такий: якщо теорія повна, і множина її аксіом рекурсивно зліченна, то існують напіврозв'язувальні процедури для перевірки істинності будь-якого твердження, так само як і його заперечення. Якщо запустити обидві ці процедури паралельно, то враховуючи повноту теорії, одна з них повинна коли-небудь зупинитися і видати позитивну відповідь.
Якщо теорія повна щодо деякого класу інтерпретацій, це можна використовувати для побудови розв'язувальної процедури. Наприклад пропозиціональна логіка повна щодо інтерпретації на таблицях істинності. Тому побудова таблиці істинності за цією формулою буде прикладом розв'язувального алгоритму для пропозиційної логіки.