I am aware of no standard modal logic which allows for such a derivation.
What you do have in system K is □(p → q), □p ⊨ □q:
In system K, we have the Axiom scheme K/Distribution axiom
□(A → B) → (□A → □B)
If we had □(p → q), then using distributivity we could obtain (□p → □q), which, combined with the premise □p, immediately gives us □q by modus ponens.
The problem is that we can't immediately deduce □(p → q) from (p → q) alone. For this step to be valid, we would need a particular setting: If we want to claim that from the fact that a formula is valid in some world, we can deduce that it is necessarily true, this amounts to stating that the only possible scenario any world can reach, if anything, is itself (we must exclude the possibility that the world can "imagine" other worlds at which the formula might not be true, which would invalidate the necessity), so every world just has nothing but themselves in mind, if at all:
You can easily verify that in such a setting, if A is true at any given world , then so is □A: The only world that w can access is w itself, so A is true at all w-accessible worlds, hence □A. If w can not even see itself, then □A becomes vacuously true, as there are no w-accessible worlds for which A does not hold, which is consistent with A → □A. So a frame setting where each world can access at most itself gives us the desired property A → □A. Conversely, we could prove by contraposition that if A → □A is a theorem, then we obtain a frame were no world must see any other than itself. This gives us the usual duality between the formulation of logical axioms and properties of the permissible frames.
Note that we don't need the reverse direction of the implication to be true: To deduce our desired formula, we don't need □A → A. This axiom, which defines system T (together with the axiom K), is equivalent to reflexivity:
□A → A
where R is the accessibility relation. In a reflexive frame, the world w itself is always among the set of worlds that are accessible from w, so if A is necessary (true at all worlds which w can reach), then A is also true at w itself. And conversely, if for any world from A follows □A, then we must demand that every world can see itself. Hence, the axiom and the frame property are equivalent.
But we don't need this in our frame: It might just be that □A is true without A being true, so it is permissible that a world can not even reach itself.¹
So the only thing we need to make sure is that every world can see at most itself, i.e. no worlds other than itself. Let's call this the axiom of necessitation², or the frame property of isolation:
A → □A
∀ww'(R(w,w') → w=w') (or equivalently, ∀w¬∃w'(R(w,w')∧w≠w')))
You can easily verify that the axiom A → □A and the isolation property are equivalent.
If we assume this, we can make the desired deduction (here presented in a Hilbert-style manner):
- p → q (premise)
- (p → q) → □(p → q) (new axiom of necessitation, instantiated to A = p → q)
- □(p → q) (modus ponens on 1,2)
- □(p → q) → (□p → □q) (axiom K, instantiated to A = p, B = q)
- □ p → □ q (modus ponens on 3,4)
- □ p (premise)
- □ q (modus ponens on 5,6)
As said, I am not aware of any standard modal logic that includes such an axiom.
If we were to combine isolation with reflexivity, the result would be a frame where the set of possible worlds accessible from any given world is exactly that world itself, so every world has itself and only itself in mind - let's call this this the property of egocentrism:
∀w,w'(R(w,w') ↔ w=w')
In such a setting, we would obtain a bi-implication between any formula and its necessitation:
A ↔ □A
It is easily verifiable that we would even obtain equivalence with ◇:
A ↔ □A ↔ ◇A
Egocentrism makes the idea of the modal operators a somewhat trivial one: If the only possible world you can imagine is your own one, then there is not point in setting up a model of interconnected possible worlds in the first place, and possiblity and necessity reduces to truth in your own world.
² This is not to be confused with the necessitation rule A ⊢ □A which holds in deduction sytems like Hilbert calculus for system K: Applying this rule requires that the formula A be derived by rules, not a free assumption (as (p → q) in our case). A → □A is not an axiom (and neither a derivable rule) in system K.