Проблема разрешимости

Проблема разрешимости, или проблема разрешения — это логическая проблема нахождения в рамках какой-либо дедуктивной теории (см. Теория) общего метода (см. Метод), позволяющего решать, может ли отдельное утверждение, сформулированное в терминах данной теории, быть доказано в ней или нет. Этот общий метод, являющийся эффективной процедурой, то есть алгоритмом (см. Алгоритм), называется разрешающей процедурой, а теория, для которой такая процедура существует, — разрешимой теорией.

Проблема разрешения возникла в связи с осознанием невозможности провести некоторые построения в логике (см. Логика) и математике дозволенными методами. Первыми примерами неразрешимых задач явились решение в радикалах уравнений выше четвёртой степени и невозможность провести некоторые построения циркулем и линейкой. В 1928 году Д. Гилберт сформулировал «проблему разрешения», которая заключалась в нахождении общего метода, или эффективной процедуры (алгоритма), с помощью которой относительно любого утверждения на языке формальной логики (см. Логика формальная) можно решить вопрос, является ли оно истинным. Обнаружение К. Гёделем арифметических истин, которые недоказуемы, оказало решающее воздействие на решение проблемы разрешения. По свидетельству историков сам Гилберт вплоть до 1930 года верил, что нет такого объекта как неразрешимая проблема. Однако, чтобы ответить на вопрос Гилберта потребовалось уточнение того, что понимается под эффективной процедурой, или, по-другому, потребовалось уточнение неформального понятия «алгоритма» в виде формальной модели потенциальной вычислимости. Например, метод построения истинностной таблицы для проверки пропозициональной формулы на тавтологичность, является эффективной процедурой. В 1936–1937 годах А. Чёрч и А. Тьюринг предложили первые приемлемые уточнения понятия вычислимости (соответственно «лямбда-исчисление» и «машина Тьюринга»), с помощью которых показали, что не существует универсального алгоритма для проверки истинности утверждений арифметики, а поэтому и более общая проблема разрешения также не имеет решения.

Общая формулировка проблемы разрешения состоит в следующем: дан класс методов Ф, дан класс проблем P. Можно ли найти единый метод f ∈ Φ (разрешающий метод), позволяющий решить каждую из проблем P, для которой в принципе существует решение?

Часто в текстах по логике и математике рассматривается более частная формулировка проблемы разрешения, называемая алгоритмической разрешимостью, в которой разрешающий метод должен быть алгоритмом, то есть класс методов Φ фиксируется и считается множеством алгоритмов. Исторически алгоритмическая неразрешимость была первым явно выделенным случаем общей проблемы разрешения.

В последнее время в связи с осознанием разницы между теоретической и практической вычислимостью появилась третья формулировка, когда разрешающий метод — не просто алгоритм, а алгоритм ограниченной сложности. Например, линейная разрешимость — разрешимость программой, вычислимая за линейное время относительно длины исходных данных, NP-полная проблема — проблема, разрешимая лишь программой полного перебора.

Известными примерами в разной степени неразрешимых проблем являются:

• построение модели любой непротиворечивой классической теории — неразрешима однозначно определёнными (без аксиомы выбора) теоретико-множественными функционалами;
• проверка истинности формул арифметики либо (соответствия) программ их спецификации — неразрешима средствами формальных теорий с алгоритмически заданным множеством аксиом;
• проверка доказуемости в формальной арифметике или в классической логике предикатов — алгоритмически неразрешима; задача нормализации выводов в логике предикатов — неразрешима примитивно-рекурсивными алгоритмами;
• задача перестройки естественного вывода в резолюционный — неразрешима алгоритмами, делающими не более:
  2^{2 … n} } (k раз)

  Шагов, где n — длина вывода, k — любое фиксированное число;

• проверка тавтологичности формул классической логики высказываний — переборно разрешима, но неразрешима менее чем переборными алгоритмами.

Проблема разрешения решается в классической логике высказываний с помощью таблиц истинности. Примеры: построение таблицы истинности для пропозициональной формулы и проверка главного столбца на отсутствие значения «ложь» есть алгоритм, решающий проблемы разрешения классической логики высказываний; множество простых натуральных чисел (числа записываются, например, в десятичной системе счисления; число называется простым, если это натуральное число, больше или равное 2, имеющее только два натуральных делителя — самое себя и 1) и соответствующая проблема выяснения простоты натурального числа разрешима с помощью алгоритма перебора возможных делителей.

Разрешающий алгоритм существует и для логики одноместных предикатов, для силлогизма категорического и других простых дедуктивных теорий. Но уже для логики предикатов общего решения проблемы разрешения не существует. В математике также невозможно установить общий метод, который дал бы возможность провести различие между утверждениями, которые могут быть доказаны в ней, и теми, которые в ней недоказуемы.

Следует отметить, что невозможность найти для теории общий разрешающий метод не исключает поиска процедуры разрешения для отдельных классов её утверждений. Неразрешимость проблемы означает лишь отсутствие единого метода, хотя в каждом конкретном случае её можно пытаться решать, если решение не претендует на слишком большую общность. В последнее время выявилось общее свойство частных решений неразрешимых проблем: по мере расширения класса решаемых задач сложность методов с некоторого момента быстро растёт, а эффективность столь же быстро убывает. Точно так же результат о достаточно простой разрешимости проблемы может оказаться дезориентирующим, если эта достаточная простота достигается лишь на очень больших объектах, а для малых всё равно приходится практически действовать перебором.

Сведение к неразрешимым проблемам стало столь же мощным методом установления некорректности задач либо решений, каким является в физике сведение к возможности построить вечный двигатель. Неразрешимость проблемы разложения числа на простые множители достаточно простым алгоритмом стала основой современной теории надёжных индивидуальных шифров. Одним из методов решения неразрешимых проблем является переход к вероятностным алгоритмам разрешения и к квантовым вычислениям. Показано, что для многих переборных задач есть быстрые алгоритмы, решающие их со сколь угодно близкой к единице заранее заданной вероятностью.

В последние десятилетия в связи с приложениями к проблемам, имеющим практическое значение, к проблеме разрешения относят и вопросы оптимизации найденных алгоритмов, то есть требуется не только предоставить разрешающий алгоритм, но и обосновать, что этот алгоритм имеет наименьшую возможную сложность вычисления в том или ином смысле (по затратам времени, памяти, и так далее). С точки зрения этой подпроблемы проблема разрешения многие теории (или множества конструктивных объектов), для которых проблемы разрешения были положительно решены, оказались практически неразрешимыми или, по крайней мере, найденные алгоритмы не годятся для практического применения.