Is the $\varphi \to \varphi$ axiom in Hilbert calculus redundant? When I see the Hilbert calculus in logic, I sometimes notice that $T \vdash \varphi \to \varphi$ is listed as an axiom and sometimes not. Is there some reason? Could I get it somehow from the other axioms? If so, how?
Thanks in advance :)
 A: Here I show how to derive $a\to a$ from
$$\begin{array}{ll}
a\to(b\to a) & \text{axiom K} \\
(a\to (b\to c))\to ((a\to b)\to (a\to c)) & \text{axiom S}
\end{array}$$
which are usually axioms of a Hilbert system.  
$$
\begin{array}{rll}
1& (a\to (b\to c))\to ((a\to b)\to (a\to c)) &  \text{axiom S}\\
2& (a\to (b\to a))\to ((a\to b)\to (a\to a))  & \text{replace $c$ with $a$ in (1)}\\
3& a\to (b\to a)                     &   \text{axiom K}\\
4& (a\to b)\to (a\to a)              &     \text{2, 3, M.P.}\\
5& (a\to (b\to a))\to (a\to a)       &     \text{replace $b$ with $b\to a$ in (4)}\\
6& a\to a                         &    \text{5, 3, M.P.}\\
\end{array}
$$
It's interesting to observe that in combinatory logic, we have the identity $$(S K) K \equiv I$$ which is formally identical to this proof, which first applies  makes K the antecedent of S and uses modus ponens to detach the consequent $S K$, and then makes K the antecedent of that $S K$ and detaches the consequent again, which is I. This is not a coincidence; it's an example of the Curry-Howard correspondence.
I see now that the Wikipedia article has a proof of $a\to a$ substantially similar to the one I showed.
