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

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

Eq1:

(a b) (a b)

Eq2:

(a b) (b a)

Eq3:

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

Метатеорема MT_Eq_1 (введение/удаление ):


X Y, Y X X Y    (1)
X Y X Y    (2)
X Y Y X    (3)

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


X, X Y Y    (1)
Y, X Y X    (2)

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

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