Вывод в исчислении высказываний.

[im_ieee]

Нужно вывести следующую формулу (\neg A \rightarrow \neg (B \rightarrow \neg C)) \rightarrow \neg ((\neg A \rightarrow B) \rightarrow \neg (\neg A \rightarrow C)) Аксиомы: $(A \rightarrow (B \rightarrow A))$, $((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C) ))$, $((\neg B \rightarrow \neg A)\rightarrow((\neg B \rightarrow A) \rightarrow B))$ Также есть теорема дедукции, MP, правила сечения и транзитивности. Единственное, что, на мой взгляд, здесь можно сделать - применить теорему дедукции: (\neg A \rightarrow \neg (B \rightarrow \neg C)) \vdash \neg ((\neg A \rightarrow B) \rightarrow \neg (\neg A \rightarrow C)), как действовать дальше, не знаю.

[Sonic86]

im_ieee в сообщении #792050 писал(а):

правила сечения и транзитивности.

А что это за правила?

[im_ieee]

Sonic86
соответственно
A \rightarrow (B \rightarrow C), B \vdash A \rightarrow C
A \rightarrow B, B \rightarrow C \vdash A \rightarrow C

[arseniiv]

im_ieee в сообщении #792050 писал(а):

как действовать дальше, не знаю.

Попробуйте применить то, что применяется. Потом снова. Некоторые варианты, будет видно, ничего не дают, а некоторые «распутывают».

Теперь с другой стороны: посмотрите внимательно на формулу. Видно, что в ней $A$ всегда входит только в виде $\neg A$, т. е. если выводима формула $(D \to\neg (B \to\neg C)) \to\neg ((D \to B) \to\neg (D \to C))$, выводима и ваша. Вид второй меньше отвлекает «несмысловыми» отрицаниями, и по нему механически строится вывод вашей с помощью замены везде $D$ на $\neg A$.