(~ forall x . A(x)) ==> (exists x . ~A(x))
It is valid classically, invalid intuitionistically, and still invalid intuitionistically if you slap a not-not out front of it. It is an example (unless I made a mistake in pronouncing it unprovable) of the kind of formula I was looking for, one that demonstrates the necessity of the full recursive Goedel-Kolmogorov-Gentzen double-negation translation, but sadly it's first-order. I was hoping a nice little example would exist in the propositional fragment, but I'm finally starting to believe that none exists. I guess that means the type-theoretic consequences of a "classically true" modality are only going to be nontrivial in a system which is already saddled with dependent types. That's kind of a bummer.
---
Okay,