@paralipupa

Помогите, пожалуйста, построить вывод (исчисление высказываний):
├ (A->B)-> ̚ (А ˄ ̚ В )
Использовать можно только аксиомы (Клини) и modus ponens
Аксиомы :
1) A→(B→A)
2) (A→B)→((A→(B→C))→(A→C))
3) A→(B→A˄B)
4) A˄B→A
5) A˄B→B
6) A→A∨B
7) B→A∨B
8) (A→C)→((B→C)→(A∨B→C))
9) (A→B)→((A→ ̚ B)→ ̚ A)
10) ̚ ̚ A→A

Не могу понять принцип выбора нужных аксиом для построения.

Люди добрые, помоги. Укажите хотя бы направление. Я уже отчаялся. .
Все эти выводы и подстановки как натягивание совы на глобус. Все варианты приводят в тупик.

(A->B)->~(A&~B)

1 A->B , посылка
2 (A->B) -> (~(A&~B)->(A->B)), A1
3 (~(A&~B)->(A->B)), MP1,2
4 (~(A&~B)->(A->B))->((~(A&~B)->~(A->B))->(A&~B)), A9
5 ((~(A&~B)->~(A->B))->(A&~B)), MP 3,4
6 ((~(A&~B)->~(A->B))->(A&~B))->(((~(A&~B)->~(A->B))->~(A&~B))->~((~(A&~B)->~(A->B)))) ,A9,A=(~(A&~B)->~(A->B)),B=(A&~B)
7 ((~(A&~B)->~(A->B))->~(A&~B))->~((~(A&~B)->~(A->B))) ,MP5,6


1 A->B , посылка
2 (A->B) -> ((A&~B)->(A->B)), A1
3 (A&~B)->(A->B), MP1,2
4 (A&~B)->(A->B))->(((A&~B)->~(A->B))->~(A&~B)), A9
5 ((A&~B)->~(A->B))->~(A&~B), MP 3,4
6 ((A&~B)->(A->B))->((A&~B)->((A->B)->~(A&~B)))->((A&~B)->~(A&~B))
7 ((A&~B)->((A->B)->~(A&~B)))->((A&~B)->~(A&~B))


1 A->B , посылка
2 (A->B)->((A->(B->~~B))->(A->~~B)) ,A2,C=~~B
3 (A->(B->~~B))->(A->~~B) ,MP1,2
4 (B->~~B) ,A10
5 (B->~~B)->(A->(B->~~B)) ,A1,A=(B->~~B),B=A
6 (A->(B->~~B)), MP3,5
7 (A->(B->~~B))->((A->~(B->~~B))->~A) ,A9, A=A,B=(B->~~B)
8 (A->~(B->~~B))->~A ,MP 6,7


1 A->B, посылка
2 (A->B)->((A->(B->A&B))->(A->A&B)), A2, C=A&B
3 (A->(B->A&B))->(A->A&B) ,MP1,2
4 (A->(B->A&B)) ,A3
5 (A->A&B) ,MP3,4
6 (A->B)->(~B->~A) ,закон контрапозиции
7 (~B->~A) ,MP 1,6
8 (~B->~A)->((~B->(~A->~A&~B))->(~B->~A&~B)) ,A2 , A=~B,B=~A,C=~A&~B
9 (~B->(~A->~A&~B))->(~B->~A&~B) ,MP 7,8
10 (~B->(~A->~A&~B)) ,A3,A=~B,B=~A
11 (~B->~A&~B) ,MP 9,10
12 (~B->~A&~B)->(~B->~(~A&~B))->B ,A9, A=~B, B=~A&B
13 (~B->~(~A&~B))->B ,MP 11,12
14 (~B->~A&~B)->((~B->(~A&~B->B))->(~B->B)) ,A2,A=~B,B=~A&~B,C=B
15 (~B->(~A&~B->B))->(~B->B) ,MP 11,14
16 (~B->((~A&~B->B)->~B)) ,A1
17 (~B->(~A&~B->B))->((~B->((~A&~B->B)->(~B->B)))->(~B->(~B->B))) ,A2,A=~B,B=(~A&~B->B),C=(~B->B)
18 (~B->((~A&~B->B)->(~B->B)))->(~B->(~B->B)) ,MP16,17
19 (~B->~A&~B)->(~(~A&~B)->B)
20 (~(~A&~B)->B) ,MP 11,19
21 (~(~A&~B)->B)->(~B->(~A&~B)) ,закон контрапозиции
22 ~B->(~A&~B) ,MP 21,21 тоже что и в стр.11 ???


1 A->B, посылка
2 (A->B)->((A->(B->A&B))->(A->A&B)), A2, C=A&B
3 (A->(B->A&B))->(A->A&B) ,MP1,2
4 (A->(B->A&B)) ,A3
5 (A->A&B) ,MP 3,4
6 A ,посылка
7 (B->A&B) ,MP6,3
8 A&B ,MP 5,6

0