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 language 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 including all the theorems of M (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) including all the theorems 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.

Another way of looking at things is that, fixing a set S of variables and taking a propositional theory (or modal logic) to be always a theory including S many particular propositions, K is precisely the propositional theory of a propositional theory extending K (thus, its models are in correspondence with a subset of the variables interpreted as true, along with some propositional extension of K to interpret the box as; in particular, it has a model in which its box operator is interpreted as provability in K itself). K4 is precisely the propositional theory of a normal modal logic extending K4. And GL is precisely the propositional theory of a normal modal logic extending GL.

[TODO: Expand on this, noting how the minimal normal modal logic extending K4 and axioms A is given by K + 4 + Box 4 + A + Box A, and similarly for the minimal normal modal logic extending K and A being given by K + Box^n A for each n ≥ 0. GL is interesting in that it admits axiomatization as either K4 + internal Löb or K4 + external Löb rule, the former of which is the theory of normal modal extensions of the latter.]

Anyway, in general, say a normal modal logic M is "auto-reflecting" if the corresponding Tr holds for all 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 $$\Box p \vdash p$$. This obviously satisfies reflection, but is it auto-reflecting? (We may similarly ask whether S4 or S5 are auto-reflecting)

It seems viciously circular. But here's a way out:

Define $$\Tr_2$$ via nearly the same recursive definition as $$\Tr$$, but with $$\Tr_2(\Box p) = M \vdash p \wedge \Tr_2(p)$$. [Just as we can think of $$\Tr$$ as truth at an irreflexive world accessing precisely the models of $$M$$, we can think of $$\Tr_2$$ as doing the same thing but using a reflexive world.]

Clearly, $$M \subseteq \Tr_2$$ iff $$\Tr_2 = \Tr$$. Thus, $$M \subseteq \Tr$$ iff $$M \subseteq \Tr_2$$. But $$\Tr_2$$ clearly satisfies axiom $$T$$ (that $$\Box p \vdash p$$), and when $$M$$ is a normal modal logic (or normal modal logic extending K4), we furthermore have that so is $$\Tr_2 \cap M$$. Thus, in the case where $$M$$ is the minimal normal modal logic (or minimal normal modal extension of K4) generated by $$T$$, we have that $$M \subseteq \Tr_2 \cap M \subseteq \Tr_2$$, and thus $$\Tr = \Tr_2$$ contains $$M$$.

(As a bit of trivia, note that even just having $$M \subseteq \Tr \cup \Tr_2$$ entails that $$\Tr_2 = \Tr$$, since any minimum sentence which $$\Tr$$ and $$\Tr_2$$ disagree on must be of the form $$\Box p$$ for some sentence $$p$$, where $$\Tr$$ and $$\Tr_2$$ agree on $$p$$, $$M$$ contains $$p$$, and $$\Tr_2$$ does not contain $$p$$, which is precisely to say, a sentence $$p$$ witnessing that $$M$$ is not contained in the union of $$\Tr$$ and $$\Tr_2$$.)

This shows that both T and S4 are satisfied by their $$\Tr$$.

As for S5 (with at least one variable), it manifestly is not satisfied by its $$\Tr$$: S5 proves $$\Box p \vee \Box \neg \Box p$$. If its $$\Tr$$ satisfied this, this would mean S5 either proves $$p$$ or proves $$\neg \Box p$$ for every proposition $$p$$. But this is not the case when, for example, $$p$$ is a variable.

[TODO: Clean this section up]

[TODO: Note that this propositional argument for T or S4 does NOT generalize to showing things like, e.g., the free cartesian closed lexcategory C_0 with an internal category C_1 and an internal cartesian closed lex co-presheaf F_1 on C_1 admits a cartesian closed lexfunctor F_0 to Set which takes C_1 to C_0 and F_1 to F_0. Even though such categorical analogues ARE available for the results for K, K4, and GL.]