(~~) A double-negation translation takes classical (modal or not) logic to intuitionistic (modal or not) logic
(Simp) Replacing modal operators with simple quantifiers a la simpson takes classical modal logic to classical logic
(Pf-D) A focal-constructive-semantics translation takes intuitionistic modal logic to intuitionistic logic, yielding the effects of Pfenning-Davies
So I can do (~~) then (Pf-D), or I can do (Simp) then (~~). Either way I get from classical modal to plain intuitionistic logic.
The only difference between them is that the modalities and shifts end up getting translated slightly differently, namely □N gets sent to
(~~);(Pf-D) → ∀x≥t.Nx ⇒ #(x)
(Simp);(~~) → ∀x≥t.Nx ⇒ #
and ↓N gets sent to
(~~);(Pf-D) → Nt ⇒ #(t)
(Simp);(~~) → Nt ⇒ #
and similarly for ⋄ and ↑.
So it's really all a matter of whether the "falsehood" token keeps track of the current modal world or not. Unfortunately this doesn't give me any insight yet into any kind of Glivenko-ish interchange principle that would work for all propositional connectives that aren't quantifiers...