General Strategy for Derivations in Propositional Logic In Propositional Logic, one is often tasked with showing that some particular formula is a theorem of a given deductive system, i.e. $\emptyset \vdash \psi$. These formulas can look very simple and intuitive, e.g. $(\alpha \rightarrow \alpha)$, but the derivation can be rather cumbersome. That examples takes around 6 steps for instance, and is one of the simpler cases.
My question is immediate then: Is there any way of anticipating the correct strategy for making such derivations, and thus avoiding the lengthy 'trial and error' process of applying different axioms (and rules of inference) until something works?
Essentially, are there any 'tricks' that are unlikely to appear in notes etc. but which you are aware of the help look ahead and spot the right path?
For completeness (no pun intended), I've included the particular deductive system I am working with below, and a few indicative theorems.
$((\neg \alpha \rightarrow \alpha)\rightarrow\alpha))$
$(\neg\neg\alpha\rightarrow\alpha)$
$(\neg\alpha\rightarrow(\alpha\rightarrow\beta))$
EDIT
The above cases can be dealt with a little more tidily by applying the Deduction Theorem. Do any other results like this exist? Also, supposing the Deduction Theorem cannot be used, do strategies still exist?

Let $\mathcal{L}_0=\mathcal{L}[\{\neg, \rightarrow\}]$. Define the system $L_0$ as follows:
An axiom of $L_0$ is any formula of $\mathcal{L}_0$ of the form


*

*(A1) $(\alpha \rightarrow ( \beta \rightarrow \alpha))$

*(A2) $((\alpha \rightarrow ( \beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow ( \alpha \rightarrow \gamma)))$

*(A3) $((\neg \beta \rightarrow \neg \alpha ) \rightarrow (\alpha \rightarrow \beta))$


The only rule of inference in $L_0$ is modus ponens, i.e. from $\alpha$ and $(\alpha \rightarrow \beta)$ infer $\beta$.
 A: Some proofs of the completeness of a propositional proof system can actually be turned easily to an algorithm for proving any propositional statement $Q$ from a proposition statement $P$ if $Q$ is a consequence of $P$
This gives you a strategy for always finding proofs of propositional consequences.
A: \begin{sermon}

In Propositional Logic, one is often tasked with showing that some particular formula is a theorem of a given deductive system [of a Hilbert style]

Often tasked by whom? Teachers with a very mean streak, perhaps. But surely very rarely in real logical life, so to speak. If you genuinely want to know whether a bunch of propositional assumptions do or don't entail a given conclusion (not just because some instructor asks you, and moreover asks you to do it with one hand tied behind your back), either you do a truth-table, or (usually faster) use a tableau, or (if you think the argument is valid and just want to confirm that) run up an informal natural deduction proof (the clue is in the name! -- such proofs do indeed  regiment natural ways of reasoning).
Over three-quarters of a century since Gentzen, it is pretty odd still to be making students tackle Hilbert systems. For there is very little serious logical interest in the combinatorial puzzle-solving task of finding Hilbert proofs (as opposed to proofs in more user-friendly systems of logic). 
\end{sermon}
A: There exists a similar question here... my best response to that question may be the September 30th response (I employ the same conventions in this answer as I did in that answer).  Condensed detachment may help, as well as using a theorem-prover.
For this system you can prove everything by the deduction (meta) theorem, a theorem which allows to get NCpNq (this is Polish notation) from "p" and "q", and a form of proof-by-contradiction.  The proof-by-contradiction roughly goes "if we assume the negation of a well-formed formula "Nw" and it leads to a contradiction, then the formula "w" is either a theorem or true under the scope of the other hypotheses."  The relevant theorems you need for this are (in Polish notation):
Recursive Letter Prefixing [RLP]: CpCqp
Self-Distribution [SD]: CCpCqrCCpqCpr  [these two give you The Deduction Theorem, and if you have The Deduction Theorem, then these two are theorems].
Conjunction-introduction [Ki]: CpCqNCpNq.
and
Negation elimination [No]: CCNpNCqNNqp.
I used Prover9 to find proofs of the last two theorems in this system.
Proofs of CNNpp and CNpCpq emerged when I ran Prover9 for the proofs of negation elimination and conjunction introduction.  Now say you want to prove Clavius: CCNppp, which you mentioned before.  We can assume CNpp as a hypothesis and proceed as follows.
 hypothesis 1 |  CNpp  
 hypothesis 2 || Np   
 D1.2       3 || p    
 D[Ki.3]*4  4 || CNaNCpNa
 D4.2*5     5 || NCpNNp
 Ci 2-5 *6  6 |  CNpNCpNNp
 D[No.6]*7  7 |  p
 Ci 1-7*8   8    CCNppp

C2-2 is the law of identity.  C2-3 is the hypothesis.
 hypothesis   1 | CNpp
 D[RLP.Ki]*2  2 | CaCbCcNCbNc  (this enables C2-Ki)
 D[SD.2]*3    3 | CCabCaCcNCbNc  
 D3.1*4       4 | CNpCcNCpNc  (this enables C2-4)
 D[SD.4]*5    5 | CCNpcCNpNCpNc
 D5.[Cpp]*6   6 | CNpNCpNNp
 D[No.6]*7    7 | p
 Ci 1-7*8     8   CCNppp

 axiom        0 CCNpNqCqp (not used here)
 axiom        1 CpCqp
 axiom        2 CCpCqrCCpqCpr
 theorem      3 CpCqNCpNq
 theorem      4 CCNpNCqNNqp
 D2.1*5       5 CCpqCpp
 D5.1*6       6 Cpp  (this enables C1-1)
 D1.3*7       7 CpCqCrNCqNr (this enables C1-Ki)
 D1.4*8       8 CpCqCrCsNCrNs (this enables C1-2)
 D1.1*9       9 CpCqCrq (this enables C1-RLP)
 D1.2*10     10 CpCCqCrsCCqrCqs
 D2.10*11    11 CCpCqCrsCpCCqrCqs
 D11.8*12    12 CpCCqrCqCsNCrNs (this enables C1-3) 
 D12.6*13    13 CCpqCpCrNCqNr (this enables C1-4)
 D11.3*14    14 CCpqCCprCpNCqNr (this enables C1-5)  
 D1.6*15     15 CpCqq (this enables C1-Cpp)
 C2.14*16    16 CCCpqCprCCpqCpNCqNr
 D16.15*17   17 CCpqCpNCqNp  (this enables C1-6)
 D1.4*18     18 CpCCNqNCrNNrq
 D2.18*19    19 CCpCNqNCrNNrCpq
 D19.17*20   20 CCNppp

A useful pattern here is to take any axiom or theorem "x", then go D[RLP.x], and then distribute that result.  D[SD].[D[RLP.x]].  Interestingly enough, you can prove CNpCpq by starting this way... D D[SD].[D[RLP.0]].[RLP] is a proof of CNpCpq.
