Нормальные формы для формул алгебры предикатов

Формула исчисления предикатов Φ находится в пренексной (соответственно, предклазуальной) нормальной форме (сокращенно ПНФ и ПкНФ), если она имеет вид

,

где – некоторые кванторы и Y – бескванторная формула, находящейся в ДНФ (соответственно, КНФ). При этом последовательность кванторов называется кванторной приставкой и формула Y называется дизъюнктивным (соответственно, конъюнктивным) ядром формулы Φ.

Теорема 1. Любая формула исчисления предикатов логически эквивалентна формуле , находящейся в ПНФ (соответственно, ПкНФ).

Такая формула называется пренексной нормальной формой (сокращенно ПНФ) формулы (соответственно, предклазуальной нормальной формой (сокращенно ПкНФ) формулы ).

Пусть замкнутая формула исчисления предикатов Φ находится в ПкНФ:

,

где – некоторые кванторы и – конъюнктивное ядроформулы Φ, т.е. бескванторная формула со свободными переменными , находящаяся в КНФ. Пусть квантор для некоторого являетсяпервым в формулеΦ квантором существования.

В частности, если первый квантор являетсяквантором существования, то в формулеΦ нет предшествующих ему кванторов общности.

Предположим, что r>1. Тогда с помощью обозначения

формула Φ представляется в виде:

,

где – формуласо свободными переменными .

Тогда выполнимость формулы Φ в интерпретации M равносильна выполнимости в интерпретации M формулы

с соответствующей интерпретацией в M нового функционального символа f арности r-1.

В случае r=1 формула можетзависеть только от свободной переменной и выполнимость формулы Φ в интерпретации M равносильна выполнимости в интерпретации M формулы с соответствующей интерпретацией в M нового предметного символа c.

Аналогичным образом в кванторной приставке формуле Φ можно удалить любой квантор существования для по следующему правилу:

1) если левее квантора существованиявформуле Φ не стоит никакой квантор общности, то выбираем новый предметный символ c, заменяем этим символом c все вхождения переменной x_s в конъюнктивное ядроформулы Φ и вычеркиваем из кванторной приставки формулы Φ;

2) если же левее квантора существованиястоят кванторы общности

для значений , то выбираем новый m-арный функциональный символ f, заменяем все вхождения переменной x_s в конъюнктивное ядроформулы Φ выражением и вычеркиваем из кванторной приставки формулы Φ.

В результате такой замены всех кванторов существования в формуле Φ получим замкнутую ПкНФ ,кванторная приставка которой получается из кванторной приставки формулы Φ удалением всех кванторов существованияи которая содержит новые символы – функциональные или предметные.

При этом формула Φ выполнима или противоречива одновременно с формулой .

Рассмотренный прием удаления квантора существования был введен Скулемом и называется скулемизацией формул. Вводимые в процессе скулемизации новые функциональные и предметные символы называются функторами Скулема или скулемовскими функциями.

Полученную в результате скулемизации замкнутую ПкНФ называют скулемовской стандартной формой (сокращенно ССФ) или клазуальной нормальной формой (сокращенно КлНФ).

Теорема 1. Любая замкнутая формула исчисления предикатов эффективно преобразуется (с помощью некоторого алгоритма) в логически эквивалентную ей формулу , находящуюся в клазуальной нормальной форме, которая называется скулемовской стандартной формой или клазуальной нормальной формой (сокращенно ССФ или КлНФ) формулы Φ.

При этом формула Φ выполнима или противоречива одновременно с ее КлНФ.

Пример. Как показано в предыдущем примере, замкнутая формула

имеет ПкНФ

,

результатом скулемизации которой является формула

с новым предметным символом c.

Значит, является КлНФ формулы .

Метод Эрбрана

По предыдущей теореме противоречивость замкнутой формулы исчисления предикатов Φ равносильна противоречивости ее скулемовской стандартной формы , которая является универсально замкнутой формулой

с конъюнктивным ядром ,где –некоторые дизъюнкты исчисления предикатов.

С другой стороны, по теореме полноты, формула противоречива в том и только том случае, если она невыполнима.

Так как кванторы общности проносятся через конъюнкции, то формула представляется в виде:

=

=

и, значит, ее невыполнимость равносильна невыполнимости множества универсальных замыканий

формул из множества дизъюнктов .

Невозможно рассмотреть все интерпретации множества формул S на всех областях интерпретации, так как множество таких областей интерпретации бесконечно.

Однако Эрбран показал, что при доказательстве невыполнимости такого множества формул S можно ограничиться рассмотрением интерпретаций в одной специальной области интерпретации, которая называется эрбрановским универсумом.

Пусть – множество всех предметных символов и – множество всех функциональных символов, встречающихся в формулах множества S.

На первом шаге индукции для множества S определяется множество констант нулевого уровня H₀ по правилу:

, если Æ, и для одного нового постоянного символа a, если Æ.

Затем для каждого натурального значения определяется множество констант i-го уровня H_i как множество всех выражений вида

,

где и f – n-арный функциональный символ из множества .

Объединение всех множеств H_i называется эрбрановским универсумом множества S и обозначается .

Примеры. 1. Для множества дизъюнктов

эрбрановский универсум

.

2. Для множества дизъюнктов

эрбрановский универсум

На множестве естественно определяется алгебра сигнатуры по правилу:

для каждого n-арного функционального символа f из множества и любых термов значение – есть терм из множества .

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

Интерпретацией каждого n-арного предикатного символа P, встречающегося в формулах множества S является некоторое n-арное отношение на эрбрановском универсуме .

Символически такие отношения могут быть заданы перечислением атомарных формул:

.

Множество всех атомарных формул с термами из и предикатными символами, встречающимися в формулах множества S, называется эрбрановским базисом и обозначается символом B.

Базис B является счетным множеством:

.

Интерпретация b_P предикатных символов из формул множества S естественно задается в виде множества литер:

,

где , если атомарная формула истинна в интерпретации b, и , если атомарная формула ложна в интерпретации b.

Интерпретации b множества формул S в называются H-интерпретациями, если:

1) для каждого предметного символа c, встречающегося в формулах множества S, выполняется равенство: ;

2) для каждого n-арного функционального символа f , встречающегося в формулах множества S, соответствующая n-арная операция на множестве удовлетворяет условию: при любых ;

3) для некоторого наперед заданного множества литер интерпретация каждого n-арного предикатного символа P, встречающегося в формулах множества S, определяется как n-арное отношение на множестве по формуле:

– элемент .

Пример. Для множества дизъюнктов

эрбрановский универсум имеет вид:

.

Значит, эрбрановский базис имеет вид:

.

Теорема. Множество дизъюнктов S невыполнимо в том и только том случае, если множество S ложно при всех его H-интерпретациях.

Таким образом, при доказательстве невыполнимости множества дизъюнктов S можно ограничиться рассмотрением его H-интерпретаций.

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

Теорема Эрбрана.

Пусть – замкнутая формула с конъюнктивным ядром и – эрбрановский универсум множества дизъюнктов S формулы . Тогда формула Φ невыполнима в том и только том случае, если для некоторого конечного набора термов невыполнима конъюнкция формул

.

Не нашли, что искали? Воспользуйтесь поиском по сайту: