Непротиворечивость КИВ
[предыдущая глава]  [оглавление]  [следующая глава]

Обратите винмание на метатеорему MT_Not_2. Согласно ей, в КИВ можно доказать любую формулу, если найти хоть одно противоречие. Да, это так, но... дело в том, что ни одного противоречия в КИВ найти не удастся. Докажем это.

Пусть сначала была доказана формула КИВ X. Поскольку все доказанные формулы КИВ соответствуют тавтологиям булевой алгебры, то в булевой алгебре ей соответствует так же записанная тавтология X. Ей соответствует таблица истинности с одними только true в правом столбце. Составим таблицу истинности для формулы булевой алгебры ~X. Применение операции ~ к каждому true даст false, так что в таблице формулы ~X в правом столбце будут стоять одни только false.

Значит, формула ~X в булевой алгебре - невыполнимая формула, а вовсе не тавтология. Поскольку все доказанные формулы КИВ соответствуют тавтологиям булевой алгебры, то формула ~X никогда не будет доказана в КИВ.

Теперь пусть сначала была доказана формула КИВ ~X. Поскольку все доказанные формулы КИВ соответствуют тавтологиям булевой алгебры, то в булевой алгебре ей соответствует тавтология ~X. Ей соответствует таблица истинности с одними только true в правом столбце. Составим таблицу истинности для формулы булевой алгебры ~~X. Применение операции ~ к каждому true даст false, так что в таблице формулы ~~X в правом столбце будут стоять одни только false. Значит, формула ~~X в булевой алгебре - невыполнимая формула.

В булевой алгебре есть тавтология ~~a a. Согласно правилу замены переменной из этой формулы получим тавтологию ~~X X. Согласно правилу равноистинности формулы ~~X и X равноистинны. Значит, поскольку формула ~~X невыполнимая, то и формула X - тоже невыполнимая, а не тавтология. Поскольку все доказанные формулы КИВ соответствуют тавтологиям булевой алгебры, то формула X никогда не будет доказана в КИВ.

Получается, что если удастся доказать X, то никак не удастся доказать ~X, и наоборот. Противоречие никогда не будет получено.

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