Some General Completeness Results for Propositionally Quantified Modal Logics

Propositionally quantified modal logics (pqmls henceforth) are modal logics augmented with propositional quantifiers, a special kind of quantifiers that can be intuitively understood as capturing the quantification implicit in English sentences such as “Everything Jane believes is false” and “It’s likely that there’s something I will never know”. One can also understand the expression “For all the police knows, John is dead already” as “That John is dead already is compatible with everything the police knows” and see that propositional quantification is involved.

Normal propositional modal logic has been studied fruitfully in relation to the possible world-based Kripke frames. For propositional quantifiers, it is natural to consider them as quantifying over sets of possible worlds, since in Kripke frames, propositional variables are interpreted as sets of worlds, and propositional quantifiers bind these variables.¹¹1This is obviously not the only way: another well known approach to propositionally quantified formulas is to view them as uniform interpolants [34, 41, 9, 5], and semantically we also have the related bisimulation quantifiers [23, 16, 17, 14, 37, 10]. A detailed comparison is well beyond the scope of this paper, and we only note that understanding propositional quantifiers as bisimulation quantifiers would immediately lead to the atomless principle $\forall p(\Diamond p\to\exists q(\Diamond(p\land q)\land\Diamond(p\land\lnot q)))$, assuming a reasonably rich model class. As we will see, one of the hallmarks of Kripke frames is that they validate the opposite atomicity principle, and quantifiable frames in general are silent on this issue. This immediately gives pqmls a second-order flavor, and indeed they are also known as second-order propositional modal logics when interpreted on Kripke frames. We may also impose a distinction between sets of worlds that count as propositions (possible value of propositional variables) and sets of worlds that do not count, thereby adding a propositional domain (also called the set of admissible sets) to Kripke frames and obtaining general frames. General frames in which every formula under every variable assignment expresses a proposition are called quantifiable frames, and they have the desirable logical property of validating instantiation reasonings such as from “Everything I believe is true” and “I believe that the Moon is made of cheese” to “The Moon is made of cheese”.

The theory of pqmls based on Kripke frames and quantifiable frames has been studied since the early days of modal logic (see [22] for a nice survey). The early landmark paper is Fine’s [15] in which, among many other things, it is shown that the pqml consisting of formulas valid on the class of reflexive and transitive Kripke frames is not recursively axiomatizable while the pqml of the class of Kripke frames with a universal relation is decidable and can be axiomatized by simply adding to the modal logic $\mathtt{S5}$ the standard quantificational logic and an atomicity principle stating that there is always a world proposition that is itself true and entails every truth. Related questions of decidability, axiomatizability, and expressivity under various kinds of frames were under sustained investigation [29, 28, 1, 31, 8, 32, 4, 30, 18, 42, 12, 3]. A recent breakthrough is by Fritz in [19] where he established many new results on the decidability and axiomatizability of pqmls in a very general fashion. Prior to this work, it was not even known whether the pqml of Euclidean Kripke frames is decidable, and the decidability of the pqml of the Kripke frames validating $\mathtt{KD45}$ was only established in [12].

In this paper, we focus on the question of when an axiomatically defined pqml is complete w.r.t. the quantifiable/Kripke frames it defines. In particular, we aim for a counterpart of the celebrated Sahlqvist Completeness Theorem for pqmls. For example, the 5 axiom $\Diamond p\to\Box\Diamond p$ defines the class of Euclidean Kripke frames, and we know by Sahlqvist Completeness Theorem that 5 is also sufficient to axiomatize the normal modal logic of Euclidean Kripke frames. But is 5 sufficient also for the pqml of Euclidean Kripke frames, even with the help of some atomicity principles? A full generalization of the Sahlqvist Completeness Theorem was already declared impossible by Fine’s results, as the pqml of the class of all Kripke frames is not recursively axiomatizable but the class is trivially definable. Thus, we must build on some general condition for axiomatizability, and [19] provided an elegant one: the finiteness of the diversity of Kripke frames. Given a Kripke frame $\mathbb{F}$, two worlds in it are called duplicates if the permutation switching them is an automorphism of $\mathbb{F}$. Being duplicates is an equivalence relation, and the diversity of $\mathbb{F}$ is the cardinality of the set of equivalence classes of this relation, while the diversity of a class $\mathsf{C}$ of Kripke frames is the supremum of the diversity of all point-generated subframes of frames in $\mathsf{C}$. Fritz [19] shows that if a class $\mathsf{C}$ of Kripke frames is defined by a finite set $\Theta$ of formulas and has finite diversity, then the pqml of $\mathsf{C}$ is decidable. Decidability itself does not provide much information on whether there can be a simple and intuitive axiomatization or if a given axiomatically defined logic is complete, but as we mentioned above, Fine gave a simple axiomatization of the pqml of Kripke frames with a universal relation (equivalently, Kripke frames validating S5), and more recently, for Kripke frames validating $\mathtt{KD45}$, it is shown [12] that we only need to add the quantificational axioms and rules, the Barcan scheme Bc, and the atomicity principle for completeness. Can this result be generalized? Our finding is that if $\Theta$ is a set of Sahlqvist formulas and the class $\mathsf{KFr}(\Theta)$ of Kripke frames it defines has diversity $n$, then the normal pqml axiomatized by $\Theta$, the Barcan scheme Bc, an atomicity principle $\mathtt{At}^{n}$, and an axiom $\mathtt{R}^{n}$ stating that the successor sets of propositions are propositions, is sound and complete w.r.t. $\mathsf{KFr}(\Theta)$. The last two axioms are parametrized by $n$ as they use iterated modalities to simulate the reflexive and transitive closure of the primitive modality. While we can replace the condition of $\Theta$ being Sahlqvist by suitable technical conditions, we cannot drop it completely; and while for $\mathtt{KD45}$ $\mathtt{R}^{n}$ is redundant, for $\mathtt{K5}$ it is not.

Our method is based on saturated (witnessed) maximally consistent sets and the saturated canonical general frame built from them. Fine [15] claims that this method can be used to show the completeness of $\mathtt{S5}$ with atomicity principle w.r.t. Kripke frames with a universal relation but provided only an extremely terse sketch. We will first show that if $\Lambda$ is a normal pqml with the Barcan scheme Bc, then its saturated canonical general frame is quantifiable and indeed validates $\Lambda$. A corollary is that any normal pqml containing Bc is sound and complete w.r.t. the class of quantifiable frames it defines. Note that since quantifiable frames are essentially multi-sorted first-order structures, pqmls on them are no longer second-order and we are not bound by the non-axiomatizability issues. This basic general completeness result may have been realized by multiple scholars before, but a formal proof for the fully general statement appears to be missing.

For the main theorem, we start with the saturated canonical general frame and gradually turn it into a Kripke frame that validates the original logic and satisfies a given consistent set of formulas. The strategy is as follows: first (1) take a point-generated general frame, then (2) keep only the worlds that are named by world propositions and obtain what we call the atomic general frame, and (3) finally show that we can expand the propositional domain of the atomic general frame to the full powerset without affecting the semantic value of any formula. Step (2) also happens in some completeness proofs of hybrid logics (see e.g. [39], Definition 5.2.6). The resulting atomic general frame has the special property of being discrete and tense, and Sahlqvist formulas are shown to be persistent over these general frames [40]. This is essential in showing that the final frame validates the original logic. Step (3) can also be utilized to show completeness for the monadic second-order theory of $\omega$ [35].

In Section 2 we review the basic definitions and provide a Tarski-Vaught-style test for the expansion of the propositional domain to the full powerset to preserve the value of all formulas with propositional quantifiers. In Section 3, we show that the saturated canonical general frame of any pqml containing Bc validates the logic. In Section 4, we show how finite diversity allows a quantifiable frame to pass the Tarski-Vaught test. In Section 5 we prove our main result. Finally, we conclude in Section 6.

Now we present the Tarski-Vaught-style test for expanding the propositional domain safely.

Substitutions play an important role in our later proofs. Many authors define substitution only when it is free to do so, but we need the version that renames the bound variables when conflicts arise.

Finally, we introduce logic. For the convenience of certain proofs, we opted for $\Diamond$ as the primitive modality. For this reason, the Dual axiom is necessary.

Recall that the famous Barcan scheme Bc is $\Diamond\exists p\varphi\to\exists p\Diamond\varphi$.

This section introduces saturated canonical general frames for npqmls containing all instances of the Barcan scheme and shows that they validate the original logic and are automatically quantifiable. A consequence is the following:

Fix a npqml $\Lambda\supseteq\mathsf{K}_{\Pi}\mathtt{Bc}$. To construct the saturated canonical general frame for $\Lambda$, we extend $\mathsf{Prop}$ to $\mathsf{Prop}^{+}$ with countably infinitely many new variables and obtain the extended language $\mathcal{L}^{+}$. Semantics and logics for $\mathcal{L}^{+}$ are defined completely analogously. Let $\Lambda^{+}$ be the smallest npqml in $\mathcal{L}^{+}$ extending $\Lambda$.

Now define the saturated canonical general frame $\mathbf{F}_{\Lambda}=(W,R,B)$ where

• •

  $W$ is the set of all saturated $\Lambda^{+}$-MCSs,

• •

  $wRv$ iff for all $\varphi\in v$, $\Diamond\varphi\in w$,

• •

  $B=\{[\varphi]\mid\varphi\in\mathcal{L}^{+}\}$ where $[\varphi]=\{w\in W\mid\varphi\in w\}$.

The following two lemmas are completely analogous to their first-order modal logic counterparts. The proof of the first extension lemma is almost identical for example to the proof of Theorem 14.1 of [33]. The full power of (EI) is not used, and all we need is (EE) and that npqmls can prove equivalences between formulas that differ only by renaming of bound variables. The second existence lemma can also be proved by repeating the steps in the proof of the existence lemma for first-order modal logic with Bc. For an example, see the proof of Theorem 14.2 of [33].

The truth lemma is replaced by a more general statement for all valuations arising from substitutions. This is a common idea in algebraic semantics.

Now we are ready to prove Theorem 3.1. First we show that $\mathbf{F}_{\Lambda}$ is indeed a quantifiable frame, for any valuation $v\in B^{\mathsf{Prop}}$ for $\mathbf{F}_{\Lambda}$, given how $B$ is defined, consider the substitution $\sigma_{v}:p\mapsto\varphi_{p}$ where $v(p)=[\varphi_{p}]$. Then $v=[\sigma_{v}]$. It follows that $\mathbf{F}_{\Lambda}$ is quantifiable by Lemma 3.5. Next, $\mathbf{F}_{\Lambda}\vDash\Lambda$ as for $\varphi\in\Lambda\subseteq\Lambda^{+}$ and arbitrary $v\in B^{\mathsf{Prop}}$, $[\varphi]^{\mathbf{F}_{\Lambda}}(v)=[\varphi]^{\mathbf{F}_{\Lambda}}(\sigma_{v})=[\sigma_{v}(\varphi)]=W$ since $\sigma(\varphi)$ is also in $\Lambda^{+}$. Finally, taking $\sigma$ as $\iota$ in Lemma 3.5, $\llbracket\varphi\rrbracket^{\mathbf{F}_{\Lambda}}([\iota])=[\varphi]$, which means under valuation $[\iota]$, each $\Lambda^{+}$-MCS is satisfied by itself on a general frame $\mathbf{F}_{\Lambda}$ that validates $\Lambda$. Hence Theorem 3.1 follows.

We first introduce the concepts of duplicates and diversity.

Intuitively, duplicate classes are ‘positions’ a world could be in, and the diversity of a Kripke frame counts the number of positions in that frame. We use some examples to illustrate the concept of diversity.

The following lemma collects some easy but very useful properties of the duplicate classes and how they interact with $R$ and $m_{\Diamond}$.

What follows is the core of the proof of our main result. We want to show that if the underlying Kripke frame of the quantifiable frame $(W,R,B)$ has finite diversity and $B$ contains all singletons and duplicate classes, then $B$ is a pqml-invariant subdomain of $\wp(W)$. The key idea is that whenever $\varphi$ is true at $w$ where at most one $p\in\mathsf{Fv}(\varphi)$ is evaluated to a set $X\subseteq W$ that is not necessarily in $B$, we can always swap the valuation of $p$ to a $Y\in B$ while keeping $\varphi$ true at $w$. For this to be true, we must establish that $\varphi$’s truth at $w$ is insensitive to certain changes in the valuation of $p$. For monadic second-order logic, this can be done with EF-game, but for modal logic, we cannot only focus on how $\varphi$’s truth at $w$ is insensitive to change since modality requires us to also consider the truth of $\varphi$ at other worlds. We must take a more global perspective and strive to show that $\varphi$’s ‘meaning’ is insensitive to certain changes. In the end, we arrive at a qualified quantifier-elimination: when restricted to a duplicate class $D$ and relative to a valuation $v$, the ‘meaning’ of $\varphi$ can be written as a Boolean formula $f_{\varphi}(v,D)$ using variables in $\mathsf{Fv}(\varphi)$, and when valuations $u$ and $v$ are close enough, $f_{\varphi}(v,D)=f_{\varphi}(u,D)$.

Let $qd(\varphi)$ be the quantifier depth of $\varphi$.