Дискретная математика:
логика, группы, графы, фракталы

Акимов О.Е.

1.4. Введение в логику высказываний

Построение доказательств в логике высказываний

Логика — это наука о способах доказательства. Выясним, в чем, собственно, состоит различие в построении доказательств в логике высказываний и логике Буля.

В булевой логике все доказательства строились на отношении эквивалентности. Даже если во множественных выражениях и фигурировало отношение включения, что является частным случаем отношения порядка, то его мы переводили в тождество. Две логические функции считались эквивалентными, если они давали на соответствующих наборах аргументов абсолютно одинаковые значения нулей и единиц. При использовании формальной записи логических выражений отдельные звенья цепи любого доказательства там были связаны через символ равенства « = ». Отношение эквивалентности удовлетворяет трем законам —

рефлексивности: А = А;
симметричности: если А = В , то В = А;
транзитивности: если А = В и В = С, то А = С.

В логике высказываний доказательства строятся на отношении порядка, т.е. на отношении, которое существует между причиной и следствием. Здесь уже отдельные звенья цепи доказательства связаны символом импликации. Однако символ импликации «→ » при логическом выводе мы будем заменять на символ « ⇒ », подобно тому, как в логике Буля используются два символа эквивалентности — « ~ » и « = ». Символ « ~ » является объектным, а символ « = » — субъектным. Таким образом, следует различать язык логики высказываний и метаязык исследователя. Чтобы избежать путаницы, введем еще два метасимвола: вместо объектной конъюнкции « ∧ » будем использовать субъектный символ метаконъюнкции — « , », а вместо объектной дизъюнкции «∨ » — субъектную метадизъюнкцию « ; ». Тогда утверждение, которое требуется доказать, оформляется в виде следующего причинно-следственного отношения:

Р₁, Р₂, ... , Р_{n – 1}, Р_n ⇒  С    (1.1)

где Р_i — посылка (причина), С — заключение (следствие). Читается: «Если посылки Р₁, Р₂, ... , Р_{n – 1}, Р_n истинны, то заключение С тоже истинно» или, по-другому: «Если причины Р₁, Р₂, ... , Р_{n – 1}, Р_n имели место, то будет иметь место и следствие С».

Чтобы не спутать объектное высказывание (предложение) с субъектным высказыванием, справедливость которого мы намереваемся установить, условимся предложения типа (1.1) называть клаузой (clause — предложение). Клауза — это метапредложение, в котором использовано отношение порядка, оформленное через символ метаимпликации « ⇒ ». Как и отношение эквивалентности отношение порядка удовлетворяет трем законам

рефлексивности: А ⇒ А;
антисимметричности: если А ⇒ В, то В ⇒ А;
транзитивности: если А ⇒ В и В ⇒ С, то А ⇒ С.

Отношение порядка предполагает выполнение закона антисимметричности, который записывается ещё и так:

если А ⇒  В и В ⇒  А, то А = В;
если А = В, то А ⇒  В и В ⇒  А. 

Клауза есть именно формальная запись доказываемого предложения. Вместо букв в ней можно подставить объектные высказывания, и тогда клауза наполняется конкретным содержанием, которое уже именуется семантикой или легендой. Пример клаузы:

А → В, А ⇒  В.

Если принять, что А = «сверкнула молния», В = «грянул гром», то можно составить следующую легенду: «Известно, что если сверкнула молния, то после этого грянет гром. Молния сверкнула. Следовательно, должен грянуть и гром».

Над субъектом, который формулирует метапредложения, может стоять другой субъект, для которого предложения первого субъекта окажутся объектными. Тогда клаузу (1.1) второй субъект или метасубъект запишет для себя следующим логическим выражением:

Р₁ ∧ Р₂ ∧ ... ∧ Р_{n – 1} ∧ Р_n → С.

Преобразуем это выражение в дизъюнкт, получим:

Р₁ ∨ Р₂ ∨ ... ∨ Р_{n – 1} ∨ Р_n ∨ С.

Отсюда находим:

(Р₁ ∧ Р₂ ∧ ... ∧ Р_{n – 1} ) → (Р_n ∨ С).

Поэтому клауза (1.1) может быть представлена в другой эквивалентной форме:

Р₁, Р₂, ... , Р_{n – 1} ⇒  Р_n ; С     (1.2)

В силу коммутативности конъюнкции на месте посылки Р_n может оказаться любая другая, причем не одна. Например, клауза:

Р₁, Р₂, Р₃, Р₄ ⇒  С₁; С₂ ; С₃.

может быть преобразована в другую эквивалентную форму:

Р₄, C₂, Р₁, C₁ ⇒  P₁ ; С₃ ; P₂.    (1,3)

Однако клауза (1.1) по сравнению с (1.2), (1.3) и другими подобными формами имеет определенные преимущества и, в частности, используется в языке логического программирования ПРОЛОГ. Ее называют хорновской. Произвольную клаузу всегда можно свести к хорновскому виду путем эквивалентных преобразований.

Если символ метаимпликации « ⇒» клаузы (1. 2) сместить в крайнее левое положение, то она превратится в тавтологию; если же его сместить в крайнее правое положение, то — в противоречие:

1 ⇒  Р₁ ; Р₂ ; ...  ; Р_{n – 1} ; Р_n ; С — тавтология,
Р₁, Р₂, ... , Р_{n – 1}, Р_n , С ⇒  0 — противоречие.

Ниже мы рассмотрим пять конкретных методов доказательства справедливости логических клауз — аксиоматический метод, метод таблиц истинности, метод резолюций, метод Вонга и метод натурального исчисления. Как и в логике Буля, в логике высказываний существуют аксиоматический и конструктивный подходы доказательств логических выражений. Два первых из только что названных пяти как раз являются яркими представителями таких подходов, остальные три метода — смешанной стратегии. Аксиоматическое построение логики высказываний состоит в том, чтобы попытаться вычленить из бесконечного числа истинных клауз независимую систему аксиом, с помощью которой можно было бы установить справедливость любых других клауз.