5.7 Эквивалентные соотношения. Префиксная нормальная форма

Формулы называются эквивалентными, если при любых подстановках констант они принимают одинаковые значе­ния. В частности, все ТИ-формулы (тождественно-истинные формулы) (и все ТЛ-формулы) эк­вивалентны. Если формулы F1и F2 эквивалентны, F1 ~ F2 - ТИ-формулы.

Множество ТИ-формул логики предикатов входит в лю­бую теорию, исследование этого множества - важная цель логики предикатов. При этом выделяются две проблемы:

1) получение ТИ-формул (проблема построения порож­дающей процедуры для множества ТИ-формул);

2) проверка формулы на истинность (проблеморазреша­ющей процедуры).

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

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

˥х Р(х) ~x ˥P(x). (5.3)

˥x P(x) ~ x ˥Р(х). (5.4)

x (P₁(x) & Р₂(х)) ~ (x P₁(x) & x P₂ (х)). (5.5)

x (P₁(x) v Р₂(х)) ~ (х P₁(x) v х Р₂(х)) (5.6)

x y Р(х, у) ~ y x P(x, у). (5.7)

х у Р(х, у) ~ух Р(х, у). (5.8)

x(P(x) & Y) ~ (x P(x) & Y). (5.9)

x(P(x) v Y) ~ (x P(x) v Y). (5.10)

х(Р(х) & Y) ~ (х P(х) & Y). (5.11)

х(Р(х) v Y) ~ (x P(x) v Y). (5.12)

Используя соотношения (5.3), (5.4), можно выразить один квантор через другой. Соотношения (5.5) и (5.6) показыва­ют дистрибутивность квантора общности x относительно конъюнкции & и квантора существования х относитель­но дизъюнкции v. Если в этих выражениях поменять мес­тами кванторы x и х, то получим соотношения, верные лишь в одну сторону:

x (P₁(x) & Р₂(х)) → (х P₁(x) & х Р₂(х));

(x P₁(x) v x Р₂(х)) → x(P₁(x) v Р₂(х))

Поэтому в таких случаях эквивалентных преобразований применяют переименование переменной х в одном из пре­дикатов на новую переменную:

(х P₁(x) & y Р₂(y)) ~ хy (P₁(x) & Р₂(y))

(x P₁(x) v y Р₂(y)) → x y (P₁(x) v Р₂(y))

Соотношения (5.7), (5.8) отражают в некотором смысле коммутативность одноименных кванторов (возможность ме­нять местами одноименные кванторы), что несправедливо для разноименных кванторов, например x у Р(х, у)и уx P(x, у) не эквивалентны. Соотношения (5.9) - (5.12) по­зволяют формулу, не содержащую переменную х, выносить за пределы действия квантора, связывающего эту перемен­ную. Указанных соотношений (5.3) - (5.12), а также эквива­лентных соотношений логики (алгебры) высказываний дос­таточно для выполнения преобразований формул логики (ал­гебры) предикатов.

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

Префиксной нормальной формой (ПНФ) называется фор­мула, имеющая вид:

Q₁ x₁ Q₂ x₂ … Q_n x_n F

где Q₁ x₁, Q₂ x₂,…, Q_n x_n - кванторы; F-формула, не имею­щая кванторов, с операциями {&, v, ˥}. В логике предика­тов для любой формулы существует эквивалентная ей пре­фиксная нормальная форма.

Процедура получения ПНФ:

1. Используя формулы

Р₁ ~ Р₂ = (Р₁ → Р₂) & (Р₂ → Р₁), (5.13) Р₁ → Р₂ = ˥Р₁ v Р₂, (5.14)

заменить операции ->, ~ на &, v, ˥.

2. Воспользовавшись выражениями (5.3), (5.4), а также правилом двойного отрицания и правилами де Моргана,

˥˥P = P (5.15)

˥(Р₁vР₂) = ˥Р₁&˥Р₂ (5.16) ˥ (Р₁ & Р₂ ) = ˥Р₁ v ˥Р₂ (5.17)

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

3. Для формул, содержащих подформулы вида

x Р₁ (х) v x Р₂ (х), х Р₁ (х) & х Р₂ (х),

ввести новые переменные, позволяющие использовать соот­ношения (5.9)- (5.12).

4. С помощью формул (5.5) - (5.12) получить формулы в виде ПНФ.