Нормальные напарники интуиционистских модальных логик

Ранее К. Дошен и М. Божич ввели четыре независимые интуиционистские модальные логики — по одной для каждого из четырёх типов модальных операторов: необходимости ${\mathsf{N}}$, возможности ${\mathsf{P}}$, невозможности ${\mathsf{Im}}$ и не-необходимости ${\mathsf{Un}}$. Эти логики обозначаются $\mathsf{HK}{\mathsf{M}}$, где ${\mathsf{M}}\in\{{\mathsf{N}},{\mathsf{P}},{\mathsf{Un}},{\mathsf{Im}}\}$. Интерес к тому, чтобы рассматривать четыре типа модальных операторов по отдельности, связан именно с тем, что над интуиционистской логикой они не могут быть сведены друг к другу. Здесь изучаются расширения логик $\mathsf{HK}{\mathsf{M}}$, у которых есть нормальные напарники. Оказывается, что нормальные напарники есть у всех расширений логик $\mathsf{HK}{\mathsf{N}}$ и $\mathsf{HK}{\mathsf{Un}}$. Для расширений $\mathsf{HK}{\mathsf{P}}$ и $\mathsf{HK}{\mathsf{Im}}$ получен критерий существования нормальных напарников, который заключается в присутствии некоторого модального закона двойного отрицания. Также показывается, как добавление этого закона влияет на выразительные возможности логики. Особый интерес представляет результат о том, что расширения $\mathsf{HK}{\mathsf{P}}$ и $\mathsf{HK}{\mathsf{Im}}$ имеют нормальных напарников, только если они дефинициально эквивалентны расширениям $\mathsf{HK}{\mathsf{N}}$ и $\mathsf{HK}{\mathsf{Un}}$ соответственно. Этот результат является ещё одним примером различия в поведении четырёх типов модальных операторов над интуиционистской логикой.