Consider the classical modal logic $\mathsf K$, given by the following axioms and rules over a language containing the standard propositional connectives and $\Box$:
- A complete set of axiom schemes for classical propositional logic
- $\Box(\phi\rightarrow\psi)\rightarrow(\Box\phi\rightarrow\Box\psi)$
- From $\phi$ and $\phi\rightarrow\psi$, infer $\psi$
- From $\vdash\phi$, infer $\vdash\Box\phi$
The formulation of the necessitation rule shall mean that it should only be applied to theorems (to allow derivations from premises) where $\vdash$ denotes provability in $\mathsf K$.
It is well known that $\mathsf K$ is complete with respect to its classical Kripke semantics.
What I am interested in is the following metatheorem:
$$\text{If }\vdash\Box\phi\text{, then }\vdash\phi$$
It is the converse to the necessitation rule and a weakening of the principle $\Box\phi\rightarrow\phi$ (of course only valid in reflexive models) to theorems of the logic.
By appealing to the completeness theorem, it is obvious that it is valid, by assuming $\not\vdash\phi$, i.e. there is a countermodel for $\phi$ and transforming this into a countermodel of $\Box\phi$.
This means that the rule is admissible in $\mathsf K$. My question is if there is a proof of the metatheorem which just appeal to the proof system $\mathsf K$ and not to any semantic issue.