Математика - Классическое исчисление высказываний

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

Докажем несколько метатеорем, описывающих свойства символа в КИВ. Будем пользоваться только аксиомами для материальной импликации (Imp1, Imp2) и исключающего "ИЛИ" (Xor1, Xor2, Xor3). Операция в булевой алгебре представляет собой своего рода зеркальное отражение операции ... и в КИВ свойства этих двух операций имеют определенное сходство.

Xor1:

(a b) (~a b)

Xor2:

(a b) (b ~a)

Xor3:

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

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

X ~Y, ~Y X X Y    (1)
X Y ~X Y    (2)
X Y Y ~X    (3)
X Y ~Y X    (4)
X Y X ~Y    (5)

Посмотреть доказательство

Метатеорема 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)

Посмотреть доказательство

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

Если имеются доказательства
G_₁, G_₂,... G_{_β} X ~Y
и
G_₁, G_₂,... G_{_β} ~Y X,
то можно составить доказательство
G_₁, G_₂,... G_{_β} X Y

Посмотреть доказательство

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

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

...	все строки доказательства 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

1)	Xor1	(X Y) (~X Y)	// a ~> X, b ~> Y
2)	X Y, №1	~X Y	// MP

1)	Xor2	(X Y) (Y ~X)	// a ~> X, b ~> Y
2)	X Y, №1	Y ~X	// MP