How to prove that a statement is a theorem using Hilbert's system? I'm looking for an actual step-by-step way of proving that a statement is a theorem using Hilbert's system. For instance:

As can be seen from the above picture, the solution consists in a series of steps starting from one of the three axioms (I can only use P2, P3 and P4 and Modus ponens from this https://en.wikipedia.org/wiki/Hilbert_system#Logical_axioms). However, how do I know which axiom to start with? Should I go backwards, starting from the actual statement provided and work my way until I find an axiom? I've also seen ways where you use Modus Ponens (a, a->b/b), but it's unclear exactly the process.
Can anybody help me with the actual step-by-step process on how to do this?
 A: I figured out a way of doing these, from the bottom-up, starting from the statement provided without having to induce anything upfront. First off you should look into some algebra for this system (which is deduced from the main 3 axioms) here: https://it.wikibooks.org/wiki/Logica/Calcolo_delle_proposizioni/Sistema_di_Hilbert#Regole_derivate - it's in italian but what matters are the actual properties.
Now, let's say you're given a statement and you have to show it's a theorem in Hilbert's system. First thing is you write it down your page so you can write stuff on top of it:


*

*$¬(A → B) → (B → C)$


Whenever you're confronted with something like $¬(A → B)$ - a NOT of two terms - you have to find a way to get rid of the NOT in front of it either by using the contrast property where $A → B$ is equal to $¬B → ¬A$, or by using the so called exchange of premises property where $A → (B → C)$ is equal to $B → (A → C)$. So from the above we go ahead and apply the exchange of premises property and exchange the $¬(A → B)$ with the $B$:


*

*$B → (¬(A → B) → C)$

*$¬(A → B) → (B → C)$


We moved it inside so we can get rid of the NOT, which as I said earlier, should be our main goal. In fact, now that $¬(A → B)$ is inside, we can apply the contrast property to help us negate it and therefore get rid of the NOT as such:


*

*$B → (¬C → (A → B))$

*$B → (¬(A → B) → C)$

*$¬(A → B) → (B → C)$


Great so remember that our goal is to continue this process until we find a statement which is an instance of one of the 3 axioms of Hilbert (linked in the question). It seems we're getting close to match Axiom P2 $A → (B → A)$, if we just move the B inside:


*

*$¬C → (B → (A → B))$

*$B → (¬C → (A → B))$

*$B → (¬(A → B) → C)$

*$¬(A → B) → (B → C)$


Now we simply need to move ¬C out and we matched our P2 Axiom and therefore showed that the initial statement was in fact a theorem.


*

*$¬C \vdash B → (A → B))$

*$¬C → (B → (A → B))$

*$B → (¬C → (A → B))$

*$B → (¬(A → B) → C)$

*$¬(A → B) → (B → C)$

