Алгоритм приведения к сколемовской нормальной форме

Шаги 1 – 3 – те же, что и в предыдущем алгоритме.

Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме (алгоритм описан в §5 главы 1).

Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага мы получили формулу

F = (∃ x)(∀ y)(∃ z)(∀ u)(∃ v) H (x, y, z, u, v), где H – не содержит кванторов. Предположим, что она не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле H заменим x на c, z – на f (y), v заменим на g (y, u). Все кванторы существования вычеркнем. Получим формулу

G = (∀ y)(∀ u) H (c, y, f (y), u, g (y, u)). Это и есть результат выполнения шага 5.

Пример 2. Приведем пример приведения к СНФ. Пусть

F = (∃ x)(∀ y)[ P (x, y) → (∃ z)(Q (x, z) & R (y))].

 Применяя законы 20 и 23, получаем формулу

F ₁ = (∃ x)(∀ y)(∃ z)[ P (x, y) ∨ (Q (x, z) & R (y))].

Она имеет предваренную нормальную форму. Используя закон 12, приводим бескванторную часть к КНФ:

F ₂ = (∃ x)(∀ y)(∃ z)[(P (x, y) ∨ Q (x, z)) & & (P (x, y) ∨ R (y))].

Сделав подстановку x = a, z = f (y), получим искомую формулу

G = (∀ y)[(P (a, y) ∨ Q (a, f (y))) & (P (a, y) ∨ R (y))].  

Теорема 2.4. Для всякой формулы F существует формула G, имеющая сколемовскую нормальную форму и одновременно с F выполнимая или невыполнимая.

Доказательство. Пусть G – результат работы алгоритма приведения к СНФ. То, что результатом работы алгоритма является формула в сколемовской нормальной форме, ясно из описания алгоритма. Формула, которая получается после выполнения шагов 1–4, равносильна исходной, и, в частности, одновременно с ней выполнима или невыполнима.

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

E (u ₁, …, u_n) = (∃ y) E ^/(y, u ₁, …, u_n).

(Формула E ^/ может содержать кванторы.) Рассмотрим интерпретацию ϕ с областью M, при которой формула E выполнима. Выполнимость означает, что найдутся элементы а₁, …, a_n ∈ M такие, что высказывание (ϕ E)(a ₁, …, a_n) или (что тоже самое) высказывание (∃ y)(ϕ E ^/)(y, a ₁, …, a_n) истинно. Отсюда следует, что существует элемент b ∈ M такой, что высказывание (ϕ E ^/)(b, a ₁, …, a_n) также истинно. Исключение квантора существования по y на пятом шаге приводит к формуле D (u ₁, …, u_n) = E ^/(c, u ₁, …, u_n), где c – константа, отсутствующая в E ^/. Расмотрим интерпретацию ψ, которая совпадает с ϕ на всех символах предикатов и функций, входящих в запись формулы F, и ψ(c) = b. Тогда

(ψ D)(a ₁, …, a_n) = (ϕ E ^/)(b, a ₁, …, a_n). Мы доказали, что если формула E выполнима, то выполнима и формула D. Предположим теперь, что выполнима формула D (u ₁, …, u_n) = E ^/(c, u ₁, …, u_n).

Это означает, что существует интерпретация ψ с областью M и элементы а₁, …, a_n ∈ M такие, что высказывание (ψ E ^/)(ψ(c), a ₁, …, a_n) истинно. Но отсюда следует истинность высказывания (∃ y)(ψ E ^/)(y, a ₁, …, a_n). Следовательно, формула E (u ₁, …, u_n) выполнима. Мы доказали, что из выполнимости формулы D следует выполнимость формулы E.

Рассмотрим теперь случай, когда исключается квантор существования, впереди которого есть k кванторов общности, т.е.

E (u ₁, …, u_n) = (∀ x ₁)…(∀ x_k)(∃ y) E ^/(x ₁, …, x_k, y, u _{1, …}, u_n).

(Формула E ^/ может содержать кванторы.) Исключение квантора по у на шаге 5 приведет к формуле D (u ₁, …, u_n) =

 (∀ x ₁)…(∀ x_k) E (x ₁, …, x_k, f (x ₁, …, x_k), u ₁, …, u_n), где f – символ k -местной функции, не содержащийся в E. Предположим, что формула E выполнима. Выполнимость означает существование интерпретации ϕ с областью M и элементов a ₁, …, a_n ∈ M таких, что высказывание (ϕ E)(a ₁, …, a_n) истинно. Истинность этого высказывания означает, что для любых элементов x ₁, …, x_k ∈ M найдется элемент y ∈ M такой, что высказывание E ^/(x ₁, …, x_k, y, a ₁, …, a_n) истинно. Если для данных элементов x ₁, …, x_k таких элементов y несколько, то зафиксируем один. Тем самым мы определили на M функцию i: Mx … xM → M такую, что высказывание 

(ϕ E ^/)(x ₁, …, x_k, i (x ₁, …, x_k), a ₁, …, a_n) истинно для всех x ₁, …, x_k ∈ M. Рассмотрим интерпрета-

цию ψ, которая совпадает с ϕ на всех символах функций и предикатов, входящих в запись формулы Е, и (ψ f)(x ₁, …, x_n)

= i (x ₁, …, x_n). Тогда 

(ψ D)(a ₁, …, a_n) =

(∀ x ₁)…(∀ x_k)(ϕ E ^/)(x ₁, …, x_k, i (x ₁, …, x_k), a ₁, …, a _n).

Последнее высказывание, как мы видели истинно. Следовательно, формула D (u ₁, …, u_n) выполнима. Мы показали, что из выполнимости формулы E следует выполнимость формулы D.

Пусть выполнима формула D. Это означает, что существует интерпретация ψ с областью M и элементы a ₁, …, a_n ∈ M такие, что высказывание (ψ D)(a ₁, …, a_n) или (что то же самое) высказывание

(∀ x ₁)…(∀ x_k)(ψ E ^/)(x ₁, …, x_k, (ψ f)(x ₁, …, x_k), a ₁, …, a_n) истинно. Отсюда следует, что для любых x ₁, …, x_k найдется y (равный (ϕ f)(x ₁, …, x_k)) такой, что высказывание

(ψ E ^/)(x ₁, …, x_k, y, a ₁, …, a_n)

истинно. Следовательно, истинно высказывание

(∀ x ₁)…(∀ x_k)(∃ y)(ψ E ^/)(x ₁, …, x_k, y, a ₁, …, a_n),

т.е. высказывание (ψ E)(a ₁, …, a_n). Мы доказали, что из выполнимости формулы D следует выполнимость формулы E.