The fragment of the Heyting propositional calculus which contains double negation but does not contain negation is axiomatized by treating double negation as a necessity operator. The resulting system is shown sound and complete with respect to a specific class of Kripke-style models with two accessibility relations, one intuitionistic and the other modal.