Философская энциклопедия - разрешения проблема
Разрешения проблема
РАЗРЕШЕНИЯ ПРОБЛЕМА — возникла в связи с осознанием невозможности провести некоторые построения дозволенными методами. Первыми примерами неразрешимых задач явились решение в радикалах уравнений выше четвертой степени и невозможность провести некоторые построения циркулем и линейкой.
Общая формулировка проблемы разрешения следующая: дан класс методов Ф, дан класс проблем Р. Можно ли найти единый метод/? Ф (разрешающий метод), позволяющий решить каждую из проблем Р, для которой в принципе существует решение?
Часто в текстах по логике и математике рассматривается более частная формулировка проблемы разрешения, называемая алгоритмической разрешимостью, в которой разрешающий метод должен быть алгоритмом, т. е. класс методов Ф фиксируется и считается множеством алгоритмов. Исторически алгоритмическая неразрешимость была первым явно выделенным случаем общей проблемы разрешения. В последнее время в связи с осознанием разницы между теоретической и практической вычислимостью появилась третья формулировка, когда разрешающий метод — не просто алгоритм, а алгоритм ограниченной сложности. Напр., линейная разрешимость — разрешимость программой, вычислимая за линейное время относительно длины исходных данных, NP — полная проблема — проблема, разрешимая лишь программой полного перебора.
Примерами в разной степени неразрешимых проблем являются: построение модели любой непротиворечивой классической теории — неразрешима однозначно определенными (без аксиомы выбора) теоретико-множественными функционалами; проверка истинности формул арифметики либо (соответствия) программ их спецификации — неразрешима средствами формальных теорий с алгоритмически заданным множеством аксиом; проверка доказуемости в формальной арифметике или в классической логике предикатов — алгоритмически неразрешима; задача нормализации выводов в логике предикатов — неразрешима примитивно-рекурсивными алгоритмами; задача перестройки естественного вывода в резолюционный — неразрешима алгоритмами, делающими не более
У