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

.
Если

общезначима, то она выводима из аксиом ИП - можно устроить перебор всех выводов формул из аксиом ИП (упорядочить их по суммарной длине вывода, подстановки тоже перебирать).
Если же

не общезначима, значит общезначимо ее отрицание

, и значит

можно вывести перебором всех выводов из аксиом ИП.
Теперь мы можем взять и построить алгоритм вывода

и

параллельно. Поскольку либо

, либо

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

и, таким образом, дает алгоритм разрешимости

, которого не существует по теореме Черча

Где я ошибаюсь?
Я не смогу перебрать счетное число переменных в правилах постановки?