Секвенция

[Maximum]

Не могу вывести в ИС секвенцию $C\to A\vdash A\vee (\neg A\& B)\vee \neg C.$
Пытаюсь использовать удаление дизъюнкции, но, конечно, не помогает, так как остается везде один член дизъюнкции, а из него ничего не получишь.

[Maximum]

Получается вывести только $C, C \to A\vdash A\vee (\neg A\& B)\vee \neg C$. Но это не то!

[Dandan]

наверное, для начала нужно вывести $C\to A\vdash A\vee \neg C.$

[Maximum]

Как это вывести? Для дизъюнкции я знаю только правило введения дизъюнкции, но тут ясно, что должно выводиться целиком $A\vee \neg C$.

[luitzen]

Maximum писал(а):

Как это вывести? Для дизъюнкции я знаю только правило введения дизъюнкции, но тут ясно, что должно выводиться целиком $A\vee \neg C$.

Секвенция $C \to A \vdash A \vee \neg C$ невыводима интуиционистски. Посмотрите, какие правила вывода в Вашей формулировке исчисления секвенций ответственны за «косвенные способы рассуждений». Оно Вам должно пригодиться… :)

[Maximum]

Maximum писал(а):

Как это вывести? Для дизъюнкции я знаю только правило введения дизъюнкции, но тут ясно, что должно выводиться целиком $A\vee \neg C$.

Эта вещь вывелась! Помогло правило контрапозиции.