Доказательство приведением к противоречию

При построении выводов не всегда целесообразно ждать появления искомого заключения, просто применяя правила вывода. Именно такое часто случается, когда делается допущение В для доказательства импликации В-->С. Применяем цепное правило и модус поненс к В и другим посылкам, чтобы в конце получить С. Однако можно пойти по неправильному пути, и тогда будет доказано много предложений, большинство из которых не имеют отношения к нашей цели. Этот метод носит название прямой волны и имеет тенденцию порождать лавину промежуточных результатов, если его запрограммировать для компьютера и не ограничить глубину.

Другая возможность- использовать одну из приведенных выше эквивалентностей и попытаться, например, доказать ~С-->~В вместо В-->С. Тогда допустим ~С и попробуем доказать ~В. Т.е. допускается, что заключение С (правая часть исходной импликации) неверно, и делается попытка опровергнуть посылку В. Это позволяет двигаться как бы назад от конца к началу, применяя правила так что старое заключение играет роль посылки. Такая организация поиска называется поиском от цели.

Можно использовать также комбинацию этих методов, называемую приведением к противоречию. В этом случае для доказательства В-->С допускаем одновременно В и ~С, т.е. предполагаем, что заключение ложно:

~(В-->C)=~(~B C)=В~С.

Теперь можно двигаться и вперед от В, и назад от ~С Если С выводимо из В. то, допустив В, доказали бы С. Поэтому допустив С. получим противоречие. Если же мы выведем ~В из ~С, то тем самым получим противоречие с В. В общем случае мы можем действовать с обоих концов, выводя некоторое предложение Р, двигаясь вперед, и его отрицание ~Р, двигаясь назад. В случае удачи это доказывает, что посылки несовместимы, или противоречивы. Отсюда выводим, что дополнительная посылка (В~С) должна быть ложна, а значит противоположное ей утверждение (В С) истинно.

Следует отметить, что если предложение В-->С ложно, то никогда не получим противоречия, сколько бы ни рассуждали. При автоматизации поиска доказательства здесь снова возникает проблема, так как ЭВМ не может сказать, когда нужно остановиться.