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

Докажем несколько метатеорем, описывающих свойства символа в КИВ. Будем пользоваться только аксиомами для материальной импликации (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):

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

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

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

1)	Eq3	(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)	Eq3	(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)	Eq1	(X Y) (X Y)	// a ~> X, b ~> Y
2)	X Y, №1	X Y	// MP

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