Доказательство секвенции

[mvb13]

Нужно построить доказательство секвенции (генценовское исчислении высказываний)
$A \to B$ |- $(A\cup C ) \to (B\cup C )$

Аксиома-секвенция A|-A
Правила вывода | допустимые правила


Я пытаюсь постороить вывод в обратной последовательности.

1. Для доказательства необходимой секвенции можно воспользоваться правилом вывода №7
и секвенцией $A \to B , A\cup C $ |- $ B\cup C $ (1)
2.(1) можно получить из правила вывода №4 и $A \to B , A\cup C $ |- $ B$ (2)
3.(2) из $A \to B $ |- $ B$ и правила вывода №12 (3)

А вот (3) уже вывести не могу(не знаю вообще выводится ли такая секвенция)
Пробовал искать вывод секвенции $A\cup C $ |- $ B\cup C $ .Тоже ничего не получается.
Подскажите пожалуйста как начать решать данную задачу ?

[Профессор Снэйп]

Сначала седьмое правило, потом шестое...

[mvb13]

Я пытаюсь применить правила 7 и 6 к секвенции ,которую требуется доказать, но у меня ничего не получается. Не могли бы Вы объяснить, что требуется сделать, более подробно ?

[Профессор Снэйп]

После седьмого правила (тут всё однозначно) шестое с $B = C$ и $C = B \vee C$. Получается три ветки. В одной одиннадцатое правило сразу ведёт к аксиоме. В другой пятое и одиннадцатое тоже дают аксиому. В третьей четвёртое и восьмое дают две аксиомы.

[mvb13]

У меня снова затруднее .
1. Правильно ли я понял , что даная последовательность действий служит доказательством секвенции $A\cup C$|-$B\cup C$?

Цитата:

После седьмого правила (тут всё однозначно)

2. К какой секвенции нужно применить 7-е правило ?

[Профессор Снэйп]

1) Правилами форума запрещено размещать полные решения.

2) Слушай, если проблемы настолько серьёзны, то, может, ну их, эти секвенции? Переведись на гумфак или в институт физкультуры, там секвенций не будет