Теорема дедукции. 
Системы поддержки принятия решений часть 1

Проблема разрешимости тесно связана с проблемой вывода. Таких методов много, но процесс вывода остается достаточно утомительным даже для простых примеров. Проблема вывода существенно упрощается, если применить теорему дедукции. Пусть имеется множество гипотез {//}, и Н_п — одна из них.

Теорема утверждает, что необходимым и достаточным условием выводимости В из гипотез {Я} является выводимость импликации (Н_п —> В), т.е. из утверждения (Н_{, Я₂, Я") В следует:

Пусть это условие выполняется и (Н_п —> В) выводимо. Обозначим эту формулу через Ml. Тогда по условию теоремы должна быть выводимой формула (Я_/М —"Ml). Обозначим ее через М2; теперь будет выводима формула (Н_п_2 —> М2) и т. д. Формулировка теоремы, следовательно, сводится к следующей:

Если В выводима из гипотез {Я}, то истинно выражение

Необходимость утверждения доказывается следующим образом. Допустим, В истинна, тогда импликация (Н_п —> В) также истинна при любой Н_п. Но это в свою очередь означает, что истинна следующая импликация (Н_п- —> (Н_п —> В)) и т. д. — вплоть до заключительной импликации (Н_х —" —> (Я₂—> …)…), что и требовалось доказать.

Выражение типа (3.6) с вложенными импликациями называется /г-кратной импликацией. Доказав необходимость (3.6), мы вывели такое логическое утверждение: если в я-кратной импликации заключение В истинно, то, по всей вероятности, ее посылки H_i тоже истинные.

Докажем, что это так и есть, т. е. докажем теперь достаточность, которая доказывается простым применением правила заключения. И действительно, предположим, что выражение (3.6) истинно.

Если Я₁ принимает значение Я, то по modus ponens истинно и все выражение (Я₂—> (Я₃ —". .)…). Но по тому же правилу интерпретации истинна и Я₂, откуда следует, что истинно и выражение (Я₃ —" (Я₄ —> …)…) и т. д. В конце цепочки рассуждений приходим к выводу, что истинна импликация Н_п —> В (выполнение условия (3.4)). Но Н_п — тоже гипотеза, и она — тоже истинная.

Отсюда ВИ.

Пример 3.7

Доказать свойство транзитивности импликации: из условия (А —> В) и (В —" С) следует (А —> С).

Вопрос сводится к доказательству логического следствия:

Доказательство здесь неочевидно, но согласно теореме дедукции нам достаточно доказать условие:

Итак, имеем гипотезы:

a) Н{.А^>В

b) Н₂: В —> С;

c) Я₃: А.

Применяя modus ponens к (а) и ©, получаем: d )В

и далее:

с) С (modus ponens к (Ь) и (d)), что и требовалось доказать.

Доказать выражение (3.7), пользуясь условием (3.6). Гипотезы у нас уже обозначены. Подставляем их в (3.6):

Импликация Л —> С является логическим следствием, если она принимает значение Я тогда, когда все Я, = Я. Пусть формула (3.7) истинная. Если теперь положим, что (Л —> В) = истинная, то по modus ponens

Но (В —" С) = Я₂тоже истинная, и тогда (Л —> С) = Я, и потому является логическим следствием по условию (3.7).

Вернемся к выражению (3.1) (Н_{, Я₂, #") f-> В

и предположим, что оно выполняется, т. е. В — выводимо из {II}. Если это так, то присоединение В к множеству {Я} не влияет на_полноту множества {II, В} и не приводит его к противоречию. Иное дело В, которая при этих условиях невыводима. Ее присоединение к (Я}, очевидно, приведет к противоречивости, т. е. можно написать:

При этих условиях тождественность импликации (3.4), естественно, нарушается, и она становится невыполнимой. Возьмем отрицание импликации (3.4). Теперь должно выполняться условие:

Доказав невыполнимость (3.9) или (3.10), мы косвенно докажем выполнимость условия (3.2). Такой метод доказательства «от противного» называется доказательством методом опровержения.

Метод опровержения очень удобен. На самом деле, вместо того чтобы кропотливо доказывать общезначимость какой-либо формулы F, достаточно доказать невыполнимость ее отрицания F, что в ряде случаев значительно проще. В 1960;е гг. был открыт и разработан принцип резолюций, весьма подходящий для доказательств подобного рода.

Метод опровержения реализует принцип дедукции, который формулируется следующим образом: формула В является логическим следствием множества {Я} тогда и только тогда, когда множество {Я, В} невыполнимо, т. е. (Н_х, Я₂,…, Н_п) -> В, если (H_v Я₂,…, Н_п, В) ь-> JI.

Докажем условие (3.10).

Исключим импликацию:

и, но правилу де Моргана получим.

что эквивалентно выражению.

т.е. все сводится к доказательству невыполнимости:

Формула (3.11) в таком виде уже является элементом КНФ, даже если все Я, — элементарные высказывания. Если же Я, — сложные выражения, то они приводимы к виду КНФ, и их подстановка в (3.11) не меняет ее нормальной формы. Поэтому в дальнейшем мы вправе считать каждое из Я, дизъюнктом, состоящим из одного или многих «слагаемых».

Условие (3.12) требует, чтобы формула (3.11) была невыполнима, т. е. тождественно равна 0. Это возможно, если среди се «сомножителей» найдется хотя бы один пустой дизъюнкт. Такой дизъюнкт не может появиться в явном виде. Но он может быть определен на множестве {II, В} путем определенных эквивалентных преобразований.

Из вышесказанного следует, что согласно принципу дедукции вопрос о выводимости (невыводимости) некоторой формулы В сводится, в конечном счете, к анализу невыполнимости множества дизъюнктов. Но множество дизъюнктов невыполнимо тогда и только тогда, когда пустой дизъюнкт Л является логическим следствием из него. Таким образом, невыполнимость множества {Я, В} можно проверить, порождая логические следствия из него до тех пор, пока не получится пустой дизъюнкт. Метод, позволяющий получить логические следствия из множества дизъюнктов, основан на применении принципа резолюций.