On intuitionistic modal epistemic logic (Q1185042)

Consider the language of modal propositional logic extended by one new unary operation \(K\) (`it is verified that'). Let \(IKT_ *\) denote the smallest modal system obtained by adding the modal axiom schema (\(*\)) \(A\leftrightarrow\diamondsuit KA\) to the intuitionistic version \(IKT\) of the normal modal propositional logic \(KT\). It is observed that (i) \(\diamondsuit A\) collapses into \(A\) in \(IKT*+\vdash\diamondsuit\diamondsuit A\to\diamondsuit A\) and \(IKT*+\vdash KA\to KKA\), (ii) in \(IKT*\), \(\vdash KA\to A\), (iii) a certain proof of \(A\to KA\) in \(KT+(*)+(c_ \to)\vdash K(A\land B)\to (KA\land KB)\) (called Fitch's problem) does not go through in \(IKT*+(c_ \to)\), (iv) the latter system is not a conservative extension of \(IKT\), (v) \(IKT+(*_ \to)+(\text{Close}_ K)\) is a conservative extension of \(IKT\), where \((*_ \to)\) is the left to right direction of (\(*\)) and \((\text{Close}_ K)\) is a certain strong deductive closure rule for \(K\), and (vi) \(\diamondsuit\), \(\square\), and \(K\) are non-redundant operations in \(IKT*+\text{(Close}_ K)\) (even if Dummett's schema is added) and hence \(A\to KA\) cannot be proved in \(IKT*+(c_ \to)\). Moreover, there is a section on failures of the finite model property. The paper ends with a characterization theorem and certain corollaries thereof for a modal intuitionistic system \(IZ\) wrt the class of all so-called \(Z\)-models.