6.6. ПРЕДЛОЖЕНИЯ

Любую п. п. формулу исчисления предикатов можно представить в виде предложения, применяя к ней последовательность простых операций. Наша ближайшая задача состоит в том, чтобы показать, как придать произвольной п. п. формуле форму предложения. Мы будем иллюстрировать этот процесс на п. п. формуле

Процесс состоит из следующих этапов:

1) Исключение знаков импликации. В форме предложения в исчислении предикатов явно используются лишь связки V и Знак импликации можно исключить подстановкой в исходном утверждении вместо Такая подстановка в нашем примере дает

2) Уменьшение области действия знаков отрицания. Мы хотим, чтобы знак отрицания применялся не более чем к одной предикатной букве. С помощью повторного применения указанных ниже подстановок можно свести область действия каждого знака до отдельной предикатной буквы:

Тогда наша п. п. формула примет сначала вид

а потом

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

4) Исключение кванторов существования. Рассмотрим правильно построенную формулу

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

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

Так, исключая из п. п. формулы

получаем

Если исключаемый квантор существования не принадлежит области действия ни одного из кванторов всеобщности, то функция Сколема не содержит аргументов, т. е. является просто константой. Так, превращается в где а— константа, про которую мы знаем, что она «существует».

Чтобы исключить все переменные, относящиеся к кванторам существования, надо применить описанную выше процедуру по очереди, к каждой переменной. В нашем примере исключение кванторов существования (здесь лишь один такой квантор) дает

где функция Сколема.

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

6) Приведение матрицы к конъюнктивной нормальной форме. Любую матрицу можно представить в виде конъюнкции конечного множества дизъюнкций предикатов и (или) их отрицаний.

Говорят, что такая матрица имеет конъюнктивную нормальную форму. Дадим примеры матриц в конъюнктивной нормальной форме:

Любую матрицу можно привести в конъюнктивную нормальную форму, применяя несколько раз правило:

После приведения матрицы нашей п. п. формулы в конъюнктивную нормальную форму она принимает вид

7) Исключение кванторов всеобщности. Так как все переменные п. п. формулы должны быть связанными, то все оставшиеся на этом этапе переменные относятся к кванторам всеобщности. Так как порядок расположения кванторов всеобщности несуществен, то можно эти кванторы явным образом не указывать, условившись, что все переменные в матрице относятся к кванторам всеобщности. Теперь у нас остается лишь матрица в конъюнктивной нормальной форме.

8) Исключение связок «и». Теперь можно исключить знак «и» А, заменяя двумя п.п. формулами А, В. Результатом многократной замены будет конечное множество п. п. формул, каждая из которых представляет собой дизъюнкцию атомных формул и (или) их отрицаний. Атомную формулу или ее отрицание называют литералом, а правильно построенную формулу, состоящую лишь из дизъюнкций литералов, — предложением. Итак, каждая п. п. формула в нашем множестве будет лредложением.

Наша п. п. формула теперь представлена в виде следующих предложений:

Заметим, что в литералах предложения могут содержаться переменные, которые всегда следует считать относящимися к кванторам всеобщности. Если вместо переменных литерала

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

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