Let $ML$ be a modal logic which contains the Reflection Rule (from $\vdash\Box F$ infer $\vdash F$). For a modal formula $F$, let $H(F)=\{\ \Box G\rightarrow G~|~\Box G$ is a subformula of $F\}$. A Kripke model for $ML$ is called $F$-sound if the root of the model satisfies $H(F)$.


**Soundness**. If $ML\vdash F$, then $F$ is valid in every $F$-sound Kripke model of $ML$.


The proof of soundness is by induction on the derivation of $F$. 


My question is about the proof of soundness in the induction step when $F$ is obtained by Modus Ponens from $G$ and $G\rightarrow F$. Since $F$-sound models are not necessarily $G$-sound and $(G\rightarrow F)$-sound models, I do not no how to manage this case.



Soundness of modal logics which contain the reflection rule
I don’t think your proof strategy will work as is. Here is one way to prove the result. Assume $\vdash\_{ML}A$, and let $M$ be a model with a root $r$ such that $r\models\bigwedge H(A)$. Let $M^\circ$ be the model which differs from $M$ only in that $r$ is made reflexive (accessible from itself). Prove by induction on the length of the proof that $A$ holds in $M^\circ$. Then using the fact that $M,r\models H(A)$, show by induction on the length of $B$ that for every subformula $B$ of $A$, and every $x\in M$, we have
$$M,x\models B\iff M^\circ,x\models B.$$
Taking $B=A$ then gives that $A$ holds in $M$.


You didn’t specify the base logic $L$ on top of which you add the $\Box B\mathbin/B$ rule. The argument above works whenever $L$ is a Kripke-complete normal modal logic whose class of frames is closed under the reflexivization operation I just described. (The Kripke completeness assumption can be relaxed by working with general frames instead.) The result is actually false for normal modal logics in general. For example, let $L=K\oplus\Box\bot$. Then $L$ plus the reflection rule proves $\bot$ (i.e., it is inconsistent). However, since $\bot$ has no boxed subformula, *every* rooted $L$-model is $\bot$-sound.


Note that most naturally defined modal logics $L$ are in fact already closed under the reflection rule (i.e., the reflection rule is $L$-admissible). Apart from extensions of T (obviously), this holds e.g. for the minimal normal logic K, as well as K4, D, GL, etc. In these cases, you simply get that a formula $A$ provable using the reflection rule is valid in *all* models, whether $A$-sound or not. One way to prove the admissibility of $\Box B\mathbin/B$ in a logic $L$ is to use a modification of the construction above, where instead of changing the reflexivity of $r$, you attach a *new* reflexive point $s$ which sees $r$ and all its successors. For logics like GL which do not allow reflexive points at all, you can instead attach to $r$ an infinite descending chain of irreflexive points; then you show that every formula provable using the reflection rule is true in the new model (and therefore in the old model, which is its generated submodel) by induction on the length of the proof.


