Hilbert Calculus statement proof

Question

I want to prove in $HPC$ that

$$ \vdash_{HPC} (A\rightarrow B)\rightarrow ((B\rightarrow C) \rightarrow (A\rightarrow C ))$$

I tried using different combinations of the $A\rightarrow (B \rightarrow A)$ and $ (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) $ axioms but didn't reach the result. What am I missing?

thanks.

Answer 1

Solution:

Using the deduction theorem for $HPC$, this is correct iff: $$ A\rightarrow B, B \rightarrow C, A \vdash_{HPC} C$$

which is easily proven by using the $MP$ rule 2 times.

Answer 2

I use Polish notation. This means that well-formed formulas get re-defined such that every wff of the form ($\alpha$$\rightarrow$$\beta$) gets translated to C$\alpha$$\beta$. I don't spell out the substitutions made in the below, but I use spacing to show that a substitution follows the form of the axiom. The basic idea runs as follows: we prove CCbcCCabCac and then change the positions of 'Cbc' and 'Cab'.

1. CaCba axiom 
2. CCaCbcCCabCac axiom 
3. C CCaCbcCCabCac C Cbc CCaCbcCCabCac 1
4. CCbcCCaCbcCCabCac 3, 2
5. CC Cbc C CaCbc CCabCac CC Cbc CaCbc C Cbc CCabCac 2
6. CCCbcCaCbcCCbcCCabCac 5, 4
7. C Cbc C a Cbc 1
8. CCbcCCabCac 6, 7
9. CC Cbc C Cab Cac CC Cbc Cab C Cbc Cac 2
10. CCCbcCabCCbcCac 9, 8
11. C CCCbcCabCCbcCac C Cab CCCbcCabCCbcCac 2
12. CCabCCCbcCabCCbcCac 11, 10
13. CC Cab C CCbcCab CCbcCac CC Cab CCbcCab C Cab CCbcCac 2
14. CCCabCCbcCabCCabCCbcCac 13, 12
15. C Cab C Cbc Cab 1
16. CCabCCbcCac 14, 15