I need to find a proof of $\top \vdash \Box \top$ (where $\top$ is the truth constant and $\Box$ is the necessity modal operator) in the natural deduction system of IS4 modal logic.
In the axiomatic system, it is an axiom (namely, necessity rule) that if $A$ is a theorem, then so is $\Box A$, but in the natural deduction system I have no such rule. Can it be derived from other rules (for instance, the box introduction rule)?
The proof of $\top\vdash\Box\top$ is derrived from the necessitation rule (if $\vdash A$ then $\vdash\Box A$), which in turn is a special case of the box introduction rule (where no modal formulae are needed as assumptions to prove A, so neither proofs of those modal formulae are needed).
I hope this was helpful for whoever has the same question.