До сих пор мы использовали только аксиомы Imp1, Imp2, Imp2', описывающие свойства символа
Not1:
a
Not2:
b) ((a ~b) ~a)
Докажем несколько метатеорем, описывающих свойства символа
Почти все доказательства в этой и в последующих главах (вплоть до главы "Непротиворечивость") довольно просты и требуют минимальных пояснений (которые будут даны). Можете относиться к ним как к упражнениям: некоторые (или все) метатеоремы можно попробовать сначала доказать самому, а уже потом подсмотреть одно из возможных решений, кликнув на надпись "Посмотреть доказательство" (Java-скрипты в браузере должны быть включены).
Метатеорема MT_Not_1 (сокращение означает "(М)ета(т)еорема для операции "Not" номер 1").
Это - основное орудие для доказательства формул, начинающихся со значка
Из доказательства противоречия на основе гипотез, можно получить опровержение любой из этих гипотез на основе остальных.
Или формально:
Если имеются доказательства
Y ~Y
то можно составить доказательство:
~X
(X
Метатеорема MT_Not_2
Если бы можно было доказать противоречие, то можно было бы доказать все, что угодно.
Или формально:
Можно составить доказательство: Y
Метатеорема MT_Not_3:
Двойное отрицание доказывается из формулы без двойного отрицания и наоборот.
Или формально:
~~X X X X ~~X ~~X
Метатеорема MT_Not_4:
Вывод и любую гипотезу можно заменять на ее двойное отрицание и обратно.
Или формально:
Если имеется доказательство:
Y
то можно составить как доказательство
~~Y
так и доказательство
Y
и обратно.
Метатеорема MT_Not_5 (правила обращения импликации):
Из материальной импликации доказывается обратная материальная импликация с отрицаниями.
Или формально:
Y) (~Y ~X) Y) (~Y ~X) ~Y) (Y X) ~Y) (Y X) Y) (~Y X) Y) (~Y X) ~Y) (Y ~X) ~Y) (Y ~X)
Метатеорема modus tollens.
Y, ~Y ~X
Метатеорема MT_Not_6 (эта теорема нам понадобится для доказательства очередной связи между булевой алгеброй и КИВ):
Если имеются доказательства
Y Y
то можно составить доказательство:
Y
Замечание: доказательство длинное, самостоятельно искать придется долго, лучше посмотреть: