Working in Hilbert-style axiomatic systems tends to be a rather cumbersome affair. Their beauty is in their small size, which also helps in reasoning about them. Developing intuitive proof strategies is much easier in natural deduction style systems. That said, there are still some techniques that you can use to help develop proofs in an axiomatic system like this. It is important to understand what sort of formulae each axiom schema gives you.
- A1 gives a sort of weakening; once you know that $A$ is true, then any $B$ implies $A$.
- A2 gives you a way of decomposing an inference problem. If you're starting with $A \to (B \to C)$, then if you had $A$, you could get $B \to C$. Even if you don't have $A$, though, you still might be able to infer $A \to B$. Then, since if you had $A$, you'd have $B$ as well as $B \to C$, from which you could get $C$. A2 gives you a way to get from $A \to (B \to C)$ that if $A$ would lead you to $B$, then $A$ also leads you to $C$.
- A3 is about non-contradiction. If some formula implies both $B$ and $\lnot B$, then that formula cannot be true. A3 captures this saying, if $\lnot A$ leads to $B$ and also to $\lnot B$, then $\lnot A$ mustn't be true, so $A$ must be true.
Now, an axiomatic proof system is only concerned with symbol manipulation, so the intuitive description just mentioned does not have any real formal standing, but it might help in making a choice about which axioms to use when you are trying to construct a proof.
In constructing a proof of $p$ from the hypothesis $\lnot(p \to p)$, I started by considering that $\lnot(p \to p)$ is a contradiction (indeed, you presented a proof of $p \to p$ in your question). Since you can prove $p \to p$, you should be able to prove that
and since you have $\lnot(p \to p)$ as a hypothesis, you should be able to prove, without too much trouble, that
- $\lnot p \to \lnot(p \to p)$.
At this point, you should be looking at A3 and wanting to instantiate as
- $(\lnot p \to (p \to p)) \to ((\lnot p \to \lnot(p \to p)) \to p)$.
Then you can apply modus ponens to infer
- $(\lnot p \to \lnot(p \to p)) \to p$,
and then apply modus ponens again, yielding
That's an example of the type of intuition that you might apply to proof construction in these sorts of axiomatic systems. It gets easier with practice, but these systems really are not designed for ease of use, but rather simplicity. It often helps to consider the typical semantics of the formulae (even though the proof system can used as a pure symbol manipulation system), and to ask what the intended conclusion means, and how it relates to the meanings of the hypotheses. Sometimes syntactic considerations are important too, though. For instance, you were given a premise that has a negation sign, and only one of your axiom schemata involves a negation. That does not necessarily mean that that axiom schema is the place to start, but it is worth considering, heuristically.