Проверка
правил вывода

[предыдущая глава]  [оглавление]  [следующая глава]

Теперь проверим правила вывода. Начнем с правила подстановки. В нем выполняется замена переменных на формулы. Правило подстановки применяется к аксиомам, которые, как нам доказал компьютер, соответствуют тавтологиям булевой алгебры. Из курса булевой алгебры мы знаем, что замена переменных в тавтологии дает тавтологию. Вывод: все формулы КИВ, которые можно получить с помощью правила подстановки, соответствуют тавтологиям булевой алгебры.

Теперь о правиле вывода modus ponens:

X, X Y Y // MP,

Формулам КИВ X и Y соответствуют формулы булевой алгебры, которые выглядят так же, но не доказываются, а вычисляются по таблицам истинности. Докажем, что:

Если X и X Y тавтологии, то Y - тоже тавтология.

Таблица истинности для формулы X Y:

X	Y	X Y
false	false	true
false	true	true
true	false	false
true	true	true

Поскольку X и X Y у нас - тавтологии, в этой таблице в столбце X будет получаться true, и в столбце X Y будет получаться true - независимо от значений переменных. Такая строка всего одна из четырех, и в ней для Y стоит true. То есть, Y должно давать true при любых значениях переменных.

Отсюда следует, что применение правила вывода modus ponens к формулам КИВ, которым соответствуют тавтологии булевой алгебры, всегда будет приводить к получению формулы, которая таже соответствует тавтологии булевой алгебры. Итак, любой аксиоме КИВ соответствует тавтология булевой алгебры (которая выглядит точно так же). Применение любого правила вывода КИВ дает теорему, которой также соответствует тавтология булевой алгебры. Получается, что любая доказанная формула КИВ имеет "сестренку"-тавтологию в булевой алгебре.

Возникает вопрос: а как насчет обратного утверждения? Можно ли для всякой тавтологии булевой алгебры взять такую же формулу в КИВ и доказать ее? А вот это утверждение обосновать намного, намного сложнее. Но все-таки можно. Чем мы теперь и займемся.