Разрешимость логики первого порядка

[Ysan_Asanov]

Здравствуйте! Изучаю математическую логику и дошёл до теоремы Чёрча о неразрешимости логики первого порядка. Насколько я понимаю, теорема о полноте гарантирует нам алгоритм, который перечисляет множество истинных формул логики первого порядка. В таком случае, если мы хотим установить истинность или ложность замкнутой формулы $A$, то мы запускаем этот алгоритм на формуле $A$ и параллельно на формуле $\neg A$. Один из этих алгоритмов обязательно закончит работу и после этого результатом работы "разрешающего" алгоритма будет 0 или 1 исходя из того, какой алгоритм закончил работу. То есть таким образом мы получаем алгоритм, который логику первого порядка "разрешает". Где ошибка?

[mihaild]

Ysan_Asanov в сообщении #1568567 писал(а):

теорема о полноте гарантирует нам алгоритм, который перечисляет множество истинных формул логики первого порядка

Не истинных, а общезначимых (истинных в любой модели; истинность формулы всегда в какой-то модели, а не вообще).

[warlock66613]

Ysan_Asanov в сообщении #1568567 писал(а):

Один из этих алгоритмов обязательно закончит работу

С учётом сказанного выше mihaild вот это совсем не обязательно.

[Ysan_Asanov]

Большое спасибо