I have a question about the necessitation rule in normal modal logics. Using an axiomatic system, once I proved $P$ I can apply necessitation and prove that $P$ is necessary ($\Box P$). In tableaux, once I prove $P$, I do not see how the rules allow me to infer $\Box P$.
What I mean essentially, is that tableaux only allows to prove formulas and does not capture, as far as I can see, the provability relation used in the necessitation rule. When you assume $P$ and try to prove $\Box P$ in tableaux, what you are essentially trying to prove is $P \to\Box P$, which is of course not provable.
Therefore, if $\Box P$ is inferred from the assumption $P$ in a normal modal logic but it cannot be proved in the corresponding tableaux system, how can the tableaux system be a complete procedure for the corresponding modal logic?
One example is the following, for the modal logic KD  p. 45. Assume the following set of assumptions:
- $\Box \neg q$
- $q \Rightarrow \Box p$
- $p \Rightarrow q$
Which abstracts the gentle murder paradox of standard deontic logic.
You can infer $\Box q$ using the following steps:
- from (2) and (3) infer $\Box p$
- from (4) and the inheritance principle (based on the necessitation rule) infer $\Box p \Rightarrow \Box q$
- from (5) and (6) infer $\Box q$
- contradiction since $\Box q \wedge \Box\neg q$ is inferrable and contradicts deontic consistency
Now, I was wondering how to imitate this proof using a tableau system for KD (K would be enough here). For example (using unsigned prefix tableaux):
- a. $\Box \neg q$
- a. $q \Rightarrow \Box p$
- a. $q$
- a. $p \Rightarrow q$
- a. $\neg (\Box q)$ (negation of the goal)
- a. $\neg q$ | a. $\Box p$ (on 2)
- closed (6 and 3) | $\Box p$
- b. $\neg q$ (from 5 and working only on the right branch)
- b. $p$ (from 6)
Now, in order to close the proof, I would need to elevate (4) into $\Box p \Rightarrow \Box q$ but there is no such rule in talbeaux.
The result, as far as I can see, is that a theorem of KD cannot be proved in tableaux.
 Navarro, Pablo E., and Jorge L. Rodríguez. Deontic logic and legal systems. Cambridge University Press, 2014.