Intuitionistic Double Negation as a Necessity Operator

Kosta Došen

An intuitionistic propositional modal logic in which we have a necessity operator equivalent to intuitionistic double negation is proved sound and complete with respect to Kripke-style models with two relations, one intuitionistic and the other modal. It is shown how the holding of formulae characteristic for this logic is equivalent to conditions for the relations of the models.