We study the completeness problem for propositionally quantified modal logics on quantifiable general frames, where the admissible sets are the propositions the quantifiers can range over and expressible sets of worlds are admissible, and Kripke frames, where the quantifiers range over all sets of worlds. We show that any normal propositionally quantified modal logic containing all instances of the Barcan scheme is strongly complete with respect to the class of quantifiable general frames validating it. We also provide a sufficient condition for the truth of all formulas, possibly with quantifiers, to be preserved under passing from a quantifiable general frame to its underlying Kripke frame. This is reminiscent of both the idea of elementary submodel in model theory and the persistence concepts in propositional modal logic. The key to this condition is the concept of finite diversity (Fritz 2023), and with it, we show that if $\Theta$ is a set of Sahlqvist formulas whose class of Kripke frames has finite diversity, then the smallest normal propositionally quantified modal logic containing $\Theta$, Barcan, a formula stating the existence of world propositions, and a formula stating the definability of successor sets, is Kripke complete. As a special case, we have a simple finite axiomatization of the logic of Euclidean Kripke frames.

翻译：我们研究了命题量化模态逻辑在可量化一般框架与克里普克框架上的完备性问题。在可量化一般框架中，可容许集合是量词可作用的命题且世界可表达集是可容许的；在克里普克框架中，量词作用于所有世界集合。我们证明：任何包含巴肯模式所有实例的正规模态命题量化逻辑，对于验证该逻辑的可量化一般框架类都是强完备的。我们还给出了一个充分条件，使得所有可能包含量词的公式在从可量化一般框架转换到其底层克里普克框架时真值得以保持。这既令人联想到模型论中的初等子模型思想，也类似于命题模态逻辑中的持久性概念。该条件的核心是有限多样性概念（Fritz 2023），基于此我们证明：若$\Theta$是一组Sahlqvist公式，其克里普克框架类具有有限多样性，则包含$\Theta$、巴肯公式、断言世界命题存在性的公式以及断言后继集可定义性的公式的最小正规命题量化模态逻辑是克里普克完备的。作为特例，我们得到了欧几里得克里普克框架逻辑的一个简洁有限公理化系统。