Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics (Q757342)

The paper proves some translation theorems for intuitionistic modal logics (IML) using Kripke bundle semantics for intermediate predicate logics (IPL). They are based on the correspondence between Kripke bundles (introduced by the reviewer and \textit{D. P. Skvortsov} [``Semantics of non-classical first-order predicate logics'', in: Mathematical logic (\textit{P. Petkov} (ed.)) (1990)]) and intuitionistic modal frames (introduced by \textit{H. Ono} [Publ. Res. Inst. Math. Sci., Kyoto Univ. 13, 687-722 (1977; Zbl 0373.02026)]). More precisely, let \(\psi\) be a translation from (intuitionistic) modal propositional formulas to predicate formulas transforming \(\square\) to \(\forall x\) and \(\diamondsuit\) to \(\exists x\). An IML K is a modal analogue of an IPL L \((<K,L>\) is an associate, in terms of the paper) iff \(K\vdash A\Leftrightarrow L\vdash \psi (A)\) for any formula A. R. Bull and H. Ono constructed modal analogues of H (intuitionistic logic) and \(H+D\) (the logic of constant domains). The author gives simpler proofs of these results and also finds modal analogues of \(H+\tilde P_ n\), \(H+\tilde P_ n+D\) (\(\tilde P_ n\) is a predicate formula axiomatizing Kripke frames of height \(\leq n)\).