Is the $\varphi \to \varphi$ axiom in Hilbert calculus redundant?

Question

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 :)

Answer 1

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.