A modal analog for Glivenko's theorem and its applications (Q1203789)

The paper proves a modal analog of Glivenko's Theorem: \((\square \diamondsuit A \to \square \diamondsuit B) \in K4\) iff \((\diamondsuit A \to \diamondsuit B) \in S4\). Glivenko's Theorem for Heyting propositional calculus is among the corollaries of this theorem. Another corollary is: \(\diamondsuit A \in S5\) iff \(\square \diamondsuit A \vee \diamondsuit \square \perp \in K4\) (the formulation of this corollary contains a misprint). The Theorem allows to investigate a special class of ``NP- formulas'' (which are built from subformulas of the form \(\square \diamondsuit C)\): it is proved that the decidability and the f.m.p. are preserved after adding a finite number of NP-axioms to a modal logic containing \(K4\); on the other hand there exists an extension of \(Grz\) by an infinite recursive set of NP-formulas, which lacks the f.m.p. (The definition of the formula \(Grz\) contains a misprint: the consequent ``p'' is missed).