Алгоритмічна розв'язність: відмінності між версіями
| [перевірена версія] | [перевірена версія] |
Вилучено вміст Додано вміст
Немає опису редагування |
уточнення |
||
Рядок 1:
'''Алгоритмічна розв'язність'''
== Історія питання та передумови ==
Поняття алгоритму та аксіоматичної системи мають давню історію. І те й інше відоме ще з часів [[Античність|античності]]. Досить згадати [[Евклідова геометрія|постулати геометрії]] [[Евклід
Значного прогресу у формалізації цих понять було досягнуто на початку [[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'''}} за скінченний час видає однозначну відповідь: так, дане речення виводиме в рамках числення або ні
Очевидно, що суперечлива теорія розв'язна, оскільки будь-яка формула буде виводимою. З іншого боку, якщо числення не має {{iw|Рекурсивно-зліченна множина|рекурсивно зліченної множини|ru|Рекурсивно перечислимое множество}} аксіом, як наприклад, [[Логіка другого порядку|логіка другого порядку]], воно, очевидно, не може бути розв'язним.
Рядок 17:
=== Приклади розв'язаних теорій ===
{{У планах|дата=26 лютого 2019}}
=== Приклади нерозв'язних теорій ===
{{У планах|дата=26 лютого 2019}}
== Напіврозв'язність і автоматичне доведення ==
Розв'язність
Вимога напіврозв'язності еквівалентна можливості ефективно перелічити всі теореми даної теорії. Іншими словами, множина теорем повинна бути рекурсивно-зліченною. Більшість використовуваних на практиці теорій задовольняють цій вимозі.
Рядок 27 ⟶ 29:
== Зв'язок розв'язності та повноти ==
У [[Математична логіка|математичній логіці]] традиційно використовується два поняття повноти: власне повнота і повнота щодо деякого класу інтерпретацій (або структур). У першому випадку, теорія повна, якщо будь-яке речення в ній є або істинним, або хибним. У другому
Обидва ці поняття тісно пов'язані з розв'язністю. Наприклад, якщо множина аксіом повної теорії першого порядку рекурсивно зліченна, то вона розв'язна. Це випливає з відомої [[Критерій Поста|теореми Поста]], яка стверджує, що якщо множина і її доповнення обидва рекурсивно зліченні, то вони також {{нп|Розв'язна множина|розв'язні|ru|Разрешимое множество}}. Інтуїтивно, аргумент, який засвідчує істинність наведеного твердження, такий: якщо теорія повна, і множина її аксіом рекурсивно зліченна, то існують напіврозв'язувальні процедури для перевірки істинності будь-якого твердження, так само як і його заперечення. Якщо запустити обидві ці процедури [[Рівночасні обчислення|паралельно]], то враховуючи повноту теорії, одна з них повинна коли-небудь зупинитися і видати позитивну відповідь.
Рядок 39 ⟶ 41:
* [[Теза Черча — Тюрінга]]
* [[Обчислювана функція]]
* {{нп|Розв'язна множина||ru|Разрешимое множество}}
* [[Алгоритмічно нерозв'язна задача]]
| |||