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

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

¶История

¶Формулировка проблемы

В начале XX века, под влиянием идей Д. Гильберта, в математике сформировалась программа обоснования, известная как формализм. Гильберт поставил задачу доказать непротиворечивость и полноту формальных аксиоматических систем, в которых вся математика могла бы быть представлена в виде формальных выводов. В рамках этой программы в 1928 году на Международном математическом конгрессе в Болонье Гильберт и В. Аккерманн в явном виде сформулировали проблему разрешимости (Entscheidungsproblem) для логики предикатов первого порядка. Вопрос состоял в том, существует ли эффективная процедура (алгоритм), позволяющая для любой формулы логики предикатов установить, является ли она общезначимой (т.е. истинной во всех интерпретациях).

¶Работы Гёделя и Чёрча

Первые шаги к решению проблемы были сделаны К. Гёделем. В 1930 году он доказал теорему о полноте логики предикатов первого порядка, из которой следовало, что общезначимость формулы эквивалентна её выводимости в некоторой формальной системе. Однако это не решало проблему разрешимости, так как процедура поиска вывода могла быть бесконечной. В 1931 году Гёдель доказал теоремы о неполноте, показав, что для достаточно богатых формальных систем (включая арифметику Пеано) невозможно установить непротиворечивость средствами самой системы. Это подорвало оптимизм формалистской программы, но не давало прямого ответа на вопрос о разрешимости логики предикатов.

В 1936 году А. Чёрч, используя формализм λ-исчисления, доказал, что проблема разрешимости для логики предикатов первого порядка алгоритмически неразрешима. Он показал, что не существует алгоритма, который бы для любой формулы определял её общезначимость. Чёрч ввёл понятие рекурсивной функции как формального аналога алгоритма и доказал, что множество общезначимых формул не является рекурсивным.

¶Работы Тьюринга и Поста

Почти одновременно с Чёрчем, в 1936—1937 годах, А. Тьюринг и независимо от него Э. Пост предложили свои формальные модели вычислений — машину Тьюринга и машину Поста соответственно. Тьюринг, используя свою модель, дал альтернативное доказательство неразрешимости проблемы разрешимости. Он показал, что проблема остановки машины Тьюринга (определение, остановится ли данная машина на данном входе) алгоритмически неразрешима, и свёл к ней проблему разрешимости. Работы Тьюринга и Поста окончательно установили, что проблема разрешимости в общем виде не имеет положительного решения.

¶Основные результаты

¶Неразрешимость логики предикатов

Центральный результат теории алгоритмов: проблема разрешимости для логики предикатов первого порядка алгоритмически неразрешима. Это означает, что не существует единого алгоритма, который, получив на вход любую формулу логики предикатов, за конечное число шагов давал бы ответ «да» (если формула общезначима) или «нет» (если не общезначима). Доказательство неразрешимости обычно проводится путём сведения к ней проблемы остановки машины Тьюринга или к проблеме разрешимости для диофантовых уравнений (десятая проблема Гильберта).

¶Частичная разрешимость

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

¶Разрешимые подклассы

Хотя общая проблема неразрешима, для некоторых подклассов формул логики предикатов существуют эффективные алгоритмы разрешимости. К таким подклассам относятся, например:

• Логика высказываний — проблема разрешимости для неё тривиально разрешима (например, методом таблиц истинности).
• Односортная логика предикатов с одноместными предикатами (без функциональных символов и равенства) — разрешима.
• Логика предикатов с конечными моделями — для каждого конечного размера модели проблема разрешима, но в целом для всех конечных моделей — неразрешима.
• Логика предикатов с ограниченной квантификацией (например, формулы с двумя кванторами) — разрешима для некоторых классов.

¶Связь с другими проблемами

¶Проблема остановки

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

¶Десятая проблема Гильберта

Десятая проблема Гильберта (1900) заключалась в нахождении общего метода для определения, имеет ли данное диофантово уравнение целочисленные решения. В 1970 году Ю. В. Матиясевич, опираясь на работы М. Дэвиса, Х. Патнема и Дж. Робинсон, доказал, что эта проблема алгоритмически неразрешима. Доказательство использует сведение к проблеме разрешимости для логики предикатов.

¶Теорема Райса

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

¶Практическое значение

Неразрешимость проблемы разрешимости имеет фундаментальные последствия для математики, информатики и философии. В частности:

• Автоматическое доказательство теорем — не существует алгоритма, который мог бы доказать или опровергнуть любое математическое утверждение. Однако существуют программы (например, Prover9, Vampire, E), которые успешно работают для многих практически важных классов формул, используя эвристики и ограничения.
• Проверка моделей (model checking) — в ограниченных формализмах (например, в темпоральной логике) проблема разрешимости может быть разрешима, что позволяет автоматически верифицировать программы и цифровые схемы.
• Теория баз данных — проблема разрешимости для логических запросов к базам данных (например, в реляционной алгебре) часто разрешима, но для более выразительных языков (например, с рекурсией) может быть неразрешима.
• Искусственный интеллект — системы, основанные на логическом выводе, сталкиваются с принципиальными ограничениями, вытекающими из неразрешимости.

¶Философские аспекты

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

¶Интересные факты

• Термин «Entscheidungsproblem» был введён Гильбертом в 1928 году, хотя сама проблема обсуждалась и ранее, в частности, в работах Г. Фреге и Б. Рассела.
• Доказательство Чёрча было опубликовано в 1936 году, а Тьюринга — в 1937 году. Тьюринг, узнав о работе Чёрча, добавил в свою статью приложение, в котором показал эквивалентность своих идей.
• В 1936 году А. Чёрч и С. Клини доказали, что проблема разрешимости для λ-исчисления также неразрешима.
• В 1950-х годах были найдены разрешимые подклассы логики предикатов, например, класс формул с двумя кванторами (так называемый «класс Бернайса-Шёнфинкеля»).
• В 1970-х годах была доказана неразрешимость проблемы разрешимости для логики предикатов с равенством и функциональными символами.

¶Источники

• Чёрч А. «Введение в математическую логику» (1944).
• Тьюринг А. «О вычислимых числах с приложением к проблеме разрешимости» (1936).
• Клини С. К. «Введение в метаматематику» (1952).
• Мендельсон Э. «Введение в математическую логику» (1964).
• Матиясевич Ю. В. «Десятая проблема Гильберта» (1993).
• Гёдель К. «О формально неразрешимых предложениях Principia Mathematica и родственных систем» (1931).