2. A Strong Hybrid Language with Propositional Quantifiers

We begin by defining PIL, the strong hybrid language with propositional quantifiers that we will work with for most of this paper. So, assume we have some language of basic (propositional) modal logic – that is, a propositional language built over a collection of propositional variables $\textit {PVAR}= \{ p, q, r, \dots \}$ using Boolean connectives and unary operators $\Box$ and $\Diamond$ . In modal logic, propositional variables are standardly thought of as being true at some subset of possible worlds; this intuition lies at the heart of the Kripke semantics for modal logic, and nowadays it is common to identify ‘propositions’ with ‘subsets of possible worlds’. We will not discuss basic modal logic further here, but turn straight to the task of enriching this simple language. It will be useful to think of the enrichment as having three main components; all three components play a prominent role in Prior’s work, as we shall discuss in more detail in Section 6.

Component 1: Basic Hybrid Logic.

We turn our basic modal language into a basic hybrid language by adding nominals and satisfaction operators. Nominals are usually written $i$ , $j$ , $k$ , and, crucially, each nominal is true at a unique possible world. Nominals play two syntactic roles in basic hybrid logic. First, they can be used as atomic formulas, in precisely the same way as ordinary propositional variables $p$ , $q$ , and $r$ are. Because of the ‘true at a unique world’ restriction on their interpretation, in this first role, nominals can be thought of either as $0$ -place world-naming modalities or as special world-naming propositions; either way, nominals ‘name’ the unique worlds they are true at. Second, any nominal $i$ can occur as a subscript to the symbol $@$ . Any such $@_i$ is called a satisfaction operator, and for any formula $\varphi$ , $@_i\varphi$ is true at a world $w$ iff $\varphi$ is true at the world that $i$ names (i.e., at the unique world where $i$ is true). Satisfaction operators can be thought of as $1$ -place rigidifying modalities. Note that any expression of the form $@_i\varphi$ is either true at all worlds or false at all worlds: it rigidly denotes the truth value that $\varphi$ has at the world that $i$ names. Any formula of the form $@_i\varphi$ is called a satisfaction statement.

Component 2: Strong Hybrid Logic.

We turn our basic hybrid language into a strong hybrid language by adding the universal modality and the downarrow binder. The box form of the universal modality is $A$ , and $A\varphi$ means $\varphi$ is true at all possible worlds in a model; its diamond form is $E$ , and $E\varphi$ means $\varphi$ is true at some world. A formulas like $\downarrow\! i\varphi$ allows us to assign a nominal to the possible world at which we are evaluating. More precisely, $\downarrow \! i \varphi$ assigns nominal $i$ as a name for the world $w$ at which we are evaluating, and $\varphi$ is then evaluated with all (free) occurrences of $i$ in $\varphi$ interpreted as true at $w$ (‘name this world $i$ and evaluate $\varphi$ accordingly!’). As we shall see, downarrow is highly expressive, especially in combination with the universal modality.

Component 3: Propositional quantifiers

Lastly, we add propositional quantification. That is, we also allow ourselves to write expressions like $\forall p \varphi$ , where $p$ is a propositional variable of the underlying basic modal language.

Accordingly, we define the syntax of PIL as follows. Let $\textit {PVAR}= \{ p, q, r, \dots \}$ be a set of propositional variables and let $\textit {NOM} = \{i, j, k \dots \}$ be a set of nominals. We assume that both sets are countable and disjoint, write ATOM for $\textit {PVAR}\cup \textit {NOM}$ and call any element of ATOM an atomic symbol. Then the language $\mathcal {L}_{\textit {}}$ of PIL built over ATOM is defined by the following grammar:

\begin{equation*}\varphi \; ::= \; p \; | \; i \; | \; \neg \varphi \; | \; \varphi \wedge \varphi \; | \; \square \varphi \; | \; @_i \varphi \; | \; \forall p \varphi \; | \; A \varphi \; | \; \downarrow \! i \varphi ,\end{equation*}

where $p \in \textit {PVAR}$ and $i \in \textit {NOM}$ . Other Boolean connectives are defined as expected, and $\Diamond$ and $E$ are defined by $\neg \square \neg \equiv \Diamond$ and $\neg A \neg \equiv E$ . Similarly, $\exists p$ is defined by $\neg \forall \neg p \equiv \exists p$ .

It is clear from this definition that nominals in PIL can occur in formulas in three ways: either as an atomic formula (i.e., in formula position), as part of a satisfaction operator (in operator position), or right after a downarrow binder. Downarrow is a binder: occurrences of $\downarrow \! i$ bind all the free occurrences of $i$ they have scope over. Note, however, that occurrences of $@_i$ do not bind occurrences of $i$ ; as we remarked above, satisfaction statements are modal operators. Unsurprisingly, occurrences of $\forall p$ bind all the free occurrences of the propositional variable $p$ in their scope. The notions of free and bound nominals and propositional variables are defined standardly, and a sentence is a formula that contains no free nominals and no free propositional variables.

The result of substituting a formula $\psi$ for a propositional variable $q$ occurring in some formula $\varphi$ , written $\varphi [\psi /q]$ , is defined in the expected way. It is always possible to carry out such a substitution safely (i.e., without accidental binding) by relabelling the bound variables in $\varphi$ . Similarly, $\varphi [j/i]$ is the result of substituting a nominal $j$ for a nominal $i$ ; by relabelling the bound nominals in $\varphi$ , such substitutions can always be carried out safely too.

In the Hilbert-style system presented in Section 4, the universal instantiation axiom has a side condition: only quantifier and downarrow free formulas with no nominals in formula position can be used to instantiate universal quantifications. We call such formulas soft-QDF formulas. The ‘soft’ part means: no nominals in formula position. The QDF part means: quantifier and downarrow free. That is, soft-QDF formulas are built using the grammar

\begin{equation*}\varphi \; ::= \; p \; | \; \neg \varphi \; | \; \varphi \wedge \varphi \; | \; \square \varphi \; | \; @_i \varphi \; | \; A \varphi ,\end{equation*}

where $p \in \textit {PVAR}$ and $i \in \textit {NOM}$ . A substitution $\varphi [\psi / q]$ is called a soft-QDF substitution iff $\psi$ is a soft-QDF formula.

Soft-QDF formulas behave well with respect to the Henkin-style semantics, that is, they are guaranteed to denote an admissible set in this semantics. On the other hand, nominals denote singleton sets, which need not be admissible, while downarrow can be thought of as introducing ‘a hidden nominal in formula position’ (we will see why in Section 6). Similarly, a quantified formula denotes an intersection of admissible sets, but admissible sets are only required to be closed under finite intersections, not arbitrary ones (see Definition 7 and Lemma 8).

3. A Henkin-Style Semantics

Our first goal in this paper is to prove completeness and pure completeness result for PIL. But we immediately face a problem. The basic propositional modal logic K (the set of basic modal formulas valid on all frames) is decidable in PSPACE. But when propositional quantifiers are added, and standardly interpreted on Kripke frames and models, the resulting set of validities is not even recursively enumerable! This was shown in Kit Fine’s pioneering paper on modal languages with propositional quantifiers, namely Fine (Reference Fine1970). Such languages may look simple, but they are powerful second-order systems.

Nearly 75 years ago, Leon Henkin introduced a way of ‘taming’ higher-order logics; see Henkin (Reference Henkin1950).Footnote ¹ His idea was to increase the number of models in a semantically natural way, thereby reducing the number of validities to the point where validity became recursively enumerable. An important paper by S. K. Thomason introduced a Henkin-style strategy into modal logic; see Thomason (Reference Thomason1972). Thomason first showed an unexpected result: there are Priorean tense logics that are not complete with respect to any class of frames. The definition of frame validity requires us to quantify across all subsets of a Kripke frame, that is, across all propositions, and Thomason gave an elegant example showing that this form of second-order quantification was far from innocent. But Thomason also introduced a Henkin-style cure: he also showed that every Priorean tense logic is complete with respect to a class of what are now called general frames. Thomason’s use of general frames to ‘tame’ standard Kripke semantics has become a fundamental semantical tool in modal logic, and general Kripke frames and models will provide the foundation of our semantics for PIL. The technical question that drives this paper is thus: do general frames allow us to ‘tame’ the basic logic of PIL, and all its pure extensions?

A general frame is a Kripke frame $\langle W, R \rangle$ together with a selection of propositions $\Pi$ , that is, subsets of $W$ . We don’t insist that all subsets of $W$ belong to $\Pi$ ; we simply insist that $\Pi$ has enough structure to behave like a set of propositions. In particular, in any general frame, the set of admissible propositions should be closed under the operations corresponding to the Boolean operators and $\Box$ . So there are a lot more general frames than frames – a single Kripke frame gives rise to multiple general frames, one for each choice of $\Pi$ – and, it turns out that this expansion successfully ‘tames’ the set of validities. So, writing $\mathcal {P}(W)$ for the powerset of $W$ , we define:

Next we must interpret PIL on general frames. The interpretation of the nominals will be taken care of by a naming function (or nomination) $N$ assigning a world to each nominal, while the interpretation of the propositional variables will be given by a modal valuation function $V$ .

This definition builds in our central semantic design decision for PIL: the interpretation of the nominals is independent of the choice of $\Pi$ . Nominals directly ‘tag’ arbitrary worlds via the nomination. This is important, because $\Pi$ may not contain all – or even any – singleton subsets of $W$ as admissible propositions. Our nominals ignore $\Pi$ . They are hardwired to the underlying Kripke frame.

Now for a Henkin-style definition of satisfaction and truth:

We could also have defined notions of standard validity and standard consequence; these are defined exactly as above but with ‘standard model(s)’ replacing ‘general model(s)’. But, as discussed earlier, for the purposes of the present paper standard structures are of little interest. Completeness results are rare when working with standard structures, but by working with general models we will be able to prove Henkin-style completeness results that covers the basic logic and all its pure extensions.

The following semantic lemmas will be used in our soundness and completeness proofs. We start with the Agreement Lemma. This tells us that to ensure that nominations and valuations agree on whether $\varphi$ is satisfied, it suffices that they agree on the atomic symbols occurring in $\varphi$ .

Definition 7. Let $\mathcal {M} = \langle W, R, \Pi , N, V\rangle$ be a general model. Then for all formulas $\varphi$ , we define

\begin{equation*}[\mathcal {M}]_{\varphi } = \{w \in W \; | \; \mathcal {M},w \models \varphi \}.\end{equation*}

Next we see that all soft-QDF formulas pick out admissible propositions.

Our next lemma tells us that the set of all propositions picked out by soft-QDF formulas is a subset of $\Pi$ that is a closed collection of admissible propositions. Let us write $[\mathcal {M}]^{\textit {sqf}}$ for $\{ [\mathcal {M}]_{\varphi } \; | \; \varphi \textit { is a soft-QDF formula} \}$ . Then:

Now for substitution lemmas. We need a lemma for when a formula is substituted for a propositional variable and another for when a nominal is substituted for a nominal. Note the restriction to soft-QDF formulas in the following.

Lemma 10 (Substitution Lemma for Propositional Variables). Let $\mathcal {M} = \langle W, R, \Pi , N, V\rangle$ be a general model. Then for any safe substitution $\varphi [\psi /p]$ , where $\psi$ is a soft-QDF formula, we have that:

\begin{equation*}\mathcal {M},w \models \varphi [\psi /p] \textit { iff } \mathcal {M}',w \models \varphi ,\end{equation*}

where $\mathcal {M}' = \langle W, R, \Pi , N, V'\rangle$ such that $V' \sim _p V$ is defined by setting $V'(p)= [\mathcal {M}]_{\psi }$ .

Lemma 11 (Substitution Lemma for Nominals). Let $\mathcal {M} = \langle W, R, \Pi , N, V\rangle$ be a general model. Then for any safe substitution $\varphi [j/i]$ , we have that:

\begin{equation*}\mathcal {M},w \models \varphi [j/i] \textit { iff } \mathcal {M}',w \models \varphi ,\end{equation*}

where $\mathcal {M}' = \langle W, R, \Pi , N', V\rangle$ such that $N' \sim _i N$ is defined by setting $N'(i)= N(j)$ .

4. The K $_{PIL}$ Axiom System

We now present K $_{PIL}$ , our axiomatisation of PIL with respect to general frames. We first introduce K $_h$ $+$ RULES, the axiomatisation of basic propositional hybrid logic presented in Chapter 7 Section 3 of Blackburn et al. (Reference Blackburn, de Rijke and Venema2001). We discuss both components of K $_h$ $+$ RULES system (i.e., the K $_h$ part and the RULES part) and then add what is required to handle the universal modality, the downarrow binder, and propositional quantification. K $_{PIL}$ is the result.

Definition 12 (The K $_h$ axiom system). The K $_h$ axiom system contains as axioms all propositional tautologies, and all instances of $K$ for the modalities:

\begin{align*} \begin{array}{rl} \displaystyle K_{\Box }: & \Box (\varphi \rightarrow \psi ) \rightarrow (\Box \varphi \rightarrow \Box \psi )\\ \displaystyle K_{@}:& @_i(\varphi \rightarrow \psi ) \rightarrow (@_i \varphi \rightarrow @_i \psi ).\\ \end{array} \end{align*}

It also contains all instances of the following interaction schemas:

\begin{align*} \begin{array}{rl} \displaystyle \textit {Intro}: & i\wedge \varphi \rightarrow @_{i}{\varphi } \\ \displaystyle \textit {Agree}: & @_{j}{@_{i}{\varphi }} \leftrightarrow @_{i}{\varphi } \\ \displaystyle \textit {Back}: & \Diamond @_{i}{\varphi } \rightarrow @_{i}{\varphi } \\ \displaystyle \textit {Sdual}: & @_{i}{\varphi }\leftrightarrow \neg @_{i}{\neg \varphi }, \\ \end{array} \end{align*}

and in addition, all instances of the modal equality schemas:

\begin{align*} \begin{array}{rl} \displaystyle \textit {Ref}: & @_{i}{i}\\ \displaystyle \textit {Sym}: & @_{i}{j} \leftrightarrow @_{j}{i} \\ \displaystyle \textit {Nom}: & @_{i}{j} \wedge @_{j}{\varphi } \rightarrow @_{i}{\varphi }. \end{array} \end{align*}

The proof rules of K $_h$ are:

\begin{align*} \begin{array}{rl} \displaystyle MP: & If \vdash \varphi \rightarrow \psi and \vdash \varphi then \vdash \psi \\ \displaystyle Gen_{\Box }: & If \vdash \varphi then \vdash \Box \varphi \\ \displaystyle Gen_{@}: & If \vdash \varphi then \vdash @_i \varphi \\ \end{array} \end{align*}

K $_h$ proofs are Hilbert-style proofs and it is fairly straightforward to adapt the usual modal machinery of canonical models and prove that K $_h$ is a (sound and) strongly complete axiom system for minimal propositional hybrid logic (see Chapter 7, Section 3 of Blackburn et al. Reference Blackburn, de Rijke and Venema2001 for details). The interaction axioms (together with the Gen $_{@}$ rule) capture the logic of the satisfaction operators: self-dual normal modal operators that interact smoothly with the other connectives. The axioms Ref, Sym, and Nom capture the logic of atomic satisfaction statements like $@_ij$ ; such statements are ‘modal equality assertions’, modal equivalents of first-order atomic formulas of the form $i=j$ . Clearly Ref and Sym express the reflexivity and symmetry of identity. The Nom axiom is more interesting. It can be read as a Leibniz-style identity axiom: ‘if $i$ and $j$ are identical, and $i$ has property $\varphi$ , then $j$ has property $\varphi$ too’. But also note an important special case: if $\varphi$ is $k$ this becomes $@_{i}{j} \wedge @_{j}{k} \rightarrow @_{i}{k}$ , which expresses the transitivity of identity.

Below are two schemas, both provable in K $_h$ , that are used in the completeness proof. Note that Elim is a contraposed form of the Intro axiom (using the Sdual axiom).

\begin{align*} \begin{array}{ll} \displaystyle \textit {Elim}: & i\wedge @_{i}{\varphi } \rightarrow \varphi \\ \displaystyle \textit {Bridge}: & \Diamond i\wedge @_{i}{\varphi } \rightarrow \Diamond \varphi \\ \end{array} \end{align*}

Nonetheless, despite the fact that K $_h$ is complete with respect to the class of all Kripke models (i.e., it is the ‘minimal hybrid logic’), it is more usual to work with more powerful proof systems such as K $_h$ $+$ RULES.Footnote ²

Definition 13 (The K $_h$ $+$ RULES axiom system). The K $_h$ $+$ RULES axiom system contains all the axioms and rules of K $_h$ plus the following two proof rules:

\begin{equation*} \begin{array}{l@{}lll@{}l} {NAME}\,: & \begin{array}{c} \underline {\vdash j\rightarrow \theta } \\ \vdash \theta \end{array} & \mbox {}\qquad \qquad & {PASTE}: & \begin{array}{c} \underline {\vdash @_{i}\Diamond j \wedge @_{j}\varphi \rightarrow \theta } \\ \vdash @_{i}\Diamond \varphi \rightarrow \theta \end{array} \end{array} \end{equation*}

In both rules, $j$ is a nominal distinct from $i$ that does not occur in $\varphi$ or $\theta$ .

As we shall see later, these two rules allow us to do some things that are not possible in K $_h$ , and these things will become important when we look at the pure extensions of K $_h$ . Anticipating this, we include the two rules already at this stage.

Having defined the axiom system K $_h$ $+$ RULES for basic hybrid logic, we must next handle the strong hybrid component. Here are the axioms and rules for the universal modality and the downarrow binder.

That is, the axiomatisation for $A$ exactly mirrors the axiomatisation for $\Box$ , but with one extra axiom which says: $i$ must be true somewhere in any model (we return to this point in Section 6). As for downarrow, several different options are explored in Blackburn and ten Cate (Reference Blackburn and ten Cate2006). We chose this one as it reflects the semantics of the downarrow binder in a particularly simple and direct way.Footnote ³ So we are now ready to assemble the system we are really interested in: K $_{PIL}$ , our axiomatisation of PIL.

Definition 15 (The K $_{PIL}$ axiom system). The K $_{PIL}$ axiom system contains all the axioms and rules of K $_h$ $+$ RULES plus the above axioms for the universal modality and the downarrow binder. Moreover, it contains the following axioms:

\begin{align*} \begin{array}{rl} \displaystyle \textit {Q1}: & \forall p (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \forall p \psi ), where\,\, \varphi\,\, contains\,\,no\,\,free\,\,occurrences\,\,of\,\,p \\ \displaystyle \textit {Q2}\text{-}\textit {sqf}: & \forall p \varphi \rightarrow \varphi [\psi /p], where \,\,\varphi [\psi /p] is\,\, a\,\, soft\text{-}QDF\,\, substitution \\ \displaystyle \textit {Barcan}_@: & \forall p @_i \varphi \leftrightarrow @_i \forall p \varphi , \\ \end{array} \end{align*}

and one more proof rule:

\begin{align*} \begin{array}{rl} \displaystyle Gen_{\forall }: & If \vdash \varphi\,\, then \vdash \forall p \varphi . \\ \end{array} \end{align*}

While $\textit {Q1}$ is familiar from modal and classical logic, and $\textit {Barcan}_@$ from hybrid logic, the side condition on Q2-sqf deserves comment. We cannot substitute nominals (as not all admissible sets of propositions contain singleton subsets) nor can we substitute quantified formulas either (our Substitution Lemma 10 does not cover such substitutions, since the admissible sets are only required to be closed under finite intersections, not arbitrary intersections). Allowing only soft-QDF substitutions ensures soundness.Footnote ⁴

One final remark. We formulated $\textit {Barcan}_@$ in its $\forall$ -form, that is, in the form $\forall p @_i \varphi \leftrightarrow @_i \forall p \varphi$ . Its $\exists$ -form is $@_i \exists p \varphi \leftrightarrow \exists p @_i \varphi$ . Strictly speaking, the left-to-right arrows of both forms are Barcan formulas, while the right-to-left directions of both are converse Barcan formulas.

5. Pure Completeness

We will now extend a standard model-building strategy used to prove the strong completeness of $\textbf {K}_{h}+{{RULES}}$ (Chapter 7, Section 3 of Blackburn et al. Reference Blackburn, de Rijke and Venema2001) to show that every $\textbf {K}_{PIL}$ -consistent set of formulas has a general model. The general model we shall construct has a number of special properties (described below) which will enable us to prove strong completeness not only for $\textbf {K}_{PIL}$ itself, but for all of its pure extensions as well.

The $\Delta _i$ in this lemma are called the named sets yielded by $\Gamma$ . Clause 1 of the previous lemma tells us that each of these is a MCS containing at least one nominal; all of these MCSs are ‘hidden inside’ the original $\textbf {K}_{h}$ -MCS. Clause 2 tells us that each nominal picks out a unique such MCS, and Clause 3 tells us that any satisfaction statement is either in all the $\Delta _j$ or in none of them. So every $\textbf {K}_{h}$ -MCS contains almost all that is required to build structures in which every world is named by some nominal. But not quite. Note that Clause 4 is only a conditional – we have no guarantee that $\Gamma$ itself is one of the MCSs ‘hidden inside’ $\Gamma$ .

Indeed, this weakness in Clause 4 is the key reason for using $\textbf {K}_{h}$ $+$ RULES instead of $\textbf {K}_{h}$ . The addition of the NAME and PASTE rules does allow us to guarantee that $\Gamma$ itself is one of the MCSs ‘hidden inside’ $\Gamma$ . This will let us create a ‘named and pasted’ MCS, which contains all the information required to build a frame in which each world is named by a nominal, which will prove crucial for the pure extensions completeness result. Furthermore, the axioms and rules for propositional quantification in $\textbf {K}_{PIL}$ also ensure that this MCS is ‘witnessed’, which allows us to define a suitable set of admissible propositions over its frame, thereby creating a general model. We first define what we mean by ‘named’, ‘pasted’ and ‘witnessed’ and then prove the Lindenbaum-style lemma which will lead us to these goals.

To prove a Lindenbaum-style lemma for K $_{PIL}$ , we must extend the language. Suppose we start with language $\mathcal { L}$ . We will add a countably infinite set of nominals (called NewN) and a countably infinite set of new propositional variables (called NewL), and call the extended language $\mathcal { L}'$ . We will use NewN for naming and pasting and NewL for witnessing.

We now check that this definition does indeed give rise to Kripke frames and general models where every world is named by some nominal.

So from now on we will call $\langle W^{\Gamma },R^{\Gamma }\rangle$ the canonical named Kripke frame yielded by $\Gamma$ , and $\mathcal {M}^{\Gamma }$ the canonical named general model yielded by $\Gamma$ . We now examine them more closely. Our first lemma tells us that $R^{\Gamma }$ works exactly as it does in ordinary propositional modal logic.

Next for a simple but important lemma:

The previous lemma is important because it gives us a syntactic handle on the elements of $\Pi ^{\Gamma }$ : every proposition in $\Pi ^{\Gamma }$ is ‘picked out’ by some soft-QDF formula; this syntactic characterisation enables us to prove the final lemma leading to completeness.

Proof. For any formula $\varphi$ , let $ \textit {con}(\varphi )$ be the number of connectives in $\varphi$ . Moreover, let $\textit {quan}(\varphi )$ be the maximal depth of quantifier nesting in $\varphi$ , that is:

\begin{equation*} \begin{array}{c} \textit {quan}(\varphi ) = \left \{ \begin{array}{ll} 0 & \mbox {if } \varphi \mbox { is atomic} \\ \textit {sup} \{ \textit {quan}(\psi ), \textit {quan}(\theta ) \} & \mbox {if } \varphi = \psi \wedge \theta \\ \textit {quan}(\psi ) & \mbox {if } \varphi \in \{ \neg \psi , @_{i} \psi , \square \psi , A \psi , \downarrow \! i \psi \} \\ \textit {quan}(\psi ) + 1 & \mbox {if } \varphi = \forall p \psi \end{array} \right . \end{array} \end{equation*}

We prove the result by induction on pairs $(\textit {quan}(\varphi ),\textit {con}(\varphi ))$ ordered lexicographically, that is, $(b',c') \lt (b,c)$ iff (1) $b'\lt b$ or (2) $b'=b$ and $c'\lt c$ .

Note that Lemma 28 has established this for all formulas $\varphi$ associated with the pair $(0,0)$ (i.e., atomic formulas) and indeed for all formulas associated with pairs $(0,n)$ for any natural number $n$ (i.e., all quantifier-free formulas). So the base cases are established. As our inductive hypothesis (IH) we assume that for natural numbers $q$ and $c$ , we have that $\mathcal {M}^{\Gamma } , u\models \varphi$ iff $ \varphi \in u$ for all formulas $\varphi$ associated with pairs $(b',c') \lt (b,c)$ .

We proceed case by case. If $\theta$ is a Boolean formula, or of the form $\Box \psi$ , $A\psi$ , $@_{i}\psi$ or $\downarrow \! i \psi$ , we can argue as in Lemma 28, where we use our new IH just as before to formulas associated with pairs $(b,c')$ such that $c'\lt c$ . The critical case is where $\theta$ is of the form $\forall p\psi$ .

We want to show that $\mathcal {M}^{\Gamma }, u\models \forall p\psi$ iff $\forall p\psi \in u$ . For the left-to-right direction, we show the contrapositive. So suppose that $\forall p\psi \not \in u$ . As $u$ is an MCS, $\neg \forall p\psi \in u$ , that is, $\exists p\neg \psi \in u$ . The MSC $\Gamma$ is witnessed, so for some propositional variable $q$ , $@_j \neg \psi [q/p] \in \Gamma$ . But then $\neg \psi [q/p] \in \Delta _j$ . But $\neg \psi [q/p] \in \Delta _j$ is associated with $(b-1,c)$ , so the IH applies and we have $\mathcal {M}^{\Gamma },u\models \neg \psi [q/p]$ . It follows from the Substitution Lemma that $\mathcal {M}, u\models \neg \psi$ where $\mathcal {M}=\langle W^{\Gamma },R^{\Gamma }, \Pi ^{\Gamma }, N^{\Gamma }, V\rangle$ such that $V \sim _p V^{\Gamma }$ is defined by setting $V(p)= [\mathcal {M}^{\Gamma }]_{q}$ . Hence, $\mathcal {M}, u\not \models \psi$ . It follows that $\mathcal {M}^{\Gamma }, u\not \models \forall p \psi$ , and we have proved the contrapositive.

For the right-to-left direction, suppose that $\forall p\psi \in u$ , and further suppose for the sake of contradiction that $\mathcal {M}^{\Gamma }, u\not \models \forall p \psi$ . Then for some $V \sim _p V^{\Gamma }$ we have $\mathcal {M}, u\models \neg \psi$ where $\mathcal {M}=\langle W^{\Gamma },R^{\Gamma }, \Pi ^{\Gamma }, N^{\Gamma }, V\rangle$ . Now $V(p) \in \Pi ^{\Gamma }$ , but by Lemma 29 we know $\Pi ^{\Gamma } = [\mathcal {M}^{\Gamma }] ^{\textit {sqf}}$ , hence $V(p) = [\mathcal {M}^{\Gamma }]_{\theta }$ for some soft-QDF formula $\theta$ . The Substitution Lemma tells us that $\mathcal {M}^{\Gamma }, u\models \neg \psi [\theta /p] \textit { iff } \mathcal {M},u \models \neg \psi$ , and hence we have $\mathcal {M}^{\Gamma }, u\models \neg \psi [\theta /p]$ . As $\neg \psi [\theta /p]$ is associated with the pair $(b-1,c')$ for some $c'$ , we can apply the IH to conclude $\neg \psi [\theta /p] \in u$ . But this leads to a contradiction. As $u$ is a MCS, for all soft-QDF formulas $\xi$ , we have $\psi [\xi /p] \in u$ by the Q2-sqf axiom. In particular, $\psi [\theta /p] \in u$ . We conclude that $\mathcal {M}^{\Gamma }, u\models \forall p \psi$ after all.

So we have proved the basic strong completeness result. But the general model we have built is named, so we can immediately extend this to cover all pure extensions of $\textbf {K}_{PIL}$ . In hybrid logic, a formula is called ‘pure’ if all its atomic subformulas are nominals. Here are three well-known examples: $i\rightarrow \Diamond i$ (the Irreflexivity axiom), $i \rightarrow \Box (\Diamond i \rightarrow i)$ (the Antisymmetry axiom), and $@_i \Diamond j \vee @_i j \vee @_j \Diamond i$ (the Trichotomy axiom). A pure formula $\varphi$ defines a class of frames $\mathsf {F}$ iff: $(W,R) \in \mathsf {F} \Leftrightarrow (W,R)\models \varphi$ . It is easy to check that our three examples define the class of irreflexive, antisymmetric, and trichotomous frames respectively. More importantly: adding any (combination of) pure formula(s) as extra axiom(s) to $\textbf {K}_{h}+{{RULES}}$ is a proof system that is complete with respect to the class of frames defined. For a more detailed statement and discussion of this result, see Blackburn and ten Cate (Reference Blackburn and ten Cate2006). Here we shall simply record that:

Let us look at an example using $\downarrow$ . As a first step, let $\Lambda = \{ i\rightarrow \neg \Diamond i, \Diamond \Diamond i \rightarrow \Diamond i\}$ . These two formulas jointly define the class of strictly partially ordered frames: $i\rightarrow \neg \Diamond i$ defines irreflexivity, and $\Diamond \Diamond i \rightarrow \Diamond i$ defines transitivity, so adding them as axioms to $\textbf {K}_{PIL}$ gives us the complete logic of this frame class. But suppose we want to work with confluent strictly partially ordered frames. Confluence means that ‘any two successors of a given world share a common successor world’. This property is not definable using a basic pure formula (see Proposition 4.2.11 in Ten Cate Reference Ten Cate2005) but it can be defined using the following strong pure formula:

\begin{equation*}@_i \wedge @_j \rightarrow \Diamond (i \wedge \Diamond \downarrow k @_j \Diamond k)). \end{equation*}

This says: ‘if the world at which we are evaluating has successors $i$ and $j$ , then there is a successor state of $i$ – call it $k$ – such that $k$ is also a successor to $j$ ’. So adding this as a third axiom yields the logic of confluent strictly partially ordered frames.

6. Prior’s Ideal Language

Having proved Theorem 5, pure completeness for $\textbf {K}_{PIL}+\Lambda$ , we are in a better position to explain why we called this system ‘Prior’s Ideal Language’. First some historical background.

Arthur Prior was a philosophical logician, best known as the inventor of tense logic (see Copeland Reference Copeland and Zalta2017; Øhrstrøm and Hasle Reference Øhrstrøm and Hasle2007). However he also invented hybrid logic (see Blackburn Reference Blackburn2006; Braüner Reference Braüner and Zalta2021), and routinely used propositional quantification throughout his career. Shortly before his death in 1969, Prior began to explore such ideas as ‘quasi-modalities’ and developed a system he called ‘egocentric logic’. With the benefit of hindsight, it is now clear that egocentric logic was an early example of the description logics that would become popular in computer science in the 1980s. Such investigations lead him to start rethinking the boundaries between logics of time, worlds, and individuals, but this last phase of his work remains little known and under-discussed.Footnote ⁵ We believe that PIL provides an excellent setting for exploring Prior’s work, and in particular the work from this period. We now explain why.

First, PIL is a general tool. In this paper, our basic hybrid language contained only one box-diamond pair, $\Box$ and $\Diamond$ . But the results of this paper, and in particular Theorem 5, generalise straightforwardly to basic hybrid languages containing multiple modalities. Actually, our treatment of the universal modality pretty much shows how to do this. Recall from Definition 14 that we axiomatised $A$ by insisting that it had the same basic axioms and rules as $\Box$ and then adding the pure axiom

\begin{equation*}Ei\end{equation*}

which tells us what is special about the universal modality (namely that it sees every world/time/individual). We can extend this strategy to as many box-diamond pairs $\Box _m$ and $\Diamond _m$ as we like. We simply add them to the basic hybrid language, interpret each by its own relation $R_m$ on $W$ , let each of these modalities mirror the same logic as $\Box$ , and then add extra pure axioms to shape them to our needs.Footnote ⁶

For example, if we want a Prior-style tense logic, we could start with a basic hybrid language containing the pairs $G$ and $F$ , and $H$ and $P$ , interpret these by relations $R_G$ and $R_H$ . To axiomatise this, we would give each of these the logic of $\Box$ , exactly as in Definition 14, and also add the following two pure axioms:

\begin{equation*}i \rightarrow HFi \, \, \, \, \, \, \, \, \, \, \, \, \, \, i\rightarrow GPi.\end{equation*}

These guarantee that $R_G$ and $R_H$ are converse relations, thus we have a tense logic: paired operators that look forward and backward along the same relation.

It was sometime during the late 1960s that Prior had the insight that led him to rethink the boundaries between logics of time, worlds, and individuals. An unexpected result of his successful investigation of strong hybrid logic in the setting of tense logic, was the realisation – which anticipated a major theme of the Amsterdam-style modal logic by more than 20 years – that modalities could be used to talk about absolutely anything. Modal logic was not just a tool for reasoning about abstract entities like possible worlds and times, it could be applied to everyday objects as well. This shift in Prior’s thinking was clearly and dramatically marked in a remarkable pair of papers, namely ‘Tense logic and the logic of earlier and later’, and ‘Quasi-propositions and quasi-individuals’, both of which can be found in the first edition of Papers on Time and Tense; Prior (Reference Prior1968).Footnote ⁷ Egocentric logic was introduced in ‘Quasi-propositions and quasi-individuals’, and is an early example of what is computer scientists now call description logic (see Baader et al. Reference Baader, Calvanese, McGuinness, Patel-Schneider, Nardi and Schneider2003): it is a modal logic, indeed a hybrid logic, for reasoning about people.Footnote ⁸ In Prior’s egocentric logic, the ‘worlds’ are people and their properties and relationships (e.g., their relative heights) are described using what Prior called ‘quasi modalities’ such as $[\textit {taller}]$ , $\langle \textit {taller}\rangle$ , $[\textit {shorter}]$ and $\langle \textit {shorter}\rangle$ .Footnote ⁹ Prior talks about ‘people propositions’ (nominals), and makes use of the universal modality, quantification over nominals, and propositional quantification. It is an important paper, and set the agenda for the final phase of his work.

Egocentric logic is something that PIL can deal with; indeed, egocentric logic was a major motivation for PIL. As we have already noted, PIL can handle multiple modalities such Prior’s $[\textit {taller}]$ and $[\textit {shorter}]$ ; a pure axiomatisation that captures Prior’s egocentric logic of relative heights can be found in Kofod (Reference Kofod2022). More generally, we are interested in reviving Prior’s project of rethinking the boundaries between logics of time, worlds, and individuals. There are interesting connections to be made with description logic here, and perhaps with other logics for knowledge representation too; for example Belardinelli et al. (Reference Belardinelli, Van Der Hoek and Kuijer2018) recently suggested that epistemic logic augmented with propositional quantifiers was useful for reasoning about knowledge in AI.

A second reason we think that PIL is a useful setting for exploring Prior’s work because it offers a powerful – yet nuanced – form of expressivity. How powerful? Well, we said that the strong component of PIL was $A$ and $\downarrow$ . But this is not exactly the way Prior did it: he allowed direct quantification over nominal. That is, Prior used expressions like

\begin{equation*}\forall i (i \rightarrow \neg \Diamond i).\end{equation*}

Note that this is universal closure of the pure axiom for irreflexivity. So, if we place the universal $A$ in front of it we get

\begin{equation*}A\forall i (i \rightarrow \neg \Diamond i)\end{equation*}

a statement which is true only in models where every point is irreflexive. So it is fairly easy to say how powerful Prior’s version of strong hybrid logic is: it allows us to capture ‘full first-order classical quantification’ over the elements of $W$ . Prior himself knew this in the late 1960s: he showed that his strong language captured the UT-calculus, which is essentially what modal logicians would nowadays call the first-order correspondence language; see Blackburn (Reference Blackburn2006) for further discussion and Blackburn and Seligman (Reference Blackburn and Seligman1995) for relevant technical results.

But the PIL approach is as powerful as Prior’s. First, given Prior’s language, we can define $\downarrow$ as follows:

\begin{equation*}\downarrow \! i \varphi := \exists i (i \wedge \varphi ).\end{equation*}

Note that this translation reveals the hidden nominal in formula position that motivates the ‘D’ in ‘soft-QDF’. On the other hand, using PIL we can define Priors direct quantification over nominals as follows:

\begin{equation*}\exists i \varphi := \downarrow \! j E \! \downarrow \! i E(j \wedge \varphi ).\end{equation*}

So the approaches are expressively equivalent. But we like the locality of $\downarrow$ . Prior himself emphasised the locality of modal logic, and although he did not isolate downarrow, he came close: for example, he drew attention to the strong validity $\exists i i$ , ‘some proposition is true right here and now’. For example, this formula is axiom T9 in the paper ‘Tense logic and the logic of earlier and later’. Furthermore, expressing $\exists i \varphi$ as $\downarrow \! j E \! \downarrow \! i E(j \wedge \varphi )$ breaks down the classical quantifier in a suggestive way: it decomposes it into global search for truth (using $E$ ) combined with local binding (using  $\downarrow$ ). Finally, the fragment of strong hybrid logic containing $\downarrow$ and $@$ (but without $A$ ) has turned out to be important: it is equivalent to the bounded fragment of first-order logic, and gives rise to general interpolation results for many forms of hybrid logic (see Areces et al. Reference Areces, Blackburn and Marx2001). Indeed, this fragment even turns out to have an unexpected link with propositional quantification. Every formula of modal logic with propositional quantifiers (interpreted over standard models) expresses a second-order property. Some of these properties don’t have first-order equivalents, but many important ones do. Balder ten Cate showed that every such elementary property is equivalent to a sentence of $\downarrow$ and $@$ ; see (see Theorem 12.0.3, p. 179, in Ten Cate Reference Ten Cate2005). Note that Ten Cate’s result shows that Theorem 5, the pure completeness theorem for $\textbf {K}_{PIL}+\Lambda$ , covers all elementary frame classes definable in modal logic with propositional quantifiers under the standard interpretation. In short, both conceptually and technically, PIL embodies ideas that seem relevant to a deeper and more nuanced technical understanding of Prior’s later work.

Our third and final point concerns propositional quantification. As we have mentioned, Arthur Prior was an ‘early adopter’ of propositional quantifiers in modal logic (see, in particular, Prior Reference Prior1958, Reference Prior1961), and his students Robert Bull and Kit Fine both published important technical papers of the subject (see Bull Reference Bull1969 and Fine Reference Fine1970). But Arthur Prior was also the inventor of hybrid logic, and these two interests became intertwined. For much of his career, Prior had oscillated between two views of nominals: we call these his ‘tag’ view and his ‘telescope’ view. The ‘tag’ view is standard in contemporary hybrid logic, and that is the way we presented nominals in this paper: nominals are ‘labels’ or ‘indices’ or ‘0-place world identifying modalities’. However, when he adopts the ‘telescope’ view, Prior speaks of nominals identifying worlds, times or individuals by means of content. As he puts it in his paper ‘Tense Logic and the Logic of Earlier and Later’, nominals combine ‘all those propositions which would ordinarily be said to be true’ at that world, time or individual. He seemed to view this combination as being something like the infinite conjunction of all the relevant propositions describing that world, time or individual.

And here propositional quantifiers enter the picture in an interesting way. Sometimes Arthur Prior introduced nominals not as a second sort of primitive propositional symbol, but as an ordinary propositional variables preceded by the $Q$ operator, and he spelt out what $Qp$ meant using propositional quantifiers:

\begin{equation*} Qp = E p \wedge \forall q (A (p \rightarrow q) \vee A (p \rightarrow \neg q)) \end{equation*}

(Prior uses the symbols $\Box$ and $\Diamond$ , rather than $A$ and $E$ , in this definition. But it is clear that he is using what is nowadays called the universal modality.) In particular, he defines nominals using the $Q$ -operator in both ‘Quasi-propositions and quasi-individuals’ and the later and more detailed ‘Egocentric Logic’ in both papers it seems pretty clear that he views $Q$ as giving rise to the tag interpretation. And this is correct: under the standard interpretation of propositional quantification, this definition of $Q$ makes a ‘nominal’ defined by the formula $Qp$ true at a unique element of $W$ , that is, $Qp$ says that $p$ is true somewhere and that $p$ strictly implies every proposition $q$ or its negation (read $A (p \rightarrow q)$ as ‘ $p$ is included in $q$ ’). More interestingly, however, is that under the general interpretation of propositional quantification, $Qp$ does not say that $p$ is true at a unique element of $W$ , but rather that $p$ is true at exactly the elements of some atom, that is, a non-empty minimal admissible subset. Thus, $p$ is true at the elements of an atom belonging to ‘all those propositions which would ordinarily be said to be true’. So $Qp$ read in this way can be thought of identifying worlds, times and individuals via descriptions, via content. It is a tool for making telescope nominals.

Thus, PIL offers access to both tag and telescope nominals. The tag nominals are built into the basic syntax of PIL, and together with the satisfaction operators and downarrow binder which manipulate them, they give rise to many strong ‘logics of indices’, as Theorem 5 testifies. But, in parallel to this, we can also define ‘telescope nominals’ of the form $Qp$ , at least when working with the general frame semantics of this paper.