Techniques for showing non-derivability in logics and other formal proof systems
IME, the following list is easiest to hardest (of course, it's also least to most powerful):


If your system is sound, and you can prove $\lnot \phi$, then you have a nonderivability result, of course.
If you have a lattice-theoretic semantics for your logic, relative to which all your proof rules are valid, then if the meaning of a proposition is not the topmost element of the lattice, then it is not a derivable proposition. 
If you know that your logic is complete with respect to a class of models, check to see if there is a particular model in that class which invalidates $\phi$. 
Sometimes you can get away with a translation into another logic, and show that derivability over here implies a known nonderivability result over there. 
If you have a natural deduction or sequent calculus, check to see if there is a cut-elimination result known, or if you can prove one. If there is, then you can often exploit the subformula property to give simple inductive arguments about nonderivability. (Eg., consistency via cut-elimination is just the statement that there are no cut-free proofs of false, and so if all cuts can be eliminated then there are no inconsistencies.)
If nothing else works, then you can often show consistency/nonderivability results via a logical relations argument. This is the big gun, which works when nothing else does -- in set-theoretic terms, it boils down to a use of the axiom of Replacement, which lets you show huge sets are well-ordered. (This is why you can use it to prove things like normalization of System F.)