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