Kripke semantics for the logic of problems and propositions

In this paper we study the propositional fragment $\mathrm{HC}$ of the joint logic of problems and propositions introduced by Melikhov. We provide Kripke semantics for this logic and show that $\mathrm{HC}$ is complete with respect to those models and has the finite model property. We consider examples of the use of $\mathrm{HC}$-models usage. In particular, we prove that $\mathrm{HC}$ is a conservative extension of the logic $\mathrm{H4}$. We also show that the logic $\mathrm{HC}$ is complete with respect to Kripke frames with sets of audit worlds introduced by Artemov and Protopopescu (who called them audit set models).
Bibliography: 31 titles.