Kripke type semantics for the joint logic of problems and propositions

We consider the joint logic of problems and propositions QHC suggested by S. A. Melikhov. We prove that this logic is complete with respect to Kripke models obtained by enrichment of Kripke models with audit set for a propositional part HC of this logic. We also show that this logic conservatively extends the predicate version of intuitionistic epistemic logic IEL+ constructed by S. Artemov and T. Protopopesku.