How to prove $(a\rightarrow \neg{b})\rightarrow(\neg{(b \rightarrow c)}\rightarrow \neg{a})$

Question

I'm trying to prove this by using Hilbert systems:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP) A, A → B ⊢ B

Is there a specific approach to these things that i'm not seeing ?

here is my approach but it's always hard for me to carry on from it :

From the given i see $\Phi=\{a\rightarrow\neg{b}\}\vdash \neg{(b\rightarrow c)}\rightarrow \neg{a}.$ By using the deduction theorem we recieve $\Phi\cup \neg{(b\rightarrow c)} =\{a\rightarrow\neg{b},\neg{(b\rightarrow c)}\}\vdash\neg a$ which needs to be proved to show that the original logic proposition is true.

Here i get stuck ,i try to solve this by saying that $\neg{a}$ then i try to see the previous steps that i need to to make to reach $\neg{a}$ for example if i do modus ponens on $\varphi_1=\neg{(b\rightarrow c)}$ and $\varphi_2=\neg{(b\rightarrow c)}\rightarrow \neg{a}$ i will reach the end of the proof, but i think this is a bad approach for this. I need help with ways to approach these kind of proofs.

Answer 1

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$\rightarrow$y) translates to C(x, y) and $\lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))).  [deny(1)].
7 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).  [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))).  [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))).  [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)).  [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))).  [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).  [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))).  [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).  [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))).  [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))).  [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))).  [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)).  [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))).  [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))).  [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))).  [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))).  [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))).  [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))).  [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))).  [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)).  [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))).  [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))).  [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))).  [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))).  [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)).  [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))).  [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))).  [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))).  [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))).  [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))).  [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))).  [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))).  [hyper(2,a,3180,a,b,21589,a)].
29514 $F.  [resolve(29513,a,6,a)].