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

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

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

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

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