Алгоритмически неразрешимые проблемы

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

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

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

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

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