3.3. Логические следования

Как мы уже упоминали, исчисление предикатов первого порядка является примером неразрешимой формальной системы. В доказанной А. Чёрчем теореме говорится об отсутствии эффективной процедуры при решении вопроса относительно произвольной формулы исчисления предикатов первого порядка, является ли эта формула теоремой. Однако при доказательстве заключительного утверждения (цели) из начальной системы аксиом, посылок мы придерживаемся правила, что если все аксиомы и посылки принимают истинностное значение И, то и заключительное утверждение также принимает значение И. Из-за этого ограничения иногда исчисление предикатов первого порядка и называют полуразрешимым. Рассмотрим пример.

Пример 3.10. Горничная сказала, что она видела дворецкого в гостиной. Гостиная находится рядом с кухней. Выстрел раздался на кухне и мог быть услышан во всех близлежащих комната. Дворецкий, обладающий хорошим слухом, сказал, что он не слышал выстрела. Детектив должен доказать, что если горничная сказала правду, то дворецкий солгал.

1. P  Q: если горничная сказала правду, то дворецкий был в гостиной.

2. Q  R: если дворецкий был в гостиной, то он находился рядом с кухней.

3. R  L: если дворецкий был рядом с кухней, то он слышал выстрел.

4. M  L: если дворецкий сказал правду, то он не слышал выстрела.

Требуется доказать, что если горничная сказала правду, то дворецкий солгал, т.е. P  M.

Представим посылки в КНФ: (P  Q) & (Q  R) & (R  L) & (M  L).

Аналогично заключение: P  M.

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

Таким образом, если даны формулы F₁, F₂, …, F_n и G, то говорят, что формула G является логическим следствием F₁, F₂, …, F_n (или G логически следует из F₁, F₂, …, F_n) тогда и только тогда, когда для любой интерпретации I, в которой F₁ & F₂ & … & F_n истинна, G также истинна.

Для обозначения логического следования формулы G из посылок F₁, F₂, …, F_n будем писать F₁, F₂, …, F_n ╞ G. Символ ╞ есть некоторое отношение между формулами, причем, если посылки соединены знаком &, то имеет место двуместное отношение: F₁ & F₂ & … & F_n ╞ G. Теперь приведем две простые, но важные теоремы, связывающие понятия логического следования с понятиями общезначимости и противоречивости.

Теорема 3.2. Даны формулы F₁, F₂, …, F_n и G. Формула G является логическим следствием формул F₁, F₂, …, F_n тогда и только тогда, когда формула F₁ & F₂ & … & F_n  G общезначима, т.е. ╞ F₁ & F₂ & … & F_n  G. Формула F₁ & F₂ & … & F_n  G называется теоремой, а G называется заключением теоремы.

Теорема 3.3. Даны формулы F₁, F₂, …, F_n и G. Формула G является логическим следствием формул F₁, F₂, …, F_n тогда и только тогда, когда формула F₁ & F₂ & … & F_n & G противоречива.

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

Обозначим общезначимую формулу через , а противоречивую – через . Вернемся к примеру 3.10 и покажем, что формула (P  Q) & (Q  R) & (R  L) & (M  L)  (P  M) общезначима.

Действительно, [(P  Q) & (Q  R) & (R  L) & (M  L)]  P  M = = P & Q  Q & R  R & L  M & L  P  M = = Q  R  L  M  P  M = .

Аналогично можно показать противоречивость формулы (P  Q) & (Q  R) & (R  L) & (M  L) &  (P  M) = .

Аналогичный подход может быть использован и для логики предикатов. Вернемся к примеру 3.4 и покажем, что конъюнкция посылки и отрицания заключения есть противоречивая формула, т.е. y (S(y)  C(y)) & x (y (S(y) & V(x, y))  z (C(z) & V(x, z))) = .

Для этого приведем ее к ССФ.

Посылка имеет вид: S(y)  C(y).

Отрицание заключения: x (y (S(y) & V(x, y))  z (C(z) & V(x, z))) = x (y(S(y)  V(x, y))   z (C(z) & V(x, z))) = xyz (S(y)  V(x, y)  (C(z) & V(x, z))) = xyz (S(y) & V(x, y) & (C(z)  V(x, z))) и ССФ имеет вид: S(b) & V(a, b) & (C(z)  V(a, z)).

Таким образом, (S(b)  C(b)) & S(b) & V(a, b) & (C(b)   V(a, b)) = S(b) & S(b) & V(a, b) & C(b)  C(b) & S(b) &V(a, b) & V(a, b) = .

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

В заключение отметим, что из двух теорем (3.2 и 3.3), как правило, применяется вторая теорема, т.е. если формула G является логическим следствием формул F₁, F₂, …, F_n, то надо доказать противоречивость формулы F₁ & F₂ & … & F_n & G. Так как в этой формуле заключение теоремы G опровергается, то и процедуры поиска доказательства называются процедурами поиска опровержения, т.е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво. Потери общности нет.

Задачи. Доказать утверждения п.2.2.2. (IV), используя аппарат логических следований.