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

Акимов О.Е.

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

Метод натурального исчисления (метод Генцена)

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

Доказательный вывод в натуральном исчислении строится как упорядоченная цепь преобразований, связанных с удалением или введением логических связок на основе следующих десяти правил:

1) правило введения конъюнкции (ВК) —
    (⇒  А) & (⇒  В) // ⇒  А ∧ В;
2) правило удаления конъюнкции (УК) —
⇒ А ∧ В // ⇒  А;
3) правило введения импликации (ВИ) —
⇒ В // ⇒ А → В, А ⇒ В // ⇒  А → В;
4) правило удаления импликации (УИ) —
    (⇒  А) & (⇒ А → В) // ⇒ В, ⇒  А → В // А ⇒ В;
5) правило введения дизъюнкции (ВД) —
⇒ А // ⇒ А ∨ В;
6) правило удаления дизъюнкции (УД) —
    (⇒  А ∨ В) & (А ⇒ С) & (В ⇒  С) // ⇒  С;
7) правило введения отрицания (ВО) —
    А, В ⇒  0 // А ⇒ В;
8) правила удаления отрицания (УО) —
    (А ⇒  В) & (А ⇒ В) // А ⇒  0;
9) правило введения эквивалентности (ВЭ) —
    (А ⇒  В) & (В ⇒ А) // ⇒  А ~ В;
10) правило удаления эквивалентности (УЭ) —
⇒ А ~ В // (А ⇒ В) & (В ⇒  А).

Эти правила надо понимать так: если слева от символа « // » стоят истинные клаузы, то справа от символа « // » тоже будут стоять истинные клаузы. Например, первое правило, введения конъюнкции, можно прочитать следующим образом: если высказывания А и В (метасвязка «и» передается знаком амперсант « & ») порознь истинные (о чем говорят рядом стоящие с этими буквами символы метаимпликации « ⇒  »), то будет истинной и их конъюнкция А ∧ В. При этом надо помнить, что во всех десяти правилах перед символом метаимпликации « ⇒ » может стоять любой перечень посылок Р. Так, десятое правило может выглядеть следующим образом:

Р ⇒  А ~ В // (Р, А ⇒ В) & (Р, В ⇒  А).

Кроме перечисленных десяти правил, имеется еще одно — базовое правило (БП), которое сначала сформулируем словами: во-первых, любая посылка может выступать в роли следствия, т.е.

  А, В, С ⇒  А,    А, В, С ⇒ В     и     А, В, С ⇒ С,

будут всегда истинными и не требуют доказательства, так как удовлетворяют аксиоме порядка; во-вторых, в перечень посылок истинной клаузы всегда можно добавить новые посылки, т.е. если клауза

А, В, С ⇒  Х

верна, то будут истинными и все клаузы, построенные на ее основе, например:

А, В, С, D ⇒ Х,     А, В, С, ... ⇒ Х.

В обобщенной форме базовое правило можно записать так:

P ⇒  X // P, Y ⇒  X,

где X — любая посылка из Р, а Y — произвольная посылка.

Действенность метода натурального исчисления продемонстрируем на примере следующей тавтологии:

1 ⇒  (А → В) → ((А → В) → А).

Доказательство:

1. А, А → В ⇒  В, (УИ)
2. А, А → В ⇒  В, (УИ)
3. А, А → В, А → В ⇒  В, (1, БП)
4. А, А → В, А → В ⇒  В, (2, БП)
5. А, А → В, А → В ⇒  0, (3, 4, УО)
6. А → В, А → В ⇒  А, (5, ВО)
7. А → В ⇒  (А → В) → А, (6, ВИ)
8. 1 ⇒  (А → В) → ((А → В) → А). (7, ВИ)

Справа в круглых скобках указан номер строки, из которой получена данная клауза, а также начальные буквы используемого правила. Приведем доказательство еще одной клаузы:

1 ⇒  (А → В) → ((С → D) → ((A ∨ C) → (B ∨ D))).

Доказательство:

1. А → В ⇒  (С → D) → ((A ∨ C) → (B ∨ D)), (УИ)
2. А → В, С → D ⇒  (A ∨ C) → (B ∨ D), (1, УИ)
3. А → В, С → D, A ∨ C ⇒  B ∨ D, (2, УИ)
4. Р₁, Р₂, Р₃ ⇒  B ∨ D, (3)
5. Р ⇒  А → В, (Р₁, БП)
6. Р, А ⇒  В, (5, УИ)
7. Р, А ⇒  В ∨ D, (6, ВД)
8. Р ⇒  С → D, (Р₂, БП)
9. Р, С ⇒  D, (8, УИ) 
10. Р, С ⇒  D ∨ В, (9, ВД)
11. Р ⇒  А ∨ С, (Р₃, БП)
12. Р ⇒  В ∨ D. (7, 10, 11, УД)