К счастью, имеется знаменитая теорема, предложенная Жаком Эрбраном [650], согласно которой, если некоторое высказывание следует из первоначальной базы знаний в логике первого порядка, то существует доказательство, которое включает лишь конечное подмножество этой пропозиционализированной базы знаний. Поскольку любое такое подмножество имеет максимальную глубину вложения среди его базовых термов, это подмножество можно найти, формируя вначале все конкретизации с константными символами (Richard и John), затем все термы с глубиной 1 (Father (Richard) и Father (John)), после этого все термы с глубиной 2 и т.д. до тех пор, пока мы не сможем больше составить пропозициональное доказательство высказывания, которое следует из базы знаний.

Выше был кратко описан один из подходов к организации вывода в логике первого порядка с помощью пропозиционализации, который является полным, т.е. позволяет доказать любое высказывание, которое следует из базы знаний. Это — важное достижение, если учесть, что пространство возможных моделей является бесконечным. С другой стороны, до тех пор пока это доказательство не составлено, мы не знаем, следует ли данное высказывание из базы знаний! Что произойдет, если это высказывание из нее не следует? Можем ли мы это определить? Как оказалось, для логики первого порядка это действительно невозможно. Наша процедура доказательства может продолжаться и продолжаться, вырабатывая все более и более глубоко вложенные термы, а мы не будем знать, вошла ли она в безнадежный цикл или до получения доказательства остался только один шаг. Такая проблема весьма напоминает проблему останова машин Тьюринга. Алан Тьюринг [1518] и Алонсо Черч [255] доказали неизбежность такого состояния дел, хотя и весьма различными способами. Вопрос о следствии для логики первого порядка является полу разрешимым; это означает, что существуют алгоритмы, которые позволяют найти доказательство для любого высказывания, которое следует из базы знаний, но нет таких алгоритмов, которые позволяли бы также определить, что не существует доказательства для каждого высказывания, которое не следует из базы знаний.