Задача, состоящая в отыскании процедуры, позволяющей для любой формулы выяснить, к какому из трех вышеназванных классов она принадлежит, называется также семантической проблемой разрешения. В соответствии с этим процедура, позволяющая конечным числом простых действий решить эту проблему, называется разрешающей процедурой. Самое естественное решение здесь — обратиться к таблице истинности. Таблица даст исчерпывающий ответ о поведении формулы при всех возможных интерпретациях. Но этот прием малоэффективен, поскольку практически он применим лишь для малого числа аргументов (литер). Если формула из двух литер имеет четыре варианта интерпретаций (т.е. четыре строки), то формула из четырех литер — уже 16, из пяти — соответственно 32 и т. д. — по степени 2п строк таблицы истинности. Кстати, этот прием мы применили, когда доказывали тождественность первого постулата ИВ (А1).
Заметим, однако, что, для того чтобы получить разрешающую процедуру, достаточно найти способ, позволяющий отличить тождественные формулы от всех остальных. Применяем эту процедуру к некоторой формуле Л, и, если окажется, что А общезначима, то проблема решена. Если же выясняется, что А не общезначима, то применяем эту процедуру для формулы А. Если А окажется тождественной, то, очевидно, Л — противоречивая. Если А так же, как и Л, не тождественная, то это значит, что формула Л просто выполнима.
Существует несколько методов оценки тождественности формулы:
- 1) оценка с помощью таблицы истинности;
- 2) оценка через преобразование, упрощение и приведение к нормальным формам;
- 3) оценка путем логического вывода из системы аксиом;
- 4) оценка методом редукции;
- 5) оценка методом опровержения.
Некоторые из этих методов мы уже «прошли», с другими предстоит познакомиться.
В ряде случаев для определения тождеств удобен так называемый алгоритм редукции. Алгоритм основан на доказательстве путем приведения к абсурду. Метод работает особенно хорошо, когда формула содержит много импликаций. Рассмотрим его на примере второго постулата (А2) исчисления высказываний.
Предположим невероятное, что (А2) ложный, тогда докажем абсурдность этого предположения.
Итак, пусть:
1) [(Л, А (В -> С)) -> ((Л ~^В)^(А^ С))] = Л.
По свойству импликации она ложна, если антецедент истинен, а консеквент — ложен:
- 2) (А^(В^ С)) = И;
- 3) ((Л ~^В)^{А^ С)) = Л.
Тогда из равенства (3) следует:
- 4) (А^В) = И;
- 5) (Лэ С) = Л.
Ложность (Л —> С) означает, что А = И, С = Л.
Применив modusponens к (Л —> В), получаем: если А = И, то и В = И. Подставим теперь полученные значения Л, В и С в (2), получим:
6) ((Л С)) = (#->(#-> Л)) = Д что противоречит ранее полученному значению (2). Мы пришли к абсурду и тем самым показали, что исходный постулат общезначим. К сожалению, алгоритм редукции применять удобно далеко не всегда, поэтому его не следует рассматривать в качестве универсального метода определения тождествен ности.
