Косвенные методы доказательства

Рассмотрим условное высказывание вида AÉB, где A - конъюнкция посылок, B - заключение. Иногда удобнее вместо доказательства истинности этого условного высказывания установить логическую истинность некоторого другого высказывания, равносильного исходному. Такие формы доказательства называются косвенными методами доказательства.

Еще одной формой косвенного метода доказательства, является доказательство по закону контрапозиции, основанное на равносильности

AÉB º ØBÉØA,

когда вместо истинности AÉB мы доказываем истинность ØBÉØA.

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

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

Другая возможность - использовать контрапозицию и попытаться, например, доказать ØB É ØA вместо AÉB. Тогда мы допустим ØB и попробуем доказать ØA. Иными словами, допускается, что заключение B (правая часть исходной импликации) неверно, и делается попытка опровергнуть посылку A. Это позволяет двигаться как бы назад от конца к началу, применяя правила так, что старое заключение играет роль посылки. Такая организация поиска может лучше показать, какие результаты имеют отношение к делу. Она называется поиском от цели.