By a reflection rule for a modal logic, I mean a rule that allows the derivation of \(\vdash p\) from \(\vdash \Box p\). In this post, I sketch out an interesting technique for establishing such reflection rule for logics such as K, K4, and GL.

(For simplicity of exposition, I’ll take the object logic to be Boolean propositional modal logic and the metalogic to be Boolean as well, but the following can generalize to predicate logics, non-Boolean logics, etc.) \(\newcommand \Tr{\mathrm{Tr}}\) \(\newcommand \Blahblah{\mathrm{Blahblah}}\)

Given a normal modal logic \(M\) (in the sense of https://en.wikipedia.org/wiki/Normal_modal_logic ), and some arbitrary predicate \(\Blahblah\) on its propositional variables, recursively define the predicate \(\Tr\) on sentences of \(M\) like so:

\(\Tr\) commutes with all non-modal propositional logical operations (&, ~, etc)

\(\Tr(v) = \Blahblah(v)\) for each propositional variable \(v\)

\(\Tr(\Box p) = M \vdash p\)

[We can think of \(\Tr\) as interpretation at a world which accesses precisely the worlds (in any frame anywhere) which validate \(M\).]

Define the theory \(\mathrm{Th}\) as the set of \(p\) such that \(\Tr(p)\). Though \(\mathrm{Th}\) itself may not be a normal modal logic, it’s easy to see that \(\mathrm{Th} \cap M\) is. Thus, if \(M\) is the minimal normal modal logic generated by axioms \(A\), and \(\Tr\) holds of all of \(A\) (thus, \(A\) is contained in \(\mathrm{Th} \cap M\)), we may conclude that \(M\) is contained in \(\mathrm{Th}\) (thus, \(\Tr\) holds of all of \(M\)). In this case, if \(M \vdash \Box p\), we may conclude \(\Tr(\Box p)\), which is to say \(M \vdash p\).

Thus, to conclude the reflection rule for the minimal modal logic generated by axioms \(A\), it suffices to establish that the corresponding \(\Tr\) (for at least some choice of \(\Blahblah\)) holds of all of \(A\).

In particular, we automatically have the reflection rule for K (the minimal normal modal logic simpliciter; the case where \(A\) is empty). We also have the reflection rule for K4 (the minimal normal modal logic generated by the axiom schema \(\Box p \to \Box \Box p\)). To say that \(\Tr\) holds of this is to say that \(M\) satisfies the necessitation rule allowing the derivation of \(\vdash \Box p\) from \(\vdash p\), which is part of the definition of \(M\) being a normal modal logic).

And in the same way, we may conclude the reflection rule for GL (the minimal normal modal logic generated by the axiom schema \(\Box (\Box p \to p) \to \Box p\). That \(\Tr\) holds of this is the argument from “internal Löb’s theorem” to “external Löb’s theorem” given at the end of here).

Are these proofs of the reflection rule “syntactic”? Well, note that our definition and use of \(\Tr\) breaks down into two parts:

First, there’s a purely syntactic translation of sentences from the languge of modal logic into the language of ordinary logic augmented with new propositional constants “M ⊢ p” for each p in the language of modal logic (call the latter language the meta-language. Incidentally, note that the translation from modal language into this meta-language can just send each propositional variable to itself, so Blahblah needn’t play any role here). At this purely syntactic level, we obtain that whenever M ⊢ []p, the sentence “M ⊢ p” of the meta-language is derivable in ordinary logic from the theory that M is a normal modal logic (which is expressible via axiom schemes in the meta-language).

Then, pedantically, the second part is concluding that, as M is indeed a normal modal logic (easily seen syntactically; basically part of the definition of M), and ordinary logic is sound (and, pedantically, Blahblah is available as an interpretation for its variables), it is indeed the case that M ⊢ p. Is the soundness of ordinary logic purely syntactic? Well, I don’t know what it even means to ask that, but at any rate, the soundness of ordinary propositional logic has nothing to do with Kripke frames or modal logic or whatever. Ordinary logic is sound for ordinary reasons.

Anyway, in general, say a normal modal logic M is “auto-reflecting” if the corresponding Tr holds for all of M (more properly, we should speak of being auto-reflecting for particular choices of Blahblah, and then can also consider the property of being auto-reflecting for all choices of Blahblah. Or perhaps we should say M is auto-reflecting if the translation of M into the meta-language is entailed in ordinary logic by the meta-language theory of the normality of M).

We’ve shown above that any auto-reflecting normal modal logic satisfies the reflection rule. But what about the converse?

For example, here’s a puzzle: Consider the modal logic T, which is the minimal normal modal logic generated by the axiom schema []p -> p. This obviously satisfies reflection, but is it auto-reflecting? (We may similarly ask whether S4 or S5 are auto-reflecting)

I don’t know the answer off the top of my head!