Відмінності між версіями «Алгоритмічна розв'язність»

уточнення
(уточнення)
 
'''Алгоритмічна розв'язність'''  — властивість [[Формальна система|формальної теорії]] володіти [[Алгоритм|алгоритмом]], який визначає за даною [[Формула|формулою]], виводиться вона з множини [[Аксіома|аксіом]] даної теорії чи ні. Теорія називається '''розв'язною''', якщо такий алгоритм існує, і '''нерозв'язною''', в іншому випадку. Питання про виводимість у формальній теорії є частковим, але разом з тим найважливішим випадком більш загальної [[Проблема вибору|проблеми розв'язності]].
 
== Історія питання та передумови ==
Поняття алгоритму та аксіоматичної системи мають давню історію. І те й інше відоме ще з часів [[Античність|античності]]. Досить згадати [[Евклідова геометрія|постулати геометрії]] [[Евклід|Евкліда]]а і його ж [[Алгоритм Евкліда|алгоритм знаходження найбільшого спільного дільника]]. Незважаючи на це, чіткого математичного визначення числення та особливо алгоритму не існувало дуже довгий час. Особливість проблеми, пов'язаної з формальним визначенням нерозв'язності полягала в тому, що для того, щоб показати, що існує певний алгоритм, достатньо його просто знайти і продемонструвати. Якщо ж алгоритм не знаходиться, можливо його не існує і це тоді потрібно строго довести. А для цього потрібно точно знати, що таке алгоритм.
 
Значного прогресу у формалізації цих понять було досягнуто на початку [[XX століття]] [[Давид Гільберт|Гільбертом]] і його школою. Тоді, спочатку, сформувалися поняття числення і формального виводу, а потім Гільберт у своїй знаменитій {{нп|Програма Гільберта|програмі обґрунтування математики||Hilbert's program}} поставив мету формалізації всієї математики. Програма передбачала, зокрема, можливість автоматичної перевірки будь-якої математичної формули на предмет істинності. Відштовхуючись від робіт Гільберта, [[Курт Гедель|Гедель]] вперше описав клас так званих [[Рекурсія (програмування)|рекурсивних функцій]], за допомогою якої довів свої [[Теореми Геделя про неповноту|теореми про неповноту]]. Згодом було введено низку інших формалізмів, таких як [[Машина Тюрінга|машина Тюрінга]], [[Лямбда-числення|λ-числення]], які виявилися еквівалентними рекурсивним функціям. У даний час кожен з них вважається формальним еквівалентом інтуїтивного поняття обчислюваної функції. Ця еквівалентність постулюється [[Теза Черча — Тюрінга|тезою Черча]].
 
Коли поняття числення і алгоритму були уточнені, з'явилась низка результатів про нерозв'язності різних теорій. Одним з перших таких результатів була теорема, доведена {{нп|Петро Сергійович Новіков|Новіковим|ru|Новиков, Пётр Сергеевич}}, про нерозв'язність {{нп|Слово (теорія груп)|проблеми слів||Word (group theory)}} у [[Група (математика)|групах]]. Розв'язні ж теорії були відомі задовго до цього.
 
Інтуїтивно зрозуміло, що чим складніша і виразніша теорія, тим більше шансів, що вона виявиться нерозв'язною. Тому, грубо кажучи, «нерозв'язна теорія»  — «складна теорія».
 
== Загальні відомості ==
[[Формальна система|Формальне обчислення]] в загальному випадку має визначати [[Мова|мову]], правила побудови {{нп|Терм (логіка)|термів|ru|Терм (логика)}} та [[Формула|формул]], аксіоми і правила виводу. Таким чином, для кожної теореми {{Math|'''T'''}} завжди можна побудувати ланцюжок {{Math|'''A<sub>1</sub>''', '''A<sub>2</sub>''', … , '''A<sub>n</sub>'''{{=}}'''T'''}}, де кожна формула {{Math|'''A<sub>i</sub>'''}} або є аксіомою, або виводима з попередніх формул за одним з правил виведення. Розв'язність означає, що існує алгоритм, який для кожного правильно побудованого речення {{Math|'''T'''}} за скінченний час видає однозначну відповідь: так, дане речення виводиме в рамках числення або ні &nbsp;— воно невиводиме.
 
Очевидно, що суперечлива теорія розв'язна, оскільки будь-яка формула буде виводимою. З іншого боку, якщо числення не має {{iw|Рекурсивно-зліченна множина|рекурсивно зліченної множини|ru|Рекурсивно перечислимое множество}} аксіом, як наприклад, [[Логіка другого порядку|логіка другого порядку]], воно, очевидно, не може бути розв'язним.
=== Приклади розв'язаних теорій ===
{{У планах|дата=26 лютого 2019}}
 
=== Приклади нерозв'язних теорій ===
{{У планах|дата=26 лютого 2019}}
 
== Напіврозв'язність і автоматичне доведення ==
Розв'язність &nbsp;— дуже сильна властивість, і більшість корисних і використовуваних на практиці теорій нею не володіють. У зв'язку з цим було введено слабше поняття ''напіврозв'язності''. Напіврозв'язність означає наявність алгоритму, який за скінченний час завжди підтвердить, що речення істинне, якщо це дійсно так, але якщо ні &nbsp;— може працювати нескінченно.
 
Вимога напіврозв'язності еквівалентна можливості ефективно перелічити всі теореми даної теорії. Іншими словами, множина теорем повинна бути рекурсивно-зліченною. Більшість використовуваних на практиці теорій задовольняють цій вимозі.
 
== Зв'язок розв'язності та повноти ==
У [[Математична логіка|математичній логіці]] традиційно використовується два поняття повноти: власне повнота і повнота щодо деякого класу інтерпретацій (або структур). У першому випадку, теорія повна, якщо будь-яке речення в ній є або істинним, або хибним. У другому &nbsp;— якщо будь-яке речення, істинне при всіх інтерпретаціях з даного класу, виводиме.
 
Обидва ці поняття тісно пов'язані з розв'язністю. Наприклад, якщо множина аксіом повної теорії першого порядку рекурсивно зліченна, то вона розв'язна. Це випливає з відомої [[Критерій Поста|теореми Поста]], яка стверджує, що якщо множина і її доповнення обидва рекурсивно зліченні, то вони також {{нп|Розв'язна множина|розв'язні|ru|Разрешимое множество}}. Інтуїтивно, аргумент, який засвідчує істинність наведеного твердження, такий: якщо теорія повна, і множина її аксіом рекурсивно зліченна, то існують напіврозв'язувальні процедури для перевірки істинності будь-якого твердження, так само як і його заперечення. Якщо запустити обидві ці процедури [[Рівночасні обчислення|паралельно]], то враховуючи повноту теорії, одна з них повинна коли-небудь зупинитися і видати позитивну відповідь.
* [[Теза Черча — Тюрінга]]
* [[Обчислювана функція]]
* {{нп|Розв'язна множина||ru|Разрешимое множество}}
* [[Алгоритмічно нерозв'язна задача]]