7. Доказательство логических клауз методом натурального исчисления

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

1. Правило введения конъюнкции (В К)

2. Правило удаления конъюнкции (УК)

3. Правило введения импликации (В И)

4. Правило удаления импликации (УИ)

5. Правило введения дизъюнкции (ВД)

6. Правило удаления дизъюнкции (УД)

7. Правило введения отрицания (ВО)

8. Правило удаления отрицания (УО)

9. Правило введения эквивалентности (ВЭ)

10. Правило удаления эквивалентности (УЭ)

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

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

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

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

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

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

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

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

1. (УИ)

2. (УИ)

3. (1, БП)

4. (2, БП)

5. (3,4, УО)

6. (5, ВО)

7. (6, ВИ)

8. (7, ВИ)

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

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

1. (УИ)

2. (1, УИ)

3. (2, УИ)

4. (3)

5. (P₁, БП)

6. (5, УИ)

7. (6, ВД)

8. (P₂, БП)

9. (8, УИ)

10. (9, ВД)

11. (P₃, БП)

12. (7, 10, 11, УД)