Логический вывод
Проблема доказательства в логике состоит в нахождении доказательства формулы B (заключения), если предполагается истинность формул A1,...,An (посылок). Мы записываем это в виде
A1,A2,...,An |= B.
Основной метод решения этой проблемы следующий. Записываем посылки и применяем правила вывода, чтобы получить из них другие истинные формулы. Из этих формул и исходных посылок выводим последующие формулы и продолжаем этот процесс до тех пор, пока не будет получено нужное заключение. Мы называем это выводом; именно такой метод обычно применяется в математических доказательствах.
Посмотрим, как это делается.
Два классических правила вывода были открыты очень давно. Одно из них носит латинское название modus ponens (модус поненс или сокращение посылки). Его можно записать следующим образом:
A, A Þ B |= B.
Второе правило (цепное) позволяет вывести новую импликацию из двух данных импликаций. Можно записать его следующим образом:
A Þ B, B Þ C |= A Þ C.
Доказательство с введением допущения. В этом и следующих разделах речь пойдет о трех стратегиях доказательства. Первая называется введения допущения. Для доказательства импликации вида A Þ B допускается, что левая часть A истинна, т.е. A принимается в качестве дополнительной посылки, и делаются попытки доказать правую часть, B.
Этот метод часто применяется в геометрии. Например, при доказательстве равенства боковых сторон треугольника, у которого углы при основании равны, допускается, что эти углы равны, а затем это используется в доказательстве равенства сторон.
Приведение к противоречию. При построении выводов не всегда целесообразно ждать появления искомого заключения, просто применяя правила вывода. Именно такое часто случается, когда мы делаем допущение B для доказательства импликации B Þ C. Мы применяем цепное правило и модус поненс к B и другим посылкам, чтобы в конце получить C. Однако можно пойти по неправильному пути, и тогда будет доказано много предложений, большинство из которых не имеет отношения к нашей цели.
Этот метод носит название прямой волны и имеет тенденцию порождать лавину промежуточных результатов, если его запрограммировать для компьютера и не ограничить глубину.
Другая возможность - использовать одну из приведенных выше эквивалентностей и попытаться, например, доказать ØC Þ ØB вместо BÞC. Тогда мы допустим ØC и попробуем доказать ØB. Иными словами, допускается, что заключение C (правая часть исходной импликации) неверно, и делается попытка опровергнуть посылку B. Это позволяет двигаться как бы назад от конца к началу, применяя правила так, что старое заключение играет роль посылки. Такая организация поиска может лучше показать, какие результаты имеют отношение к делу. Она называется поиском от цели.
Можно использовать также комбинацию этих методов, называемую приведением к противоречию. В этом случае для доказательства B Þ C мы допускаем одновременно B и ØC, т.е. предполагаем, что заключение ложно:
Ø(BÞC) = Ø(ØBÚC) = B Ù ØC.
Теперь мы можем двигаться и вперед от B, и назад от ØC. Если C выводимо из B, то, допустив B, мы доказали бы C. Поэтому, допустив ØC, мы получим противоречие. Если же мы выведем ØB из ØC, то тем самым получим противоречие с B. В общем случае мы можем действовать с обоих концов, выводя некоторое предложение P, двигаясь вперед, и его отрицание ØP, двигаясь назад. В случае удачи это доказывает, что наши посылки несовместимы
или противоречивы. Отсюда мы выводим, что дополнительная посылка BÙØC должна быть ложна, а значит противоположное ей утверждение BÞC истинно. Метод приведения к противоречию часто используется в математике. Например, в геометрии мы можем допустить, что углы при основании некоторого треугольника равны, а противолежащие стороны не равны, и попробовать показать, что при этом и углы должны быть не равны, или получить еще какое-то противоречие.
Доказательство методом резолюции. Правило резолюции следующее: XÚA, YÚØA |= XÚY.
Оно позволяет нам соединить две формулы, удалив из одной атом A, а из другой ØA. Сравним это правило с уже известными нам:
цепное правило: ØX Þ A, A Þ Y |= ØX Þ Y,
модус поненс: A, AÞY |= Y.
Правило резолюции можно рассматривать как аналог цепного правила в применении к формулам, находящимся в конъюнктивной нормальной форме. Правило модус поненс также можно считать частным случаем правила резолюции для случая ложного X.
Чтобы применить правило резолюции, будем действовать следующим образом. Используем доказательство от противного и допускаем отрицание заключения.
1. Приводим все посылки и отрицание заключения, принятое в качестве дополнительной посылки, к конъюнктивной нормальной форме.
а) Устраняем символы Þ и Û с помощью эквивалентностей
AÛB = (AÞB)Ù(BÞA),
AÞB = ØAÚB.
б) Продвигаем отрицания внутрь с помощью закона де Моргана.
в) Применяем дистрибутивность AÚ(BÚC) = (AÚB)Ù(AÚC).
2. Теперь каждая посылка превратилась в конъюнкцию дизъюнктов, может быть, одночленную. Выписываем каждый дизъюнкт с новой строки; все дизъюнкты истинны, так как конъюнкция истинна по предположению.
3. Каждый дизъюнкт - это дизъюнкция (возможно, одночленная), состоящая из предложений и отрицаний предложений. Именно к ним применим метод резолюций. Берем любые два дизъюнкта, содержащие один и тот же атом, но с противоположными знаками, например,
XÚYÚZÚØP,
XÚPÚW.
Применяем правило резолюции и получаем XÚYÚZÚW.
4. Продолжаем этот процесс, пока не получится P и ØP для некоторого атома P. Применяя резолюцию и к ним, получим пустой дизъюнкт, выражающий противоречие, что завершает доказательство от противного.
В качестве примера рассмотрим доказательство соотношения
PÚQ,PÞR,QÞS |= RÚS.
Приводим посылки к нормальной форме и выписываем их на отдельных строках.
|
PÚQ |
(1) |
|
ØPÚR |
(2) |
|
ØQÚS |
(3) |
Ø(RÚS) = ØRÙØS
|
ØR |
(4) |
|
ØS |
(5) |
|
ØP из (2) и (4) |
(6) |
|
Q из (1) и (6) |
(7) |
|
ØQ из (3) и (5) |
(8) |
|
пустой из (7) и (8) |
- это позитивная или негативная атомарная формула. Каждая фраза (или клауза) - это множество литералов, соединенных символом Ú. Фразу можно рассматривать как обобщение понятия импликации. Если A и B - атомарные формулы, то формула
AÞB
может также быть записана как
B Ú ØA.
Простейшая фраза содержит только один литерал, позитивный или негативный.
Фраза с одним позитивным литералом называется фразой (или клаузой) Хорна.
Любая фраза Хорна представляет импликацию: так, например,
D Ú ØF Ú ØE равносильно FÙE Þ D.
Правило резолюции действует следующим образом. Две фразы могут быть резольвированы друг с другом, если одна из них содержит позитивный литерал, а другая - соответствующий негативный литерал с одним и тем же обозначением предиката и одинаковым количеством аргументов, и если аргументы обоих литералов могут быть унифицированы (т.е. согласованы) друг с другом. Рассмотрим две фразы:
|
P(a) Ú ØQ(b,c), |
(1) |
|
Q(b,c) Ú ØR(b,c). |
(2) |
В результате этого получается фраза (3), которая называется резольвентой:
|
P(a) Ú ØR(b,c). |
(3) |
|
P(a) Ú ØQ(b,c), |
(4) |
|
Q(c,c) Ú ØR(b,c). |
(5) |
"x"y (Q(x,y)ÚØR(x,y)).
Если в качестве аргумента выступает переменная, то она унифицируема с любой константой. Если в одной и той же фразе переменная встречается более одного раза и эта переменная в процессе резолюции унифицируется с константой, то резольвента будет содержать данную константу на тех местах, где рассматриваемая переменная располагалась в исходной фразе. К примеру, фразы
|
P(a) Ú ØQ(a,b) |
(6) |
|
Q(x,y) Ú R(x,y) |
(7) |
|
P(a) Ú ØR(a,b), |
(8) |
Любую формулу исчисления предикатов можно привести к конъюнктивной нормальной форме, т.е. представить в виде множества фраз.
