исчисление высказываний

[Serliks]

Помогите разобраться с исчислением высказываний. Есть пример:
$((\neg C\to(\neg A\to\neg B)) \equiv A\vee (\neg B\vee C)$
К сожалению у меня только пока мысли по его решению:
Преобразуем тождесто в $A\vee (\neg B\vee C) \vdash ((\neg C\to(\neg A\to\neg B))$. Так же тут можно применить теорему дедукции $\vdash (A\vee (\neg B\vee C)) \to ((\neg C\to(\neg A\to\neg B))$.
Еще есть мысли, что согласно вот этой теореме $F\to G, G\to H\vdash F\to H $, можно найти некую $H$ выводимую из первой и второй части тождества.

Следовательно используя секвенции мне надо из $A\vee (\neg B\vee C)$ вывести $((\neg C\to(\neg A\to\neg B))$ или некую третью формулу. Вот тут и начинаются проблемы, я не могу понять: по какому признаку мне выбирать секвенции и аксиомы? С чего начать? Правильно ли я вообще думаю?

P.S.как упростить и построить таблицу истинности знаю, но этого и не требуется(( Хочется научится именно ив.

[Deggial]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Причина переноса: формулы не оформлены $\TeX$ом

Serliks
Наберите все формулы и термы $\TeX$ом.
Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»
Формулы поправил и вернул

[Mysterious Light]

Аксиомы и правила вывода бы указывать явно...

Я бы делал так (схематически, ведь аксиомы-то не указаны и даже не указано, следует ли $\equiv$ понимать как самостоятельный символ или как сокращение):
исходил бы из законов:

• $\neg\alpha\to\beta \equiv \alpha\vee\beta$
• $\alpha\vee\beta \equiv \beta\vee\alpha$
• $(\alpha\vee\beta)\vee\gamma \equiv \alpha\vee(\beta\vee\gamma)$

Например, если можно пользоваться теоремой $\frac{\vdash \alpha\equiv\beta \quad \vdash \beta\equiv\gamma}{\vdash \alpha\equiv\gamma},$ то легко чередой её применений получить нужный результат.

[gefest_md]

В интуиционисткой системе Клини предложение $A\vee(\neg B\vee C),\ \neg C,\ \neg A\vdash\neg B$ можно доказать так:

1. $A\vee(\neg B\vee C)$ - допущение.
2. $\neg A$ - допущение.
3. $\neg C$ - допущение.
4. $\neg A\to(A\to\neg B)$ - схема аксиома $8^\prime.$
5. $\neg C\to(C\to\neg B)$ - схема аксиома $8^\prime.$
... [сюда вставляете доказательство формулы 6.]
6. $\neg B\to\neg B$ - $5^{(n-1)},\ 5^{(n)}$.
7. $A\to\neg B$ - модус поненс 2, 4.
8. $C\to\neg B$ - модус поненс 3, 5.
9. $(\neg B\to\neg B)\to((C\to\neg B)\to(\neg B\vee C\to\neg B))$ - схема аксиома 6.
10. $(C\to\neg B)\to(\neg B\vee C\to\neg B)$ - модус поненс 6, 9.
11. $\neg B\vee C\to\neg B$ - модус поненс 8, 10.
12. $(A\to\neg B)\to((\neg B\vee C\to\neg B)\to(A\vee(\neg B\vee C)\to\neg B))$ - схема аксиома 6.
13. $(\neg B\vee C\to\neg B)\to(A\vee(\neg B\vee C)\to\neg B)$ - модус поненс 7, 12.
14. $A\vee(\neg B\vee C)\to\neg B$ - модус поненс 11, 13.
15. $\neg B$ - модус поненс 1, 14.

Эта последовательность строк (вывод) доказывает предложение $A\vee(\neg B\vee C),\ \neg C,\ \neg A\vdash\neg B$. Далее по теореме дедукции, $A\vee(\neg B\vee C)\vdash\neg C\to(\neg A\to\neg B).$
В классической системе Клини надо перед строками 4 и 5 вставить соответствующие доказательства, которые не трудно найти (в своей книге Клини доказывает предложение $A,\ \neg A\vdash B$).