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

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

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

Or1:

a (a b)

Or2:

b (a b)

Or3:

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

Or3, сокращенно:

ac (bc (ab c))

Метатеорема MT_Or_1 (введение ):

X X Y    (1)
Y X Y    (2)
X X Y    (3)
Y X Y    (4)

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

Метатеорема MT_Or_2 (удаление ):

Два доказательства, отличающиеся одной гипотезой, можно объединить в одно, если объединить различающиеся гипотезы через .

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

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

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

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

строки доказательства G_₁, G_₂,... G_{_β} X Z
строки доказательства G_₁, G_₂,... G_{_β} Y Z
1)	Or3	(X Z) ((Y Z) (X Y Z))	// a ~> X, b ~> Y, c ~> Z
2)	X Z, №1	(Y Z) (X Y Z)	// MP
3)	Y Z, №2	X Y Z	// MP
4)	X Y, №3	Z	// MP