Notes on Some Ideas in Lloyd Humberstone’s Philosophical Applications of Modal Logic


Lloyd Humberstone’s recently published Philosophical Applications of Modal Logic presents a number of new ideas in modal logic as well explication and critique of recent work of many others. We extend some of these ideas and answer some questions that are left open in the book.

Steven Kuhn (Georgetown University) , Brian Weatherson (University of Michigan)
April 14 2018

Lloyd Humberstone’s recently published Philosophical Applications of Modal Logic (Humberstone (2016)) presents a number of new ideas in modal logic as well explication and critique of recent work of many others. In this note we extend some of these ideas and answer some questions that are left open in the book. Numbers without other identification refer to pages in that book.

Local and Global Conditions

One theme sounded frequently in Humberstone (2016) is the relation between a local condition, which describes a point in a frame and a global condition, which concerns the frame as a whole. For example, the local conditions of being reflexive (\(Rxx\)) and being reflexive with reflexive successors (\(Rxx \land \forall y(Rxy \rightarrow Ryy)\)) are distinct, but their universal possession by the points in a frame describes the same global condition of reflexivity. As a consequence, the non-equivalent modal axioms \(\Box p\rightarrow p\) and \((\Box p\rightarrow p) \land \Box(\Box q\rightarrow q)\) both define the class of reflexive frames. This example leads Humberstone to ask (189) whether there is a local property not implying that a point possessing it is reflexive whose universal possession makes the frame reflexive. Affirmative answers are supplied by the following formulas: \(\forall y(y{=}x\wedge Rxx) \vee (\exists y(y\ne x) \wedge \forall y(y\ne x \rightarrow Ryy))\) (either x is the only world and it is reflexive or else there are other worlds, all of which are reflexive), and \(\exists zRxz \wedge \forall z(Rzx \rightarrow Rzz)\) (x has a successor and every world that can see x is reflexive). The second example implies that the tense-logical formulas \({\mathbf{F}}\top \wedge \mathbf{H}(\mathbf{G}p\rightarrow p)\) and \(\mathbf{G}p\rightarrow p\) both define the class of reflexive frames.

Fully Modalized Logics

Another topic that gets well-deserved attention in Humberstone (2016) is the property of logics that Humberstone calls being “fully modalized.” (See 290-304.) The idea is that in alethic modal systems the axiom \(\Box A\rightarrow A\) provides a logical connection between the modal and nonmodal formulas, whereas in a doxastic or deontic logic we expect that matters concerning what is believed or what ought to be the case should be logically independent of those concerning what is the case. The latter, but not the former, are fully modalized. But the idea needs to formulated with some care because we don’t want the presence of, for example, \(A\rightarrow \Box \top\) as a theorem to count against a logic’s being fully modalized. As Humberstone puts it, in a fully modalized logic, “…we don’t expect…the forging of any…logical connections between \(\Box A\) and \(A\) for any given \(A\) – other than those which hold…derivatively” (291). The notion is captured in a rather complicated way by E. Zolin in Zolin (2000) and Humberstone shows that the characterization there is equivalent to the following simpler one: if there is a theorem of the form \(M\vee N\) where \(M\) is fully a fully modalized formula (i.e., containing no sentence letters not within the scope of a modal operator) and \(N\) is non-modal (i.e., containing no occurrences of modal operators) then either \(M\) or \(N\) is itself a theorem. In this section we show that Zolin’s characterization is also equivalent to an even simpler one that is closer in spirit to the motivating remarks in Humberstone (2016): every theorem is a tautological consequence of a fully modalized theorem. (Thus the theorems can be divided into two categoriesthe essentially nonmodal ones, i.e., the tautologies, and the essentially modal ones, i.e., the non-tautologies that are tautological consquences of fully modalized theorems).

We begin by restating Zolin’s definition in our own terminology. If \(p_1,{\ldots},p_n\) are sentence letters, then a state description in \({p_1,{\ldots},p_n}\) is a conjunction \(p_1^*\wedge {\ldots}\wedge p_n^*\), where, for \(1\le i\le n, p_i^*\) is either \(p_i\) or \(\neg p_i\). The (truth-functional) constituents of a formula \(A\) are the sentence-letters and \(\Box\)-formulas occurring in \(A\) that do not properly occur within the scope of any \(\Box\). Zolin observes that every formula \(A\) can be “decomposed” into a formula of the form \({\bigvee}\{(\vec{p}\wedge B(\vec{p}))\!:\vec{p}\) is a state description in the sentence letter constituents of \(A\)}, where, for each \(\vec{p}\) , \(B(\vec{p})\) is some truth functional combination of the modal constituents of \(A\). By fixing on a particular ordering of formulas and taking the \(B(\vec{p})\)’s to be in a disjunctive normal form that conforms to this ordering, we can single out a unique decomposition of this kind. Let’s call it the Zolin form of \(A\) and let’s call the formulas \(B(\vec{p})\) that occur as right conjunct of a disjunct in the Zolin form of \(A\), the Zolin components of \(A\). Note that every formula is truth-funtionally equivalent to its Zolin form. Then, according to Zolin’s definition, a logic is fully modalized if \(\vdash A\) implies \(\vdash B(\vec{p})\) for every \(B(\vec{p})\) that is a Zolin component of \(A\).

Theorem 1. A logic L is fully modalized (according to Zolin’s definition) iff every theorem of L is a tautological consequence of a fully modalized theorem.

Proof. (Left to right). Suppose L satisfies Zolin’s definition and \(\vdash_L A\). Let \((\vec{p}_1\wedge B(\vec{p}_1))\vee {\ldots}\vee (\vec{p}_n\wedge B(\vec{p}_n))\) be the Zolin form of \(A\). Then, according to Zolin’s definition, \(\vdash_L B(\vec{p}_i)\) for each \(i\), \(1\le i\le n\). Let \(A^\prime = B(\vec{p}_1)\wedge {\ldots}\wedge B(\vec{p}_n)\). \(A^\prime\) is fully modalized and, since each of its conjuncts is provable in L, \(A^\prime\) is as well. All that remains is to show that \(A\) is a truth-functional consequence of \(A^\prime\). Let \(\alpha\) be any assignment of truth values to the constituents of \(A\) such that \(\alpha\models A^\prime\). Let \(\vec{p}_\alpha\) be the state description in the sentence letters that are truth-functional constiuents of \(A\) that corresponds to \(\alpha\) in the sense that each conjunct of \(\vec{p}_\alpha\) is the literal \(p\) or \(\neg p\) according to whether \(\alpha(p)\) is true or false. Then \(\alpha\) verifies \((\vec{p}_\alpha \wedge B(\vec{p}_\alpha))\), which is a disjunct of \(A\) and so \(\alpha\models A\) as required.

(Right to left). We are given that every theorem of L is a tautological consequence of some fully modalized theorem. Now suppose \(\vdash_L A\) and \(B(\vec{p})\) is a Zolin component of \(A\), with a view towards showing \(\vdash_L B(\vec{p})\). By the initial suppositions, \(A\) is a truth-functional consequence of some fully modalized formula \(A^\prime\). Then the Zolin form of \(A\), call it \((\vec{p}_1\wedge B(\vec{p}_1))\vee {\ldots}\vee (p_n\wedge B(\vec{p}_n))\), is also a truth functional consequence of \(A^\prime\), where for some \(i\), \(1\le i\le n\), \(B(\vec{p}_i)=B(\vec{p})\). We show that \(B(\vec{p})\) is provable in L by showing that it is also a truth-functional consequence of the theorem \(A^\prime\). To that end, let \(\alpha\) be any assignment of truth values to the constituents of \(A\), such that \(\alpha\models A^\prime\). Since \(A^\prime\) is fully modalized, its truth value under an assignment is not affected by the truth assignments to sentence letters, so we can assume without loss of generality that these conform to the state description . Since the disjunction \((\vec{p}_1\wedge B(\vec{p}_1))\vee {\ldots}\vee (\vec{p}_n\wedge B(\vec{p}_n))\) is a truth functional consequence of \(A^\prime\), \(\alpha\) must verify this disjunction. But \(\vec{p}_1,{\ldots},\vec{p}_n\) are state descriptions, so \(\alpha\) can verify only one disjunct of this formula, namely \(\wedge B(\vec{p})\). Hence \(\alpha\models B(\vec{p})\) as required. ◻

It is possible that there are applications for which Zolin’s more detailed normal-form characterization of a fully modalized logic is more useful than the simple characterization given here. But the proof below shows that property that Humberstone extracts in Humberstone (2016) can be proved at least as easily from our simple characterization.

Theorem 2. Suppose every theorem of L is a tautological consequence of a fully modalized theorem. Then \(\vdash_LM\vee N\) where \(M\) is fully modalized and \(N\) is modality-free implies either \(\vdash_LM\) or \(\vdash_LN\).

Proof. Assume the hypothesis of the claim and \(\vdash_LM\vee N\) for appropriate \(M\) and \(N\). Then there is some fully modalized L-theorem \(A^\prime\) such that \(M\vee N\) is a truth functional consequence of \(A^\prime\). Suppose for reductio that neither \(M\) nor \(N\) is provable. Then neither \(M\) nor \(N\) is a truth functional consequence of \(A^\prime\). So there is an assignment \(\alpha\) of truth values to the constituents of \(A^\prime\) and \(M\) that makes the former true and the latter false. Similarly, there is an assignment \(\beta\) to the constituents of \(A^\prime\) and \(N\) that makes \(A^\prime\) true and \(N\) false. Now extend the assignment \(\alpha\) to the sentence letters in \(N\) by assigning them the same truth values as \(\beta\) does, and call the result \(\alpha^\prime\). Since \(\alpha^\prime\) agrees with \(\alpha\) on the modal constituents it verifies \(A^\prime\) and falsifies \(M\). Since it agrees with \(\beta\) on sentence letters, it falsifies \(N\). This contradicts the earlier observation that \((M\vee N)\) is a truth functional consequence of \(A^\prime\). ◻

“Nothing in Between” and the Equivalence of Modal Logics

The impetus for Section 4.4 of Humberstone’s book (304-324) is Arthur Prior’s observation that the logical structure of moral concepts appears to be unlike those of quantity and alethic modality:

In between “S must be P” and “S may be P” stands the simple “S is in fact P,” just as “This S is P stands in between”Every S is P and “Some S is P.” … But so far as I can see there is nothing among the moral or ‘deontic’ modalities that corresponds to these intermediary ‘existential’ or ‘alethic’ modalities. (Prior (1951) p145, quoted on 304 in Humberstone (2016).)

Early in the section,Humberstone notes that, in fact, there are strict logical intermediaries between “\(A\) is obligatory” and “\(A\) is permitted” or indeed between any sentences \(A\) and B of decreasing logical strength in any reasonably well behaved modal logic, whether their connectives are given a deontic reading or any other. For one can simply take as intermediary, any formula \(A\vee (B\wedge p)\) where \(p\) is a sentence letter that does not occur in \(A\) or \(B\). In this section we wish to point out that a consequence of this observation is that there is a sense in which all modal logics meeting certain minimal requirements are the same.

We identify a “logic” with a many-one deducibility relation on formulas satisfying the usual structural conditions. (So the logic with all tautologies as axioms and no rules of inference is distinct from a similar logic with modus ponens as a rule of inference.) The minimal requirements are just that logics are classically based and substitution-closed.By classically based we mean that their languages contain the Booleanconnectives (or at least some truth-functionally complete subset thereof) and that these behave classically under the deducibility relation, so that, for example \(A \wedge B \vdash C\) iff \(A \vdash (B \rightarrow C)\).1 If a logic is classical, we may safely identify it with the set of its theorems, knowing that these will determine the deducibility relation. By substitution-closed we mean that \(A_1^\prime,{\ldots},A_n^\prime \vdash B^\prime\) whenever \(A_1^\prime,{\ldots},A_n^\prime\) and \(B^\prime\) are the result of uniformly replacing sentence letters by formulas in \(A_1,{\ldots},A_n\) and \(B\) such that \(A_1,{\ldots},A_n \vdash B\). The requirement that the logic is classically based ensures that \(A\vee (B\wedge p)\) is a logical intermediary between \(A\) and \(B\). The requirement that it is substitution-closed implies that it is a strict intermediary. For if it provably implied \(A\), then its substitution instance \(A\vee (B\wedge B)\) would provably imply \(A\), and \(A\) would be provably equivalent to \(B\). And if it was provably implied by \(B\), then \(A\vee (B\wedge A)\) would be provably implied by \(B\) and again \(A\) would be equivalent to \(B\). By saying that these logics are the same we mean something close to what is sometimes called translationally equivalent.2 Let us say that logics \(L_1\) and \(L_2\) are weakly translationally equivalent if there is a map \(s\colon A{\mapsto}A^s\) from formulas of \(L_1\) to formulas of \(L_2\) and a map \(t\colon C{\mapsto}C^t\) from formulas of \(L_2\) to formulas of \(L_1\) satisfying the following conditions (where \(\vdash_i\) is \(\vdash_{L_i}\) for \(i=1,2\)):

  1. \(A_1,{\ldots},A_n \vdash_1 B\) implies \({A_1}\!^s,{\ldots},{A_n}\!^s \vdash_2 B^s\)

  2. \(C_1,{\ldots},C_m \vdash_2 D\) implies \({C_1}^t,{\ldots},{C_m}^t \vdash_1 D^t\)

  3. \(A ~_1\!{\dashv}{\vdash}\!_1 (A^s)^t\)

  4. \(C ~_2\!{\dashv}{\vdash}\!_2 ~ (C^t)^s\).

\(s\) and \(t\) are to be thought of as translations between the logics. If \(L_1\) and \(L_2\) are weakly translationally equivalent then the word implies in i and ii can be strengthened to if and only if, so that \(s\) and \(t\) are faithful embeddings. For example, by condition ii, \({A_1}^s,{\ldots},{A_n}^s \vdash_2 B^s\) implies \(({A_1}^s)^t,{\ldots},({A_n}^s)^t \vdash_1({B^s})^t\), and so, by condition iii \(A_1,{\ldots},A_n \vdash_1 B\). But the strengthened versions of i and ii still do not imply iii and iv. (See, for example, French (2010) pp 111-124.) \(L_1\) and \(L_2\) are said to be translationally equivalent if the translations securing their weak equivalence meet some additional requirement, commonly that they be compositional, i.e., that they be maps \(f\) such that for every n-ary connective \(\#\) in the source language there is formula schema \(\sigma\) of the target language with \(n\) schematic variables such that \(f(\#A_1{\ldots}A_n)=\sigma(f(A_1),{\ldots},f(A_n))\). If we are interested in what can be said within a logic rather than the structure of the formulas saying it, however, the restriction to compositional translations seems unwarranted. A translation can be “sentence by sentence” rather than “symbol by symbol.” It is plausible to take formulas to be saying the same thing in a logic when they are provably equivalent. In that case the structure of the things that can be said in a logic is given by its Lindenbaum lattice. By this, we mean the structure \((X,\le )\) where the members of X are the equivalence classes \([A]_L\) of formulas \(A\) under the relation \(_L\!{\dashv}{\vdash}\!_L~\) and \([A]_L\le [B]_L\) iff \(A\vdash \!_LB\). In that case, we may say that two logics are the same with regards to what they can say if their Lindenbaum lattices are isomorphic. It is not difficult to show that under conditions of interest here, this condition coincides with weak translational equivalence.

Theorem 3. (i) If \(L_1\) and \(L_2\) are weakly translationally equivalent then they have isomorphic Lindenbaum lattices. (ii) If \(L_1\) and \(L_2\) are classically based and they have isomorphic Lindenbaum lattices then they are weakly translationally equivalent.

Proof. Here and below, we drop the subscripts from the brackets and turnstile symbols, when the logic is intended is clear. To prove i, suppose \(s\) and \(t\) satisfy conditions i-iv defining weak translational equivalence. Let \(\Phi([A])=[A^s]\). We show that \(\Phi\) is an isomorphism. i)\(\Phi\) is well defined. Suppose \([A]=[B]\). Then \(A{\dashv}{\vdash}B\). By condition i, this implies \(A^s{\dashv}{\vdash}B^s\). Hence \([A^s] = [B^s]\) and \(\Phi([A])=\Phi([B])\), as required. ii)\(\Phi\) is 1-1. Suppose \(\Phi([A])=\Phi([B])\). Then \([A^s]=[B^s]\) and so \(A^s{\dashv}{\vdash}B^s\). By condition ii, \((A^s)^t{\dashv}{\vdash}(B^s)^t\). By condition iii, \(A{\dashv}{\vdash}B,\) and so \([A]=[B]\), as required. iii)\(\Phi\) is onto. Take any \(C\) in the language of \(L_2\). By condition iv, \(C{\dashv}{\vdash}(C^t)^s\). Hence \([C] = [(C^t)^s]\). Therefore \([C]=\Phi([C^t])\), and \([C]\) is in the range of \(\Phi\), as required.

The proof of ii is facilitated by a lemma. Let us say that a translation \(f\colon A{\mapsto}A^f\) conforms to falsum if \(\bot^f {\dashv}{\vdash} \bot\); to negation if \((\neg A)^f {\dashv}{\vdash} \neg A^f\); to conjunction if \((A\wedge B)^f {\dashv}{\vdash}A^f \wedge B^f\) and similarly for all the other Boolean connectives. To prove part ii of the theorem, we use only that \(s\) and \(t\) conform to conjunction, but we take the opportunity to prove something more general.

Lemma 1. Suppose \(s\) and \(t\) are translations securing the weak equivalence of classically based modal logics \(L_1\) and \(L_2\). Then \(s\) and \(t\) conform to all the Boolean connectives.

Proof. . Suppose \(s\) and \(t\) satisfy the hypothesis of the lemma. We show that \(s\) and \(t\) conform to falsum (i) and the conditional (ii) and that it follows that they conform to all the other Boolean connectives (iii).

\(i\) (We include the subscripts for clarity here.) Since \(L_1\) and \(L_2\) are classically based, \(\bot\vdash_2 \bot^s\) and \(\bot \vdash_1 \bot^t\). From the second of these it follows that \(\bot^s \vdash_2 (\bot^t)^s\), and therefore that \(\bot^s \vdash_2 \bot\). Hence \(\bot_2\!{\dashv}{\vdash}\!_2 \bot^s\) and so \(s\) conforms to \(\bot\). The proof that \(t\) conforms to \(\bot\) is similar.

\(ii\) Since \(L_1\) is classically based, \((A\rightarrow B),A \vdash B\). By condition i of weak translational equivalence \((A\rightarrow B)^s, A^s \vdash B^s\). Since \(L_2\) is classically based, \((A\rightarrow B)^s \vdash (A^s\rightarrow B^s)\). Similarly, since \(L_2\) is classically based, \((A\rightarrow B)^t,A^t \vdash B^t\). By condition (ii) of weak translational equivalence, \((A^s\rightarrow B^s)^t,(A^s)^t \vdash (B^s)^t\). By condition iii, \((A^s)^t {\dashv}{\vdash}A\) and \((B^s)^t {\dashv}{\vdash}B\), and so \((A^s\rightarrow B^s)^t,A \vdash B\). Since \(L_1\) is classically based, \((A^s\rightarrow B^s)^t \vdash A\rightarrow B\). By condition i, \(((A^s\rightarrow B^s)^t)^s \vdash (A\rightarrow B)^s\), which implies by condition iv that \((A^s\rightarrow B^s) \vdash (A\rightarrow B)^s\). We have now shown that \((A\rightarrow B)^s{\dashv}{\vdash}(A^s\rightarrow B^s)\), and so \(s\) conforms to \(\rightarrow\). The proof that \(t\) conforms to \(\rightarrow\) is similar.

\(iii\) It can be shown that \(s\) and \(t\) conform to each of the remaining Boolean connectives by expressing them in terms of falsum and the conditional. For example \((\neg A)^s {\dashv}{\vdash} (A\rightarrow \bot)^s\). Since \(s\) conforms to the conditional and falsum, \((\neg A)^s {\dashv}{\vdash} A^s \rightarrow \bot\). Since the logics are classically based, \((\neg A)^s {\dashv}{\vdash} \neg A^s\). The other cases are similar. ◻

We proceed to the proof of part ii of the theorem. Suppose \(\Phi\) is an isomorphism between the Lindenbaum lattices \((X_1,\le _1)\) and \((X_2,\le _2)\) of \(L_1\) and \(L_2\). Let \(s\) map each formula \(A\) in the language of \(L_1\) to any member of \(\Phi([A])\) and let \(t\) map each formula \(C\) in the language of \(L_2\) to any member of \(\Phi^{-1}([C])\). We show that \(s\) and \(t\) meet the four conditions for weak translational equivalence. For i, suppose \(A_1,{\ldots},A_n \vdash B\). Since \(L_1\) is classically based \(A_1\wedge {\ldots}\wedge A_n \vdash B\), and so \([A_1\wedge {\ldots}\wedge A_n] \le [B]\). Since \(\Phi\) is an isomorphism, \(\Phi([A_1\wedge {\ldots}\wedge A_n]) \le \Phi([B])\), and so \((A_1\wedge {\ldots}\wedge A_n)^s \vdash B^s\). Since \(s\) conforms to conjunction, \(({A_1}^s\wedge {\ldots}\wedge {A_n}^s) \vdash B^s\). Since \(L_2\) is classically based, \({A_1}^s,{\ldots},{A_n}^s \vdash B^s\). The proof that condition ii is satisfied is similar. For conditions iii and iv note that, since \(A^s \in \Phi([A]), [A^s]= \Phi([A])\). Similarly, \([C^t]= \Phi^{-1}([C^t])\). Together these two identities imply \([(A^s)^t] = \Phi^{-1}(\Phi([A])\) and \([(C^t)^s]= \Phi(\Phi^{-1}[C])\). It follows that \([(A^s)^t] = [A]\) and \([(C^t)^s]=[C]\) and therefore that conditions iii and iv are satisfied. ◻

Since the modal logics under consideration are classically based, their Lindenbaum lattices are Boolean algebras, i.e., we can define from \(\le\) operations \(\wedge\),\(\vee\), and \(\neg\) satisfying the usual Boolean axioms. Humberstone’s observation that these logics provide strict intermediaries implies that they are dense. Using \(X{<}Y\) to mean \(X\le Y\) and not \(Y\le X\), we have that \([A]{<}[B]\) implies that there is some element \([I]\) such that \([A]{<}[I]{<}[B]\). But a Boolean algebra is dense iff it is atomless. (If the algebra is dense and \(0{<}X\) then there is is an element \(I\), that precedes \(X\), in the sense that \(0{<}I{<}X\), so \(X\) cannot be an atom. Conversely if the algebra has no atoms, then there is an intermediary \(I\) between \(0\) and \(X\), so if \(X{<}Y\), \(X\vee (I\wedge Y)\) is an intermediary between \(X\) and \(Y\).) A basic theorem of Boolean algebra states that the theory of atomless Boolean algebras is \(\aleph_0\)-categorical, i.e., that any two countable atomless Boolean algebras are isomorphic.It follows that any two reasonably well-behaved modal logics are weakly translationally equivalent. There is a sense in which adding \(\Box\) or any other non-Boolean connectives to the language of propositional logic and axioms and rules of derivation to the usual rules for classical logic adds nothing to what can be said. This observation contrasts starkly with what happens when translations are required to be compositional. In Pelletier and Urquhart (2003), it is shown that if well-behaved modal logics \(L_1\) and \(L_2\) are are translationally equivalent, then, for any number \(n\), the number of Kripke frames with \(n\) worlds validating \(L_1\) is the same as the number validating \(L_2\). It follows if two logics have the finite frame property (as all the most familiar modal logics do) and one is a sublogic of the other, they cannot be translationally equivalent. The observation here demonstrates the importance for the Pelletier/Urquhart result of the requirement that the translations be compositional.

We do know that the translations between classically based modal logics conform to the Boolean connectives. This allows us to sharpen the result slightly in the direction of Pelletier/Urquhart.

Theorem 4. Suppose \(L_1\) and \(L_2\) are classically based modal logics. Then \(L_1\) and \(L_2\) are weakly translationally equivalent by way of translations \(s^*\) and \(t^*\) that preserve the Boolean connectives.

Proof. Since the logics are classically based they have isomorphic Lindenbaum lattices. By the previous theorem they are weakly translationally equivalent. Let \(s\) and \(t\) be the translations securing this similarity. We define \(s^*\) and \(t^*\) by cases:

  1. \(s^*(A)=A^s\) if \(A\) is a sentence letter or \(A = {\#}A_1{\ldots}A_n\) for \({\#}\) an \(n\)-ary non-Boolean connective

  2. \(s^{*}(\bot)=\bot\)

  3. \(s^{*}(\neg A)= \neg A^{s^{*}}\)

  4. \(s^{*}(A{\#}B) = A^{s^{*}}\!{\#} B^{s^{*}}\) if \({\#}\) is \(\wedge ,\vee ,\rightarrow\) or \(\leftrightarrow\).

The clauses for \(t^*\) are similar.

Induction using sentence letters and formulas \({\#}A_1{\ldots}A_n\) for \({\#}\) non-Boolean as a base and appeal to the conformity property establishes that \(s^*\!(A){\dashv}{\vdash}A^s\) and \(t^*(C){\dashv}{\vdash}C^t\). It follows that \(s^*\) and \(t^*\), which preserve the Boolean connectives, also satisfy the conditions for weak translational equivalence. ◻

Note, however, that the result of Pelletier and Urquhart (2003) ensures that \(s^*\) and \(t^*\) are not in general compositional. So one should not presume, for example, that the \(s^*\)-translation of \(\Box (p\wedge q)\) is any function of the \(s^*\) translations of \(p\) and \(q\).

S4 \(\oplus\) 5\(^\prime\) = S4\(\oplus\)F

Consider the following two axioms:

These emerge in Humberstone’s survey (402-420) of the logical terrain between S4 and S5 for plausible epistemic logics. F figures prominently in Stalnaker (2006) and 5\(^\prime\) in Voorbraak (1991). Humberstone (410) asks whether it is possible to derive F from S4 and 5\(^\prime\). The point of this section is to argue that it is. We’ll also show something that is already clear in Humberstone’s text, which is that 5\(^\prime\) can be proven in S4F, so S4F = S45\(^\prime\). Humberstone in fact shows something considerably stronger, namely that S4F is complete with respect to the class of transitive, reflexive, semi-Euclidean frames, and 5\(^\prime\) is sound with respect to the class of those frames. (The semi-Euclidean frames are those which satisfy \(\forall xyz((xRy \wedge xRz) \rightarrow (yRz \vee zRx))\). The term semi-Euclidean is taken from Voorbraak (1991).) From these results it follows there must be some proof of 5\(^\prime\) in S4F. But the status of F in S45\(^\prime\) was an open question.

It will be convenient to label three additional formulas that appear in the course of our derivation of F:

We will show the following:

Theorem 5.

  1. 5\(^{\prime}~_{\text{K}}\!{\dashv}{\vdash}_\text{K}~\textbf{5}^{\prime\prime}\)

  2. \(\vdash_\text{KT4} ~ \neg \textbf{F}\rightarrow \textbf{A}\)

  3. \(\vdash_{\text{5}^{\prime\prime}} ~\textbf{A}\rightarrow \Diamond\textbf{B}\)

  4. \(\vdash_\text{S4} ~\neg \Diamond\textbf{B}\)

i allows us to work within S45\(^{\prime\prime}\) rather than S45\(^\prime\), and ii, iii, iv constitute a reductio proof of F within that system. It should be noted that Humberstone uses 5\(^\prime\) as a label for the schema corresponding to the axiom given here. We work within a natural deduction system that allows us to use a rule of truth-functional consequence under assumptions, and to apply rules of necessitation and uniform substitution to formulas that are not under any assumptions.

Proof. To prove i we note the following chain of K-equivalent formulas:

  1. \((p \wedge \neg \Box p \wedge \Box (p \vee \Box (p \rightarrow \Box p))) \rightarrow \Box \neg \Box p~~~\)(=5\(^\prime\))

  2. \((p \wedge \neg \Box p \wedge \neg \Box \neg \Box p) \rightarrow \neg \Box (p \vee \Box (p \rightarrow \Box p))\)

  3. \((p \wedge \Diamond\neg p \wedge \Diamond\Box p) \rightarrow \Diamond\neg (p \vee \Box (p \rightarrow \Box p))\)

  4. \((p \wedge \Diamond\neg p \wedge \Diamond\Box p) \rightarrow \Diamond(\neg p \wedge \neg \Box (p \rightarrow \Box p))\)

  5. \((p \wedge \Diamond\neg p \wedge \Diamond\Box p) \rightarrow \Diamond(\neg p \wedge \Diamond(p \wedge \neg \Box p))~~~\)(=5\(^{\prime\prime}\))

A derivation sketch establishing ii is given below. We make free use of K and truth functional logic, but we note steps that use T or 4.

  1. \(\neg ((p\wedge \Diamond\Box q) \rightarrow \Box (\Diamond{p}\vee q))\)(Assumption \(\neg\)F)

  2. \(p\) (from 1)

  3. \(\Diamond{p}\vee \Box q\)(from 2 using T)

  4. \(\Diamond(\neg \Diamond{p}\wedge \neg q)\) (from 1)

  5. \(\Diamond(\neg \Diamond{p}\wedge \neg \Box q)\) (from 4 using T)

  6. \(\Diamond\neg (\Diamond{p}\vee \Box q)\)(from 5)

  7. \(\Diamond\Box q\)(from 1)

  8. \(\Diamond\Box \Box q\)(from 7 using 4)

  9. \(\Diamond\Box (\Diamond{p}\vee \Box q)\) (from 8)

  10. \((\Diamond{p}\vee \Box q) \wedge \Diamond\neg (\Diamond{p}\vee \Box q)\wedge \Diamond\Box (\Diamond{p}\vee \Box q)\)(from 3,6,9)

  11. \(\neg \textbf{F} \rightarrow \textbf{A}\)(from 1-10)

For iii note that a substitution of \(\Diamond{p}\vee \Box q\) for \(p\) in 5\(^{\prime\prime}\) results in the formula A\(\rightarrow \Diamond\textbf{B}\). Finally, we establish iv by the derivation sketch below.

  1. \(\neg (\Diamond{p}\vee \Box q) \wedge \Diamond((\Diamond{p}\vee \Box q) \wedge \neg \Box (\Diamond{p}\vee \Box q))\)
    (Assumption B)

  2. \(\neg (\Diamond{p}\vee \Box q)\) (from 1)

  3. \(\Box \neg p\) (from 2)

  4. \(\Box \Box \neg p\) (from 3 using 4)

  5. \(\Diamond((\Diamond{p}\vee \Box q) \wedge \neg \Box (\Diamond{p}\vee \Box q))\) (from 1)

  6. \(\Diamond(\Box \neg p \wedge (\Diamond{p}\vee \Box q) \wedge \neg \Box (\Diamond{p}\vee \Box q))\) (from 4,5)

  7. \(\Diamond(\Box \neg p \wedge \Box q \wedge \neg \Box (\Diamond{p}\vee \Box q))\) (from 6)

  8. \(\Diamond(\Box \neg p \wedge \Box \Box q \wedge \neg \Box (\Diamond{p}\vee \Box q))\) (from 7 using 4)

  9. \(\Diamond(\Box \neg p \wedge \Box \Box q \wedge \neg \Box \Box q)\) (from 8)

  10. \(\neg\)B (from 1-9 by reductio)

  11. \(\Box \neg\)B (from 10 by necessitation)

  12. \(\neg \Diamond\)B (from 11)


As we mentioned above, Humberstone shows that there must be a proof of 5\(^\prime\) in S4F. For the sake of symmetry, we sketch that proof. As it turns out, only KF is required, which we could not have known from Humberstone’s completeness result.

  1. \((p\wedge \Diamond\Box q) \rightarrow \Box (\Diamond{p}\vee q)\)(F)

  2. \((\neg (p\rightarrow \Box p) \wedge \Diamond\Box p) \rightarrow \Box (\Diamond\neg (p\rightarrow \Box p)\vee p)\)(from 1 by substitution)

  3. \(\neg ((p \wedge \neg \Box p \wedge \Box (p \vee \Box (p \rightarrow \Box p))) \rightarrow \Box \neg \Box p)\)(Assumption \(\neg \textbf{5}^\prime)\)

  4. \(p \wedge \neg \Box p \wedge \Box (p \vee \Box (p \rightarrow \Box p)) \wedge \Diamond\Box p\)(from 3)

  5. \(\neg (p\rightarrow \Box p) \wedge \Diamond\Box p\)(from 4)

  6. \(\Box (\Diamond\neg (p\rightarrow \Box p)\vee p)\)(from 2,5)

  7. \(\Diamond\neg p\)(from 4)

  8. \(\Diamond(\neg p \wedge \Diamond\neg (p\rightarrow \Box p)\vee p)\)(from 6,7)

  9. \(\Diamond(\neg p \wedge \Diamond\neg (p\rightarrow \Box p))\)(from 8)

  10. \(\Box (p \vee \Box (p \rightarrow \Box p))\)(from 4)

  11. \(\Diamond(\neg (p\vee \Box (p\rightarrow \Box p)) \wedge (p\vee \Box (p\wedge \Box p))\)(from 9, 10)

  12. \(\textbf{5}^\prime\)(from 3-11 by reductio)


Ain’t Necessarily So

Humberstone’s “logic of coming about” (452-469) adds to the language of classical sentential logic a modal operator \(\mathbf{D}\). \(\mathbf{D}A\) is to be read as it comes about that \(A\) and understood as being something like Nuel Belnap’s a sees to it that \(A\), except that it abstracts from the idea of agency. Models are triples \(\langle U,f,V\rangle\) where \(U\) and \(V\) are sets and valuations of the kind familiar from modal logic and \(f\) is a unary function from \(U\) to \(U\). The truth definition has the usual clauses for the classical connectives and the additional clause:

Truth in the model is truth at all \(u{\in}U\), and validity is is truth in all models. Among the valid schemas and validity-preserving rules that he draws attention to are the following:

The last rule schema is intended to include the cases \(m=0\) and \(n=0\) with the usual stipulation that an empty conjunction is \(\top\) and an empty disjunction is \(\bot\). The reader is asked to show that D2 and D3 are provable from the remaining schemas as an exercise and the valid formulas are then shown to be axiomatized by D0, D1, MP and all the RD rules. In this section we consider two additional schemas.

We show that the valid formulas of coming-about logic are axiomatized by D0, D1, D3, D4, D5 MP and RD\(_{1,1}\). Since we can always add a rule of substitution while replacing the schematic variables in D1, D3, D4 by sentence letters and replacing D0 by a finite set of axioms for sentential logic, this shows that Humberstone’s infinite axiomatization can be replaced by a simple finite one.

D4 plays a special role among the axioms and rules considered. Suppose \(\mathbf{D}{A}\) is interpreted as it is contingently true that \(A\) (or, as the section head suggests, that \(A\), while true, is not necessarily so). More precisely, replace the function \(f\) in Humberstone’s models by an accessibility of the usual kind and his truth clause for \(\mathbf{D}\) by the following:

It is easy to check that D0, D1, D2, D3 and D5 all remain valid and MP and RD\(_{1,1}\) still preserve validity. But when \(R\) is not a function then D4 can be falsified: Let \(U=\{w,u,v\}, R=\{(w,u),(w,v)\}, V(p)=\{w,u\}\) and \(V(q)=\{w,v\}\). So D4 is independent of the five axioms and two rules just given. In fact, as we shall show, these axioms and rules are sufficient to axiomatize the contingently true operator under the interpretation CT.

First, however, we turn to the connection between the formula schemas and the rule schema RD\(_{m,n}\) and the proof that the logic of coming about is finitely axiomatizable. Note that any logic containing D0 and closed under MP is closed under truth-functional consequence (TFC). This facilitates the proof of the following:

Claim 1. In the presence of D0, D1 and MP: D2 is provable from RD\(_{1,1}\), D3 is provable from RD\(_{2,1}\), D4 is provable from RD\(_{1,2}\) and D5 is provable from RD\(_{0,1}\)

Proof. The required derivations are sketched below.

  1. \((A\wedge B)\rightarrow B\) by D0

  2. \((A\wedge B)\rightarrow (\mathbf{D}B\rightarrow \mathbf{D}(A\wedge B))\)from 1 by RD\(_{1,1}\)

  3. \((A\wedge B\wedge \mathbf{D}B)\rightarrow \mathbf{D}(A\wedge B))\)from 2 by TFC

  4. \((A\wedge \mathbf{D}B)\rightarrow \mathbf{D}(A\wedge B))\)from 3 and D1 by TFC

  1. \((A\wedge B)\rightarrow (A\wedge B)\) by D0

  2. \((A\wedge B)\rightarrow (\mathbf{D}(A\wedge B)\rightarrow (\mathbf{D}A\vee \mathbf{D}B))\)from 1 by RD\(_{2,1}\)

  3. \(\mathbf{D}(A\wedge B)\rightarrow (\mathbf{D}A\vee \mathbf{D}B)\)from 2 and D1 by TFC

  1. \((A\wedge B)\rightarrow (A\vee B)\) by D0

  2. \((A\wedge B)\rightarrow ((\mathbf{D}A\wedge \mathbf{D}B)\rightarrow \mathbf{D}(A\vee B))\) from 1 by RD\(_{1,2}\)

  3. \(\mathbf{D}(A\wedge B)\rightarrow \mathbf{D}(A\vee B)\)from 2 and D1 by TFC

  1. \(\top \rightarrow \top\)by D0

  2. \(\top \rightarrow (D\top \rightarrow \bot)\)from 1 by RD\(_{0,1}\)

  3. \(\neg D\top\)from 2 by TFC


Since Humberstone has already shown that D0 and D1 are valid and that modus ponens and every instance of RD\(_{m,n}\) preserves validity, the claim is sufficient to show that our new axiom system is sound. To prove sufficiency, it is sufficient to show that, for all \(m,n\!\ge\!0\), RD\(_{m,n}\) is derivable in the new system. To this end, notice first that D3 and D4 generalize, i.e., if \(\vdash\) indicates provability in the new axiom system then:

For these claims to be sensible without grouping conjuncts and disjuncts our logic must allow replacement of truth-functional equivalents. Humberstone’s proof (453) of the claim that his logic satisfies the stronger property of being “congruential,” i.e., closed under replacement of provable equivalents uses only D0 and RD\(_{1,1}\) so we can help ourselves to this result. The claims can then be proved by induction on \(n\). In each case the basis case follows from D0. The inductive step for D3* uses D3 and that for D4* uses D4.

This allows us to show that RD\(_{m,n}\) is derivable for all positive \(m\) and \(n\): Suppose \(\vdash (B_1 \wedge {\ldots}\wedge B_m) \rightarrow (A_1\vee {\ldots}\vee A_n)\). Then by RD\(_{1,1}\),
\(\vdash (B_1 \wedge {\ldots}\wedge B_m) \rightarrow (\mathbf{D}(A_1\vee {\ldots}\vee A_n) \rightarrow \mathbf{D}(B_1 \wedge {\ldots}\wedge B_m))\). By D3* and TFC, \(\vdash (B_1 \wedge {\ldots}\wedge B_m) \rightarrow (\mathbf{D}(A_1\vee {\ldots}\vee An) \rightarrow (\mathbf{D}B_1 \vee {\ldots}\vee \mathbf{D}B_m))\). By D4* and TFC, \(\vdash (B_1 \wedge {\ldots}\wedge B_m) \rightarrow ((\mathbf{D}A_1\wedge {\ldots}\wedge \mathbf{D}An) \rightarrow (\mathbf{D}B_1 \vee {\ldots}\vee \mathbf{D}B_m))\).

It remains only to check the cases \(m{=}0\) and \(n{=}0\). But for all \(m\), RD\(_{m,0}\) is a consequence of TFC: if \((B_1\wedge {\ldots}\wedge B_m)\rightarrow \bot\) is provable then so is any formula with \(B_1\wedge {\ldots}\wedge B_m\) as antecedent, including the consequence of RD\(_{m,0}\).

For the case \(m=0\) we will need D4* and D5. Suppose \(\vdash \top \rightarrow (A_1\vee {\ldots}\vee A_n)\). Then \((A_1\vee {\ldots}\vee A_n)\) is provably equivalent to \(\top\). Since \(\vdash \neg D\top\) and our logic is congruential it follows that \(\vdash \neg \mathbf{D}(A_1\vee {\ldots}\vee A_n)\). By D4, \(\vdash \neg (\mathbf{D}A_1\wedge {\ldots}\wedge \mathbf{D}A_n)\). By TFC, \(\vdash \top \rightarrow ( (\mathbf{D}A_1\wedge {\ldots}\wedge \mathbf{D}An) \rightarrow \bot)\), and so RD\(_{0,n}\) is derivable.\(\blacksquare\)

Our proof that Humberstone’s logic of coming about has a simple, finite axiomatization is complete and so we turn our attention to the axiomatization of the logic of contingent truth.

Theorem 6. The axioms D0, D1, D3, D4, D5 and rules MP and RD\(_{1,1}\) provide a complete axiomatization of the logic of contingently true* under the interpretation CT.*

Proof. Soundness was observed above so it is sufficient to prove sufficiency. This can be done by constructing a canonical model out of maximally consistent sets in a familiar way. Let \(M^c=(W^c\!, R^c\!,V^c)\), where \(W^c\) is the set of all maximally consistent formulas, \(V^c(p)=\{w{\in}W^c\!: p{\in}w\}\), and \(xR^cy\) iff \(A{\in}y\) whenever both \(A{\in}x\) and \(\mathbf{D}A{\notin}x\).

Lemma 2 (Witness lemma). If \(\mathbf{D}A{\in}x\) then \(\exists y (xR^cy\) and \(A{\in}y)\).

Proof. Suppose \(\mathbf{D}A {\in}x\) and let \(y^- = \{B{:}~ B{\in}x\) and \(\mathbf{D}B{\in}x\}\cup\{\neg A\}\). Then \(y^-\) is consistent. For otherwise either \(\vdash A\) or there are formulas \(B_1,{\ldots},B_n\) such that for \(1\le i\le n, B_i{\in}x\) and \(\mathbf{D}B_i{\in}x\) and \(\vdash B_1\wedge {\ldots}\wedge B_n\rightarrow A\). In the first case, by D0, \(\vdash A{\leftrightarrow}\top\). Since the logic is congruential, \(\vdash \mathbf{D}\top\), violating D5. So we may assume that the second case obtains. By RD\(_{1,1}\), \(\vdash B_1\wedge {\ldots}\wedge B_n\rightarrow (\mathbf{D}A\rightarrow \mathbf{D}(B_1\wedge {\ldots}\wedge B_n))\). Each \(B_i\) is a member of \(x\) by construction and \(\mathbf{D}A\) is a member of \(x\) by supposition, so it follows that \(\mathbf{D}(B_1\wedge {\ldots}\wedge B_n){\in}x\). By D3* this implies \(\mathbf{D}B_1\vee {\ldots}\vee \mathbf{D}B_n \in x\). But by construction none of the formulas \(\mathbf{D}B_i\) is a member of \(x\), so we have reached a contradiction. Thus \(y^-\) is consistent as claimed. By Lindenbaum’s lemma, it can be extended to a maximal consistent set y satisfying the conditions of the lemma. ◻

Lemma 3 (Truth Lemma). In the canonical model for our logic, \(\models _x A\) iff \(A{\in}x\).

Proof. By induction on \(A\). We consider the case \(A=\mathbf{D}B\). First suppose \(\models _x A\). By the truth definition, \(\models _x B\) and \(\exists y (xR^cy\) and \({\nvDash_y}B)\). By induction hypothesis, \(B{\in}x\) and \(\exists y (xR^cy\) and \(B{\notin}y)\). By the definition of \(R^c\), \(\mathbf{D}B{\in}x\) as required.

For the converse, suppose \(A{\in}x\). By the witness lemma, \(\exists y (xR^cy\) and \(B{\in}y)\). By induction hypothesis, \(\exists y( xR^cy\) and \({\models_y}B)\). Furthermore, since \(A{\in}x\), D1 implies that \(B{\in}x\), and,by induction hypothesis, this implies that \(\models _x B\). So, by the truth definition, \(\models _x A\), as required. ◻

To prove the theorem note that, by Lindenbaum’s lemma, any consistent set in the logic described can be extended to a maximal consistent set, which will be one of the worlds in the canonical model. By the truth lemma, all the members of the set will be true at that world. ◻

French, Rohan. 2010. “Translational Embeddings in Modal Logic.” PhD thesis, Department of Philosophy, Monash University.
Humberstone, Lloyd. 2011. The Connectives. Cambridge, MA: MIT Press.
———. 2016. Philsophical Applications of Modal Logic. Milton Keynes: College Publications.
Kuhn, Steven. 1978. Many-Sorted Modal Logics. Uppsala: Department of Philosophy, Uppsala University.
Pelletier, Francis Jeffry, and Alasdair Urquhart. 2003. “Synonymous Logics.” Journal of Philosophical Logic 32 (3): 259–85.
Prior, Arthur N. 1951. “The Ethical Copula.” Australasian Journal of Philosophy 29 (3): 137–54.
Stalnaker, Robert. 2006. On Logics of Knowledge and Belief.” Philosophical Studies 128 (1).
Voorbraak, Frans. 1991. “The Logic of Objective Knowledge and Rational Belief.” In Logics in AI, edited by J. van Eijck, 499–515. Berlin, Heidelberg: Springer, Berlin.
Zolin, Evgeni E. 2000. “Embeddings of Propositional Monomodal Logics.” Logic Journal of IGPL 8 (6): 861–82.

  1. In the terminology of Humberstone (2011) (page 62), these logics are \(\#\)-classical for every Boolean connective \(\#\). Humberstone (2011) spells out necessary and sufficient conditions that are omitted here. The term classical which might have been preferred over classically based is avoided because classical modal logic is sometimes used for other purposes.↩︎

  2. A paradigm case is the relation between classical propositional logic formulated with \(\neg\) and \(\wedge\) and that formulated with the Sheffer stroke. The notion has been defined in a number of ways, which are nicely surveyed in chapter 5 of French (2010). The definitions that follow are close to those in Kuhn (1978). Other definitions may diverge when certain Boolean connectives are absent or fail to behave classically, but our emphasis here is on logics for which they coincide.