Метатеорема mt_Xor_2 (вариант modus ponens для равноистинности):

~ X, X Y |— Y (1)

Y, X Y |— ~X (2)

~ Y, X Y |— X (3)

X, X Y |— ~Y (4)

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

Доказательство (1) получается из доказательства (2) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

Доказательство (2) получается из доказательства (3) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

Доказательство (3) получается из доказательства (4) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

Доказательство (4) получается из доказательства (5) в MT_Xor_1 передвиганием символа |— на шаг вправо и перестановкой гипотез.

Метатеорема MT_Xor_3 (вариант пункта 1 в MT_Xor_1):

Если имеются доказательства

G₁, G₂,... G_β |— X => ~Y

и

G₁, G₂,... G_β |— ~Y => X,

то можно составить доказательство

G₁, G₂,... G_β |— X Y

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

Составляем новое доказательство из таких частей:

... все строки доказательства G₁, G₂,... G_β |— X => ~Y

... все строки доказательства G₁, G₂,... G_β |— ~Y => X

1 ) Xor3 |-> (X => ~Y) => ((~Y => X) => (X Y)) // a ~> X, b ~> Y

2 ) X => ~Y, №1 |-> (~Y => X) => (X Y) // MP

3 ) ~Y => X, №2 |-> X Y // MP

Непротиворечивость КИВ

Обратите внимание на метатеорему 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, и наоборот. Противоречие никогда не будет получено.

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