PhiloDream

Табличное построение предполагает определение логических отношений между формулами. Существенное значение для анализа рассуждений имеет отношение логического следования (символ├), которое определяется следующим образом.

Из Ai, ., An как посылок логически следует В как заключение, если при истинности каждого Ai, ., Ап истинным является и В. В языке-объекте отношение следования адекватно выражается импликацией. Значит, если A1, ., Аn ,├ В, то формула, представляющая собой импликацию вида (A1 ^ А2 ^ . ^ Аn) → В, должна быть тождественно истинной.

Табличное построение логики высказываний позволяет определять логические отношения между высказывания и проверять правильность умозаключений, используя приведенный выше критерий. В качестве примера предлагаем провести табличным способом проверку правильности рассуждения формы (p→q) ├ (ˉ|q→ˉ|p). Заменив знак логического следования между посылкой и заключением на импликацию и построив таблицу для полученной формулы, видим, что она является тождественно истинной. Значит, рассуждение является правильным.

Если в рассуждении содержится более трех переменных, то строить полную таблицу для проверки его правильности затруднительно и тогда используют сокращенный метод проверки, рассуждая от противного. Поскольку при правильном рассуждении формула вида (A1 ^ . ^ Аn) → В должна быть тождественно истинной, посмотрим, не может ли она при каком-то наборе значений переменных оказаться ложной. Предположим, что может. Если из этого предположения получим какое-нибудь противоречие, то предположение неверно (и проверяемое рассуждение правильно), а если из этого предположения не получим противоречия, то увидим набор значений переменных, при котором формула ложна, т. е. тот набор, который опровергает проверяемое рассуждение.

Логика высказываний как исчисление — это прежде всего так называемая система натурального вывода (СНВ). Аппаратом в ней служат правила вывода, каждое из которых является какой-нибудь элементарной формой умозаключения. Переходя по этим правилам от посылок или некоторых допущений к новым формулам, постепенно доходят до заключения. Вывод из посылок осуществлен, если удалось элиминировать все сделанные допущения. Таким образом, под выводом формулы В (заключения) из формул A1 – An (посылок) имеется в виду последовательность формул, каждая из которых является либо посылкой, либо допущением, либо получается по правилам вывода из предыдущих и последняя формула этой последовательности есть формула В, а все допущения при этом элиминированы.

Правила СНВ позволяют оперировать со всеми связками, имеющимися в алфавите языка. Они делятся на правила введения (в) и правила исключения (и) связок.

Кроме этих прямых правил получения новых строк вывода, в СНВ приняты непрямые правила, определяющие стратегию построения вывода. Например, если нужно вывести из посылок формулу вида импликации (Х1→(X2 → . (Xn-1→Xn))), то после выписывания посылок выписываются в качестве допущений все антецеденты заключения, начиная с антецедента главного знака импликации, т. е. Х1,X2, X3 .,Xn-1. Если при этом удастся вывести Xn, то по непрямому правилу

собираем последовательно формулы: (Xn-1→Xn)

(при этом исключается допущение Xn-1), (Xn-2→(Xn-1→Xn)(Xn-2 исключается из числа допущений) и т. д., пока ни получим требуемое заключение

X1→(Xn-2→…(Xn-1→Xn).

Это правило построения прямого вывода.

Приведем пример вывода с применением этого правила:

((рq)→r)├ (р→ (q├ r))

Другое непрямое правило используется для построения косвенного вывода, при котором допущением является отрицание В или отрицание последнего консеквента х„. Это правило имеет вид