Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

hilbert-calculuslogic

I'm reading Wikipedia and it lists the first four logical axioms that allow (together with modus ponens) for the manipulation of logical connectives.

  1. $\phi \to \phi $
  2. $\phi \to \left(\psi \to \phi \right)$
  3. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$
  4. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

Then it states "The axiom 1 is redundant, as it follows from 3, 2 and modus ponens."

I see that if I substitute (2) into (3), I get

$$\left(\phi \to \left(\psi \rightarrow \phi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \phi \right)\right)$$

Since (2) is true, modus ponens tells me

$$\left(\phi \to \psi \right)\to \left(\phi \to \phi \right)$$

So (1) would be true if I knew that $\left(\phi \to \psi \right)$ is true. But how do I know that?

If there's a better way to do this proof than the way I approached it, I'll also accept that answer.

Best Answer

Hint: Remember you get to pick what $\psi$ is. Is there any formula $\psi$ such that you know $(\phi\to\psi)$ is true?

More details are hidden below.

By axiom 2, if you choose $\psi$ to have the form $(\psi'\to\phi)$ for some formula $\psi'$, then you know $(\phi\to \psi)$ is true.

Related Question