Т. А. Сливина математическая логика и теория алгоритмов

§ 7. Неразрешимые алгоритмические проблемы (обзор)
Переход от интуитивного понятия алгоритма к точному понятию машины Тьюринга позволяет уточнить и вопрос об алгоритмической разрешимости данной массовой проблемы. Теперь этот вопрос можно сформулировать так: существует ли машина Тьюринга, решающая данную массовую проблему или же такой машины не существует?
На этот вопрос теория алгоритмов в ряде случаев дает отрицательный ответ. Один из первых результатов такого типа получен американским математиком Чёрчем в 1936 году. Он касается проблемы распознавания выводимости в математической логике.
1.Неразрешимость проблемы распознавания выводимости в математической логике.
Как известно, аксиоматический метод в математике заключается в том, что все предложения (теоремы) данной теории получаются посредством формально-логического вывода из нескольких предложений (аксиом), принимаемых в данной теории без доказательства.
В математической логике описывается специальный язык формул, позволяющий любое предложение математической теории записать в виде вполне определенной формулы, а процесс логического вывода из посылки А следствия B может быть описан в виде процесса формальных преобразований исходной формулы. Это достигается путем использования логического исчисления, в котором указана система допустимых преобразований, изображающих элементарные акты логического умозаключения, из которых складывается любой, как угодно сложный формально-логический вывод.
Вопрос о логической выводимости предложения В из посылки А в избранном логическом исчислении является вопросом о существовании дедуктивной цепочки, ведущей от формулы А к формуле В.
В связи с этим возникает проблема распознавания выводимости: для любых двух формул А и В в логическом исчислении узнать, существует ли дедуктивная цепочка, ведущая от А к В, или нет.
Решение этой проблемы понимается в смысле вопроса о существовании алгоритма, дающего ответ при любых А и В. Результат Чёрча формулируется следующим образом: