Can either one of $P ⟹ (Q ⟹ P)$ or $Q ⟹ (P ⟹ P)$ be derived from the other in the implicational propositional calculus? I am reading a bit about the implicational propositional calculus and initially I was confused about the axiom system:

Axiom Schema 1: $P ⟹ (Q ⟹ P)$
Axiom Schema 2: $(P ⟹ (Q ⟹ R)) ⟹ ((P ⟹ Q)⟹ (P⟹R))$
Axiom Schema 3: $((P ⟹ Q) ⟹ P) ⟹ P$

Each one of these is a tautology; moreover, $P ⟹ (Q ⟹ P)$ and $((P ⟹ Q) ⟹ P) ⟹ P$ are both tautologies in $2$ variables. My initial confusion (which I still have not resolved and must point to a fundamental gap in my understanding) is that I am not sure why one of $P ⟹ (Q ⟹ P)$ or $((P ⟹ Q) ⟹ P) ⟹ P$ can't be derived from the other since they are both tautologies in $2$ variables.
In my attempts to figure out what my misunderstanding was I thought that maybe it had something to do with the fact that:

*

*$((P ⟹ Q) ⟹ P) ⟹ P$ has $3$ instances of $P$, whereas $P ⟹ (Q ⟹ P)$ has only $2$
or maybe it had something to do with the fact that

*

*$((P ⟹ Q) ⟹ P) ⟹ P$ has $3$ instances of $⟹$, whereas $P ⟹ (Q ⟹ P)$ only has $2$
And to test that theory I wanted to see if one of $P ⟹ (Q ⟹ P)$ or $Q ⟹ (P ⟹ P)$ is derivable from the other since they both are tautologies in $2$ variables with $2$ instances of $⟹$, $2$ instances of $P$, and $1$ instance of $Q$.
The problem is, I don't know how to go about showing that one is (or isn't) derivable from the other in the implicational propositional calculus.
Any insight into this issue will be greatly appreciated.
 A: Axiom 3 is known Pierce's Law, which is the implication connective form of the Law of the Excluded Middle and is known to be unprovable from the deduction theorem alone (where we include Modus Ponens as a tautology along as part of the deduction theorem; Modus Ponens is also assumed in the Implicational Propositional Logic, so this is reasonable). Just because you have things we decide to be "tautologies" of a given number of variables doesn't mean you can immediately prove other "intuitive tautologies" of the same number of variables. Your system might not be strong enough.
To conclude here, note the Wikipedia Page for the Deduction Theorem includes proofs of both your Axioms 1 and 2 using only the Deduction Theorem. If Axiom 3 could be proved from Axioms 1 and 2 this would mean Pierce's Law could be proved by the Deduction Theorem, known to be false.
I cannot yet think of a quick way to show Axiom 3 does not imply Axiom 1. If you use classical logic and translate the axioms you will find they all say very different things, and there is no reason to suspect any of the three axioms are redundant.
A: The simplest way to look at this sort of problem is to look at the axiom systems through condensed detachment.  An axiom system under Condensed detachment only produces theorems which are the most general theorems up to relettering of the variables given the axioms.  A theorem A is more general than another theorem B if by using only substitution in A we can obtain B, but we can't use substitution from B to obtain A.  For example, (P$\rightarrow$(P$\rightarrow$P)) is not a most general type of theorem in the implicational propositional, since both (Q→(P→P)) and (P→(Q→P)) are more general. 
Suppose, (Q$\rightarrow$(P$\rightarrow$P)) is our only axiom.  Alright, so we make some copy of (Q$\rightarrow$(P$\rightarrow$P)) and put that in for Q.  Then we'll obtain (P$\rightarrow$P) as a theorem.  All other theorems are substitution instances of (Q$\rightarrow$(P$\rightarrow$P) and (P$\rightarrow$P).  (P$\rightarrow$(Q$\rightarrow$P)) is not one of those theorems.  Thus, (P$\rightarrow$(Q$\rightarrow$P)) is not derivable from (Q$\rightarrow$(P$\rightarrow$P)).
Conversely, the theorems generated via condensed detachment with (P→(Q→P)) follow a pattern and always get longer.  Basically, one can see what this pattern is as follows:


*

*(P→(Q→P))

*(A1$\rightarrow$1.)

*(A2$\rightarrow$2.)
and so on ad infinitum.
(Q$\rightarrow$(P$\rightarrow$P)) isn't on that list, and thus can't get proved.
