7. Нормальные формы

Как и в логике высказываний, в логике первого порядка вводятся нормальные формы. Мы рассмотрим две из них: предваренную нормальную и сколемовскую нормальную формы.

Определение. Формула G имеет предваренную нормальную форму (сокращенно: ПНФ), если G(Q₁,x₁)…(Q_n,x_n)H, где Q₁,…,Q_n кванторы, а формула H не содержит кванторов.

Например, формула (x)(y)(P(x,y)&Q(y)) имеет предваренную нормальную форму, а формула (x)(T(x)&S(x,y)) не имеет.

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

Доказательство теоремы легко следует из анализа алгоритма приведения к ПНФ.

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

Шаг 1. Используя законы 21 и 20, исключить эквиваленцию и импликацию.

Шаг 2. Занести отрицание к атомарным формулам, пользуясь законами 17-19 и 26-27.

Шаг 3. С помощью законов 22-23, 28-31 вынести кванторы вперед, используя при необходимости переименование связанных переменных (законы 32-33).

Рассмотрим пример. Пусть F=(x)P(x)(y)(z)(P(y)&Q(y,z)).

Выполнив шаг 1 (с помощью закона 20), получим формулу F₁=(x)P(x)(y)(z)(P(y)&Q(y,z)).

С помощью закона 26 перейдем к формуле F₂=(x)P(x)(y)(z)(P(y)&Q(y,z)).

Тем самым, шаг 2 также выполнен. Применим закон 30 слева направо Q₁=, Q₂=, u=y, получим формулу F₃=(x)(y)[P(x)(z)(P(y)Q(y,z))].

(Пользуемся тем, что P(x) не содержит y, а (z)(P(y)&Q(Y,z)) не содержит х. Так как формула P(x) не содержит z, то применение закона 26 слева направо дает формулу F₄=(x)(y)(z)[P(x)(P(y)&Q(y,z))].

Это и есть искомая формула, имеющая ПНФ и равносильная формуле F.

В предыдущем примере выполнение шага 3 можно организовать по-другому. В формуле F₂ связанную переменную y заменим на переменную х (закон 33), получим формулу F₃^=(x)P(x)(x)(z)(P(x)&Q(x,z)).

Используя закон 23, перейдем к формуле F₄^=(x)[P(x)(z)(P(x)&Q(x,z))].

Затем, как и в предыдущем абзаце, с помощью закона 28 вынесем квантор по z за квадратную скобку. Получим формулу F₅^=(z)(z)[P(x)(P(x)&Q(x,z)].

Формула F₅^, как и формула F₄, имеет предваренную нормальную форму и равносильна формуле F. В некоторых ситуациях формула F₅^ предпочтительнее формулы F₄, поскольку содержит меньше кванторов. (Кстати, бескванторную часть формулы F₅^ можно упростить).

Перейдем к изучению сколемовской нормальной формы. Отметим вначале, что в логике первого порядка понятие конъюнктивной нормальной формы вводится точно так же, как и в логике высказываний. Сохраняется полностью алгоритм приведения к КНФ и утверждение теоремы 1.3.

Определение. Формула G имеет сколемовскую нормальную форму (сокращенно: СНФ), если G=(x)…(x_n)H, где формула Н не содержит кванторов и имеет конъюнктивную нормальную форму.

Например, формула (x)[P(x)(P(y)&Q(x,y)] имеет сколемовскую нормальную форму, а формулы (x)(y)Q(x,y), (x)[P(x)&(P(y)Q(x,y)] не имеют.

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

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

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

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

Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага имеем формулу F=(x)(y)(z)(u)(v)H(x,y,z,u,v), где Н – не содержит кванторов. Предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле Н заменим х на с, z – на f(y), v заменим на g(y,u). Все кванторы существования вычеркнем. Получим формулу G=(y)(u)H(c,y,f(y),u,g(g,u)).

Это и есть результат выполнения шага 5.

Приведем пример приведения к СНФ. Пусть 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))].

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

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

Проанализируем шаг 5. Предположим вначале, что исключается квантор существования, впереди которого нет кванторов общности. Можно считать, что это первый квантор в записи формулы; т.е. E(u₁,…,u_n)=(y)E′(y,u₁,…,u_n). (Формула E′ может содержать кванторы.) Рассмотрим интерпретацию  с областью М, при которой формула E выполнима. Выполнимость означает, что найдутся элементы а₁,…,a_nM такие, что высказывание (E)(a₁,…,a_n) или (что тоже самое) высказывание (y)(E′)(y,a₁,…,a_n) истинно. Отсюда следует, что существует элемент bM такой что высказывание (E′)(b,a₁,…,a_n) также истинно. Исключение квантора существования по y на пятом шаге приводит к формуле D=E′(c,u₁,…,u_n), где c – константа, отсутствующая в E′. Рассмотрим интерпретацию , которая совпадает с  на всех символах предикатов и функций, входящих в запись формулы F, и (с)=b. Тогда (D)(a₁,…,a_n)=(E′)(b,a₁,…,a_n). Мы доказали, что если формула E выполнима, то выполнима и формула D.

Предположим теперь, что выполнима формула D(u₁,…,u_n)=E′(c,u₁,…,u_n). Это означает, что существует интерпретация  с областью М и элементы а₁,…,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–местной функции, не содержащийся в Е. Предположим, что формула Е выполнима. Выполнимость означает существование интерпретации  областью М и элементов 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 несколько, то зафиксируем один. Тем самым мы определили на М функцию 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) выполнима. Мы показали, что из выполнимости формулы Е следует выполнимость формулы D.

Пусть выполнима формула D. Это означает, что существует интерпретация  с областью М и элементы 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 следует выполнимость формулы Е.

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