Axiomatization of propositional calculus Show that axiom schema $(((\lnot C)\to (\lnot B))\to (((\lnot C)\to B)\to C))$ can be replaced by schema $(\lnot B\to \lnot C)\to (C\to B)$ without altering the class of theorems.
I suppose I should show the axiom schema is equivalent to $(\lnot B\to \lnot C)\to (C\to B)$
Thus I have this $(((\lnot C)\to (\lnot B))\to (((\lnot C)\to B)\to C)) \vdash_{L_2} (\lnot B\to \lnot C)\to (C\to B)$
By deduction theorem, $(((\lnot C)\to (\lnot B))\to (((\lnot C)\to B)\to C)),  (\lnot B\to \lnot C), C\vdash_{L_2} B$
Thus I need B using the left side of $\vdash_{L_2}$.
So far, am I solving the exercise well?
 A: I'll use Polish notation, and recast the content of the axiom schema


*

*CaCba

*CCaCbcCCabCac

*CCNaNbCCNaba


The problem then becomes to show that CCNaNbCCNaba can get replaced with 4. CCNaNbCba, and from {1., 2., CCNaNbCba} 3. can get deduced.
So, assuming {CNaNb, b}, by axiom 1. CNab follows.  By axiom 3. and CNaNb, and CNab, a follows.  Thus, we have {CNaNb, b} yields a.  Then, by axioms 1. and 2., $\vdash$CCNaNbCba follows.  Thus, {1., 2., 3.} yields 4.
For the other direction, you just assume {1., 2., 4.} and then show that 3. follows.  Believe it or not, if you embed the axioms in a powerful enough theorem prover like Prover9, such as the following:
-P(C(x, y)) | -P(x) | P(y). (this works like modus ponens... though it's a bit more complicated)
P(C(x, C(y, x))). (axiom 1)
P(C(C(x, C(y, z)), C(C(x, y), C(x, z)))). (axiom 2)
P(C(C(N(x), N(y)), C(y, x))). (axiom 4)
and have
P(C(C(N(x), N(y)), C(C(N(x), y), x))).
as a goal, P(C(C(N(x), N(y)), C(C(N(x), y), x))). can get deduced in less than a minute.
Note: you can think of P as meaning $\vdash$.
