Techniques for showing non-derivability in logics and other formal proof systems In proof systems for classical propositional logic if one want to show that a certain formula $\psi$ is not derivable one simply shows that $\neg\psi$ can be derived (although other techniques certainly are possible). Non-derivability follows essentially from the soundness and completeness of the proof system.

Unfortunately for non-classical logics and more exotic proof systems (such as the rules underlying operational semantics) no such direct technique exists. This could be because the non-derivability of $\psi$ does not imply that $\neg\psi$ is derivable, as is the case with intuitionistic logics, or simply that no notion of negation exists.

My question is given a proof system $(\mathcal{L},\vdash)$, where $\vdash\;\subseteq\mathcal{L}^*\times\mathcal{L}$, (and presumably its semantics), what techniques exist to show non-derivability?

The proof systems of interest could include operational semantics of programming languages, Hoare logics, type systems, a non-classical logic, or inference rules for what-have-you.
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.)