Проблема разрешения как один из вопросов математической логики

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

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

Сегодня, общая формулировка проблемы разрешения представляет собой совокупность класса методов F и  класса проблем P, возможность решения каждой из проблем одним общим методом f∊F (методом разрешения) и является сутью проблемы разрешения.

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

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

• построение модели любой непротиворечивой классической теории неразрешимо однозначно определенными (без аксиомы выбора) теоретико-множественными функционалами;
• проверка истинности арифметических формул или (соответствия) программ их спецификации - неразрешима с помощью формальных теорий с алгоритмически заданным множеством аксиом;
• проверка доказуемости в формальной арифметике или в классической логике предикатов - алгоритмически неразрешима;
• задача нормализации выводов в логике предикатов - неразрешима примитивно-рекурсивными алгоритмами;
• проверка тавтологичности формул классической логики высказываний - переборно разрешимая, но неразрешима менее чем переборными алгоритмами [2].

Задача разрешимости в пропозициональной логике решается  при помощи таблицы истинности. Например, построение таблицы истинности для пропозициональной формулы и проверка основного столбца на отсутствие значения "false - ложь" - алгоритм, решающий проблему разрешения классической логики высказываний; множество простых натуральных чисел (числа записываются, например, в десятичной системе счисления; число называется простым, если оно является натуральным числом, большим или равным 2, имеющим только два натуральных делителя — себя и 1) и соответствующая задача нахождения простоты натурального числа разрешима алгоритмом перебора возможных делителей .

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

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

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