Построить вывод формулы (теория алгоритмов)

[Switer]

Здравствуйте! Помогите догадаться как решать это)
$(B \to \neg C)\to(C \to A)\to(((B \to \neg C)\to(C \to A))\to((B \to \neg C)\to B))$
Можно пользоваться теоремой дедукции, правилом modus ponens и тремя аксиомами:
A1. $A \to (B \to A)$
A2. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
A3. $(\neg B \to \neg A) \to (( \neg B \to A) \to B)$

Я не могу найти нормальные примеры по этой теме и не понимаю откуда что берется, сижу голову ломаю второй день. Вот до чего додумался:
По теореме дедукции получаем последовательно две гипотезы:
1. $B \to \neg C$
2. $C \to A$
Следующий шаг (не знаю насколько верный):
Берем 2 аксиому(из тех, что выше) с заменой:
1.A на $B \to \neg C$
2.В на $C \to A$
3.С на B.
Не уверен, что можно делать такие замены, но правил и исключений опять же не нашел нигде.
Остается только как то получить $((B \to \neg C) \to ((C \to A) \to B))$ и дальше по правилу mp получить то, что нужно вывести. Заранее спасибо за помощь)

[gefest_md]

Switer, первым делом надо вычислить таблицу истинности формулы. Потому что есть (мета)теорема «если формула доказуема, то она тождественно истинна».

[Pphantom]

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

- неправильно набраны формулы (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы), в частности, надо перенабрать содержимое картинок.

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Pphantom]

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

[george66]

На языке секвенций это значит
$B\to\neg C,\, C\to A,\ (B\to\neg C)\to(C\to A),\, B\to\neg C\vdash B$
Это неверно (подберите подходящие логические значения для $A,B,C$) и вид у задачи дурацкий. Нет ли опечатки? Проверьте расстановку скобок и не пропустили ли где-нибудь знак отрицания.

[Switer]

Проверю, но если опечатка есть, то не моя) такая ерунда, которая у Вас получилась, была и у меня и я тоже не знал, что с этим делать, а когда я вообще не понимаю толком тему и сталкиваюсь с такой задачей, начинаю сходить с ума