Приведённая и предварённая нормальные формы

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

С помощью известных основных равносильностей (A ® B) º ( Ú B) и (A « B) º ((A Ù B) Ú ( Ù )) в произвольной формуле исчисления предикатов можно избавиться от всех логических связок ® и « . Затем, по законам де Моргана , правилу двойного отрицания º A и равносильностям с кванторами º ($ x (x, y)), º (" x (x, y)) можно переработать все “длинные” отрицания (т.е. отрицания, стоящие над формулами, не являющимися пропозициональными переменными и предикатными символами) в “короткие”, добившись, чтобы отрицания стояли только над пропозициональными переменными или над предикатными символами.

Полученный вид формулы называется приведённым или приведённой формой (ПФ) . Таким образом, доказана следующая

Теорема (о ПФ). Любая формула исчисления предикатов равносильна некоторой приведённой форме.

Примеры: 1. (" x ($ y (P(y) ® Q(x)))) º (" x ($ y ( (y)Ú Q(x)))) – ПФ.

2. ) º

º (" y (($ x P(x)) Ù (x, y))) – ПФ.

3. º

º º

º – ПФ.

Говорят, что формула исчисления предикатов находится в предварённой нормальной форме (ПНФ), если она либо не содержит кванторов, либо имеет следующий вид: Q₁ x₁ (Q₂ x₂ (… (Q_n x_n Ф(x₁ , … , x_n )))…), где Q_i – один из кванторов " или $ (1 £ i £ n), формула Ф бескванторная и может зависеть от других переменных, кроме x₁ , … , x_n . Иными словами, кванторы в ПНФ предшествуют её бескванторной подформуле Ф и область действия каждого квантора распространяется до конца формулы (не учитывая закрывающие скобки).

Если формула является ПНФ и приведена, то говорят, что она находится в предварённой приведённой нормальной форме (ППНФ) .

Примеры: 1.(P(x) Ù Q(y)) – бескванторная формула в ПНФ и ППНФ.

2. (" x ($ y (P(y) ® Q(x)))) – ПНФ, но не ППНФ.

3. (" x (($ y P(y)) ® Q(x))) – не ПНФ, т.к. область действия квантора $ распространяется только на P(x), а не до конца формулы.

4.(P(z, y) Ú (" x Q(x))) – не ПНФ, т.к. квантор " не предшествует подформуле P(z, y).

Теорема (о ППНФ). Любая формула исчисления предикатов равносильна некоторой предварённой приведённой нормальной форме.

Доказательство. Будем исследовать формулы в процессе их создания по правилам образования формул (Ф1)-(Ф5) и приводить их к ППНФ.

Во-первых, любая бескванторная формула сама находится в ПНФ и равносильна некоторой приведённой форме ввиду предыдущей теоремы. Таким образом, любая формула, возникшая по правилам (Ф1), (Ф2), обладает ППНФ.

Во-вторых, если для формул A и B уже найдены равносильные им ППНФ:

A º Q₁ x₁ (Q₂ x₂ (… (Q_n x_n C(x₁ , … , x_n ))…)),

B º R₁ y₁ (R₂ y₂ (… (R_m y_m D(y₁ , … , y_m ))…)) = Y ,

где Q_i , R_j – один из кванторов " или $ (1 £ i £ n, 1£ j £ m), то (как уже отмечалось выше) связанные переменные в этих формулах можно переобозначить уникальными буквами так, чтобы в формуле для А не было одинаковых связанных переменных с формулой для B и чтобы все связанные переменные отличались от свободных.Найдём ППНФ, равносильную формулам , (A Ù B), (A Ú B), (A ® B), (A « B).

Для воспользуемся равносильностями (2), теоремы об основных равносильностях с кванторами:

где – кванторы, противоположные кванторам Q_i (1 £ i £ n). Последняя формула в этой цепочке – ПНФ – является искомой. Остаётся привести её к приведённому виду, избавившись от “длинных” отрицаний в бескванторной формуле. Таким образом, обладает равносильной ППНФ.

Для остальных формул вида (A w B), где w Î {Ù , Ú } рассуждения однотипны и используют равносильности (5), (6) теоремы об основных равносильностях с кванторами (следует учесть, что все связанные переменные уникальны, так что условия для применения равносильностей (5), (6) выполнены): (А w B) º

º ((Q₁ x₁ (…(Q_n x_n С(x₁ , … , x_n ))…)) w (R₁ y₁ (…(R_m y_m D(y₁ , … , y_m ))…))) =

= ((Q₁ x₁ (Q₂ x₂ (… (Q_n x_n С)…))) w Y ) º (Q₁ x₁ ((Q₂ x₂ (… (Q_n x_n С))…)) w Y )) º

º (Q₁ x₁ (Q₂ x₂ ((… (Q_n x_n С)…)) w Y ))) º …

… º (Q₁ x₁ (Q₂ x₂ (…(Q_n x_n (С w Y ))…))) º (Q₁ x₁ (Q₂ x₂ (…(Q_n x_n (Y w С))…))) º

º (Q₁ x₁ (Q₂ x₂ (… (Q_n x_n ((R₁ y₁ (R₂ y₂ (… (R_m y_m D)…))) w С))…))) º

º (Q₁ x₁ (Q₂ x₂ (… (Q_n x_n (R₁ y₁ ((R₂ y₂ (… (R_m y_m D)…)) w С)))…))) º

º (Q₁ x₁ (Q₂ x₂ (… (Q_n x_n (R₁ y₁ (R₂ y₂ ((… (R_m y_m D)…) w С))))…))) º …

… º (Q₁ x₁ (Q₂ x₂ (…(Q_n x_n (R₁ y₁ (R₂ y₂ (…(R_m y_m (D w С))…))))…))),

и последняя формула является ППНФ.

Связки ® и « выражаются через Ù , Ú , , так что для формул вида (A ® B) и (A « B) существование ППНФ следует из предыдущего.

Таким образом, все формулы, полученные по правилу (Ф3) образования формул, обладают ППНФ.

Наконец, если A(x) – формула со свободной переменной x, которая уже равносильна некоторой ППНФ:

A(x) º (Q₁ x₁ (Q₂ x₂ (… (Q_n x_n C(x, x₁ , … , x_n ))…))),

где Q_i (1 £ i £ n) – один из кванторов " или $ , то формула (Q x A(x)), очевидно, равносильна формуле (Q x (Q₁ x₁ (Q₂ x₂ (… (Q_n x_n C(x, x₁ , … , x_n ))…)))) – ППНФ. Таким образом, любая формула обладает равносильной ППНФ.

Теорема доказана.

Примеры: 1. (" x (($ y P(y))® Q(y, x))) º (" x ( Ú Q(y, x))) º

º (" x ((" y (y))Ú Q(y, x))) º (" x ((" z (z))Ú Q(y, x))) º

º (" x (" z ( (z)Ú Q(y, x)))) – ППНФ.

2. (P(u, y) Ù (" y Q(y))) º (P(u, y) Ù (" z Q(z))) º

º ((" z Q(z)) Ù P(u, y)) º (" z (Q(z) Ù P(u, y))) – ППНФ.

3. (($ x R(x, y, z)) ® ) º (($ x R(x, y, z)) ® ($ x (x, y))) º

º ( Ú ($ t (t, y))) º ((" x (x, y, z)) Ú ($ t (t, y))) º

º (" x ( (x, y, z) Ú ($ t (t, y)))) º (" x ($ t ( (x, y, z) Ú (t, y)))) – ППНФ.

4. ((" x P(x, y)) Ú (($ x P(x, x)) ® (" z ))) º

º ((" x P(x, y)) Ú (($ x P(x, x)) ® (" z ))) º

º ((" x P(x, y)) Ú (($ x P(x, x)) ® (" z (Q(y, z) Ù )))) º

º ((" x P(x, y)) Ú (($ x P(x, x)) ® (" z (Q(y, z) Ù (" x (x, z)))))) º

º ((" x P(x, y)) Ú (($ u P(u, u)) ® (" z (Q(y, z) Ù (" v (v, z)))))) º

º ((" x P(x, y)) Ú (($ u P(u, u)) ® (" z (" v (Q(y, z) Ù (v, z)))))) º

º ((" x P(x, y)) Ú ((" u (u, u)) Ú (" z (" v (Q(y, z) Ù (v, z)))))) º

º ((" x P(x, y)) Ú (" z ((" u (u, u)) Ú (" v (Q(y, z) Ù (v, z)))))) º

º ((" x P(x, y)) Ú (" z (" v ((" u (u, u)) Ú (Q(y, z) Ù (v, z)))))) º

º ((" x P(x, y)) Ú (" z (" v (" u ( (u, u) Ú (Q(y, z) Ù (v, z))))))) º

º (" z ((" x P(x, y)) Ú (" v (" u ( (u, u) Ú (Q(y, z) Ù (v, z))))))) º

º (" z (" v ((" x P(x, y)) Ú (" u ( (u, u) Ú (Q(y, z) Ù (v, z))))))) º

º (" z (" v (" u ((" x P(x, y)) Ú ( (u, u) Ú (Q(y, z) Ù (v, z))))))) º

º (" z (" v (" u (" x (P(x, y) Ú ( (u, u) Ú (Q(y, z) Ù (v, z)))))))) – ППНФ.