Intuitionistic fragments of classical logic For what conditions on P and Q, does P ⊢ Q in classical logic imply P ⊢ Q in intuitonistic logic (for higher-order logic, though of course results for more restricted logics are relevant too)?
As requested, I'm turning my comment into an answer:

For first order logic, the term you want to search for is “Glivenko classes”. Probably, very similar characterizations and techniques apply for higher order logic. See Sara Negri's Glivenko sequent classes in the light of structural proof theory.