Cardinality reduction theorem for logics ${\mathrm{QHC}}$ and ${\mathrm{QH4}}$

The joint logic of problems and propositions ${\mathrm{QHC}}$ introduced by S. A. Melikhov, as well as intuitionistic modal logic ${\mathrm{QH4}}$, is studied. An immersion of these logics into classical first-order predicate logic is considered. An analog of the Löwenheim–Skolem theorem on the existence of countable elementary submodels for ${\mathrm{QHC}}$ and ${\mathrm{QH4}}$ is established.