Some General Completeness Results for Propositionally Quantified Modal Logics

TL;DR

This paper investigates the completeness of propositional quantified modal logics on general frames, providing conditions under which these logics are complete and exploring the preservation of truth from general to Kripke frames.

Contribution

It establishes strong completeness results for certain quantified modal logics on general frames and introduces the concept of finite diversity to connect general frames with Kripke frames.

Findings

Normal propositional quantified modal logic with Barcan is strongly complete on quantifiable general frames.

Finite diversity condition ensures preservation of truth from general frames to Kripke frames.

A finite axiomatization of the logic of Euclidean Kripke frames is provided.

Abstract

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.