Composition of an intuitionistic negation and negative modalities as a necessity operator

The main objective of the paper is to axiomatize operators $-\lnot$ and $-\square'$ in logics $N^*$ and $HK\square'$, respectively. The result is formulated in terms of normal extensions $HKN\square'$ and $HKNR$ of $HK\square$, which are embedded in corresponding logics via a natural translation. In addition, for the logic $HKNR$, the finite model property and decidability are established by using a hybrid calculus.