6.5. ОБЩЕЗНАЧИМОСТЬ И ВЫПОЛНИМОСТЬ

Если некоторая п. п. формула имеет значение Т при всех интерпретациях, то ее называют общезначимой. Так, по таблице истинности п. п. формула при любой интерпретации имеет значение Т и, следовательно, она общезначима. С помощью таблиц истинности всегда можно определить, общезначима ли данная п. п. формула, не содержащая кванторов. Нужно просто проверить, имеет ли эта п. п. формула значение Т при всех возможных значениях (Т или F) содержащихся в ней атомных формул.

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

Можно установить общезначимость лишь некоторых типов формул, содержащих кванторы, и поэтому можно говорить о разрешимых подклассах исчисления предикатов. Более того, если некоторая п. п. формула на самом деле общезначима, то существует процедура для проверки ее общезначимости. (Та же процедура, примененная к п. п. формулам, не являющимся общезначимыми, может привести к неограниченной последовательности операций.) Поэтому исчисление предикатов можно назвать полуразрешимым.

Если при данной интерпретации каждая п. п. формула из некоторого множества п. п. формул имеет значение Т, то говорят, что данная интерпретация удовлетворяет этому множеству. Правильно построенная формула логически следует из некоторого множества формул, если каждая интерпретация, удовлетворяющая удовлетворяет также и Так, очевидно, что логически следует из логически следует из Менее очевидно, что логически следует из

Именно эту концепцию логического следования мы положим в основу понятия доказательства. Доказательством того, что некоторая п. п. формула логически вытекает из заданного множества правильно построенных формул, назовем демонстрацию того факта, что логически следует из Цель оставшихся глав — дать основы, по-видимому наиболее перспективного, механического метода поиска доказательства того, что данная п. п. формула логически следует из некоторого множества п. п. формул, и показать, как можно применить этот метод к решению задач.

Факт «неразрешимости» исчисления предикатов означает также, что при заданных произвольной п. п. формуле и произвольном множестве п. п. формул не существует эффективной процедуры, позволяющей всегда решить, следует ли логически из Если действительно следует из то существуют процедуры, которые в конце концов сообщат нам этот факт. Однако если не следует из то те же процедуры, к сожалению, не всегда могут это установить.

Тем не менее умение продемонстрировать, что логически следует из (когда это на самом деле так), уже достаточно полезно, и мы сосредоточим на нем свое внимание. Предположим, что логически следует из Тогда любая интерпретация, удовлетворяющая удовлетворяет также Но заметим

что эти интерпретации не удовлетворяют Следовательно, никакая интерпретации не удовлетворяет объединению и Если некоторое множества п. п. формул не удовлетворяется ни при какой интерпретации, то оно называется неудовлетворимым (или невыполнимым). Так, если логически следует из то объединение неудовлетворимо. Обратно, если неудовлетворимо, то должно логически следовать из

Мы используем этот результат для того, чтобы придать одинаковую форму всем задачам доказательства: для доказательства логического следования из мы будем показывать, что объединение неудовлетворимо. Для того чтобы показать, что некоторое множество п. п. формул неудовлетворимо, надо доказать, что нет такой интерпретации, при которой каждая из п. п. формул в этом множестве имеет значение Т. Хотя эта задача и кажется трудоемкой, существуют довольно эффективные процедуры ее решения. Для выполнения этих процедур требуется представить сначала п. п. формулы данного множества в специальном удобном виде — в виде предложений