Доказать, что правило удаления дизъюнкции (Генцена) допустимо в ИВ.
Г1|->(AvB);Г2,A|->C;Г3,B|->C
Г1, Г2, Г3, |->C
Доказываю так:
1. Г2|->A->C (по теореме о дедукции)
2. (AvB) -> (CvB) ( не знаю, как обосновать)
3. Г3|->B->C (по теореме о дедукции)
4. (СvB) -> (CvС) ( не знаю, как обосновать)
5. (AvB) -> (CvC) (по следствию из теоремы о дедукции)
6. (AvB), A -> C, B ->C |-> C (из (5) и свойства идемпотентности CvC <-> C)
Помогите, пожалуйста, разобраться, верна ли схема доказательства? Если да, то как обосновать переходы 2 и 4?