In Introduction to Metamathematics, Kleene introduces a formal system where the first three postulates in the group for propositional calculus are:
$$ 1a. A \to (B \to A)\\ 1b. (A \to B) \to ((A \to (B \to C)) \to (A \to C))\\ 2. {A, A \to B \over B} $$
As far as I understand, $1a$ and $2$ are typical for Hilbert-style deductive systems, but $1b$ is not. A more traditional choice, serving pretty much the same purpose (e.g. proving $A \to A$ to start with) would have been: $$ (A \to (B \to C)) \to ((A \to B) \to (A \to C)) $$
What is the rationale for the unique choice made for $1b$ in Introduction to Metamathematics?
References:
- S. C. Kleene, 1952, Introduction to Metamathematics (Ishi Press: 2009 reprint), page 82
- https://en.wikipedia.org/wiki/Hilbert_system
- https://en.wikipedia.org/wiki/List_of_Hilbert_systems
Let's write: \begin{align*} (1b) &\quad (A\to B)\to ((A\to (B\to C))\to (A\to C))\\ (1b') &\quad (A\to (B\to C))\to ((A\to B)\to (A\to C)) \end{align*}
Intuitively, $(1b)$ and $(1b')$ have the same meaning: If you know $(A\to B)$ and you know $(A\to (B\to C))$, then you can conclude $(A\to C)$, by using Modus Ponens $(2)$ twice. The order in which the hypotheses are stated doesn't matter.
The role of $(1b)/(1b')$ in a Hilbert system is to "internalize" Modus Ponens in order to prove the deduction theorem. Both $(1b)$ and $(1b )$ are adequate to prove the deduction theorem, and once we have the deduction theorem in place, our particular choice of axioms for $\to$ doesn't matter.