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

[Sonic86]

Как одновременно возможно, что исчисление предикатов полно, но неразрешимо?

С одной стороны, мы знаем, что исчисление предикатов (ИП) полно - любая общезначимая формула выводима из аксиом ИП.
С другой стороны, не ИП неразрешимо - не существует алгоритма, проверяющего истинность произвольной формулы ИП (даже предъявляется конкретная неразрешимая формула).
Возьмем теперь некоторую формулу $F$.
Если $F$ общезначима, то она выводима из аксиом ИП - можно устроить перебор всех выводов формул из аксиом ИП (упорядочить их по суммарной длине вывода, подстановки тоже перебирать).
Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$, и значит $\neg F$ можно вывести перебором всех выводов из аксиом ИП.
Теперь мы можем взять и построить алгоритм вывода $F$ и $\neg F$ параллельно. Поскольку либо $F$, либо $\neg F$ общезначима, то для одной из этих формул алгоритм перебора выводов найдет доказательство, а значит он всегда завершается на любой $F$ и, таким образом, дает алгоритм разрешимости $F$, которого не существует по теореме Черча

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

[mihaild]

Sonic86 в сообщении #1138723 писал(а):

Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$

Почему? Ни $\forall x P(x)$, ни $\neg \forall x P(x)$ не являются общезначимыми.

[Sonic86]

mihaild в сообщении #1138725 писал(а):

Sonic86 в сообщении #1138723 писал(а):

Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$

Почему? Ни $\forall x P(x)$, ни $\neg \forall x P(x)$ не являются общезначимыми.

Да, действительно, мог бы сам догадаться, спасибо

А если я возьму в качестве $F$ ту самую неразрешимую формулу? Она же общезначима? Или нет?
Или вообще буду брать только такие $F$, для которых либо $F$, либо $\neg F$ общезначимы? Тогда рассуждение сохраняется?

[mihaild]

Sonic86 в сообщении #1138728 писал(а):

А если я возьму в качестве $F$ ту самую неразрешимую формулу? Она же общезначима?

Нет, иначе она была бы выводима.

Sonic86 в сообщении #1138728 писал(а):

Или вообще буду брать только такие $F$, для которых либо $F$, либо $\neg F$ общезначимы? Тогда рассуждение сохраняется?

Вы получите, что множества общезначимых и тождественно ложных утверждений перечеслимы. Что вы хотите из этого получить?