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

До сих пор мы использовали только аксиомы Imp1, Imp2, Imp2', описывающие свойства символа . Теперь настало время для символа ~. Напомню соответствующие аксиомы:

Not1:

~~a a

Not2:

(a b) ((a ~b) ~a)

Докажем несколько метатеорем, описывающих свойства символа ~ в КИВ. Будем пользоваться только аксиомами для материальной импликации (Imp1, Imp2) и отрицания (Not1, Not2).

Почти все доказательства в этой и в последующих главах (вплоть до главы "Непротиворечивость") довольно просты и требуют минимальных пояснений (которые будут даны). Можете относиться к ним как к упражнениям: некоторые (или все) метатеоремы можно попробовать сначала доказать самому, а уже потом подсмотреть одно из возможных решений, кликнув на надпись "Посмотреть доказательство" (Java-скрипты в браузере должны быть включены).

Метатеорема MT_Not_1 (сокращение означает "(М)ета(т)еорема для операции "Not" номер 1"). Это - основное орудие для доказательства формул, начинающихся со значка ~.

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

Или формально:

Если имеются доказательства
G1, G2,... Gβ, X Y и
G1, G2,... Gβ, X ~Y,
то можно составить доказательство:
G1, G2,... Gβ ~X

Метатеорема MT_Not_2

Если бы можно было доказать противоречие, то можно было бы доказать все, что угодно.

Или формально:

Можно составить доказательство: X, ~X Y

Метатеорема MT_Not_3:

Двойное отрицание доказывается из формулы без двойного отрицания и наоборот.

Или формально:


~~X X    (1)
~~X X    (2)
X ~~X    (3)
X ~~X    (4)

Метатеорема MT_Not_4:

Вывод и любую гипотезу можно заменять на ее двойное отрицание и обратно.

Или формально:

Если имеется доказательство:
G1, G2,... Gβ, X Y,    (1)
то можно составить как доказательство
G1, G2,... Gβ, X ~~Y,    (2)
так и доказательство
G1, G2,... Gβ, ~~X Y,    (3)
и обратно.

Метатеорема MT_Not_5 (правила обращения импликации):

Из материальной импликации доказывается обратная материальная импликация с отрицаниями.

Или формально:


(X Y) (~Y ~X)    (1)
(X Y) (~Y ~X)    (2)
(~X ~Y) (Y X)    (3)
(~X ~Y) (Y X)    (4)
(~X Y) (~Y X)    (5)
(~X Y) (~Y X)    (6)
(X ~Y) (Y ~X)    (7)
(X ~Y) (Y ~X)    (8)

Метатеорема modus tollens.

X Y, ~Y ~X

Метатеорема MT_Not_6 (эта теорема нам понадобится для доказательства очередной связи между булевой алгеброй и КИВ):

Если имеются доказательства
G1, G2,... Gβ, X Y и
G1, G2,... Gβ, ~X Y,
то можно составить доказательство:
G1, G2,... Gβ Y

Замечание: доказательство длинное, самостоятельно искать придется долго, лучше посмотреть: